let N be invertible Matrix of 3,F_Real; :: thesis: for a, b, c being non zero Element of F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds

( (homography N) . Dir100 = Dir100 & (homography N) . Dir010 = Dir010 & (homography N) . Dir001 = Dir001 )

let a, b, c be non zero Element of F_Real; :: thesis: ( N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> implies ( (homography N) . Dir100 = Dir100 & (homography N) . Dir010 = Dir010 & (homography N) . Dir001 = Dir001 ) )

assume A1: N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> ; :: thesis: ( (homography N) . Dir100 = Dir100 & (homography N) . Dir010 = Dir010 & (homography N) . Dir001 = Dir001 )

thus (homography N) . Dir100 = Dir100 :: thesis: ( (homography N) . Dir010 = Dir010 & (homography N) . Dir001 = Dir001 )

( (homography N) . Dir100 = Dir100 & (homography N) . Dir010 = Dir010 & (homography N) . Dir001 = Dir001 )

let a, b, c be non zero Element of F_Real; :: thesis: ( N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> implies ( (homography N) . Dir100 = Dir100 & (homography N) . Dir010 = Dir010 & (homography N) . Dir001 = Dir001 ) )

assume A1: N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> ; :: thesis: ( (homography N) . Dir100 = Dir100 & (homography N) . Dir010 = Dir010 & (homography N) . Dir001 = Dir001 )

thus (homography N) . Dir100 = Dir100 :: thesis: ( (homography N) . Dir010 = Dir010 & (homography N) . Dir001 = Dir001 )

proof

thus
(homography N) . Dir010 = Dir010
:: thesis: (homography N) . Dir001 = Dir001
consider u, v being Element of (TOP-REAL 3), uf being FinSequence of F_Real, p being FinSequence of 1 -tuples_on REAL such that

A2: Dir100 = Dir u and

A3: not u is zero and

A4: u = uf and

A5: p = N * uf and

A6: v = M2F p and

A7: not v is zero and

A8: (homography N) . Dir100 = Dir v by ANPROJ_8:def 4;

not |[1,0,0]| is zero by EUCLID_8:def 1, Th13;

then are_Prop u,|[1,0,0]| by A2, A3, ANPROJ_1:22;

then consider d being Real such that

d <> 0 and

A9: u = d * |[1,0,0]| by ANPROJ_1:1;

A10: u = |[(d * 1),(d * 0),(d * 0)]| by A9, EUCLID_5:8

.= |[d,0,0]| ;

then ( u `1 = d & u `2 = 0 & u `3 = 0 ) by EUCLID_5:2;

then A11: ( uf . 1 = d & uf . 2 = 0 & uf . 3 = 0 ) by A4, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

u in TOP-REAL 3 ;

then u in REAL 3 by EUCLID:22;

then A12: <*uf*> @ = <*<*d*>,<*0*>,<*0*>*> by A11, A4, EUCLID_8:50, ANPROJ_8:77;

then reconsider Mu = <*uf*> @ as Matrix of 3,1,F_Real by ANPROJ_8:4;

reconsider z = 0 as Element of F_Real ;

reconsider d = d as Element of F_Real by XREAL_0:def 1;

A13: p = N * Mu by A5, LAPLACE:def 9

.= <*<*(((a * d) + (z * z)) + (z * z))*>,<*(((z * d) + (b * z)) + (z * z))*>,<*(((z * d) + (z * z)) + (c * z))*>*> by A1, A12, Th08

.= <*<*(a * d)*>,<*0*>,<*0*>*> ;

v = |[(a * d),0,0]|

.= a * u by A10, EUCLID_5:8 ;

not a is zero ;

then are_Prop v,u by A16, ANPROJ_1:1;

hence (homography N) . Dir100 = Dir100 by A2, A3, A7, A8, ANPROJ_1:22; :: thesis: verum

end;A2: Dir100 = Dir u and

A3: not u is zero and

A4: u = uf and

A5: p = N * uf and

A6: v = M2F p and

A7: not v is zero and

A8: (homography N) . Dir100 = Dir v by ANPROJ_8:def 4;

not |[1,0,0]| is zero by EUCLID_8:def 1, Th13;

then are_Prop u,|[1,0,0]| by A2, A3, ANPROJ_1:22;

then consider d being Real such that

d <> 0 and

A9: u = d * |[1,0,0]| by ANPROJ_1:1;

A10: u = |[(d * 1),(d * 0),(d * 0)]| by A9, EUCLID_5:8

.= |[d,0,0]| ;

then ( u `1 = d & u `2 = 0 & u `3 = 0 ) by EUCLID_5:2;

