let N be invertible Matrix of 3,F_Real; for n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real
for P, Q being Point of (ProjectiveSpace (TOP-REAL 3))
for u, v being non zero Element of (TOP-REAL 3) st N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & Q = Dir v & Q = (homography N) . P & u . 3 = 1 holds
ex a being non zero Real st
( v . 1 = a * (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) & v . 2 = a * (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) & v . 3 = a * (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) )
let n11, n12, n13, n21, n22, n23, n31, n32, n33 be Element of F_Real; for P, Q being Point of (ProjectiveSpace (TOP-REAL 3))
for u, v being non zero Element of (TOP-REAL 3) st N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & Q = Dir v & Q = (homography N) . P & u . 3 = 1 holds
ex a being non zero Real st
( v . 1 = a * (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) & v . 2 = a * (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) & v . 3 = a * (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) )
let P, Q be Point of (ProjectiveSpace (TOP-REAL 3)); for u, v being non zero Element of (TOP-REAL 3) st N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & Q = Dir v & Q = (homography N) . P & u . 3 = 1 holds
ex a being non zero Real st
( v . 1 = a * (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) & v . 2 = a * (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) & v . 3 = a * (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) )
let u, v be non zero Element of (TOP-REAL 3); ( N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & Q = Dir v & Q = (homography N) . P & u . 3 = 1 implies ex a being non zero Real st
( v . 1 = a * (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) & v . 2 = a * (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) & v . 3 = a * (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) ) )
assume A1:
( N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & Q = Dir v & Q = (homography N) . P & u . 3 = 1 )
; ex a being non zero Real st
( v . 1 = a * (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) & v . 2 = a * (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) & v . 3 = a * (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) )
consider u9, v9 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 u9 & not u9 is zero & u9 = uf & p = N * uf & v9 = M2F p & not v9 is zero & (homography N) . P = Dir v9 )
by ANPROJ_8:def 4;
are_Prop u,u9
by A1, A2, ANPROJ_1:22;
then consider a being Real such that
A3:
( a <> 0 & u9 = a * u )
by ANPROJ_1:1;
A4: |[(u9 `1),(u9 `2),(u9 `3)]| =
u9
by EUCLID_5:3
.=
|[(a * (u `1)),(a * (u `2)),(a * (u `3))]|
by A3, EUCLID_5:7
.=
|[(a * (u `1)),(a * (u `2)),(a * (u . 3))]|
by EUCLID_5:def 3
.=
|[(a * (u `1)),(a * (u `2)),a]|
by A1
;
reconsider uf1 = a * (u `1), uf2 = a * (u `2), uf3 = a as Element of F_Real by XREAL_0:def 1;
reconsider x1 = ((n11 * (u `1)) + (n12 * (u `2))) + n13, x2 = ((n21 * (u `1)) + (n22 * (u `2))) + n23, x3 = ((n31 * (u `1)) + (n32 * (u `2))) + n33 as Element of REAL by XREAL_0:def 1;
uf = <*uf1,uf2,uf3*>
by A2, A4, EUCLID_5:3;
then A5: v9 =
<*(((n11 * uf1) + (n12 * uf2)) + (n13 * uf3)),(((n21 * uf1) + (n22 * uf2)) + (n23 * uf3)),(((n31 * uf1) + (n32 * uf2)) + (n33 * uf3))*>
by A1, A2, PASCAL:8
.=
<*(a * (((n11 * (u `1)) + (n12 * (u `2))) + n13)),(a * (((n21 * (u `1)) + (n22 * (u `2))) + n23)),(a * (((n31 * (u `1)) + (n32 * (u `2))) + n33))*>
.=
a * |[x1,x2,x3]|
by EUCLID_5:8
;
are_Prop v,v9
by A1, A2, ANPROJ_1:22;
then consider b being Real such that
A6:
b <> 0
and
A7:
v = b * v9
by ANPROJ_1:1;
A8: v =
b * |[(a * x1),(a * x2),(a * x3)]|
by A7, A5, EUCLID_5:8
.=
|[(b * (a * x1)),(b * (a * x2)),(b * (a * x3))]|
by EUCLID_5:8
.=
|[((b * a) * (((n11 * (u `1)) + (n12 * (u `2))) + n13)),((b * a) * (((n21 * (u `1)) + (n22 * (u `2))) + n23)),((b * a) * (((n31 * (u `1)) + (n32 * (u `2))) + n33))]|
;
reconsider c = b * a as non zero Real by A3, A6;
take
c
; ( v . 1 = c * (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) & v . 2 = c * (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) & v . 3 = c * (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) )
( v `1 = c * (((n11 * (u `1)) + (n12 * (u `2))) + n13) & v `2 = c * (((n21 * (u `1)) + (n22 * (u `2))) + n23) & v `3 = c * (((n31 * (u `1)) + (n32 * (u `2))) + n33) )
by A8, EUCLID_5:2;
then
( v . 1 = c * (((n11 * (u `1)) + (n12 * (u `2))) + n13) & v . 2 = c * (((n21 * (u `1)) + (n22 * (u `2))) + n23) & v . 3 = c * (((n31 * (u `1)) + (n32 * (u `2))) + n33) )
by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then
( v . 1 = c * (((n11 * (u . 1)) + (n12 * (u `2))) + n13) & v . 2 = c * (((n21 * (u . 1)) + (n22 * (u `2))) + n23) & v . 3 = c * (((n31 * (u . 1)) + (n32 * (u `2))) + n33) )
by EUCLID_5:def 1;
hence
( v . 1 = c * (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) & v . 2 = c * (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) & v . 3 = c * (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) )
by EUCLID_5:def 2; verum