let h be Element of SubGroupK-isometry; :: thesis: for N being invertible Matrix of 3,F_Real
for n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real
for u2 being Element of (TOP-REAL 2) st h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & u2 in closed_inside_of_circle (0,0,1) holds
((n31 * (u2 . 1)) + (n32 * (u2 . 2))) + n33 <> 0
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 u2 being Element of (TOP-REAL 2) st h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & u2 in closed_inside_of_circle (0,0,1) holds
((n31 * (u2 . 1)) + (n32 * (u2 . 2))) + n33 <> 0
let n11, n12, n13, n21, n22, n23, n31, n32, n33 be Element of F_Real; :: thesis: for u2 being Element of (TOP-REAL 2) st h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & u2 in closed_inside_of_circle (0,0,1) holds
((n31 * (u2 . 1)) + (n32 * (u2 . 2))) + n33 <> 0
let u2 be Element of (TOP-REAL 2); :: thesis: ( h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & u2 in closed_inside_of_circle (0,0,1) implies ((n31 * (u2 . 1)) + (n32 * (u2 . 2))) + n33 <> 0 )
assume that
A1: h = homography N and
A2: N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> and
A3: u2 in closed_inside_of_circle (0,0,1) ; :: thesis: ((n31 * (u2 . 1)) + (n32 * (u2 . 2))) + n33 <> 0
u2 in (inside_of_circle (0,0,1)) \/ (circle (0,0,1)) by A3, TOPREAL9:55;
per cases then ( u2 in inside_of_circle (0,0,1) or u2 in circle (0,0,1) ) by XBOOLE_0:def 3;
suppose u2 in inside_of_circle (0,0,1) ; :: thesis: ((n31 * (u2 . 1)) + (n32 * (u2 . 2))) + n33 <> 0
then reconsider uic = u2 as Element of inside_of_circle (0,0,1) ;
consider Q being Element of (TOP-REAL 2) such that
A4: ( Q = uic & REAL2_to_BK uic = Dir |[(Q `1),(Q `2),1]| ) by BKMODEL2:def 3;
reconsider P = REAL2_to_BK uic as Element of BK_model ;
reconsider v = |[(Q `1),(Q `2),1]| as non zero Element of (TOP-REAL 3) ;
A5: v . 1 = v `1 by EUCLID_5:def 1
.= u2 . 1 by A4, EUCLID_5:2 ;
A6: v . 2 = v `2 by EUCLID_5:def 2
.= u2 . 2 by A4, EUCLID_5:2 ;
now :: thesis: ( P = Dir v & v . 3 = 1 )
thus P = Dir v by A4; :: thesis: v . 3 = 1
thus v . 3 = v `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ; :: thesis: verum
end;
hence ((n31 * (u2 . 1)) + (n32 * (u2 . 2))) + n33 <> 0 by A5, A6, A1, A2, Th20; :: thesis: verum
end;
suppose A7: u2 in circle (0,0,1) ; :: thesis: ((n31 * (u2 . 1)) + (n32 * (u2 . 2))) + n33 <> 0
then reconsider u2 = u2 as non zero Element of (TOP-REAL 2) by Th37;
reconsider P = REAL2_to_absolute u2 as Element of absolute ;
reconsider v = |[(u2 . 1),(u2 . 2),1]| as non zero Element of (TOP-REAL 3) ;
A8: v . 1 = v `1 by EUCLID_5:def 1
.= u2 . 1 by EUCLID_5:2 ;
A9: v . 2 = v `2 by EUCLID_5:def 2
.= u2 . 2 by EUCLID_5:2 ;
now :: thesis: ( P is Element of absolute & P = Dir v & v . 3 = 1 )
thus P is Element of absolute ; :: thesis: ( P = Dir v & v . 3 = 1 )
thus P = Dir v by A7, BKMODEL1:def 9; :: thesis: v . 3 = 1
thus v . 3 = v `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ; :: thesis: verum
end;
hence ((n31 * (u2 . 1)) + (n32 * (u2 . 2))) + n33 <> 0 by A8, A9, A1, A2, Th22; :: thesis: verum
end;
end;