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 )

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;

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

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 )

.= Dir |[1,0,f]| by A100, ANPROJ_1:22 ;

A102: ( dwq3 `1 <> 0 & dwq3 `2 <> 0 )

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]|

A122: (b2 * av111) + (a2 * au001) <> 0

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

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

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

end;

consider u001, v111, wr2 being Element of (TOP-REAL 3) such that now :: thesis: ( a <> 0 & au100 <> 0 )

hence
not a * au100 is zero
; :: thesis: not b * av010 is zero thus
a <> 0
:: thesis: au100 <> 0

end;proof

thus
au100 <> 0
by A16; :: thesis: verum
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

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;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

then
are_Prop wr1,v010
by A23, ANPROJ_1:1;
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 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

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

now :: thesis: ( b <> 0 & av010 <> 0 )

hence
not b * av010 is zero
; :: thesis: verumthus
b <> 0
:: thesis: av010 <> 0

end;proof

thus
av010 <> 0
by A19; :: thesis: verum
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

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;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

then
are_Prop wr1,u100
by A24, ANPROJ_1:1;
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 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

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

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 )

p1,p2,p3 are_collinear
by A2, A3, Th12;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;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

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

( not dhr3 is zero & not |[0,1,1]| is zero )
by A80, EUCLID_5:4, FINSEQ_1:78;
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 ;

hence contradiction by A2, A3, ANPROJ_9:16, A61, A9; :: thesis: verum

end;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 )

then
Dir dwp3 = Dir010
by ANPROJ_1:22;
dwp3 `2 <> 0

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;proof

hence
are_Prop dwp3,|[0,1,0]|
by A82, ANPROJ_1:1; :: thesis: ( not dwp3 is zero & not |[0,1,0]| is zero )
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;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

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

hence contradiction by A2, A3, ANPROJ_9:16, A61, A9; :: thesis: verum

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

then reconsider f = (dwp3 `3) / (dwp3 `1) as non zero Real ;
thus
( dwp3 `3 <> 0 & dwp3 `1 <> 0 )
:: thesis: (dwp3 `3) / (dwp3 `1) is non zero Real

end;proof

hence
(dwp3 `3) / (dwp3 `1) is non zero Real
; :: thesis: verum
assume
( dwp3 `3 = 0 or dwp3 `1 = 0 )
; :: thesis: contradiction

end;per cases then
( dwp3 `3 = 0 or dwp3 `1 = 0 )
;

end;

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

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;.= (dwp3 `1) * |[1,0,0]| by EUCLID_5:8 ;

dwp3 `1 <> 0

proof

then A92:
are_Prop |[(dwp3 `1),0,(dwp3 `3)]|,|[1,0,0]|
by A89, ANPROJ_1:1;
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 ;

hence contradiction by A61, A9, ANPROJ_9:16, A2, A3; :: thesis: verum

end;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 )

then
Dir dwp3 = Dir010
by ANPROJ_1:22;
dwp3 `2 <> 0

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;proof

hence
are_Prop dwp3,|[0,1,0]|
by A91, ANPROJ_1:1; :: thesis: ( not dwp3 is zero & not |[0,1,0]| is zero )
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;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

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

hence contradiction by A61, A9, ANPROJ_9:16, A2, A3; :: thesis: verum

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

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

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;.= (dwp3 `3) * |[0,0,1]| by EUCLID_5:8 ;

dwp3 `3 <> 0

proof

then A98:
are_Prop |[(dwp3 `1),0,(dwp3 `3)]|,|[0,0,1]|
by A95, ANPROJ_1:1;
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 ;

hence contradiction by ANPROJ_9:16, A61, A9, A2, A3; :: thesis: verum

end;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 )

then
Dir dwp3 = Dir010
by ANPROJ_1:22;
dwp3 `2 <> 0

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;proof

hence
are_Prop dwp3,|[0,1,0]|
by A97, ANPROJ_1:1; :: thesis: ( not dwp3 is zero & not |[0,1,0]| is zero )
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;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

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

hence contradiction by ANPROJ_9:16, A61, A9, A2, A3; :: thesis: verum

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

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 )

A101: Dir pp3 =
Dir |[(dwp3 `1),0,(dwp3 `3)]|
by A69, EUCLID_5:3, A10, A61
|[(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;.= (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

.= Dir |[1,0,f]| by A100, ANPROJ_1:22 ;

A102: ( dwq3 `1 <> 0 & dwq3 `2 <> 0 )

proof

then reconsider g = (dwq3 `2) / (dwq3 `1) as non zero Real ;
assume
( dwq3 `1 = 0 or dwq3 `2 = 0 )
; :: thesis: contradiction

end;per cases then
( dwq3 `1 = 0 or dwq3 `2 = 0 )
;

end;

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 ;

hence contradiction by ANPROJ_9:16, A1; :: thesis: verum

end;.= (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 )

then
(homography N) . q3 = (homography N) . q1
by A86, ANPROJ_1:22, A11, A9;A105:
dwq3 `2 <> 0

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;proof

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 )
assume A106:
dwq3 `2 = 0
; :: thesis: contradiction

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;now :: thesis: ( dwq3 = (dwq3 `3) * |[0,0,1]| & dwq3 `3 <> 0 )

then A108:
are_Prop dwq3,|[0,0,1]|
by ANPROJ_1:1;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

end;.= (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;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

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

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

hence contradiction by ANPROJ_9:16, A1; :: thesis: verum

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

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

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;.= (dwq3 `1) * |[1,0,1]| by EUCLID_5:8 ;