then A11: ( uf . 1 = d & uf . 2 = 0 & uf . 3 = 0 ) by A4, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

u in TOP-REAL 3 ;

then u in REAL 3 by EUCLID:22;

then A12: <*uf*> @ = <*<*d*>,<*0*>,<*0*>*> by A11, A4, EUCLID_8:50, ANPROJ_8:77;

then reconsider Mu = <*uf*> @ as Matrix of 3,1,F_Real by ANPROJ_8:4;

reconsider z = 0 as Element of F_Real ;

reconsider d = d as Element of F_Real by XREAL_0:def 1;

A13: p = N * Mu by A5, LAPLACE:def 9

.= <*<*(((a * d) + (z * z)) + (z * z))*>,<*(((z * d) + (b * z)) + (z * z))*>,<*(((z * d) + (z * z)) + (c * z))*>*> by A1, A12, Th08

.= <*<*(a * d)*>,<*0*>,<*0*>*> ;

v = |[(a * d),0,0]|

proof

then A16: v =
|[(a * d),(a * 0),(a * 0)]|
A14:
( <*(a * d)*> . 1 = a * d & <*0*> . 1 = 0 )
by FINSEQ_1:def 8;

A15: ( p . 1 = <*(a * d)*> & p . 2 = <*0*> & p . 3 = <*0*> ) by A13, FINSEQ_1:45;

len p = 3 by A13, FINSEQ_1:45;

hence v = |[(a * d),0,0]| by A14, A15, A6, ANPROJ_8:def 2; :: thesis: verum

end;A15: ( p . 1 = <*(a * d)*> & p . 2 = <*0*> & p . 3 = <*0*> ) by A13, FINSEQ_1:45;

len p = 3 by A13, FINSEQ_1:45;

hence v = |[(a * d),0,0]| by A14, A15, A6, ANPROJ_8:def 2; :: thesis: verum

.= a * u by A10, EUCLID_5:8 ;

not a is zero ;

then are_Prop v,u by A16, ANPROJ_1:1;

hence (homography N) . Dir100 = Dir100 by A2, A3, A7, A8, ANPROJ_1:22; :: thesis: verum

proof

thus
(homography N) . Dir001 = Dir001
:: thesis: verum
consider u, v being Element of (TOP-REAL 3), uf being FinSequence of F_Real, p being FinSequence of 1 -tuples_on REAL such that

A17: Dir010 = Dir u and

A18: not u is zero and

A19: u = uf and

A20: p = N * uf and

A21: v = M2F p and

A22: not v is zero and

A23: (homography N) . Dir010 = Dir v by ANPROJ_8:def 4;

not |[0,1,0]| is zero by EUCLID_8:def 2, Th13;

then are_Prop u,|[0,1,0]| by A17, A18, ANPROJ_1:22;

then consider d being Real such that

d <> 0 and

A24: u = d * |[0,1,0]| by ANPROJ_1:1;

A25: u = |[(d * 0),(d * 1),(d * 0)]| by A24, EUCLID_5:8

.= |[0,d,0]| ;

