let a be non zero Real; :: thesis: for N being invertible Matrix of 3,F_Real st N = symmetric_3 (a,a,(- a),0,0,0) holds
(homography N) .: absolute = absolute
let N be invertible Matrix of 3,F_Real; :: thesis: ( N = symmetric_3 (a,a,(- a),0,0,0) implies (homography N) .: absolute = absolute )
assume A1: N = symmetric_3 (a,a,(- a),0,0,0) ; :: thesis: (homography N) .: absolute = absolute
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: (homography N) . y = x by FUNCT_1:def 6;
A6: rng (homography N) c= the carrier of (ProjectiveSpace (TOP-REAL 3)) by RELAT_1:def 19;
reconsider y9 = y as Element of (ProjectiveSpace (TOP-REAL 3)) by A3;
consider u9 being non zero Element of (TOP-REAL 3) such that
A7: ( ((u9 . 1) ^2) + ((u9 . 2) ^2) = 1 & u9 . 3 = 1 & y = Dir u9 ) by A4, BKMODEL1:89;
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
A8: ( y9 = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & (homography N) . y9 = Dir v ) by ANPROJ_8:def 4;
reconsider x9 = x as Element of (ProjectiveSpace (TOP-REAL 3)) by A5, A3, A6, FUNCT_1:3;
reconsider z1 = 0 , z2 = a, z3 = - a as Element of F_Real by XREAL_0:def 1;
A9: N = <*<*z2,z1,z1*>,<*z1,z2,z1*>,<*z1,z1,z3*>*> by A1, PASCAL:def 3;
reconsider ux = u `1 , uy = u `2 , uz = u `3 as Element of F_Real by XREAL_0:def 1;
<*ux,uy,uz*> = uf by A8, EUCLID_5:3;
then A10: ( p = <*<*(((z2 * ux) + (z1 * uy)) + (z1 * uz))*>,<*(((z1 * ux) + (z2 * uy)) + (z1 * uz))*>,<*(((z1 * ux) + (z1 * uy)) + (z3 * uz))*>*> & v = <*(((z2 * ux) + (z1 * uy)) + (z1 * uz)),(((z1 * ux) + (z2 * uy)) + (z1 * uz)),(((z1 * ux) + (z1 * uy)) + (z3 * uz))*> ) by A8, A9, PASCAL:8;
are_Prop u9,u by A7, A8, ANPROJ_1:22;
then consider l being Real such that
A11: l <> 0 and
A12: u9 = l * u by ANPROJ_1:1;
A13: ( u9 . 1 = l * (u . 1) & u9 . 2 = l * (u . 2) & u9 . 3 = l * (u . 3) ) by A12, RVSUM_1:44;
reconsider w = |[(- ((u . 1) * l)),(- ((u . 2) * l)),((u . 3) * l)]| as Element of (TOP-REAL 3) ;
A15: not w is zero
proof
assume w is zero ; :: thesis: contradiction
then ( u . 1 = 0 & u . 2 = 0 & u . 3 = 0 ) by A11, FINSEQ_1:78, EUCLID_5:4;
then ( u `1 = 0 & u `2 = 0 & u `3 = 0 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
hence contradiction by A8, EUCLID_5:3, EUCLID_5:4; :: thesis: verum
end;
A16: ( (- 1) * (w `1) = (- 1) * (- ((u . 1) * l)) & (- 1) * (w `2) = (- 1) * (- ((u . 2) * l)) & (- 1) * (w `3) = (- 1) * ((u . 3) * l) ) by EUCLID_5:2;
then ( (- 1) * (w `1) = (1 * (u . 1)) * l & (- 1) * (w `2) = (1 * (u . 2)) * l & (- 1) * (w `3) = - ((1 * (u . 3)) * l) ) ;
then A17: ( (- 1) * (w `1) = (u `1) * l & (- 1) * (w `2) = (u `2) * l & (- 1) * (w `3) = - ((1 * (u `3)) * l) ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
now :: thesis: ( - (a / l) <> 0 & v = (- (a / l)) * w )
thus - (a / l) <> 0 by A11; :: thesis: v = (- (a / l)) * w
( (- (a / l)) * (w `1) = v `1 & (- (a / l)) * (w `2) = v `2 & (- (a / l)) * (w `3) = v `3 )
proof
thus (- (a / l)) * (w `1) = (a / l) * ((- 1) * (w `1))
.= (a / l) * ((u `1) * l) by A16, EUCLID_5:def 1
.= a * (u `1) by A11, XCMPLX_1:90
.= v `1 by A10, EUCLID_5:2 ; :: thesis: ( (- (a / l)) * (w `2) = v `2 & (- (a / l)) * (w `3) = v `3 )
thus (- (a / l)) * (w `2) = (a / l) * ((- 1) * (w `2))
.= (a / l) * ((u `2) * l) by A16, EUCLID_5:def 2
.= a * (u `2) by A11, XCMPLX_1:90
.= v `2 by A10, EUCLID_5:2 ; :: thesis: (- (a / l)) * (w `3) = v `3
thus (- (a / l)) * (w `3) = - ((a / l) * ((u `3) * l)) by A17
.= - (a * (u `3)) by A11, XCMPLX_1:90
.= v `3 by A10, EUCLID_5:2 ; :: thesis: verum
end;
then |[(v `1),(v `2),(v `3)]| = (- (a / l)) * |[(w `1),(w `2),(w `3)]| by EUCLID_5:8
.= (- (a / l)) * w by EUCLID_5:3 ;
hence v = (- (a / l)) * w by EUCLID_5:3; :: thesis: verum
end;
then are_Prop w,v by ANPROJ_1:1;
then A18: Dir w = Dir v by ANPROJ_1:22, A15, A8;
A19: ( ((w . 1) ^2) + ((w . 2) ^2) = 1 ^2 & w . 3 = 1 )
proof
thus 1 ^2 = ((l * (u `1)) * (l * (u . 1))) + ((l * (u . 2)) * (l * (u . 2))) by EUCLID_5:def 1, A13, A7
.= ((l * (u `1)) * (l * (u `1))) + ((l * (u . 2)) * (l * (u . 2))) by EUCLID_5:def 1
.= ((l * (u `1)) * (l * (u `1))) + ((l * (u `2)) * (l * (u . 2))) by EUCLID_5:def 2
.= (((- 1) * (w `1)) * ((- 1) * (w `1))) + (((- 1) * (w `2)) * ((- 1) * (w `2))) by A17, EUCLID_5:def 2
.= ((w `1) * (w `1)) + ((w `2) * (w `2))
.= ((w . 1) * (w `1)) + ((w `2) * (w `2)) by EUCLID_5:def 1
.= ((w . 1) * (w . 1)) + ((w `2) * (w `2)) by EUCLID_5:def 1
.= ((w . 1) * (w . 1)) + ((w . 2) * (w `2)) by EUCLID_5:def 2
.= ((w . 1) ^2) + ((w . 2) ^2) by EUCLID_5:def 2 ; :: thesis: w . 3 = 1
w `3 = (u . 3) * l by EUCLID_5:2;
hence w . 3 = 1 by A13, A7, EUCLID_5:def 3; :: thesis: verum
end;
then |[(w . 1),(w . 2)]| in circle (0,0,1) by BKMODEL1:14;
then x9 is Element of absolute by A15, A18, A8, A5, A19, BKMODEL1:86;
hence x in absolute ; :: 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 x in absolute ; :: thesis: x in (homography N) .: absolute
then consider u being non zero Element of (TOP-REAL 3) such that
A20: ( ((u . 1) ^2) + ((u . 2) ^2) = 1 & u . 3 = 1 & x = Dir u ) by BKMODEL1:89;
reconsider w = |[((u . 1) / a),((u . 2) / a),(- ((u . 3) / a))]| as Element of (TOP-REAL 3) ;
A21: not w is zero
proof
assume w is zero ; :: thesis: contradiction
then ( u . 1 = 0 & u . 2 = 0 & u . 3 = 0 ) by FINSEQ_1:78, EUCLID_5:4;
then ( u `1 = 0 & u `2 = 0 & u `3 = 0 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
hence contradiction by EUCLID_5:3, EUCLID_5:4; :: thesis: verum
end;
then reconsider P = Dir w as Element of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
reconsider v = |[(- (u . 1)),(- (u . 2)),(u . 3)]| as Element of (TOP-REAL 3) ;
A22: (- a) * ((u . 1) / a) = - (a * ((u . 1) / a))
.= - (u . 1) by XCMPLX_1:87 ;
A23: (- a) * ((u . 2) / a) = - (a * ((u . 2) / a))
.= - (u . 2) by XCMPLX_1:87 ;
A24: (- a) * (- ((u . 3) / a)) = a * ((u . 3) / a)
.= u . 3 by XCMPLX_1:87 ;
A25: not v is zero by A20, FINSEQ_1:78, EUCLID_5:4;
v = (- a) * w by A22, A23, A24, EUCLID_5:8;
then are_Prop v,w by ANPROJ_1:1;
then A26: P = Dir v by A21, A25, ANPROJ_1:22;
v `3 = u . 3 by EUCLID_5:2;
then A27: v . 3 = 1 by A20, EUCLID_5:def 3;
|[(v . 1),(v . 2)]| in circle (0,0,1)
proof
A28: ( v `1 = - (u . 1) & v `2 = - (u . 2) ) by EUCLID_5:2;
A29: (v . 1) ^2 = (v `1) * (v . 1) by EUCLID_5:def 1
.= (- (u . 1)) * (- (u . 1)) by A28, EUCLID_5:def 1
.= (u . 1) ^2 ;
A30: (v . 2) ^2 = (v `2) * (v . 2) by EUCLID_5:def 2
.= (- (u . 2)) * (- (u . 2)) by A28, EUCLID_5:def 2
.= (u . 2) ^2 ;
((v . 1) ^2) + ((v . 2) ^2) = 1 ^2 by A20, A29, A30;
hence |[(v . 1),(v . 2)]| in circle (0,0,1) by BKMODEL1:14; :: thesis: verum
end;
then reconsider P = P as Element of absolute by A26, A27, A25, BKMODEL1:86;
now :: thesis: ( P in dom (homography N) & x = (homography N) . P )
dom (homography N) = the carrier of (ProjectiveSpace (TOP-REAL 3)) by FUNCT_2:def 1;
hence P in dom (homography N) ; :: thesis: x = (homography N) . P
consider u1, v1 being Element of (TOP-REAL 3), uf being FinSequence of F_Real, p being FinSequence of 1 -tuples_on REAL such that
A31: ( P = Dir u1 & not u1 is zero & u1 = uf & p = N * uf & v1 = M2F p & not v1 is zero & (homography N) . P = Dir v1 ) by ANPROJ_8:def 4;
are_Prop u1,w by A21, A31, ANPROJ_1:22;
then consider l being Real such that
A32: l <> 0 and
A33: u1 = l * w by ANPROJ_1:1;
u1 = |[(l * ((u . 1) / a)),(l * ((u . 2) / a)),(l * (- ((u . 3) / a)))]| by A33, EUCLID_5:8;
then A34: ( u1 `1 = l * ((u . 1) / a) & u1 `2 = l * ((u . 2) / a) & u1 `3 = l * (- ((u . 3) / a)) ) by EUCLID_5:2;
reconsider z1 = 0 , z2 = a, z3 = - a as Element of F_Real by XREAL_0:def 1;
A35: N = <*<*z2,z1,z1*>,<*z1,z2,z1*>,<*z1,z1,z3*>*> by A1, PASCAL:def 3;
reconsider ux = u1 `1 , uy = u1 `2 , uz = u1 `3 as Element of F_Real by XREAL_0:def 1;
A36: a * (l * ((u . 1) / a)) = l * (a * ((u . 1) / a))
.= l * (u . 1) by XCMPLX_1:87 ;
A37: a * (l * ((u . 2) / a)) = l * (a * ((u . 2) / a))
.= l * (u . 2) by XCMPLX_1:87 ;
A38: (- a) * (l * (- ((u . 3) / a))) = l * (a * ((u . 3) / a))
.= l * (u . 3) by XCMPLX_1:87 ;
<*ux,uy,uz*> = uf by A31, EUCLID_5:3;
then ( p = <*<*(((z2 * ux) + (z1 * uy)) + (z1 * uz))*>,<*(((z1 * ux) + (z2 * uy)) + (z1 * uz))*>,<*(((z1 * ux) + (z1 * uy)) + (z3 * uz))*>*> & v1 = <*(((z2 * ux) + (z1 * uy)) + (z1 * uz)),(((z1 * ux) + (z2 * uy)) + (z1 * uz)),(((z1 * ux) + (z1 * uy)) + (z3 * uz))*> ) by A31, A35, PASCAL:8;
then ( v1 `1 = a * (u1 `1) & v1 `2 = a * (u1 `2) & v1 `3 = (- a) * (u1 `3) ) by EUCLID_5:2;
then ( v1 `1 = l * (u `1) & v1 `2 = l * (u `2) & v1 `3 = l * (u `3) ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3, A34, A36, A37, A38;
then v1 = |[(l * (u `1)),(l * (u `2)),(l * (u `3))]| by EUCLID_5:3
.= l * |[(u `1),(u `2),(u `3)]| by EUCLID_5:8
.= l * u by EUCLID_5:3 ;
then are_Prop u,v1 by A32, ANPROJ_1:1;
hence x = (homography N) . P by A20, A31, ANPROJ_1:22; :: thesis: verum
end;
hence x in (homography N) .: absolute by FUNCT_1:def 6; :: thesis: verum
end;
hence (homography N) .: absolute = absolute by A2; :: thesis: verum