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
( () . Dir100 = Dir100 & () . Dir010 = Dir010 & () . 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 ( () . Dir100 = Dir100 & () . Dir010 = Dir010 & () . Dir001 = Dir001 ) )
assume A1: N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> ; :: thesis:
thus (homography N) . Dir100 = Dir100 :: thesis:
proof
consider u, v being Element of (), 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 ;
then are_Prop u,|[1,0,0]| by ;
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
.= |[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 ;
u in TOP-REAL 3 ;
then u in REAL 3 by EUCLID:22;
then A12: <*uf*> @ = by ;
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
.= <*<*(((a * d) + (z * z)) + (z * z))*>,<*(((z * d) + (b * z)) + (z * z))*>,<*(((z * d) + (z * z)) + (c * z))*>*> by
.= <*<*(a * d)*>,,*> ;
v = |[(a * d),0,0]|
proof
A14: ( <*(a * d)*> . 1 = a * d & . 1 = 0 ) by FINSEQ_1:def 8;
A15: ( p . 1 = <*(a * d)*> & p . 2 = & p . 3 = ) by ;
len p = 3 by ;
hence v = |[(a * d),0,0]| by ; :: thesis: verum
end;
then A16: v = |[(a * d),(a * 0),(a * 0)]|
.= a * u by ;
not a is zero ;
then are_Prop v,u by ;
hence (homography N) . Dir100 = Dir100 by ; :: thesis: verum
end;
thus (homography N) . Dir010 = Dir010 :: thesis:
proof
consider u, v being Element of (), 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 ;
then are_Prop u,|[0,1,0]| by ;
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
.= |[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 ;
u in TOP-REAL 3 ;
then u in REAL 3 by EUCLID:22;
then A27: <*uf*> @ = by ;
reconsider Mu = <*uf*> @ as Matrix of 3,1,F_Real by ;
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
.= <*<*(((a * z) + (z * d)) + (z * z))*>,<*(((z * z) + (b * d)) + (z * z))*>,<*(((z * d) + (z * z)) + (c * z))*>*> by
.= <*,<*(b * d)*>,*> ;
v = |[0,(b * d),0]|
proof
A29: ( <*0*> . 1 = 0 & <*(b * d)*> . 1 = b * d ) by FINSEQ_1:def 8;
A30: ( p . 1 = & p . 2 = <*(b * d)*> & p . 3 = ) by ;
len p = 3 by ;
hence v = |[0,(b * d),0]| by ; :: thesis: verum
end;
then A31: v = |[(b * 0),(b * d),(b * 0)]|
.= b * u by ;
not b is zero ;
then are_Prop v,u by ;
hence (homography N) . Dir010 = Dir010 by ; :: thesis: verum
end;
thus (homography N) . Dir001 = Dir001 :: thesis: verum
proof
consider u, v being Element of (), 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 ;
then are_Prop u,|[0,0,1]| by ;
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
.= |[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 ;
u in TOP-REAL 3 ;
then u in REAL 3 by EUCLID:22;
then A41: <*uf*> @ = by ;
reconsider Mu = <*uf*> @ as Matrix of 3,1,F_Real by ;
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
.= <*<*(((a * z) + (z * z)) + (z * d))*>,<*(((z * z) + (b * z)) + (z * d))*>,<*(((z * z) + (z * z)) + (c * d))*>*> by
.= <*,,<*(c * d)*>*> ;
v = |[0,0,(c * d)]|
proof
A43: ( <*(c * d)*> . 1 = c * d & . 1 = 0 ) by FINSEQ_1:def 8;
A44: ( p . 3 = <*(c * d)*> & p . 2 = & p . 1 = ) by ;
len p = 3 by ;
hence v = |[0,0,(c * d)]| by ; :: thesis: verum
end;
then A45: v = |[(c * 0),(c * 0),(c * d)]|
.= c * u by ;
not c is zero ;
then are_Prop v,u by ;
hence (homography N) . Dir001 = Dir001 by ; :: thesis: verum
end;