let a, b, c, ia, ib, ic be non zero Element of F_Real; :: thesis: for P being Point of (ProjectiveSpace (TOP-REAL 3))

for N being invertible Matrix of 3,F_Real st P = Dir |[a,b,c]| & ia = 1 / a & ib = 1 / b & ic = 1 / c & N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> holds

(homography N) . P = Dir |[1,1,1]|

let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for N being invertible Matrix of 3,F_Real st P = Dir |[a,b,c]| & ia = 1 / a & ib = 1 / b & ic = 1 / c & N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> holds

(homography N) . P = Dir |[1,1,1]|

let N be invertible Matrix of 3,F_Real; :: thesis: ( P = Dir |[a,b,c]| & ia = 1 / a & ib = 1 / b & ic = 1 / c & N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> implies (homography N) . P = Dir |[1,1,1]| )

assume that

A1: P = Dir |[a,b,c]| and

A2: ia = 1 / a and

A3: ib = 1 / b and

A4: ic = 1 / c and

A5: N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> ; :: thesis: (homography N) . P = Dir |[1,1,1]|

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

A15: P = Dir u and

A16: not u is zero and

A17: u = uf and

A18: p = N * uf and

A19: v = M2F p and

A20: not v is zero and

A21: (homography N) . P = Dir v by ANPROJ_8:def 4;

not |[a,b,c]| is zero

then consider d being Real such that

A22: d <> 0 and

A23: u = d * |[a,b,c]| by ANPROJ_1:1;

A24: u = <*(d * a),(d * b),(d * c)*> by A23, EUCLID_5:8;

A25: ( uf . 1 = d * a & uf . 2 = d * b & uf . 3 = d * c ) by A24, A17, FINSEQ_1:45;

u in TOP-REAL 3 ;

then u in REAL 3 by EUCLID:22;

then A26: <*uf*> @ = <*<*(d * a)*>,<*(d * b)*>,<*(d * c)*>*> by A25, A17, EUCLID_8:50, ANPROJ_8:77;

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

reconsider z = 0 , da = d * a, db = d * b, dc = d * c as Element of F_Real by XREAL_0:def 1;

A27: p = N * Mu by A18, LAPLACE:def 9

.= <*<*(((ia * da) + (z * db)) + (z * dc))*>,<*(((z * da) + (ib * db)) + (z * dc))*>,<*(((z * da) + (z * db)) + (ic * dc))*>*> by A26, A5, Th08

.= <*<*(ia * da)*>,<*(ib * db)*>,<*(ic * dc)*>*> ;

A28: v = |[(ia * da),(ib * db),(ic * dc)]|

.= d * |[1,1,1]| by EUCLID_5:8 ;

then are_Prop v,|[1,1,1]| by A22, ANPROJ_1:1;

hence (homography N) . P = Dir |[1,1,1]| by Th11, A20, ANPROJ_1:22, A21; :: thesis: verum

for N being invertible Matrix of 3,F_Real st P = Dir |[a,b,c]| & ia = 1 / a & ib = 1 / b & ic = 1 / c & N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> holds

(homography N) . P = Dir |[1,1,1]|

let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for N being invertible Matrix of 3,F_Real st P = Dir |[a,b,c]| & ia = 1 / a & ib = 1 / b & ic = 1 / c & N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> holds

(homography N) . P = Dir |[1,1,1]|

let N be invertible Matrix of 3,F_Real; :: thesis: ( P = Dir |[a,b,c]| & ia = 1 / a & ib = 1 / b & ic = 1 / c & N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> implies (homography N) . P = Dir |[1,1,1]| )

assume that

A1: P = Dir |[a,b,c]| and

A2: ia = 1 / a and

A3: ib = 1 / b and

A4: ic = 1 / c and

A5: N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> ; :: thesis: (homography N) . P = Dir |[1,1,1]|

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

A15: P = Dir u and

A16: not u is zero and

A17: u = uf and

A18: p = N * uf and

A19: v = M2F p and

A20: not v is zero and

A21: (homography N) . P = Dir v by ANPROJ_8:def 4;

not |[a,b,c]| is zero

proof