then ( u `1 = 0 & u `2 = d & u `3 = 0 ) by EUCLID_5:2;

then A26: ( uf . 1 = 0 & uf . 2 = d & uf . 3 = 0 ) by A19, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

u in TOP-REAL 3 ;

then u in REAL 3 by EUCLID:22;

then A27: <*uf*> @ = <*<*0*>,<*d*>,<*0*>*> by A26, A19, EUCLID_8:50, ANPROJ_8:77;

reconsider Mu = <*uf*> @ as Matrix of 3,1,F_Real by A27, ANPROJ_8:4;

reconsider z = 0 as Element of F_Real ;

reconsider d = d as Element of F_Real by XREAL_0:def 1;

A28: p = N * Mu by A20, LAPLACE:def 9

.= <*<*(((a * z) + (z * d)) + (z * z))*>,<*(((z * z) + (b * d)) + (z * z))*>,<*(((z * d) + (z * z)) + (c * z))*>*> by A1, A27, Th08

.= <*<*0*>,<*(b * d)*>,<*0*>*> ;

v = |[0,(b * d),0]|

.= b * u by A25, EUCLID_5:8 ;

not b is zero ;

then are_Prop v,u by A31, ANPROJ_1:1;

hence (homography N) . Dir010 = Dir010 by A17, A18, A22, A23, ANPROJ_1:22; :: thesis: verum

end;A17: Dir010 = Dir u and

A18: not u is zero and

A19: u = uf and

A20: p = N * uf and

A21: v = M2F p and

A22: not v is zero and

A23: (homography N) . Dir010 = Dir v by ANPROJ_8:def 4;

not |[0,1,0]| is zero by EUCLID_8:def 2, Th13;

then are_Prop u,|[0,1,0]| by A17, A18, ANPROJ_1:22;

then consider d being Real such that

d <> 0 and

A24: u = d * |[0,1,0]| by ANPROJ_1:1;

A25: u = |[(d * 0),(d * 1),(d * 0)]| by A24, EUCLID_5:8

.= |[0,d,0]| ;

then ( u `1 = 0 & u `2 = d & u `3 = 0 ) by EUCLID_5:2;

then A26: ( uf . 1 = 0 & uf . 2 = d & uf . 3 = 0 ) by A19, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

u in TOP-REAL 3 ;

then u in REAL 3 by EUCLID:22;

then A27: <*uf*> @ = <*<*0*>,<*d*>,<*0*>*> by A26, A19, EUCLID_8:50, ANPROJ_8:77;

reconsider Mu = <*uf*> @ as Matrix of 3,1,F_Real by A27, ANPROJ_8:4;

reconsider z = 0 as Element of F_Real ;

reconsider d = d as Element of F_Real by XREAL_0:def 1;

A28: p = N * Mu by A20, LAPLACE:def 9

.= <*<*(((a * z) + (z * d)) + (z * z))*>,<*(((z * z) + (b * d)) + (z * z))*>,<*(((z * d) + (z * z)) + (c * z))*>*> by A1, A27, Th08

.= <*<*0*>,<*(b * d)*>,<*0*>*> ;

v = |[0,(b * d),0]|

proof

then A31: v =
|[(b * 0),(b * d),(b * 0)]|
A29:
( <*0*> . 1 = 0 & <*(b * d)*> . 1 = b * d )
by FINSEQ_1:def 8;

A30: ( p . 1 = <*0*> & p . 2 = <*(b * d)*> & p . 3 = <*0*> ) by A28, FINSEQ_1:45;

len p = 3 by A28, FINSEQ_1:45;

hence v = |[0,(b * d),0]| by A29, A30, A21, ANPROJ_8:def 2; :: thesis: verum

end;A30: ( p . 1 = <*0*> & p . 2 = <*(b * d)*> & p . 3 = <*0*> ) by A28, FINSEQ_1:45;

len p = 3 by A28, FINSEQ_1:45;

hence v = |[0,(b * d),0]| by A29, A30, A21, ANPROJ_8:def 2; :: thesis: verum

.= b * u by A25, EUCLID_5:8 ;

not b is zero ;

then are_Prop v,u by A31, ANPROJ_1:1;

hence (homography N) . Dir010 = Dir010 by A17, A18, A22, A23, ANPROJ_1:22; :: thesis: verum

proof

consider u, v being Element of (TOP-REAL 3), uf being FinSequence of F_Real, p being FinSequence of 1 -tuples_on REAL such that

A31BIS: Dir001 = Dir u and

A32: not u is zero and

A33: u = uf and

A34: p = N * uf and

A35: v = M2F p and

A36: not v is zero and

A37: (homography N) . Dir001 = Dir v by ANPROJ_8:def 4;

not |[0,0,1]| is zero by EUCLID_8:def 3, Th13;

then are_Prop u,|[0,0,1]| by A31BIS, A32, ANPROJ_1:22;

then consider d being Real such that

d <> 0 and

A38: u = d * |[0,0,1]| by ANPROJ_1:1;

A39: u = |[(d * 0),(d * 0),(d * 1)]| by A38, EUCLID_5:8

.= |[0,0,d]| ;

