let N be invertible Matrix of 3,F_Real; :: thesis: for h being Element of SubGroupK-isometry
for n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real
for P being Element of BK_model st h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> holds
(homography N) . P = Dir |[((((n11 * ((BK_to_REAL2 P) `1)) + (n12 * ((BK_to_REAL2 P) `2))) + n13) / (((n31 * ((BK_to_REAL2 P) `1)) + (n32 * ((BK_to_REAL2 P) `2))) + n33)),((((n21 * ((BK_to_REAL2 P) `1)) + (n22 * ((BK_to_REAL2 P) `2))) + n23) / (((n31 * ((BK_to_REAL2 P) `1)) + (n32 * ((BK_to_REAL2 P) `2))) + n33)),1]|
let h be Element of SubGroupK-isometry; :: thesis: for n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real
for P being Element of BK_model st h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> holds
(homography N) . P = Dir |[((((n11 * ((BK_to_REAL2 P) `1)) + (n12 * ((BK_to_REAL2 P) `2))) + n13) / (((n31 * ((BK_to_REAL2 P) `1)) + (n32 * ((BK_to_REAL2 P) `2))) + n33)),((((n21 * ((BK_to_REAL2 P) `1)) + (n22 * ((BK_to_REAL2 P) `2))) + n23) / (((n31 * ((BK_to_REAL2 P) `1)) + (n32 * ((BK_to_REAL2 P) `2))) + n33)),1]|
let n11, n12, n13, n21, n22, n23, n31, n32, n33 be Element of F_Real; :: thesis: for P being Element of BK_model st h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> holds
(homography N) . P = Dir |[((((n11 * ((BK_to_REAL2 P) `1)) + (n12 * ((BK_to_REAL2 P) `2))) + n13) / (((n31 * ((BK_to_REAL2 P) `1)) + (n32 * ((BK_to_REAL2 P) `2))) + n33)),((((n21 * ((BK_to_REAL2 P) `1)) + (n22 * ((BK_to_REAL2 P) `2))) + n23) / (((n31 * ((BK_to_REAL2 P) `1)) + (n32 * ((BK_to_REAL2 P) `2))) + n33)),1]|
let P be Element of BK_model ; :: thesis: ( h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> implies (homography N) . P = Dir |[((((n11 * ((BK_to_REAL2 P) `1)) + (n12 * ((BK_to_REAL2 P) `2))) + n13) / (((n31 * ((BK_to_REAL2 P) `1)) + (n32 * ((BK_to_REAL2 P) `2))) + n33)),((((n21 * ((BK_to_REAL2 P) `1)) + (n22 * ((BK_to_REAL2 P) `2))) + n23) / (((n31 * ((BK_to_REAL2 P) `1)) + (n32 * ((BK_to_REAL2 P) `2))) + n33)),1]| )
assume A1: ( h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> ) ; :: thesis: (homography N) . P = Dir |[((((n11 * ((BK_to_REAL2 P) `1)) + (n12 * ((BK_to_REAL2 P) `2))) + n13) / (((n31 * ((BK_to_REAL2 P) `1)) + (n32 * ((BK_to_REAL2 P) `2))) + n33)),((((n21 * ((BK_to_REAL2 P) `1)) + (n22 * ((BK_to_REAL2 P) `2))) + n23) / (((n31 * ((BK_to_REAL2 P) `1)) + (n32 * ((BK_to_REAL2 P) `2))) + n33)),1]|
consider u being non zero Element of (TOP-REAL 3) such that
A2: ( P = Dir u & u . 3 = 1 & BK_to_REAL2 P = |[(u . 1),(u . 2)]| ) by BKMODEL2:def 2;
( (BK_to_REAL2 P) `1 = u . 1 & (BK_to_REAL2 P) `2 = u . 2 & (homography N) . P = Dir |[((((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),((((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),1]| ) by A1, A2, Th23, EUCLID:52;
hence (homography N) . P = Dir |[((((n11 * ((BK_to_REAL2 P) `1)) + (n12 * ((BK_to_REAL2 P) `2))) + n13) / (((n31 * ((BK_to_REAL2 P) `1)) + (n32 * ((BK_to_REAL2 P) `2))) + n33)),((((n21 * ((BK_to_REAL2 P) `1)) + (n22 * ((BK_to_REAL2 P) `2))) + n23) / (((n31 * ((BK_to_REAL2 P) `1)) + (n32 * ((BK_to_REAL2 P) `2))) + n33)),1]| ; :: thesis: verum