let N be invertible Matrix of 3,F_Real; :: thesis: for P being Point of (ProjectiveSpace (TOP-REAL 3))

for a being non zero Element of F_Real st a * (1. (F_Real,3)) = N holds

(homography N) . P = P

let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for a being non zero Element of F_Real st a * (1. (F_Real,3)) = N holds

(homography N) . P = P

let a be non zero Element of F_Real; :: thesis: ( a * (1. (F_Real,3)) = N implies (homography N) . P = P )

assume A1: a * (1. (F_Real,3)) = N ; :: thesis: (homography N) . P = P

set aN = N;

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: P = 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) . P = Dir v by ANPROJ_8:def 4;

u in TOP-REAL 3 ;

then A9: uf in REAL 3 by A4, EUCLID:22;

A10: N * (<*uf*> @) is Matrix of 3,1,F_Real by A4, FINSEQ_3:153, ANPROJ_8:91;

p = N * (<*uf*> @) by A5, LAPLACE:def 9;

then A11: len p = 3 by A10, MATRIX_0:23;

A12: p = N * (<*uf*> @) by A5, LAPLACE:def 9

.= a * (<*uf*> @) by A1, A9, EUCLID_8:50, Lem06 ;

A13: v = <*(((a * (<*uf*> @)) . 1) . 1),(((a * (<*uf*> @)) . 2) . 1),(((a * (<*uf*> @)) . 3) . 1)*> by A6, A12, A11, ANPROJ_8:def 2;

.= <*(a * (u `1)),(a * (u `2)),(a * (u . 3))*> by EUCLID_5:def 2

.= <*(a * (u `1)),(a * (u `2)),(a * (u `3))*> by EUCLID_5:def 3

.= a * |[(u `1),(u `2),(u `3)]| by EUCLID_5:8

.= a * u by EUCLID_5:3 ;

not a is zero ;

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

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

for a being non zero Element of F_Real st a * (1. (F_Real,3)) = N holds

(homography N) . P = P

let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for a being non zero Element of F_Real st a * (1. (F_Real,3)) = N holds

(homography N) . P = P

let a be non zero Element of F_Real; :: thesis: ( a * (1. (F_Real,3)) = N implies (homography N) . P = P )

assume A1: a * (1. (F_Real,3)) = N ; :: thesis: (homography N) . P = P

set aN = N;

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: P = 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) . P = Dir v by ANPROJ_8:def 4;

u in TOP-REAL 3 ;

then A9: uf in REAL 3 by A4, EUCLID:22;

A10: N * (<*uf*> @) is Matrix of 3,1,F_Real by A4, FINSEQ_3:153, ANPROJ_8:91;

p = N * (<*uf*> @) by A5, LAPLACE:def 9;

then A11: len p = 3 by A10, MATRIX_0:23;

A12: p = N * (<*uf*> @) by A5, LAPLACE:def 9

.= a * (<*uf*> @) by A1, A9, EUCLID_8:50, Lem06 ;

A13: v = <*(((a * (<*uf*> @)) . 1) . 1),(((a * (<*uf*> @)) . 2) . 1),(((a * (<*uf*> @)) . 3) . 1)*> by A6, A12, A11, ANPROJ_8:def 2;

now :: thesis: ( ((a * (<*uf*> @)) . 1) . 1 = a * (u . 1) & ((a * (<*uf*> @)) . 2) . 1 = a * (u . 2) & ((a * (<*uf*> @)) . 3) . 1 = a * (u . 3) )

