thus not Dir101 , Dirm101 , Dir011 are_collinear :: thesis: ( not Dir101 , Dirm101 , Dir010 are_collinear & not Dir101 , Dir011 , Dir010 are_collinear & not Dirm101 , Dir011 , Dir010 are_collinear )
proof
assume A1: Dir101 , Dirm101 , Dir011 are_collinear ; :: thesis: contradiction
set p = |[1,0,1]|;
set q = |[(- 1),0,1]|;
set r = |[0,1,1]|;
A2: ( |[1,0,1]| `1 = 1 & |[1,0,1]| `2 = 0 & |[1,0,1]| `3 = 1 & |[(- 1),0,1]| `1 = - 1 & |[(- 1),0,1]| `2 = 0 & |[(- 1),0,1]| `3 = 1 & |[0,1,1]| `1 = 0 & |[0,1,1]| `2 = 1 & |[0,1,1]| `3 = 1 ) by EUCLID_5:2;
( not |[1,0,1]| is zero & not |[(- 1),0,1]| is zero & not |[0,1,1]| is zero ) by EUCLID_5:4, FINSEQ_1:78;
then 0 = |{|[1,0,1]|,|[(- 1),0,1]|,|[0,1,1]|}| by A1, Th01
.= ((((((1 * 0) * 1) - ((1 * 0) * 0)) - ((1 * 1) * 1)) + ((0 * 1) * 0)) - ((0 * (- 1)) * 1)) + ((1 * (- 1)) * 1) by A2, ANPROJ_8:27
.= - 2 ;
hence contradiction ; :: thesis: verum
end;
thus not Dir101 , Dirm101 , Dir010 are_collinear :: thesis: ( not Dir101 , Dir011 , Dir010 are_collinear & not Dirm101 , Dir011 , Dir010 are_collinear )
proof
assume A3: Dir101 , Dirm101 , Dir010 are_collinear ; :: thesis: contradiction
set p = |[1,0,1]|;
set q = |[(- 1),0,1]|;
set r = |[0,1,0]|;
A4: ( |[1,0,1]| `1 = 1 & |[1,0,1]| `2 = 0 & |[1,0,1]| `3 = 1 & |[(- 1),0,1]| `1 = - 1 & |[(- 1),0,1]| `2 = 0 & |[(- 1),0,1]| `3 = 1 & |[0,1,0]| `1 = 0 & |[0,1,0]| `2 = 1 & |[0,1,0]| `3 = 0 ) by EUCLID_5:2;
( not |[1,0,1]| is zero & not |[(- 1),0,1]| is zero & not |[0,1,0]| is zero ) by EUCLID_5:4, FINSEQ_1:78;
then 0 = |{|[1,0,1]|,|[(- 1),0,1]|,|[0,1,0]|}| by A3, ANPROJ_9:def 6, Th01
.= ((((((1 * 0) * 0) - ((1 * 0) * 0)) - ((1 * 1) * 1)) + ((0 * 1) * 0)) - ((0 * (- 1)) * 0)) + ((1 * (- 1)) * 1) by A4, ANPROJ_8:27
.= - 2 ;
hence contradiction ; :: thesis: verum
end;
thus not Dir101 , Dir011 , Dir010 are_collinear :: thesis: not Dirm101 , Dir011 , Dir010 are_collinear
proof
assume A5: Dir101 , Dir011 , Dir010 are_collinear ; :: thesis: contradiction
set p = |[1,0,1]|;
set q = |[0,1,1]|;
set r = |[0,1,0]|;
A6: ( |[1,0,1]| `1 = 1 & |[1,0,1]| `2 = 0 & |[1,0,1]| `3 = 1 & |[0,1,1]| `1 = 0 & |[0,1,1]| `2 = 1 & |[0,1,1]| `3 = 1 & |[0,1,0]| `1 = 0 & |[0,1,0]| `2 = 1 & |[0,1,0]| `3 = 0 ) by EUCLID_5:2;
( not |[1,0,1]| is zero & not |[0,1,1]| is zero & not |[0,1,0]| is zero ) by EUCLID_5:4, FINSEQ_1:78;
then 0 = |{|[1,0,1]|,|[0,1,1]|,|[0,1,0]|}| by A5, ANPROJ_9:def 6, Th01
.= (((((((|[1,0,1]| `1) * (|[0,1,1]| `2)) * (|[0,1,0]| `3)) - (((|[1,0,1]| `3) * (|[0,1,1]| `2)) * (|[0,1,0]| `1))) - (((|[1,0,1]| `1) * (|[0,1,1]| `3)) * (|[0,1,0]| `2))) + (((|[1,0,1]| `2) * (|[0,1,1]| `3)) * (|[0,1,0]| `1))) - (((|[1,0,1]| `2) * (|[0,1,1]| `1)) * (|[0,1,0]| `3))) + (((|[1,0,1]| `3) * (|[0,1,1]| `1)) * (|[0,1,0]| `2)) by ANPROJ_8:27
.= - 1 by A6 ;
hence contradiction ; :: thesis: verum
end;
thus not Dirm101 , Dir011 , Dir010 are_collinear :: thesis: verum
proof
assume A7: Dirm101 , Dir011 , Dir010 are_collinear ; :: thesis: contradiction
set p = |[(- 1),0,1]|;
set q = |[0,1,1]|;
set r = |[0,1,0]|;
A8: ( |[(- 1),0,1]| `1 = - 1 & |[(- 1),0,1]| `2 = 0 & |[(- 1),0,1]| `3 = 1 & |[0,1,1]| `1 = 0 & |[0,1,1]| `2 = 1 & |[0,1,1]| `3 = 1 & |[0,1,0]| `1 = 0 & |[0,1,0]| `2 = 1 & |[0,1,0]| `3 = 0 ) by EUCLID_5:2;
( not |[(- 1),0,1]| is zero & not |[0,1,1]| is zero & not |[0,1,0]| is zero ) by EUCLID_5:4, FINSEQ_1:78;
then 0 = |{|[(- 1),0,1]|,|[0,1,1]|,|[0,1,0]|}| by A7, ANPROJ_9:def 6, Th01
.= (((((((|[(- 1),0,1]| `1) * (|[0,1,1]| `2)) * (|[0,1,0]| `3)) - (((|[(- 1),0,1]| `3) * (|[0,1,1]| `2)) * (|[0,1,0]| `1))) - (((|[(- 1),0,1]| `1) * (|[0,1,1]| `3)) * (|[0,1,0]| `2))) + (((|[(- 1),0,1]| `2) * (|[0,1,1]| `3)) * (|[0,1,0]| `1))) - (((|[(- 1),0,1]| `2) * (|[0,1,1]| `1)) * (|[0,1,0]| `3))) + (((|[(- 1),0,1]| `3) * (|[0,1,1]| `1)) * (|[0,1,0]| `2)) by ANPROJ_8:27
.= 1 by A8 ;
hence contradiction ; :: thesis: verum
end;