let N be invertible Matrix of 3,F_Real; :: thesis: 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; :: thesis: 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)); :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum