let N be invertible Matrix of 3,F_Real; :: thesis: ( N = <*<*2,0,(- 1)*>,<*0,(sqrt 3),0*>,<*1,0,(- 2)*>*> implies (homography N) .: absolute = absolute )
assume A1: N = <*<*2,0,(- 1)*>,<*0,(sqrt 3),0*>,<*1,0,(- 2)*>*> ; :: thesis: (homography N) .: absolute = absolute
reconsider a = 2, b = 0 , c = - 1, d = 0 , e = sqrt 3, f = 0 , g = 1, h = 0 , i = - 2 as Element of F_Real by XREAL_0:def 1;
A2: (homography N) .: absolute c= absolute
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (homography N) .: absolute or x in absolute )
assume x in (homography N) .: absolute ; :: thesis: x in absolute
then consider y being object such that
A3: y in dom (homography N) and
A4: y in absolute and
A5: x = (homography N) . y by FUNCT_1:def 6;
reconsider y = y as Point of (ProjectiveSpace (TOP-REAL 3)) by A3;
consider yu being non zero Element of (TOP-REAL 3) such that
A6: ((yu . 1) ^2) + ((yu . 2) ^2) = 1 and
A7: yu . 3 = 1 and
A8: y = Dir yu by A4, BKMODEL1:89;
A9: ((yu `1) * (yu `1)) + ((yu `2) * (yu `2)) = ((yu . 1) * (yu `1)) + ((yu `2) * (yu `2)) by EUCLID_5:def 1
.= ((yu . 1) * (yu . 1)) + ((yu `2) * (yu `2)) by EUCLID_5:def 1
.= ((yu . 1) * (yu . 1)) + ((yu . 2) * (yu `2)) by EUCLID_5:def 2
.= ((yu . 1) * (yu . 1)) + ((yu . 2) * (yu . 2)) by EUCLID_5:def 2
.= ((yu . 1) ^2) + ((yu . 2) * (yu . 2)) by SQUARE_1:def 1
.= 1 by A6, SQUARE_1:def 1 ;
A10: (yu `3) * (yu `3) = (yu . 3) * (yu `3) by EUCLID_5:def 3
.= 1 by A7, EUCLID_5:def 3 ;
consider u, v being Element of (TOP-REAL 3), uf being FinSequence of F_Real, p being FinSequence of 1 -tuples_on REAL such that
A11: ( y = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & (homography N) . y = Dir v ) by ANPROJ_8:def 4;
are_Prop u,yu by A8, A11, ANPROJ_1:22;
then consider l being Real such that
l <> 0 and
A12: u = l * yu by ANPROJ_1:1;
reconsider u1 = l * (yu `1), u2 = l * (yu `2), u3 = l * (yu `3) as Element of F_Real by XREAL_0:def 1;
uf = <*u1,u2,u3*> by A12, EUCLID_5:7, A11;
then v = <*(((a * u1) + (b * u2)) + (c * u3)),(((d * u1) + (e * u2)) + (f * u3)),(((g * u1) + (h * u2)) + (i * u3))*> by A1, A11, PASCAL:8
.= <*((2 * u1) - u3),((sqrt 3) * u2),(u1 - (2 * u3))*> ;
then ( v `1 = (2 * u1) - u3 & v `2 = (sqrt 3) * u2 & v `3 = u1 - (2 * u3) ) by EUCLID_5:2;
then A13: ( v . 1 = (2 * u1) - u3 & v . 2 = (sqrt 3) * u2 & v . 3 = u1 - (2 * u3) ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
A14: (v . 1) * (v . 1) = ((2 * u1) - u3) ^2 by A13, SQUARE_1:def 1
.= (((2 * u1) ^2) - ((2 * (2 * u1)) * u3)) + (u3 ^2) by SQUARE_1:5
.= (((2 * u1) * (2 * u1)) - ((2 * (2 * u1)) * u3)) + (u3 ^2) by SQUARE_1:def 1
.= (((4 * u1) * u1) - ((4 * u1) * u3)) + (u3 * u3) by SQUARE_1:def 1 ;
A15: (v . 2) * (v . 2) = (((sqrt 3) * (sqrt 3)) * u2) * u2 by A13
.= ((sqrt (3 * 3)) * u2) * u2 by SQUARE_1:29
.= ((sqrt (3 ^2)) * u2) * u2 by SQUARE_1:def 1
.= (3 * u2) * u2 by SQUARE_1:def 2 ;
A16: (v . 3) * (v . 3) = (u1 - (2 * u3)) ^2 by A13, SQUARE_1:def 1
.= ((u1 ^2) - ((2 * u1) * (2 * u3))) + ((2 * u3) ^2) by SQUARE_1:5
.= ((u1 * u1) - (((2 * 2) * u1) * u3)) + ((2 * u3) ^2) by SQUARE_1:def 1
.= ((u1 * u1) - (((2 * 2) * u1) * u3)) + ((2 * u3) * (2 * u3)) by SQUARE_1:def 1
.= ((u1 * u1) - ((4 * u1) * u3)) + ((4 * u3) * u3) ;
reconsider P = (homography N) . y as Point of (ProjectiveSpace (TOP-REAL 3)) ;
qfconic (1,1,(- 1),0,0,0,v) = 0
proof
qfconic (1,1,(- 1),0,0,0,v) = ((((((1 * (v . 1)) * (v . 1)) + ((1 * (v . 2)) * (v . 2))) + (((- 1) * (v . 3)) * (v . 3))) + ((0 * (v . 1)) * (v . 2))) + ((0 * (v . 1)) * (v . 3))) + ((0 * (v . 2)) * (v . 3)) by PASCAL:def 1
.= (((((4 * u1) * u1) - ((4 * u1) * u3)) + (u3 * u3)) + ((3 * u2) * u2)) - (((u1 * u1) - ((4 * u1) * u3)) + ((4 * u3) * u3)) by A14, A15, A16
.= (3 * (l * l)) * ((((yu `1) * (yu `1)) + ((yu `2) * (yu `2))) - ((yu `3) * (yu `3)))
.= 0 by A9, A10 ;
hence qfconic (1,1,(- 1),0,0,0,v) = 0 ; :: thesis: verum
end;
hence x in absolute by A5, A11, PASCAL:11; :: thesis: verum
end;
absolute c= (homography N) .: absolute
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in absolute or x in (homography N) .: absolute )
assume A17: x in absolute ; :: thesis: x in (homography N) .: absolute
reconsider N1 = <*<*(2 / 3),0,(- (1 / 3))*>,<*0,(1 / (sqrt 3)),0*>,<*(1 / 3),0,(- (2 / 3))*>*> as Matrix of 3,F_Real by ANPROJ_8:19;
N1 is_reverse_of N by A1, Th13;
then reconsider N1 = N1 as invertible Matrix of 3,F_Real by MATRIX_6:def 3;
A18: (homography N1) .: absolute c= absolute by Th14;
dom (homography N1) = the carrier of (ProjectiveSpace (TOP-REAL 3)) by FUNCT_2:def 1;
then (homography N1) . x in (homography N1) .: absolute by A17, FUNCT_1:108;
then reconsider y = (homography N1) . x as Element of absolute by A18;
A19: N * N1 = 1. (F_Real,3) by A1, Th11, ANPROJ_9:1;
now :: thesis: ( y in dom (homography N) & y in absolute & (homography N) . y = x )
dom (homography N) = the carrier of (ProjectiveSpace (TOP-REAL 3)) by FUNCT_2:def 1;
hence y in dom (homography N) ; :: thesis: ( y in absolute & (homography N) . y = x )
thus y in absolute ; :: thesis: (homography N) . y = x
reconsider P = x as Point of (ProjectiveSpace (TOP-REAL 3)) by A17;
thus (homography N) . y = (homography (1. (F_Real,3))) . P by A19, ANPROJ_9:13
.= x by ANPROJ_9:14 ; :: thesis: verum
end;
hence x in (homography N) .: absolute by FUNCT_1:108; :: thesis: verum
end;
hence (homography N) .: absolute = absolute by A2; :: thesis: verum