then ( u `1 = 0 & u `2 = 0 & u `3 = d ) by EUCLID_5:2;

then A40: ( uf . 1 = 0 & uf . 2 = 0 & uf . 3 = d ) by A33, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

u in TOP-REAL 3 ;

then u in REAL 3 by EUCLID:22;

then A41: <*uf*> @ = <*<*0*>,<*0*>,<*d*>*> by A40, A33, EUCLID_8:50, ANPROJ_8:77;

reconsider Mu = <*uf*> @ as Matrix of 3,1,F_Real by A41, ANPROJ_8:4;

reconsider z = 0 as Element of F_Real ;

reconsider d = d as Element of F_Real by XREAL_0:def 1;

A42: p = N * Mu by A34, LAPLACE:def 9

.= <*<*(((a * z) + (z * z)) + (z * d))*>,<*(((z * z) + (b * z)) + (z * d))*>,<*(((z * z) + (z * z)) + (c * d))*>*> by A1, A41, Th08

.= <*<*0*>,<*0*>,<*(c * d)*>*> ;

v = |[0,0,(c * d)]|

.= c * u by A39, EUCLID_5:8 ;

not c is zero ;

then are_Prop v,u by A45, ANPROJ_1:1;

hence (homography N) . Dir001 = Dir001 by A31BIS, A32, A36, A37, ANPROJ_1:22; :: thesis: verum

end;A31BIS: Dir001 = Dir u and

A32: not u is zero and

A33: u = uf and

A34: p = N * uf and

A35: v = M2F p and

A36: not v is zero and

A37: (homography N) . Dir001 = Dir v by ANPROJ_8:def 4;

not |[0,0,1]| is zero by EUCLID_8:def 3, Th13;

then are_Prop u,|[0,0,1]| by A31BIS, A32, ANPROJ_1:22;

then consider d being Real such that

d <> 0 and

A38: u = d * |[0,0,1]| by ANPROJ_1:1;

A39: u = |[(d * 0),(d * 0),(d * 1)]| by A38, EUCLID_5:8

.= |[0,0,d]| ;

then ( u `1 = 0 & u `2 = 0 & u `3 = d ) by EUCLID_5:2;

then A40: ( uf . 1 = 0 & uf . 2 = 0 & uf . 3 = d ) by A33, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

u in TOP-REAL 3 ;

then u in REAL 3 by EUCLID:22;

then A41: <*uf*> @ = <*<*0*>,<*0*>,<*d*>*> by A40, A33, EUCLID_8:50, ANPROJ_8:77;

reconsider Mu = <*uf*> @ as Matrix of 3,1,F_Real by A41, ANPROJ_8:4;

reconsider z = 0 as Element of F_Real ;

reconsider d = d as Element of F_Real by XREAL_0:def 1;

A42: p = N * Mu by A34, LAPLACE:def 9

.= <*<*(((a * z) + (z * z)) + (z * d))*>,<*(((z * z) + (b * z)) + (z * d))*>,<*(((z * z) + (z * z)) + (c * d))*>*> by A1, A41, Th08

.= <*<*0*>,<*0*>,<*(c * d)*>*> ;

v = |[0,0,(c * d)]|

proof

then A45: v =
|[(c * 0),(c * 0),(c * d)]|
A43:
( <*(c * d)*> . 1 = c * d & <*0*> . 1 = 0 )
by FINSEQ_1:def 8;

A44: ( p . 3 = <*(c * d)*> & p . 2 = <*0*> & p . 1 = <*0*> ) by A42, FINSEQ_1:45;

len p = 3 by A42, FINSEQ_1:45;

hence v = |[0,0,(c * d)]| by A43, A44, A35, ANPROJ_8:def 2; :: thesis: verum

end;A44: ( p . 3 = <*(c * d)*> & p . 2 = <*0*> & p . 1 = <*0*> ) by A42, FINSEQ_1:45;

len p = 3 by A42, FINSEQ_1:45;

hence v = |[0,0,(c * d)]| by A43, A44, A35, ANPROJ_8:def 2; :: thesis: verum

.= c * u by A39, EUCLID_5:8 ;

not c is zero ;

then are_Prop v,u by A45, ANPROJ_1:1;

hence (homography N) . Dir001 = Dir001 by A31BIS, A32, A36, A37, ANPROJ_1:22; :: thesis: verum