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 being Element of BK_model
for 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 & v . 3 = 1 holds
( ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0 & v . 1 = (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) & v . 2 = (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((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 being Element of BK_model
for 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 & v . 3 = 1 holds
( ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0 & v . 1 = (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) & v . 2 = (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) )
let P be Element of BK_model ; :: thesis: for 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 & v . 3 = 1 holds
( ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0 & v . 1 = (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) & v . 2 = (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) )
let 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 & v . 3 = 1 holds
( ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0 & v . 1 = (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) & v . 2 = (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((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 & v . 3 = 1 implies ( ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0 & v . 1 = (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) & v . 2 = (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) ) )
assume that
A1: N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> and
A2: P = Dir u and
A3: Q = Dir v and
A4: Q = (homography N) . P and
A5: u . 3 = 1 and
A6: v . 3 = 1 ; :: thesis: ( ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0 & v . 1 = (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) & v . 2 = (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) )
consider a being non zero Real such that
A7: v . 1 = a * (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) and
A8: v . 2 = a * (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) and
A9: v . 3 = a * (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) by A1, A2, A3, A4, A5, Th18;
thus ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0 by A6, A9; :: thesis: ( v . 1 = (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) & v . 2 = (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) )
reconsider nn = ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 as non zero Real by A6, A9;
a = 1 / nn by A6, A9, XCMPLX_1:73;
hence ( v . 1 = (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) & v . 2 = (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) ) by A7, A8; :: thesis: verum