then A21: v =
<*(a * (u `1)),(a * (u . 2)),(a * (u . 3))*>
by A13, EUCLID_5:def 1
(1. (F_Real,3)) * (<*uf*> @) is 3,1 -size
by A9, EUCLID_8:50, ANPROJ_8:91;

then A14: <*uf*> @ is 3,1 -size by A9, EUCLID_8:50, ANPROJ_8:99;

A15: ( [1,1] in Indices (<*uf*> @) & [2,1] in Indices (<*uf*> @) & [3,1] in Indices (<*uf*> @) ) by A14, MATRIX_0:23, ANPROJ_8:2;

then A16: ( (a * (<*uf*> @)) * (1,1) = a * ((<*uf*> @) * (1,1)) & (a * (<*uf*> @)) * (2,1) = a * ((<*uf*> @) * (2,1)) & (a * (<*uf*> @)) * (3,1) = a * ((<*uf*> @) * (3,1)) ) by MATRIX_3:def 5;

A17: <*uf*> @ = <*<*(uf . 1)*>,<*(uf . 2)*>,<*(uf . 3)*>*> by A9, EUCLID_8:50, ANPROJ_8:77;

A18: ( len (<*uf*> @) = 3 & width (<*uf*> @) = 1 ) by A14, MATRIX_0:23;

A19: ( len (a * (<*uf*> @)) = len (<*uf*> @) & width (a * (<*uf*> @)) = width (<*uf*> @) ) by MATRIX_3:def 5;

a * (<*uf*> @) is Matrix of 3,1,F_Real by MATRIX_0:20, A19, A18;

then A20: ( [1,1] in Indices (a * (<*uf*> @)) & [2,1] in Indices (a * (<*uf*> @)) & [3,1] in Indices (a * (<*uf*> @)) ) by ANPROJ_8:2, MATRIX_0:23;

(<*uf*> @) * (1,1) = ((<*uf*> @) . 1) . 1 by A15, MATRPROB:14

.= <*(uf . 1)*> . 1 by A17, FINSEQ_1:45

.= uf . 1 by FINSEQ_1:def 8 ;

hence ((a * (<*uf*> @)) . 1) . 1 = a * (u . 1) by A4, A20, MATRPROB:14, A16; :: thesis: ( ((a * (<*uf*> @)) . 2) . 1 = a * (u . 2) & ((a * (<*uf*> @)) . 3) . 1 = a * (u . 3) )

(<*uf*> @) * (2,1) = ((<*uf*> @) . 2) . 1 by A15, MATRPROB:14

.= <*(uf . 2)*> . 1 by A17, FINSEQ_1:45

.= uf . 2 by FINSEQ_1:def 8 ;

hence ((a * (<*uf*> @)) . 2) . 1 = a * (u . 2) by A4, A20, MATRPROB:14, A16; :: thesis: ((a * (<*uf*> @)) . 3) . 1 = a * (u . 3)

(<*uf*> @) * (3,1) = ((<*uf*> @) . 3) . 1 by A15, MATRPROB:14

.= <*(uf . 3)*> . 1 by A17, FINSEQ_1:45

.= uf . 3 by FINSEQ_1:def 8 ;

hence ((a * (<*uf*> @)) . 3) . 1 = a * (u . 3) by A4, A20, MATRPROB:14, A16; :: thesis: verum

end;then A14: <*uf*> @ is 3,1 -size by A9, EUCLID_8:50, ANPROJ_8:99;

A15: ( [1,1] in Indices (<*uf*> @) & [2,1] in Indices (<*uf*> @) & [3,1] in Indices (<*uf*> @) ) by A14, MATRIX_0:23, ANPROJ_8:2;

then A16: ( (a * (<*uf*> @)) * (1,1) = a * ((<*uf*> @) * (1,1)) & (a * (<*uf*> @)) * (2,1) = a * ((<*uf*> @) * (2,1)) & (a * (<*uf*> @)) * (3,1) = a * ((<*uf*> @) * (3,1)) ) by MATRIX_3:def 5;

A17: <*uf*> @ = <*<*(uf . 1)*>,<*(uf . 2)*>,<*(uf . 3)*>*> by A9, EUCLID_8:50, ANPROJ_8:77;

A18: ( len (<*uf*> @) = 3 & width (<*uf*> @) = 1 ) by A14, MATRIX_0:23;

A19: ( len (a * (<*uf*> @)) = len (<*uf*> @) & width (a * (<*uf*> @)) = width (<*uf*> @) ) by MATRIX_3:def 5;

a * (<*uf*> @) is Matrix of 3,1,F_Real by MATRIX_0:20, A19, A18;

then A20: ( [1,1] in Indices (a * (<*uf*> @)) & [2,1] in Indices (a * (<*uf*> @)) & [3,1] in Indices (a * (<*uf*> @)) ) by ANPROJ_8:2, MATRIX_0:23;

(<*uf*> @) * (1,1) = ((<*uf*> @) . 1) . 1 by A15, MATRPROB:14

.= <*(uf . 1)*> . 1 by A17, FINSEQ_1:45

.= uf . 1 by FINSEQ_1:def 8 ;

hence ((a * (<*uf*> @)) . 1) . 1 = a * (u . 1) by A4, A20, MATRPROB:14, A16; :: thesis: ( ((a * (<*uf*> @)) . 2) . 1 = a * (u . 2) & ((a * (<*uf*> @)) . 3) . 1 = a * (u . 3) )

(<*uf*> @) * (2,1) = ((<*uf*> @) . 2) . 1 by A15, MATRPROB:14

.= <*(uf . 2)*> . 1 by A17, FINSEQ_1:45

.= uf . 2 by FINSEQ_1:def 8 ;

hence ((a * (<*uf*> @)) . 2) . 1 = a * (u . 2) by A4, A20, MATRPROB:14, A16; :: thesis: ((a * (<*uf*> @)) . 3) . 1 = a * (u . 3)

(<*uf*> @) * (3,1) = ((<*uf*> @) . 3) . 1 by A15, MATRPROB:14

.= <*(uf . 3)*> . 1 by A17, FINSEQ_1:45

.= uf . 3 by FINSEQ_1:def 8 ;

hence ((a * (<*uf*> @)) . 3) . 1 = a * (u . 3) by A4, A20, MATRPROB:14, A16; :: thesis: verum

.= <*(a * (u `1)),(a * (u `2)),(a * (u . 3))*> by EUCLID_5:def 2

.= <*(a * (u `1)),(a * (u `2)),(a * (u `3))*> by EUCLID_5:def 3

.= a * |[(u `1),(u `2),(u `3)]| by EUCLID_5:8

.= a * u by EUCLID_5:3 ;

not a is zero ;

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

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