then
are_Prop u,|[a,b,c]|
by A1, A15, A16, ANPROJ_1:22;
assume
|[a,b,c]| is zero
; :: thesis: contradiction

then ( a is zero & b is zero & c is zero ) by EUCLID_5:4, FINSEQ_1:78;

hence contradiction ; :: thesis: verum

end;then ( a is zero & b is zero & c is zero ) by EUCLID_5:4, FINSEQ_1:78;

hence contradiction ; :: thesis: verum

then consider d being Real such that

A22: d <> 0 and

A23: u = d * |[a,b,c]| by ANPROJ_1:1;

A24: u = <*(d * a),(d * b),(d * c)*> by A23, EUCLID_5:8;

A25: ( uf . 1 = d * a & uf . 2 = d * b & uf . 3 = d * c ) by A24, A17, FINSEQ_1:45;

u in TOP-REAL 3 ;

then u in REAL 3 by EUCLID:22;

then A26: <*uf*> @ = <*<*(d * a)*>,<*(d * b)*>,<*(d * c)*>*> by A25, A17, EUCLID_8:50, ANPROJ_8:77;

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

reconsider z = 0 , da = d * a, db = d * b, dc = d * c as Element of F_Real by XREAL_0:def 1;

A27: p = N * Mu by A18, LAPLACE:def 9

.= <*<*(((ia * da) + (z * db)) + (z * dc))*>,<*(((z * da) + (ib * db)) + (z * dc))*>,<*(((z * da) + (z * db)) + (ic * dc))*>*> by A26, A5, Th08

.= <*<*(ia * da)*>,<*(ib * db)*>,<*(ic * dc)*>*> ;

A28: v = |[(ia * da),(ib * db),(ic * dc)]|

proof

A31:
( not a is zero & not b is zero & not c is zero )
;
A29:
( <*(ia * da)*> . 1 = ia * da & <*(ib * db)*> . 1 = ib * db & <*(ic * dc)*> . 1 = ic * dc )
by FINSEQ_1:def 8;

A30: ( p . 1 = <*(ia * da)*> & p . 2 = <*(ib * db)*> & p . 3 = <*(ic * dc)*> ) by A27, FINSEQ_1:45;

len p = 3 by A27, FINSEQ_1:45;

hence v = |[(ia * da),(ib * db),(ic * dc)]| by A29, A30, A19, ANPROJ_8:def 2; :: thesis: verum

end;A30: ( p . 1 = <*(ia * da)*> & p . 2 = <*(ib * db)*> & p . 3 = <*(ic * dc)*> ) by A27, FINSEQ_1:45;

len p = 3 by A27, FINSEQ_1:45;

hence v = |[(ia * da),(ib * db),(ic * dc)]| by A29, A30, A19, ANPROJ_8:def 2; :: thesis: verum

now :: thesis: ( ia * da = d & ib * db = d & ic * dc = d )

then v =
|[(d * 1),(d * 1),(d * 1)]|
by A28
thus ia * da =
((1 / a) * a) * d
by A2

.= 1 * d by A31, XCMPLX_1:106

.= d ; :: thesis: ( ib * db = d & ic * dc = d )

thus ib * db = ((1 / b) * b) * d by A3

.= 1 * d by A31, XCMPLX_1:106

.= d ; :: thesis: ic * dc = d

thus ic * dc = ((1 / c) * c) * d by A4

.= 1 * d by A31, XCMPLX_1:106

.= d ; :: thesis: verum

end;.= 1 * d by A31, XCMPLX_1:106

.= d ; :: thesis: ( ib * db = d & ic * dc = d )

thus ib * db = ((1 / b) * b) * d by A3

.= 1 * d by A31, XCMPLX_1:106

.= d ; :: thesis: ic * dc = d

thus ic * dc = ((1 / c) * c) * d by A4

.= 1 * d by A31, XCMPLX_1:106

.= d ; :: thesis: verum

.= d * |[1,1,1]| by EUCLID_5:8 ;

then are_Prop v,|[1,1,1]| by A22, ANPROJ_1:1;

hence (homography N) . P = Dir |[1,1,1]| by Th11, A20, ANPROJ_1:22, A21; :: thesis: verum