A111: dwq3 `1 <> 0

proof

then A113:
are_Prop |[(dwq3 `1),(dwq3 `2),(dwq3 `1)]|,|[1,0,1]|
by A110, ANPROJ_1:1;
assume A112:
dwq3 `1 = 0
; :: thesis: contradiction

then q3 = p2 by ANPROJ_9:16, A70, A9;

hence contradiction by A1, A2, A3, A4, Th14; :: thesis: verum

end;now :: thesis: ( are_Prop dwq3,|[0,0,1]| & 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;now :: thesis: ( dwq3 = (dwq3 `3) * |[0,0,1]| & dwq3 `3 <> 0 )

hence
are_Prop dwq3,|[0,0,1]|
by ANPROJ_1:1; :: thesis: ( not dwq3 is zero & not |[0,0,1]| is zero )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;.= (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

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

then q3 = p2 by ANPROJ_9:16, A70, A9;

hence contradiction by A1, A2, A3, A4, Th14; :: thesis: verum

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

( (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;
|{|[1,0,0]|,|[0,0,1]|,|[1,0,1]|}| = 0

end;proof

hence
|[1,0,0]|,|[0,0,1]|,|[1,0,1]| are_LinDep
by ANPROJ_8:43; :: thesis: verum
( |[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;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

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

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

end;

A121:
not |[1,h,0]| is zero
by EUCLID_5:4, FINSEQ_1:78;now :: thesis: ( a * au100 <> 0 & |[(a * au100),(b * av010),0]| = (a * au100) * |[1,h,0]| )

hence
are_Prop |[(a * au100),(b * av010),0]|,|[1,h,0]|
by ANPROJ_1:1; :: thesis: verumthus
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;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

A122: (b2 * av111) + (a2 * au001) <> 0

proof

A128:
b2 * av111 <> 0
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 ;

A127: |[1,1,0]|,|[1,0,0]|,|[0,1,0]| are_LinDep

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;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 )

then A126:
Dir wr2 = Dir |[1,1,0]|
by ANPROJ_1:22;A124:
b2 <> 0

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;proof

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 )
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

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;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

then
are_Prop wr2,u001
by A125, ANPROJ_1:1;
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 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

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

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

A127: |[1,1,0]|,|[1,0,0]|,|[0,1,0]| are_LinDep

proof

( 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;
( |[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;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

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

proof

then reconsider i = ((b2 * av111) + (a2 * au001)) / (b2 * av111) as non zero Real by A122;
b2 <> 0

end;proof

hence
b2 * av111 <> 0
by A29, XCMPLX_1:6; :: thesis: verum
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

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;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

then
are_Prop wr2,u001
by A129, ANPROJ_1:1;
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 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

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

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 )

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;now :: thesis: ( |[(b2 * av111),(b2 * av111),((a2 * au001) + (b2 * av111))]| = (b2 * av111) * |[1,1,i]| & b2 * av111 <> 0 )

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 |[(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;.= |[((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

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

A132: now :: thesis: ( are_Prop |[0,wc,wc]|,|[0,1,1]| & 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;now :: thesis: ( |[0,wc,wc]| = wc * |[0,1,1]| & wc <> 0 )

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 |[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;.= wc * |[0,1,1]| by EUCLID_5:8 ; :: thesis: wc <> 0

thus wc <> 0 by A83; :: thesis: verum

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

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

then A180:
u1,u2,u3 are_LinDep
by A135, ANPROJ_8:43;
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

.= 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

.= ((- 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

.= (- 1) + (i * g) ;

hence i + h = 1 by A169, A148; :: thesis: verum

end;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

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
|{|[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;.= 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

.= 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

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
|{|[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;.= 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

.= ((- 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

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,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;.= 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

.= (- 1) + (i * g) ;

hence i + h = 1 by A169, A148; :: thesis: verum

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