let o, p1, p2, p3, q1, q2, q3, r1, r2, r3 be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear & p1,q1,r1 are_collinear & p2,q2,r2 are_collinear & p3,q3,r3 are_collinear implies r1,r2,r3 are_collinear )
assume that
A1: ( o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 ) and
A2: not o,p1,q1 are_collinear and
A3: ( o,p1,p2 are_collinear & o,p1,p3 are_collinear ) and
A4: ( o,q1,q2 are_collinear & o,q1,q3 are_collinear ) and
A5: ( p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear ) and
A6: p1,q1,r1 are_collinear and
A7: p2,q2,r2 are_collinear and
A8: p3,q3,r3 are_collinear ; :: thesis: r1,r2,r3 are_collinear
( not p1,p2,q1 are_collinear & not p1,p2,q2 are_collinear & not p1,q1,q2 are_collinear & not p2,q1,q2 are_collinear ) by A1, A2, A3, A4, Th7;
then ( not p1,q1,p2 are_collinear & not p1,p2,q2 are_collinear & not p1,q1,q2 are_collinear & not q1,p2,q2 are_collinear ) by ANPROJ_2:24;
then consider N being invertible Matrix of 3,F_Real such that
A9: ( (homography N) . p1 = Dir100 & (homography N) . q1 = Dir010 & (homography N) . p2 = Dir001 & (homography N) . q2 = Dir111 ) by ANPROJ_9:30;
consider pp3 being Element of (TOP-REAL 3) such that
A10: ( not pp3 is zero & Dir pp3 = (homography N) . p3 ) by ANPROJ_1:26;
consider pp6 being Element of (TOP-REAL 3) such that
A11: ( not pp6 is zero & Dir pp6 = (homography N) . q3 ) by ANPROJ_1:26;
consider pp8 being Element of (TOP-REAL 3) such that
A12: ( not pp8 is zero & Dir pp8 = (homography N) . r2 ) by ANPROJ_1:26;
consider pp9 being Element of (TOP-REAL 3) such that
A13: ( not pp9 is zero & Dir pp9 = (homography N) . r3 ) by ANPROJ_1:26;
set hr1 = (homography N) . r1;
set hr2 = (homography N) . r2;
set hr3 = (homography N) . r3;
consider u100, v010, wr1 being Element of (TOP-REAL 3) such that
A14: ( Dir100 = Dir u100 & Dir010 = Dir v010 & (homography N) . r1 = Dir wr1 & not u100 is zero & not v010 is zero & not wr1 is zero & u100,v010,wr1 are_LinDep ) by A6, A9, ANPROJ_8:102, ANPROJ_2:23;
not are_Prop u100,v010 by ANPROJ_9:22, A14, ANPROJ_1:22;
then consider a, b being Real such that
A15: wr1 = (a * u100) + (b * v010) by A14, ANPROJ_1:6;
( Dir u100 = Dir |[1,0,0]| & not |[1,0,0]| is zero ) by A14, EUCLID_5:4, FINSEQ_1:78;
then are_Prop u100,|[1,0,0]| by A14, ANPROJ_1:22;
then consider au100 being Real such that
A16: au100 <> 0 and
A17: u100 = au100 * |[1,0,0]| by ANPROJ_1:1;
A18: u100 = |[(au100 * 1),(au100 * 0),(au100 * 0)]| by A17, EUCLID_5:8
.= |[au100,0,0]| ;
( Dir v010 = Dir |[0,1,0]| & not |[0,1,0]| is zero ) by A14, EUCLID_5:4, FINSEQ_1:78;
then are_Prop v010,|[0,1,0]| by A14, ANPROJ_1:22;
then consider av010 being Real such that
A19: av010 <> 0 and
A20: v010 = av010 * |[0,1,0]| by ANPROJ_1:1;
v010 = |[(av010 * 0),(av010 * 1),(av010 * 0)]| by A20, EUCLID_5:8
.= |[0,av010,0]| ;
then A21: wr1 = |[(a * au100),(a * 0),(a * 0)]| + (b * |[0,av010,0]|) by A15, A18, EUCLID_5:8
.= |[(a * au100),(a * 0),(a * 0)]| + |[(b * 0),(b * av010),(b * 0)]| by EUCLID_5:8
.= |[((a * au100) + 0),(0 + (b * av010)),(0 + 0)]| by EUCLID_5:6
.= |[(a * au100),(b * av010),0]| ;
A22: ( not a * au100 is zero & not b * av010 is zero )
proof
now :: thesis: ( a <> 0 & au100 <> 0 )
thus a <> 0 :: thesis: au100 <> 0
proof
assume a = 0 ; :: thesis: contradiction
then A23: wr1 = (0 * |[(u100 `1),(u100 `2),(u100 `3)]|) + (b * v010) by A15, EUCLID_5:3
.= |[(0 * (u100 `1)),(0 * (u100 `2)),(0 * (u100 `3))]| + (b * v010) by EUCLID_5:8
.= |[0,0,0]| + (b * |[(v010 `1),(v010 `2),(v010 `3)]|) by EUCLID_5:3
.= |[0,0,0]| + |[(b * (v010 `1)),(b * (v010 `2)),(b * (v010 `3))]| by EUCLID_5:8
.= |[(0 + (b * (v010 `1))),(0 + (b * (v010 `2))),(0 + (b * (v010 `3)))]| by EUCLID_5:6
.= b * |[(v010 `1),(v010 `2),(v010 `3)]| by EUCLID_5:8
.= b * v010 by EUCLID_5:3 ;
b <> 0
proof
assume b = 0 ; :: thesis: contradiction
then wr1 = 0 * |[(v010 `1),(v010 `2),(v010 `3)]| by A23, EUCLID_5:3
.= |[(0 * (v010 `1)),(0 * (v010 `2)),(0 * (v010 `3))]| by EUCLID_5:8
.= 0. (TOP-REAL 3) by EUCLID_5:4 ;
hence contradiction by A14; :: thesis: verum
end;
then are_Prop wr1,v010 by A23, ANPROJ_1:1;
then Dir wr1 = Dir v010 by A14, ANPROJ_1:22;
then r1 = q1 by ANPROJ_9:16, A9, A14;
hence contradiction by A1, A2, A3, A4, A5, Th10; :: thesis: verum
end;
thus au100 <> 0 by A16; :: thesis: verum
end;
hence not a * au100 is zero ; :: thesis: not b * av010 is zero
now :: thesis: ( b <> 0 & av010 <> 0 )
thus b <> 0 :: thesis: av010 <> 0
proof
assume b = 0 ; :: thesis: contradiction
then A24: wr1 = (a * |[(u100 `1),(u100 `2),(u100 `3)]|) + (0 * v010) by A15, EUCLID_5:3
.= (a * |[(u100 `1),(u100 `2),(u100 `3)]|) + (0 * |[(v010 `1),(v010 `2),(v010 `3)]|) by EUCLID_5:3
.= |[(a * (u100 `1)),(a * (u100 `2)),(a * (u100 `3))]| + (0 * |[(v010 `1),(v010 `2),(v010 `3)]|) by EUCLID_5:8
.= |[(a * (u100 `1)),(a * (u100 `2)),(a * (u100 `3))]| + |[(0 * (v010 `1)),(0 * (v010 `2)),(0 * (v010 `3))]| by EUCLID_5:8
.= |[((a * (u100 `1)) + 0),((a * (u100 `2)) + 0),((a * (u100 `3)) + 0)]| by EUCLID_5:6
.= a * |[(u100 `1),(u100 `2),(u100 `3)]| by EUCLID_5:8
.= a * u100 by EUCLID_5:3 ;
a <> 0
proof
assume a = 0 ; :: thesis: contradiction
then wr1 = 0 * |[(u100 `1),(u100 `2),(u100 `3)]| by A24, EUCLID_5:3
.= |[(0 * (u100 `1)),(0 * (u100 `2)),(0 * (u100 `3))]| by EUCLID_5:8
.= 0. (TOP-REAL 3) by EUCLID_5:4 ;
hence contradiction by A14; :: thesis: verum
end;
then are_Prop wr1,u100 by A24, ANPROJ_1:1;
then Dir wr1 = Dir u100 by A14, ANPROJ_1:22;
then r1 = p1 by A14, ANPROJ_9:16, A9;
hence contradiction by A1, A2, A3, A4, A5, Th11; :: thesis: verum
end;
thus av010 <> 0 by A19; :: thesis: verum
end;
hence not b * av010 is zero ; :: thesis: verum
end;
consider u001, v111, wr2 being Element of (TOP-REAL 3) such that
A25: ( Dir001 = Dir u001 & Dir111 = Dir v111 & (homography N) . r2 = Dir wr2 & not u001 is zero & not v111 is zero & not wr2 is zero & u001,v111,wr2 are_LinDep ) by A9, A7, ANPROJ_8:102, ANPROJ_2:23;
not are_Prop u001,v111 by ANPROJ_9:22, A25, ANPROJ_1:22;
then consider a2, b2 being Real such that
A26: wr2 = (a2 * u001) + (b2 * v111) by A25, ANPROJ_1:6;
( Dir u001 = Dir |[0,0,1]| & not |[0,0,1]| is zero ) by A25, EUCLID_5:4, FINSEQ_1:78;
then are_Prop u001,|[0,0,1]| by A25, ANPROJ_1:22;
then consider au001 being Real such that
au001 <> 0 and
A27: u001 = au001 * |[0,0,1]| by ANPROJ_1:1;
A28: u001 = |[(au001 * 0),(au001 * 0),(au001 * 1)]| by A27, EUCLID_5:8
.= |[0,0,au001]| ;
( Dir v111 = Dir |[1,1,1]| & not |[1,1,1]| is zero ) by A25, EUCLID_5:4, FINSEQ_1:78;
then are_Prop v111,|[1,1,1]| by A25, ANPROJ_1:22;
then consider av111 being Real such that
A29: av111 <> 0 and
A30: v111 = av111 * |[1,1,1]| by ANPROJ_1:1;
v111 = |[(av111 * 1),(av111 * 1),(av111 * 1)]| by A30, EUCLID_5:8
.= |[av111,av111,av111]| ;
then A31: wr2 = |[(a2 * 0),(a2 * 0),(a2 * au001)]| + (b2 * |[av111,av111,av111]|) by A26, A28, EUCLID_5:8
.= |[0,0,(a2 * au001)]| + |[(b2 * av111),(b2 * av111),(b2 * av111)]| by EUCLID_5:8
.= |[(0 + (b2 * av111)),(0 + (b2 * av111)),((a2 * au001) + (b2 * av111))]| by EUCLID_5:6
.= |[(b2 * av111),(b2 * av111),((a2 * au001) + (b2 * av111))]| ;
consider du010, dv001, dwr3 being Element of (TOP-REAL 3) such that
A32: ( Dir010 = Dir du010 & Dir001 = Dir dv001 & (homography N) . r3 = Dir dwr3 & not du010 is zero & not dv001 is zero & not dwr3 is zero & du010,dv001,dwr3 are_LinDep ) by A9, A5, ANPROJ_8:102, ANPROJ_2:23;
( Dir du010 = Dir |[0,1,0]| & not |[0,1,0]| is zero ) by A32, EUCLID_5:4, FINSEQ_1:78;
then are_Prop du010,|[0,1,0]| by A32, ANPROJ_1:22;
then consider adu010 being Real such that
A33: adu010 <> 0 and
A34: du010 = adu010 * |[0,1,0]| by ANPROJ_1:1;
A35: du010 = |[(adu010 * 0),(adu010 * 1),(adu010 * 0)]| by A34, EUCLID_5:8
.= <*0,adu010,0*> ;
( Dir dv001 = Dir |[0,0,1]| & not |[0,0,1]| is zero ) by A32, EUCLID_5:4, FINSEQ_1:78;
then are_Prop dv001,|[0,0,1]| by A32, ANPROJ_1:22;
then consider adv001 being Real such that
A36: adv001 <> 0 and
A37: dv001 = adv001 * |[0,0,1]| by ANPROJ_1:1;
A38: dv001 = |[(adv001 * 0),(adv001 * 0),(adv001 * 1)]| by A37, EUCLID_5:8
.= <*0,0,adv001*> ;
A39: dwr3 = |[(dwr3 `1),(dwr3 `2),(dwr3 `3)]| by EUCLID_5:3
.= <*(dwr3 . 1),(dwr3 `2),(dwr3 `3)*> by EUCLID_5:def 1
.= <*(dwr3 . 1),(dwr3 . 2),(dwr3 `3)*> by EUCLID_5:def 2
.= <*(dwr3 . 1),(dwr3 . 2),(dwr3 . 3)*> by EUCLID_5:def 3 ;
( du010 = <*(du010 `1),(du010 `2),(du010 `3)*> & dv001 = <*(dv001 `1),(dv001 `2),(dv001 `3)*> & dwr3 = <*(dwr3 `1),(dwr3 `2),(dwr3 `3)*> ) by EUCLID_5:3;
then reconsider M = <*du010,dv001,dwr3*> as Matrix of 3,F_Real by ANPROJ_8:19;
A40: M = <*<*(du010 `1),(du010 `2),(du010 `3)*>,dv001,dwr3*> by EUCLID_5:3
.= <*<*(du010 `1),(du010 `2),(du010 `3)*>,<*(dv001 `1),(dv001 `2),(dv001 `3)*>,dwr3*> by EUCLID_5:3
.= <*<*(du010 `1),(du010 `2),(du010 `3)*>,<*(dv001 `1),(dv001 `2),(dv001 `3)*>,<*(dwr3 `1),(dwr3 `2),(dwr3 `3)*>*> by EUCLID_5:3 ;
|{du010,dv001,dwr3}| = 0 by A32, ANPROJ_8:43;
then A41: Det M = 0 by A40, ANPROJ_8:35;
MXF2MXR M = <*<*0,adu010,0*>,<*0,0,adv001*>,<*(dwr3 . 1),(dwr3 . 2),(dwr3 . 3)*>*> by A35, A38, A39, MATRIXR1:def 2;
then reconsider M1 = <*<*0,adu010,0*>,<*0,0,adv001*>,<*(dwr3 . 1),(dwr3 . 2),(dwr3 . 3)*>*> as Matrix of 3,REAL by MATRIXR1:def 2;
A42: Det M = Det M1 by A35, A38, A39, MATRIXR1:def 1
.= (adu010 * adv001) * (dwr3 . 1) by Lm3 ;
adu010 * adv001 <> 0 by A33, A36, XCMPLX_1:6;
then dwr3 . 1 = 0 by A42, A41, XCMPLX_1:6;
then dwr3 `1 = 0 by EUCLID_5:def 1;
then A43: dwr3 = |[0,(dwr3 `2),(dwr3 `3)]| by EUCLID_5:3;
consider du100, dv111, ewr3 being Element of (TOP-REAL 3) such that
A44: ( Dir100 = Dir du100 & Dir111 = Dir dv111 & (homography N) . r3 = Dir ewr3 & not du100 is zero & not dv111 is zero & not ewr3 is zero & du100,dv111,ewr3 are_LinDep ) by A5, A9, ANPROJ_8:102, ANPROJ_2:23;
are_Prop ewr3,dwr3 by A32, A44, ANPROJ_1:22;
then consider ra being Real such that
A45: ( ra <> 0 & ewr3 = ra * dwr3 ) by ANPROJ_1:1;
A46: ewr3 = |[(ra * 0),(ra * (dwr3 `2)),(ra * (dwr3 `3))]| by A45, A43, EUCLID_5:8
.= |[0,(ra * (dwr3 `2)),(ra * (dwr3 `3))]| ;
not |[1,0,0]| is zero by EUCLID_5:4, FINSEQ_1:78;
then are_Prop du100,|[1,0,0]| by A44, ANPROJ_1:22;
then consider bdu100 being Real such that
A47: bdu100 <> 0 and
A48: du100 = bdu100 * |[1,0,0]| by ANPROJ_1:1;
A49: du100 = |[(bdu100 * 1),(bdu100 * 0),(bdu100 * 0)]| by A48, EUCLID_5:8
.= <*bdu100,0,0*> ;
( Dir dv111 = Dir |[1,1,1]| & not |[1,1,1]| is zero ) by A44, EUCLID_5:4, FINSEQ_1:78;
then are_Prop dv111,|[1,1,1]| by A44, ANPROJ_1:22;
then consider bdv111 being Real such that
A50: bdv111 <> 0 and
A51: dv111 = bdv111 * |[1,1,1]| by ANPROJ_1:1;
A52: dv111 = |[(bdv111 * 1),(bdv111 * 1),(bdv111 * 1)]| by A51, EUCLID_5:8
.= <*bdv111,bdv111,bdv111*> ;
A53: ewr3 = <*0,(ra * (dwr3 . 2)),(ra * (dwr3 `3))*> by A46, EUCLID_5:def 2
.= <*0,(ra * (dwr3 . 2)),(ra * (dwr3 . 3))*> by EUCLID_5:def 3 ;
( du100 = <*(du100 `1),(du100 `2),(du100 `3)*> & dv111 = <*(dv111 `1),(dv111 `2),(dv111 `3)*> & ewr3 = <*(ewr3 `1),(ewr3 `2),(ewr3 `3)*> ) by EUCLID_5:3;
then reconsider M = <*du100,dv111,ewr3*> as Matrix of 3,F_Real by ANPROJ_8:19;
A54: M = <*<*(du100 `1),(du100 `2),(du100 `3)*>,dv111,ewr3*> by EUCLID_5:3
.= <*<*(du100 `1),(du100 `2),(du100 `3)*>,<*(dv111 `1),(dv111 `2),(dv111 `3)*>,ewr3*> by EUCLID_5:3
.= <*<*(du100 `1),(du100 `2),(du100 `3)*>,<*(dv111 `1),(dv111 `2),(dv111 `3)*>,<*(ewr3 `1),(ewr3 `2),(ewr3 `3)*>*> by EUCLID_5:3 ;
A55: |{du100,dv111,ewr3}| = 0 by A44, ANPROJ_8:43;
MXF2MXR M = <*<*bdu100,0,0*>,<*bdv111,bdv111,bdv111*>,<*0,(ra * (dwr3 . 2)),(ra * (dwr3 . 3))*>*> by A49, A52, A53, MATRIXR1:def 2;
then reconsider M1 = <*<*bdu100,0,0*>,<*bdv111,bdv111,bdv111*>,<*0,(ra * (dwr3 . 2)),(ra * (dwr3 . 3))*>*> as Matrix of 3,REAL by MATRIXR1:def 2;
Det M = Det M1 by A49, A52, A53, MATRIXR1:def 1
.= ((bdu100 * bdv111) * (ra * (dwr3 . 3))) - ((bdu100 * (ra * (dwr3 . 2))) * bdv111) by Lm4 ;
then ((bdu100 * bdv111) * (ra * (dwr3 . 3))) - ((bdu100 * (ra * (dwr3 . 2))) * bdv111) = 0 by A55, A54, ANPROJ_8:35;
then A56: ((bdu100 * bdv111) * ra) * (dwr3 . 3) = ((bdu100 * ra) * bdv111) * (dwr3 . 2) ;
bdu100 * bdv111 <> 0 by A47, A50, XCMPLX_1:6;
then A57: (bdu100 * bdv111) * ra <> 0 by A45, XCMPLX_1:6;
A58: ( dwr3 `3 = dwr3 . 3 & dwr3 . 2 = dwr3 `2 ) by EUCLID_5:def 2, EUCLID_5:def 3;
then reconsider l1 = dwr3 `2 as non zero Real by A47, A50, A45, XCMPLX_1:6, A32, A43, A56, EUCLID_5:4;
A59: now :: thesis: ( are_Prop dwr3,|[0,1,1]| & not dwr3 is zero & not |[0,1,1]| is zero )
A60: dwr3 `2 <> 0 by A32, A58, A43, A57, A56, XCMPLX_1:5, EUCLID_5:4;
dwr3 = |[(0 * l1),(1 * l1),(1 * l1)]| by A58, A43, A57, A56, XCMPLX_1:5
.= l1 * |[0,1,1]| by EUCLID_5:8 ;
hence are_Prop dwr3,|[0,1,1]| by A60, ANPROJ_1:1; :: thesis: ( not dwr3 is zero & not |[0,1,1]| is zero )
thus not dwr3 is zero by A32; :: thesis: not |[0,1,1]| is zero
thus not |[0,1,1]| is zero by EUCLID_5:4, FINSEQ_1:78; :: thesis: verum
end;
p1,p2,p3 are_collinear by A2, A3, Th12;
then consider du100, dv001, dwp3 being Element of (TOP-REAL 3) such that
A61: ( Dir100 = Dir du100 & Dir001 = Dir dv001 & (homography N) . p3 = Dir dwp3 & not du100 is zero & not dv001 is zero & not dwp3 is zero & du100,dv001,dwp3 are_LinDep ) by A9, ANPROJ_8:102, ANPROJ_2:23;
( not |[1,0,0]| is zero & not du100 is zero & Dir |[1,0,0]| = Dir du100 ) by A61, EUCLID_5:4, FINSEQ_1:78;
then are_Prop du100,|[1,0,0]| by ANPROJ_1:22;
then consider va being Real such that
A62: va <> 0 and
A63: du100 = va * |[1,0,0]| by ANPROJ_1:1;
du100 = |[(va * 1),(va * 0),(va * 0)]| by A63, EUCLID_5:8
.= |[va,0,0]| ;
then A64: ( du100 `1 = va & du100 `2 = 0 & du100 `3 = 0 ) by EUCLID_5:2;
( not |[0,0,1]| is zero & not dv001 is zero & Dir |[0,0,1]| = Dir dv001 ) by A61, EUCLID_5:4, FINSEQ_1:78;
then are_Prop dv001,|[0,0,1]| by ANPROJ_1:22;
then consider vb being Real such that
A65: vb <> 0 and
A66: dv001 = vb * |[0,0,1]| by ANPROJ_1:1;
dv001 = |[(vb * 0),(vb * 0),(vb * 1)]| by A66, EUCLID_5:8
.= |[0,0,vb]| ;
then A67: ( dv001 `1 = 0 & dv001 `2 = 0 & dv001 `3 = vb ) by EUCLID_5:2;
A68: 0 = |{du100,dv001,dwp3}| by A61, ANPROJ_8:43
.= (((((((du100 `1) * (dv001 `2)) * (dwp3 `3)) - (((du100 `3) * (dv001 `2)) * (dwp3 `1))) - (((du100 `1) * (dv001 `3)) * (dwp3 `2))) + (((du100 `2) * (dv001 `3)) * (dwp3 `1))) - (((du100 `2) * (dv001 `1)) * (dwp3 `3))) + (((du100 `3) * (dv001 `1)) * (dwp3 `2)) by ANPROJ_8:27
.= - ((va * vb) * (dwp3 `2)) by A67, A64 ;
- (va * vb) <> 0 by A62, A65, XCMPLX_1:6;
then A69: dwp3 `2 = 0 by A68, XCMPLX_1:6;
q1,q2,q3 are_collinear by A2, A4, Th13;
then consider du010, dv111, dwq3 being Element of (TOP-REAL 3) such that
A70: ( Dir010 = Dir du010 & Dir111 = Dir dv111 & (homography N) . q3 = Dir dwq3 & not du010 is zero & not dv111 is zero & not dwq3 is zero & du010,dv111,dwq3 are_LinDep ) by A9, ANPROJ_8:102, ANPROJ_2:23;
( not |[0,1,0]| is zero & not du010 is zero & Dir |[0,1,0]| = Dir du010 ) by A70, EUCLID_5:4, FINSEQ_1:78;
then are_Prop du010,|[0,1,0]| by ANPROJ_1:22;
then consider vc being Real such that
A71: vc <> 0 and
A72: du010 = vc * |[0,1,0]| by ANPROJ_1:1;
du010 = |[(vc * 0),(vc * 1),(vc * 0)]| by A72, EUCLID_5:8
.= |[0,vc,0]| ;
then A73: ( du010 `1 = 0 & du010 `2 = vc & du010 `3 = 0 ) by EUCLID_5:2;
( not |[1,1,1]| is zero & not dv111 is zero & Dir |[1,1,1]| = Dir dv111 ) by A70, EUCLID_5:4, FINSEQ_1:78;
then are_Prop dv111,|[1,1,1]| by ANPROJ_1:22;
then consider vd being Real such that
A74: vd <> 0 and
A75: dv111 = vd * |[1,1,1]| by ANPROJ_1:1;
dv111 = |[(vd * 1),(vd * 1),(vd * 1)]| by A75, EUCLID_5:8
.= |[vd,vd,vd]| ;
then A76: ( dv111 `1 = vd & dv111 `2 = vd & dv111 `3 = vd ) by EUCLID_5:2;
A77: 0 = |{du010,dv111,dwq3}| by A70, ANPROJ_8:43
.= (((((((du010 `1) * (dv111 `2)) * (dwq3 `3)) - (((du010 `3) * (dv111 `2)) * (dwq3 `1))) - (((du010 `1) * (dv111 `3)) * (dwq3 `2))) + (((du010 `2) * (dv111 `3)) * (dwq3 `1))) - (((du010 `2) * (dv111 `1)) * (dwq3 `3))) + (((du010 `3) * (dv111 `1)) * (dwq3 `2)) by ANPROJ_8:27
.= ((vc * vd) * (dwq3 `1)) - ((vc * vd) * (dwq3 `3)) by A73, A76 ;
vc * vd <> 0 by A71, A74, XCMPLX_1:6;
then A78: dwq3 `1 = dwq3 `3 by A77, XCMPLX_1:5;
A79: (homography N) . r3 = Dir |[0,1,1]| by A59, A32, ANPROJ_1:22;
consider dhp3, dhq3, dhr3 being Element of (TOP-REAL 3) such that
A80: ( (homography N) . p3 = Dir dhp3 & (homography N) . q3 = Dir dhq3 & (homography N) . r3 = Dir dhr3 & not dhp3 is zero & not dhq3 is zero & not dhr3 is zero & dhp3,dhq3,dhr3 are_LinDep ) by A8, ANPROJ_8:102, ANPROJ_2:23;
A81: not |[(dwp3 `1),0,(dwp3 `3)]| is zero
proof
assume |[(dwp3 `1),0,(dwp3 `3)]| is zero ; :: thesis: contradiction
then ( dwp3 `1 = 0 & dwp3 `3 = 0 ) by EUCLID_5:4, FINSEQ_1:78;
then A82: dwp3 = |[((dwp3 `2) * 0),((dwp3 `2) * 1),((dwp3 `2) * 0)]| by EUCLID_5:3
.= (dwp3 `2) * |[0,1,0]| by EUCLID_5:8 ;
now :: thesis: ( are_Prop dwp3,|[0,1,0]| & not dwp3 is zero & not |[0,1,0]| is zero )
dwp3 `2 <> 0
proof
assume dwp3 `2 = 0 ; :: thesis: contradiction
then dwp3 = |[(0 * 0),(0 * 1),(0 * 0)]| by A82, EUCLID_5:8
.= 0. (TOP-REAL 3) by EUCLID_5:4 ;
hence contradiction by A61; :: thesis: verum
end;
hence are_Prop dwp3,|[0,1,0]| by A82, ANPROJ_1:1; :: thesis: ( not dwp3 is zero & not |[0,1,0]| is zero )
thus not dwp3 is zero by A61; :: thesis: not |[0,1,0]| is zero
thus not |[0,1,0]| is zero by EUCLID_5:4, FINSEQ_1:78; :: thesis: verum
end;
then Dir dwp3 = Dir010 by ANPROJ_1:22;
hence contradiction by A2, A3, ANPROJ_9:16, A61, A9; :: thesis: verum
end;
( not dhr3 is zero & not |[0,1,1]| is zero ) by A80, EUCLID_5:4, FINSEQ_1:78;
then are_Prop dhr3,|[0,1,1]| by A79, A80, ANPROJ_1:22;
then consider wc being Real such that
A83: wc <> 0 and
A84: dhr3 = wc * |[0,1,1]| by ANPROJ_1:1;
A85: dhr3 = |[(wc * 0),(wc * 1),(wc * 1)]| by A84, EUCLID_5:8
.= |[0,wc,wc]| ;
A86: Dir pp6 = Dir |[(dwq3 `1),(dwq3 `2),(dwq3 `1)]| by A78, EUCLID_5:3, A11, A70;
A87: ( dwp3 `3 <> 0 & dwp3 `1 <> 0 & (dwp3 `3) / (dwp3 `1) is non zero Real )
proof
thus ( dwp3 `3 <> 0 & dwp3 `1 <> 0 ) :: thesis: (dwp3 `3) / (dwp3 `1) is non zero Real
proof
assume ( dwp3 `3 = 0 or dwp3 `1 = 0 ) ; :: thesis: contradiction
per cases then ( dwp3 `3 = 0 or dwp3 `1 = 0 ) ;
suppose A88: dwp3 `3 = 0 ; :: thesis: contradiction
then A89: |[(dwp3 `1),0,(dwp3 `3)]| = |[((dwp3 `1) * 1),((dwp3 `1) * 0),((dwp3 `1) * 0)]|
.= (dwp3 `1) * |[1,0,0]| by EUCLID_5:8 ;
dwp3 `1 <> 0
proof
assume A90: dwp3 `1 = 0 ; :: thesis: contradiction
A91: dwp3 = |[((dwp3 `2) * 0),((dwp3 `2) * 1),((dwp3 `2) * 0)]| by A88, A90, EUCLID_5:3
.= (dwp3 `2) * |[0,1,0]| by EUCLID_5:8 ;
now :: thesis: ( are_Prop dwp3,|[0,1,0]| & not dwp3 is zero & not |[0,1,0]| is zero )
dwp3 `2 <> 0
proof
assume dwp3 `2 = 0 ; :: thesis: contradiction
then dwp3 = |[(0 * 0),(0 * 1),(0 * 0)]| by A91, EUCLID_5:8
.= 0. (TOP-REAL 3) by EUCLID_5:4 ;
hence contradiction by A61; :: thesis: verum
end;
hence are_Prop dwp3,|[0,1,0]| by A91, ANPROJ_1:1; :: thesis: ( not dwp3 is zero & not |[0,1,0]| is zero )
thus not dwp3 is zero by A61; :: thesis: not |[0,1,0]| is zero
thus not |[0,1,0]| is zero by EUCLID_5:4, FINSEQ_1:78; :: thesis: verum
end;
then Dir dwp3 = Dir010 by ANPROJ_1:22;
hence contradiction by A61, A9, ANPROJ_9:16, A2, A3; :: thesis: verum
end;
then A92: are_Prop |[(dwp3 `1),0,(dwp3 `3)]|,|[1,0,0]| by A89, ANPROJ_1:1;
A93: not |[1,0,0]| is zero by EUCLID_5:4, FINSEQ_1:78;
Dir pp3 = Dir |[(dwp3 `1),0,(dwp3 `3)]| by A69, EUCLID_5:3, A10, A61
.= Dir100 by A92, A81, A93, ANPROJ_1:22 ;
hence contradiction by A1, ANPROJ_9:16, A9, A10; :: thesis: verum
end;
suppose A94: dwp3 `1 = 0 ; :: thesis: contradiction
then A95: |[(dwp3 `1),0,(dwp3 `3)]| = |[((dwp3 `3) * 0),((dwp3 `3) * 0),((dwp3 `3) * 1)]|
.= (dwp3 `3) * |[0,0,1]| by EUCLID_5:8 ;
dwp3 `3 <> 0
proof
assume A96: dwp3 `3 = 0 ; :: thesis: contradiction
A97: dwp3 = |[((dwp3 `2) * 0),((dwp3 `2) * 1),((dwp3 `2) * 0)]| by A94, A96, EUCLID_5:3
.= (dwp3 `2) * |[0,1,0]| by EUCLID_5:8 ;
now :: thesis: ( are_Prop dwp3,|[0,1,0]| & not dwp3 is zero & not |[0,1,0]| is zero )
dwp3 `2 <> 0
proof
assume dwp3 `2 = 0 ; :: thesis: contradiction
then dwp3 = |[(0 * 0),(0 * 1),(0 * 0)]| by A97, EUCLID_5:8
.= 0. (TOP-REAL 3) by EUCLID_5:4 ;
hence contradiction by A61; :: thesis: verum
end;
hence are_Prop dwp3,|[0,1,0]| by A97, ANPROJ_1:1; :: thesis: ( not dwp3 is zero & not |[0,1,0]| is zero )
thus not dwp3 is zero by A61; :: thesis: not |[0,1,0]| is zero
thus not |[0,1,0]| is zero by EUCLID_5:4, FINSEQ_1:78; :: thesis: verum
end;
then Dir dwp3 = Dir010 by ANPROJ_1:22;
hence contradiction by ANPROJ_9:16, A61, A9, A2, A3; :: thesis: verum
end;
then A98: are_Prop |[(dwp3 `1),0,(dwp3 `3)]|,|[0,0,1]| by A95, ANPROJ_1:1;
A99: not |[0,0,1]| is zero by EUCLID_5:4, FINSEQ_1:78;
Dir pp3 = Dir |[(dwp3 `1),0,(dwp3 `3)]| by A69, EUCLID_5:3, A10, A61
.= Dir001 by A98, A81, A99, ANPROJ_1:22 ;
hence contradiction by ANPROJ_9:16, A9, A10, A1; :: thesis: verum
end;
end;
end;
hence (dwp3 `3) / (dwp3 `1) is non zero Real ; :: thesis: verum
end;
then reconsider f = (dwp3 `3) / (dwp3 `1) as non zero Real ;
A100: now :: thesis: ( are_Prop |[(dwp3 `1),0,(dwp3 `3)]|,|[1,0,f]| & not |[(dwp3 `1),0,(dwp3 `3)]| is zero & not |[1,0,f]| is zero )
|[(dwp3 `1),0,(dwp3 `3)]| = |[((dwp3 `1) * 1),((dwp3 `1) * 0),((dwp3 `1) * f)]| by A87, XCMPLX_1:87
.= (dwp3 `1) * |[1,0,f]| by EUCLID_5:8 ;
hence are_Prop |[(dwp3 `1),0,(dwp3 `3)]|,|[1,0,f]| by A87, ANPROJ_1:1; :: thesis: ( not |[(dwp3 `1),0,(dwp3 `3)]| is zero & not |[1,0,f]| is zero )
thus not |[(dwp3 `1),0,(dwp3 `3)]| is zero by A81; :: thesis: not |[1,0,f]| is zero
thus not |[1,0,f]| is zero by EUCLID_5:4, FINSEQ_1:78; :: thesis: verum
end;
A101: Dir pp3 = Dir |[(dwp3 `1),0,(dwp3 `3)]| by A69, EUCLID_5:3, A10, A61
.= Dir |[1,0,f]| by A100, ANPROJ_1:22 ;
A102: ( dwq3 `1 <> 0 & dwq3 `2 <> 0 )
proof
assume ( dwq3 `1 = 0 or dwq3 `2 = 0 ) ; :: thesis: contradiction
per cases then ( dwq3 `1 = 0 or dwq3 `2 = 0 ) ;
suppose A103: dwq3 `1 = 0 ; :: thesis: contradiction
then A104: |[(dwq3 `1),(dwq3 `2),(dwq3 `1)]| = |[((dwq3 `2) * 0),((dwq3 `2) * 1),((dwq3 `2) * 0)]|
.= (dwq3 `2) * |[0,1,0]| by EUCLID_5:8 ;
now :: thesis: ( are_Prop |[(dwq3 `1),(dwq3 `2),(dwq3 `1)]|,|[0,1,0]| & not |[(dwq3 `1),(dwq3 `2),(dwq3 `1)]| is zero & not |[0,1,0]| is zero )
A105: dwq3 `2 <> 0
proof
assume A106: dwq3 `2 = 0 ; :: thesis: contradiction
now :: thesis: ( dwq3 = (dwq3 `3) * |[0,0,1]| & dwq3 `3 <> 0 )
thus A107: dwq3 = |[((dwq3 `3) * 0),((dwq3 `3) * 0),((dwq3 `3) * 1)]| by A103, A106, EUCLID_5:3
.= (dwq3 `3) * |[0,0,1]| by EUCLID_5:8 ; :: thesis: dwq3 `3 <> 0
thus dwq3 `3 <> 0 :: thesis: verum
proof
assume dwq3 `3 = 0 ; :: thesis: contradiction
then dwq3 = |[(0 * 0),(0 * 0),(0 * 1)]| by A107, EUCLID_5:8
.= 0. (TOP-REAL 3) by EUCLID_5:4 ;
hence contradiction by A70; :: thesis: verum
end;
end;
then A108: are_Prop dwq3,|[0,0,1]| by ANPROJ_1:1;
not |[0,0,1]| is zero by EUCLID_5:4, FINSEQ_1:78;
then Dir dwq3 = Dir001 by A70, A108, ANPROJ_1:22;
then q3 = p2 by ANPROJ_9:16, A70, A9;
hence contradiction by A1, A2, A3, A4, Th14; :: thesis: verum
end;
hence are_Prop |[(dwq3 `1),(dwq3 `2),(dwq3 `1)]|,|[0,1,0]| by A104, ANPROJ_1:1; :: thesis: ( not |[(dwq3 `1),(dwq3 `2),(dwq3 `1)]| is zero & not |[0,1,0]| is zero )
thus not |[(dwq3 `1),(dwq3 `2),(dwq3 `1)]| is zero by EUCLID_5:4, A105, FINSEQ_1:78; :: thesis: not |[0,1,0]| is zero
thus not |[0,1,0]| is zero by EUCLID_5:4, FINSEQ_1:78; :: thesis: verum
end;
then (homography N) . q3 = (homography N) . q1 by A86, ANPROJ_1:22, A11, A9;
hence contradiction by ANPROJ_9:16, A1; :: thesis: verum
end;
suppose A109: dwq3 `2 = 0 ; :: thesis: contradiction
then A110: |[(dwq3 `1),(dwq3 `2),(dwq3 `1)]| = |[((dwq3 `1) * 1),((dwq3 `1) * 0),((dwq3 `1) * 1)]|
.= (dwq3 `1) * |[1,0,1]| by EUCLID_5:8 ;
A111: dwq3 `1 <> 0
proof
assume A112: dwq3 `1 = 0 ; :: thesis: contradiction
now :: thesis: ( are_Prop dwq3,|[0,0,1]| & not dwq3 is zero & not |[0,0,1]| is zero )
now :: thesis: ( dwq3 = (dwq3 `3) * |[0,0,1]| & dwq3 `3 <> 0 )
thus dwq3 = |[((dwq3 `3) * 0),((dwq3 `3) * 0),((dwq3 `3) * 1)]| by A112, A109, EUCLID_5:3
.= (dwq3 `3) * |[0,0,1]| by EUCLID_5:8 ; :: thesis: dwq3 `3 <> 0
thus dwq3 `3 <> 0 by A70, A109, A112, EUCLID_5:3, EUCLID_5:4; :: thesis: verum
end;
hence are_Prop dwq3,|[0,0,1]| by ANPROJ_1:1; :: thesis: ( not dwq3 is zero & not |[0,0,1]| is zero )
thus not dwq3 is zero by A70; :: thesis: not |[0,0,1]| is zero
thus not |[0,0,1]| is zero by EUCLID_5:4, FINSEQ_1:78; :: thesis: verum
end;
then Dir dwq3 = Dir001 by ANPROJ_1:22;
then q3 = p2 by ANPROJ_9:16, A70, A9;
hence contradiction by A1, A2, A3, A4, Th14; :: thesis: verum
end;
then A113: are_Prop |[(dwq3 `1),(dwq3 `2),(dwq3 `1)]|,|[1,0,1]| by A110, ANPROJ_1:1;
A114: not |[(dwq3 `1),(dwq3 `2),(dwq3 `1)]| is zero by EUCLID_5:4, A111, FINSEQ_1:78;
not |[1,0,1]| is zero by EUCLID_5:4, FINSEQ_1:78;
then A115: (homography N) . q3 = Dir |[1,0,1]| by A113, A114, ANPROJ_1:22, A86, A11;
A116: |[1,0,0]|,|[0,0,1]|,|[1,0,1]| are_LinDep
proof
|{|[1,0,0]|,|[0,0,1]|,|[1,0,1]|}| = 0
proof
( |[1,0,0]| `1 = 1 & |[0,0,1]| `1 = 0 & |[1,0,1]| `1 = 1 & |[1,0,0]| `2 = 0 & |[0,0,1]| `2 = 0 & |[1,0,1]| `2 = 0 & |[1,0,0]| `3 = 0 & |[0,0,1]| `3 = 1 & |[1,0,1]| `3 = 1 ) by EUCLID_5:2;
then |{|[1,0,0]|,|[0,0,1]|,|[1,0,1]|}| = ((((((1 * 0) * 1) - ((0 * 0) * 1)) - ((1 * 1) * 0)) + ((0 * 1) * 1)) - ((0 * 0) * 1)) + ((0 * 0) * 0) by ANPROJ_8:27
.= 0 ;
hence |{|[1,0,0]|,|[0,0,1]|,|[1,0,1]|}| = 0 ; :: thesis: verum
end;
hence |[1,0,0]|,|[0,0,1]|,|[1,0,1]| are_LinDep by ANPROJ_8:43; :: thesis: verum
end;
( (homography N) . p1 = Dir100 & (homography N) . p2 = Dir001 & not |[1,0,1]| is zero & not |[1,0,0]| is zero & not |[0,0,1]| is zero ) by A9, EUCLID_5:4, FINSEQ_1:78;
then p1,p2,q3 are_collinear by ANPROJ_2:23, A115, A116, ANPROJ_8:102;
hence contradiction by A1, A2, A3, A4, Th9; :: thesis: verum
end;
end;
end;
then reconsider g = (dwq3 `2) / (dwq3 `1) as non zero Real ;
A117: |[(dwq3 `1),(dwq3 `2),(dwq3 `1)]| = |[((dwq3 `1) * 1),((dwq3 `1) * g),((dwq3 `1) * 1)]| by A102, XCMPLX_1:87
.= (dwq3 `1) * |[1,g,1]| by EUCLID_5:8 ;
A118: ( are_Prop |[(dwq3 `1),(dwq3 `2),(dwq3 `1)]|,|[1,g,1]| & not |[(dwq3 `1),(dwq3 `2),(dwq3 `1)]| is zero & not |[1,g,1]| is zero ) by EUCLID_5:4, FINSEQ_1:78, A102, A117, ANPROJ_1:1;
then A119: Dir pp6 = Dir |[1,g,1]| by ANPROJ_1:22, A86;
reconsider h = (b * av010) / (a * au100) as non zero Real by A22;
A120: are_Prop |[(a * au100),(b * av010),0]|,|[1,h,0]|
proof
now :: thesis: ( a * au100 <> 0 & |[(a * au100),(b * av010),0]| = (a * au100) * |[1,h,0]| )
thus a * au100 <> 0 by A22, ORDINAL1:def 14; :: thesis: |[(a * au100),(b * av010),0]| = (a * au100) * |[1,h,0]|
b * av010 = ((a * au100) * (b * av010)) / (a * au100) by A22, ORDINAL1:def 14, XCMPLX_1:89
.= (a * au100) * ((b * av010) / (a * au100)) by XCMPLX_1:74 ;
hence |[(a * au100),(b * av010),0]| = |[((a * au100) * 1),((a * au100) * ((b * av010) / (a * au100))),((a * au100) * 0)]|
.= (a * au100) * |[1,h,0]| by EUCLID_5:8 ;
:: thesis: verum
end;
hence are_Prop |[(a * au100),(b * av010),0]|,|[1,h,0]| by ANPROJ_1:1; :: thesis: verum
end;
A121: not |[1,h,0]| is zero by EUCLID_5:4, FINSEQ_1:78;
A122: (b2 * av111) + (a2 * au001) <> 0
proof
assume (b2 * av111) + (a2 * au001) = 0 ; :: thesis: contradiction
then A123: wr2 = |[((b2 * av111) * 1),((b2 * av111) * 1),((b2 * av111) * 0)]| by A31
.= (b2 * av111) * |[1,1,0]| by EUCLID_5:8 ;
now :: thesis: ( are_Prop wr2,|[1,1,0]| & not wr2 is zero & not |[1,1,0]| is zero )
A124: b2 <> 0
proof
assume b2 = 0 ; :: thesis: contradiction
then A125: wr2 = (a2 * |[(u001 `1),(u001 `2),(u001 `3)]|) + (0 * v111) by A26, EUCLID_5:3
.= |[(a2 * (u001 `1)),(a2 * (u001 `2)),(a2 * (u001 `3))]| + (0 * v111) by EUCLID_5:8
.= |[(a2 * (u001 `1)),(a2 * (u001 `2)),(a2 * (u001 `3))]| + (0 * |[(v111 `1),(v111 `2),(v111 `3)]|) by EUCLID_5:3
.= |[(a2 * (u001 `1)),(a2 * (u001 `2)),(a2 * (u001 `3))]| + |[(0 * (v111 `1)),(0 * (v111 `2)),(0 * (v111 `3))]| by EUCLID_5:8
.= |[((a2 * (u001 `1)) + 0),((a2 * (u001 `2)) + 0),((a2 * (u001 `3)) + 0)]| by EUCLID_5:6
.= a2 * |[(u001 `1),(u001 `2),(u001 `3)]| by EUCLID_5:8
.= a2 * u001 by EUCLID_5:3 ;
a2 <> 0
proof
assume a2 = 0 ; :: thesis: contradiction
then wr2 = 0 * |[(u001 `1),(u001 `2),(u001 `3)]| by A125, EUCLID_5:3
.= |[(0 * (u001 `1)),(0 * (u001 `2)),(0 * (u001 `3))]| by EUCLID_5:8
.= 0. (TOP-REAL 3) by EUCLID_5:4 ;
hence contradiction by A25; :: thesis: verum
end;
then are_Prop wr2,u001 by A125, ANPROJ_1:1;
then Dir wr2 = Dir u001 by A25, ANPROJ_1:22;
then p2 = r2 by A25, A9, ANPROJ_9:16;
hence contradiction by A1, A2, A3, A5, Th15; :: thesis: verum
end;
thus are_Prop wr2,|[1,1,0]| by A29, A124, XCMPLX_1:6, A123, ANPROJ_1:1; :: thesis: ( not wr2 is zero & not |[1,1,0]| is zero )
thus not wr2 is zero by A25; :: thesis: not |[1,1,0]| is zero
thus not |[1,1,0]| is zero by EUCLID_5:4, FINSEQ_1:78; :: thesis: verum
end;
then A126: Dir wr2 = Dir |[1,1,0]| by ANPROJ_1:22;
A127: |[1,1,0]|,|[1,0,0]|,|[0,1,0]| are_LinDep
proof
( |[1,1,0]| `1 = 1 & |[1,0,0]| `1 = 1 & |[0,1,0]| `1 = 0 & |[1,1,0]| `2 = 1 & |[1,0,0]| `2 = 0 & |[0,1,0]| `2 = 1 & |[1,1,0]| `3 = 0 & |[1,0,0]| `3 = 0 & |[0,1,0]| `3 = 0 ) by EUCLID_5:2;
then |{|[1,1,0]|,|[1,0,0]|,|[0,1,0]|}| = ((((((1 * 0) * 0) - ((0 * 1) * 0)) - ((1 * 1) * 0)) + ((1 * 1) * 0)) - ((1 * 1) * 0)) + ((0 * 1) * 0) by ANPROJ_8:27
.= 0 ;
hence |[1,1,0]|,|[1,0,0]|,|[0,1,0]| are_LinDep by ANPROJ_8:43; :: thesis: verum
end;
( not |[1,1,0]| is zero & not |[1,0,0]| is zero & not |[0,1,0]| is zero ) by EUCLID_5:4, FINSEQ_1:78;
then ( (homography N) . r2 = Dir wr2 & Dir100 = (homography N) . p1 & r2,p1,q1 are_collinear ) by A25, A9, A127, A126, ANPROJ_2:23, ANPROJ_8:102;
hence contradiction by A1, A2, A3, A4, A5, Th16; :: thesis: verum
end;
A128: b2 * av111 <> 0
proof
b2 <> 0
proof
assume b2 = 0 ; :: thesis: contradiction
then A129: wr2 = (a2 * |[(u001 `1),(u001 `2),(u001 `3)]|) + (0 * v111) by A26, EUCLID_5:3
.= |[(a2 * (u001 `1)),(a2 * (u001 `2)),(a2 * (u001 `3))]| + (0 * v111) by EUCLID_5:8
.= |[(a2 * (u001 `1)),(a2 * (u001 `2)),(a2 * (u001 `3))]| + (0 * |[(v111 `1),(v111 `2),(v111 `3)]|) by EUCLID_5:3
.= |[(a2 * (u001 `1)),(a2 * (u001 `2)),(a2 * (u001 `3))]| + |[(0 * (v111 `1)),(0 * (v111 `2)),(0 * (v111 `3))]| by EUCLID_5:8
.= |[((a2 * (u001 `1)) + 0),((a2 * (u001 `2)) + 0),((a2 * (u001 `3)) + 0)]| by EUCLID_5:6
.= a2 * |[(u001 `1),(u001 `2),(u001 `3)]| by EUCLID_5:8
.= a2 * u001 by EUCLID_5:3 ;
a2 <> 0
proof
assume a2 = 0 ; :: thesis: contradiction
then wr2 = 0 * |[(u001 `1),(u001 `2),(u001 `3)]| by A129, EUCLID_5:3
.= |[(0 * (u001 `1)),(0 * (u001 `2)),(0 * (u001 `3))]| by EUCLID_5:8
.= 0. (TOP-REAL 3) by EUCLID_5:4 ;
hence contradiction by A25; :: thesis: verum
end;
then are_Prop wr2,u001 by A129, ANPROJ_1:1;
then Dir wr2 = Dir u001 by A25, ANPROJ_1:22;
then p2 = r2 by A25, A9, ANPROJ_9:16;
hence contradiction by A1, A2, A3, A5, Th15; :: thesis: verum
end;
hence b2 * av111 <> 0 by A29, XCMPLX_1:6; :: thesis: verum
end;
then reconsider i = ((b2 * av111) + (a2 * au001)) / (b2 * av111) as non zero Real by A122;
A130: now :: thesis: ( are_Prop |[(b2 * av111),(b2 * av111),((a2 * au001) + (b2 * av111))]|,|[1,1,i]| & not |[(b2 * av111),(b2 * av111),((a2 * au001) + (b2 * av111))]| is zero & not |[1,1,i]| is zero )
now :: thesis: ( |[(b2 * av111),(b2 * av111),((a2 * au001) + (b2 * av111))]| = (b2 * av111) * |[1,1,i]| & b2 * av111 <> 0 )
thus |[(b2 * av111),(b2 * av111),((a2 * au001) + (b2 * av111))]| = |[(b2 * av111),(b2 * av111),(((b2 * av111) * ((a2 * au001) + (b2 * av111))) / (b2 * av111))]| by A128, XCMPLX_1:89
.= |[((b2 * av111) * 1),((b2 * av111) * 1),((b2 * av111) * (((a2 * au001) + (b2 * av111)) / (b2 * av111)))]| by XCMPLX_1:74
.= (b2 * av111) * |[1,1,i]| by EUCLID_5:8 ; :: thesis: b2 * av111 <> 0
thus b2 * av111 <> 0 by A128; :: thesis: verum
end;
hence are_Prop |[(b2 * av111),(b2 * av111),((a2 * au001) + (b2 * av111))]|,|[1,1,i]| by ANPROJ_1:1; :: thesis: ( not |[(b2 * av111),(b2 * av111),((a2 * au001) + (b2 * av111))]| is zero & not |[1,1,i]| is zero )
thus not |[(b2 * av111),(b2 * av111),((a2 * au001) + (b2 * av111))]| is zero by EUCLID_5:4, FINSEQ_1:78, A128; :: thesis: not |[1,1,i]| is zero
thus not |[1,1,i]| is zero by FINSEQ_1:78, EUCLID_5:4; :: thesis: verum
end;
A131: Dir pp8 = Dir |[1,1,i]| by A130, A12, A25, A31, ANPROJ_1:22;
A132: now :: thesis: ( are_Prop |[0,wc,wc]|,|[0,1,1]| & not |[0,wc,wc]| is zero & not |[0,1,1]| is zero )
now :: thesis: ( |[0,wc,wc]| = wc * |[0,1,1]| & wc <> 0 )
thus |[0,wc,wc]| = |[(wc * 0),(wc * 1),(wc * 1)]|
.= wc * |[0,1,1]| by EUCLID_5:8 ; :: thesis: wc <> 0
thus wc <> 0 by A83; :: thesis: verum
end;
hence are_Prop |[0,wc,wc]|,|[0,1,1]| by ANPROJ_1:1; :: thesis: ( not |[0,wc,wc]| is zero & not |[0,1,1]| is zero )
thus not |[0,wc,wc]| is zero by EUCLID_5:4, FINSEQ_1:78, A83; :: thesis: not |[0,1,1]| is zero
thus not |[0,1,1]| is zero by EUCLID_5:4, FINSEQ_1:78; :: thesis: verum
end;
A133: Dir pp9 = Dir |[0,1,1]| by A80, A13, A85, A132, ANPROJ_1:22;
reconsider u1 = |[1,h,0]|, u2 = |[1,1,i]|, u3 = |[0,1,1]| as Element of (TOP-REAL 3) ;
A134: ( u1 `1 = 1 & u1 `2 = h & u1 `3 = 0 & u2 `1 = 1 & u2 `2 = 1 & u2 `3 = i & u3 `1 = 0 & u3 `2 = 1 & u3 `3 = 1 ) by EUCLID_5:2;
A135: |{u1,u2,u3}| = (((((((u1 `1) * (u2 `2)) * (u3 `3)) - (((u1 `3) * (u2 `2)) * (u3 `1))) - (((u1 `1) * (u2 `3)) * (u3 `2))) + (((u1 `2) * (u2 `3)) * (u3 `1))) - (((u1 `2) * (u2 `1)) * (u3 `3))) + (((u1 `3) * (u2 `1)) * (u3 `2)) by ANPROJ_8:27
.= (1 - i) - h by A134 ;
i + h = 1
proof
A136: ( |[1,h,0]| `1 = 1 & |[0,0,1]| `1 = 0 & |[1,g,1]| `1 = 1 & |[1,h,0]| `2 = h & |[0,0,1]| `2 = 0 & |[1,g,1]| `2 = g & |[1,h,0]| `3 = 0 & |[0,0,1]| `3 = 1 & |[1,g,1]| `3 = 1 ) by EUCLID_5:2;
A137: ( |[1,1,i]| `1 = 1 & |[1,0,f]| `1 = 1 & |[0,1,0]| `1 = 0 & |[1,1,i]| `2 = 1 & |[1,0,f]| `2 = 0 & |[0,1,0]| `2 = 1 & |[1,1,i]| `3 = i & |[1,0,f]| `3 = f & |[0,1,0]| `3 = 0 ) by EUCLID_5:2;
r1,p2,q3 are_collinear by A5, ANPROJ_2:24;
then consider u, v, w being Element of (TOP-REAL 3) such that
A138: (homography N) . r1 = Dir u and
A139: (homography N) . p2 = Dir v and
A140: (homography N) . q3 = Dir w and
A141: ( not u is zero & not v is zero & not w is zero ) and
A142: u,v,w are_LinDep by ANPROJ_8:102, ANPROJ_2:23;
A143: |{u,v,w}| = 0 by A142, ANPROJ_8:43;
( not u is zero & not |[1,h,0]| is zero & Dir u = Dir |[1,h,0]| ) by A141, A138, A121, A120, ANPROJ_1:22, A14, A21;
then are_Prop |[1,h,0]|,u by ANPROJ_1:22;
then consider aa being Real such that
aa <> 0 and
A144: |[1,h,0]| = aa * u by ANPROJ_1:1;
not |[0,0,1]| is zero by EUCLID_5:4, FINSEQ_1:78;
then are_Prop |[0,0,1]|,v by A9, A139, A141, ANPROJ_1:22;
then consider b being Real such that
b <> 0 and
A145: |[0,0,1]| = b * v by ANPROJ_1:1;
A146: not |[1,g,1]| is zero by EUCLID_5:4, FINSEQ_1:78;
are_Prop |[1,g,1]|,w by A119, A11, A140, A146, A141, ANPROJ_1:22;
then consider c being Real such that
c <> 0 and
A147: |[1,g,1]| = c * w by ANPROJ_1:1;
|{|[1,h,0]|,|[0,0,1]|,|[1,g,1]|}| = 0
proof
|{|[1,h,0]|,|[0,0,1]|,|[1,g,1]|}| = aa * |{u,(b * v),(c * w)}| by A144, A145, A147, ANPROJ_8:31
.= aa * (b * |{u,v,(c * w)}|) by ANPROJ_8:32
.= aa * (b * (c * |{u,v,w}|)) by ANPROJ_8:33
.= ((aa * b) * c) * 0 by A143 ;
hence |{|[1,h,0]|,|[0,0,1]|,|[1,g,1]|}| = 0 ; :: thesis: verum
end;
then A148: 0 = ((((((1 * 0) * 1) - ((0 * 0) * 1)) - ((1 * 1) * g)) + ((h * 1) * 1)) - ((h * 0) * 1)) + ((0 * 0) * g) by A136, ANPROJ_8:27
.= h - g ;
r2,p3,q1 are_collinear by A5, ANPROJ_2:24;
then consider u, v, w being Element of (TOP-REAL 3) such that
A149: (homography N) . r2 = Dir u and
A150: (homography N) . p3 = Dir v and
A151: (homography N) . q1 = Dir w and
A152: ( not u is zero & not v is zero & not w is zero ) and
A153: u,v,w are_LinDep by ANPROJ_8:102, ANPROJ_2:23;
A154: |{u,v,w}| = 0 by A153, ANPROJ_8:43;
( Dir u = Dir |[1,1,i]| & not u is zero & not |[1,1,i]| is zero ) by A130, A25, A31, ANPROJ_1:22, A149, A152;
then are_Prop u,|[1,1,i]| by ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A155: |[1,1,i]| = a * u by ANPROJ_1:1;
( Dir v = Dir |[1,0,f]| & not v is zero & not |[1,0,f]| is zero ) by A152, EUCLID_5:4, FINSEQ_1:78, A101, A150, A10;
then are_Prop v,|[1,0,f]| by ANPROJ_1:22;
then consider b being Real such that
b <> 0 and
A156: |[1,0,f]| = b * v by ANPROJ_1:1;
( Dir w = Dir010 & not w is zero & not |[0,1,0]| is zero ) by A152, A151, A9, EUCLID_5:4, FINSEQ_1:78;
then are_Prop |[0,1,0]|,w by ANPROJ_1:22;
then consider c being Real such that
c <> 0 and
A157: |[0,1,0]| = c * w by ANPROJ_1:1;
|{|[1,1,i]|,|[1,0,f]|,|[0,1,0]|}| = a * |{u,(b * v),|[0,1,0]|}| by A155, A156, ANPROJ_8:31
.= a * (b * |{u,v,(c * w)}|) by A157, ANPROJ_8:32
.= a * (b * (c * |{u,v,w}|)) by ANPROJ_8:33
.= 0 by A154 ;
then A158: 0 = ((((((1 * 0) * 0) - ((i * 0) * 0)) - ((1 * f) * 1)) + ((1 * f) * 0)) - ((1 * 1) * 0)) + ((i * 1) * 1) by A137, ANPROJ_8:27
.= i - f ;
A159: ( |[1,h,0]| `1 = 1 & |[1,0,i]| `1 = 1 & |[1,1,1]| `1 = 1 & |[1,h,0]| `2 = h & |[1,0,i]| `2 = 0 & |[1,1,1]| `2 = 1 & |[1,h,0]| `3 = 0 & |[1,0,i]| `3 = i & |[1,1,1]| `3 = 1 ) by EUCLID_5:2;
r1,p3,q2 are_collinear by A5, ANPROJ_2:24;
then consider u, v, w being Element of (TOP-REAL 3) such that
A160: (homography N) . r1 = Dir u and
A161: (homography N) . p3 = Dir v and
A162: (homography N) . q2 = Dir w and
A163: ( not u is zero & not v is zero & not w is zero ) and
A164: u,v,w are_LinDep by ANPROJ_8:102, ANPROJ_2:23;
A165: |{u,v,w}| = 0 by A164, ANPROJ_8:43;
( not u is zero & not |[1,h,0]| is zero & Dir u = Dir |[1,h,0]| ) by A160, A121, A120, ANPROJ_1:22, A14, A21, A163;
then are_Prop |[1,h,0]|,u by ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A166: |[1,h,0]| = a * u by ANPROJ_1:1;
( Dir v = Dir |[1,0,i]| & not v is zero & not |[1,0,i]| is zero ) by A161, A10, A101, A158, A163, EUCLID_5:4, FINSEQ_1:78;
then are_Prop v,|[1,0,i]| by ANPROJ_1:22;
then consider b being Real such that
b <> 0 and
A167: |[1,0,i]| = b * v by ANPROJ_1:1;
( Dir w = Dir |[1,1,1]| & not w is zero & not |[1,1,1]| is zero ) by A162, A163, A9, EUCLID_5:4, FINSEQ_1:78;
then are_Prop w,|[1,1,1]| by ANPROJ_1:22;
then consider c being Real such that
c <> 0 and
A168: |[1,1,1]| = c * w by ANPROJ_1:1;
|{|[1,h,0]|,|[1,0,i]|,|[1,1,1]|}| = 0
proof
|{|[1,h,0]|,|[1,0,i]|,|[1,1,1]|}| = c * |{|[1,h,0]|,|[1,0,i]|,w}| by A168, ANPROJ_8:33
.= c * (b * |{|[1,h,0]|,v,w}|) by A167, ANPROJ_8:32
.= c * (b * (a * |{u,v,w}|)) by A166, ANPROJ_8:31
.= 0 by A165 ;
hence |{|[1,h,0]|,|[1,0,i]|,|[1,1,1]|}| = 0 ; :: thesis: verum
end;
then A169: 0 = ((((((1 * 0) * 1) - ((0 * 0) * 1)) - ((1 * i) * 1)) + ((h * i) * 1)) - ((h * 1) * 1)) + ((0 * 1) * 1) by ANPROJ_8:27, A159
.= ((- i) + (h * i)) - h ;
A170: ( |[1,1,i]| `1 = 1 & |[1,0,0]| `1 = 1 & |[1,g,1]| `1 = 1 & |[1,1,i]| `2 = 1 & |[1,0,0]| `2 = 0 & |[1,g,1]| `2 = g & |[1,1,i]| `3 = i & |[1,0,0]| `3 = 0 & |[1,g,1]| `3 = 1 ) by EUCLID_5:2;
r2,p1,q3 are_collinear by A5, ANPROJ_2:24;
then consider u, v, w being Element of (TOP-REAL 3) such that
A171: (homography N) . r2 = Dir u and
A172: (homography N) . p1 = Dir v and
A173: (homography N) . q3 = Dir w and
A174: ( not u is zero & not v is zero & not w is zero ) and
A175: u,v,w are_LinDep by ANPROJ_8:102, ANPROJ_2:23;
A176: |{u,v,w}| = 0 by A175, ANPROJ_8:43;
( Dir u = Dir |[1,1,i]| & not u is zero & not |[1,1,i]| is zero ) by A174, A130, A25, A31, ANPROJ_1:22, A171;
then are_Prop u,|[1,1,i]| by ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A177: |[1,1,i]| = a * u by ANPROJ_1:1;
( Dir v = Dir |[1,0,0]| & not v is zero & not |[1,0,0]| is zero ) by A174, A9, A172, EUCLID_5:4, FINSEQ_1:78;
then are_Prop |[1,0,0]|,v by ANPROJ_1:22;
then consider b being Real such that
b <> 0 and
A178: |[1,0,0]| = b * v by ANPROJ_1:1;
( Dir w = Dir |[1,g,1]| & not w is zero & not |[1,g,1]| is zero ) by A174, A118, ANPROJ_1:22, A86, A11, A173;
then are_Prop |[1,g,1]|,w by ANPROJ_1:22;
then consider c being Real such that
c <> 0 and
A179: |[1,g,1]| = c * w by ANPROJ_1:1;
|{|[1,1,i]|,|[1,0,0]|,|[1,g,1]|}| = 0
proof
|{|[1,1,i]|,|[1,0,0]|,|[1,g,1]|}| = a * |{u,|[1,0,0]|,|[1,g,1]|}| by A177, ANPROJ_8:31
.= a * (b * |{u,v,|[1,g,1]|}|) by A178, ANPROJ_8:32
.= a * (b * (c * |{u,v,w}|)) by A179, ANPROJ_8:33
.= 0 by A176 ;
hence |{|[1,1,i]|,|[1,0,0]|,|[1,g,1]|}| = 0 ; :: thesis: verum
end;
then 0 = ((((((1 * 0) * 1) - ((i * 0) * 1)) - ((1 * 0) * g)) + ((1 * 0) * 1)) - ((1 * 1) * 1)) + ((i * 1) * g) by A170, ANPROJ_8:27
.= (- 1) + (i * g) ;
hence i + h = 1 by A169, A148; :: thesis: verum
end;
then A180: u1,u2,u3 are_LinDep by A135, ANPROJ_8:43;
A181: (homography N) . r1 = Dir u1 by A121, A120, ANPROJ_1:22, A14, A21;
( not |[1,h,0]| is zero & not |[1,1,i]| is zero & not |[0,1,1]| is zero ) by EUCLID_5:4, FINSEQ_1:78;
hence r1,r2,r3 are_collinear by ANPROJ_8:102, A180, A181, A12, A13, A131, A133, ANPROJ_2:23; :: thesis: verum