let P be Element of absolute ; :: thesis: (tangent P) /\ absolute = {P}
A1: {P} c= (tangent P) /\ absolute
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {P} or x in (tangent P) /\ absolute )
assume x in {P} ; :: thesis: x in (tangent P) /\ absolute
then x = P by TARSKI:def 1;
then ( x in tangent P & x in absolute ) by Th21;
hence x in (tangent P) /\ absolute by XBOOLE_0:def 4; :: thesis: verum
end;
(tangent P) /\ absolute c= {P}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (tangent P) /\ absolute or x in {P} )
assume A2: x in (tangent P) /\ absolute ; :: thesis: x in {P}
then reconsider y = x as Element of real_projective_plane ;
consider p being Element of real_projective_plane such that
A3: p = P and
A4: tangent P = Line (p,(pole_infty P)) by Def04;
y in Line (p,(pole_infty P)) by A2, A4, XBOOLE_0:def 4;
then A5: p, pole_infty P,y are_collinear by COLLSP:11;
consider u being Element of (TOP-REAL 3) such that
A6: not u is zero and
A7: p = Dir u by ANPROJ_1:26;
consider v being non zero Element of (TOP-REAL 3) such that
A8: ( P = Dir v & v . 3 = 1 & ((v . 1) ^2) + ((v . 2) ^2) = 1 & pole_infty P = Dir |[(- (v . 2)),(v . 1),0]| ) by Def03;
are_Prop u,v by A6, A7, A8, A3, ANPROJ_1:22;
then consider a being Real such that
A9: a <> 0 and
A10: u = a * v by ANPROJ_1:1;
A11: u `1 = u . 1 by EUCLID_5:def 1
.= a * (v . 1) by A10, RVSUM_1:44 ;
A12: u `2 = u . 2 by EUCLID_5:def 2
.= a * (v . 2) by A10, RVSUM_1:44 ;
A13: u `3 = u . 3 by EUCLID_5:def 3
.= a * 1 by A8, A10, RVSUM_1:44
.= a ;
y is Element of absolute by A2, XBOOLE_0:def 4;
then consider w being non zero Element of (TOP-REAL 3) such that
A14: ((w . 1) ^2) + ((w . 2) ^2) = 1 and
A15: w . 3 = 1 and
A16: y = Dir w by BKMODEL1:89;
A17: ( |[(- (v . 2)),(v . 1),0]| `1 = - (v . 2) & |[(- (v . 2)),(v . 1),0]| `2 = v . 1 & |[(- (v . 2)),(v . 1),0]| `3 = 0 ) by EUCLID_5:2;
not |[(- (v . 2)),(v . 1),0]| is zero by A8, BKMODEL1:91;
then 0 = |{u,|[(- (v . 2)),(v . 1),0]|,w}| by A5, A6, A7, A8, A16, BKMODEL1:1
.= (((((((u `1) * (v . 1)) * (w `3)) - (((u `3) * (v . 1)) * (w `1))) - (((u `1) * 0) * (w `2))) + (((u `2) * 0) * (w `1))) - (((u `2) * (- (v . 2))) * (w `3))) + (((u `3) * (- (v . 2))) * (w `2)) by A17, ANPROJ_8:27
.= (((((u `1) * (v . 1)) * (w . 3)) - (((u `3) * (v . 1)) * (w `1))) - (((u `2) * (- (v . 2))) * (w `3))) + (((u `3) * (- (v . 2))) * (w `2)) by EUCLID_5:def 3
.= (((((u `1) * (v . 1)) * 1) - (((u `3) * (v . 1)) * (w `1))) - (((u `2) * (- (v . 2))) * 1)) + (((u `3) * (- (v . 2))) * (w `2)) by A15, EUCLID_5:def 3
.= a * (((((v . 1) * (v . 1)) + ((v . 2) * (v . 2))) - ((v . 1) * (w `1))) - ((v . 2) * (w `2))) by A11, A12, A13
.= a * ((1 - ((v . 1) * (w `1))) - ((v . 2) * (w `2))) by A8 ;
then (1 - ((v . 1) * (w `1))) - ((v . 2) * (w `2)) = 0 by A9;
then A18: 1 = ((v . 1) * (w `1)) + ((v . 2) * (w `2))
.= ((v . 1) * (w . 1)) + ((v . 2) * (w `2)) by EUCLID_5:def 1
.= ((v . 1) * (w . 1)) + ((v . 2) * (w . 2)) by EUCLID_5:def 2 ;
then A19: (v . 1) * (w . 2) = (v . 2) * (w . 1) by BKMODEL1:7, A14, A8;
x = P
proof
per cases ( v . 2 = 0 or v . 2 <> 0 ) ;
suppose A20: v . 2 = 0 ; :: thesis: x = P
then v . 1 <> 0 by A8;
then A21: w . 2 = 0 by A19, A20;
per cases ( v . 1 = 1 or v . 1 = - 1 ) by A20, A8, BKMODEL1:8;
suppose A22: v . 1 = 1 ; :: thesis: x = P
per cases ( w . 1 = 1 or w . 1 = - 1 ) by A21, A14, BKMODEL1:8;
suppose w . 1 = 1 ; :: thesis: x = P
then ( w `1 = 1 & w `2 = 0 & w `3 = 1 & v `1 = 1 & v `2 = 0 & v `3 = 1 ) by A8, A20, A22, A19, A15, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then v = |[(w `1),(w `2),(w `3)]| by EUCLID_5:3
.= w by EUCLID_5:3 ;
hence x = P by A8, A16; :: thesis: verum
end;
suppose w . 1 = - 1 ; :: thesis: x = P
hence x = P by A18, A20, A22; :: thesis: verum
end;
end;
end;
suppose A23: v . 1 = - 1 ; :: thesis: x = P
per cases ( w . 1 = 1 or w . 1 = - 1 ) by A21, A14, BKMODEL1:8;
suppose w . 1 = 1 ; :: thesis: x = P
hence x = P by A18, A20, A23; :: thesis: verum
end;
suppose w . 1 = - 1 ; :: thesis: x = P
then ( w `1 = - 1 & w `2 = 0 & w `3 = 1 & v `1 = - 1 & v `2 = 0 & v `3 = 1 ) by A23, A8, A20, A19, A15, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then v = |[(w `1),(w `2),(w `3)]| by EUCLID_5:3
.= w by EUCLID_5:3 ;
hence x = P by A8, A16; :: thesis: verum
end;
end;
end;
end;
end;
suppose A24: v . 2 <> 0 ; :: thesis: x = P
per cases ( v . 1 = 0 or v . 1 <> 0 ) ;
suppose A25: v . 1 = 0 ; :: thesis: x = P
per cases then ( v . 2 = 1 or v . 2 = - 1 ) by A8, BKMODEL1:8;
suppose A26: v . 2 = 1 ; :: thesis: x = P
A27: (v . 2) * (w . 1) = 0 * (w . 2) by A25, A18, BKMODEL1:7, A14, A8
.= 0 ;
then w . 1 = 0 by A24;
per cases then ( w . 2 = 1 or w . 2 = - 1 ) by A14, BKMODEL1:8;
suppose w . 2 = 1 ; :: thesis: x = P
then A28: ( w `1 = 0 & w `2 = 1 & w `3 = 1 & v `1 = 0 & v `2 = 1 & v `3 = 1 ) by A25, A26, A27, A8, A15, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
v = |[(w `1),(w `2),(w `3)]| by A28, EUCLID_5:3
.= w by EUCLID_5:3 ;
hence x = P by A8, A16; :: thesis: verum
end;
suppose w . 2 = - 1 ; :: thesis: x = P
hence x = P by A18, A25, A26; :: thesis: verum
end;
end;
end;
suppose A29: v . 2 = - 1 ; :: thesis: x = P
A30: (v . 2) * (w . 1) = 0 * (w . 2) by A25, A18, BKMODEL1:7, A14, A8
.= 0 ;
then w . 1 = 0 by A24;
per cases then ( w . 2 = 1 or w . 2 = - 1 ) by A14, BKMODEL1:8;
suppose w . 2 = 1 ; :: thesis: x = P
hence x = P by A18, A25, A29; :: thesis: verum
end;
suppose w . 2 = - 1 ; :: thesis: x = P
then A31: ( w `1 = 0 & w `2 = - 1 & w `3 = 1 & v `1 = 0 & v `2 = - 1 & v `3 = 1 ) by A29, A25, A30, A8, A15, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
v = |[(w `1),(w `2),(w `3)]| by A31, EUCLID_5:3
.= w by EUCLID_5:3 ;
hence x = P by A8, A16; :: thesis: verum
end;
end;
end;
end;
end;
suppose v . 1 <> 0 ; :: thesis: x = P
then reconsider l = (v . 1) / (v . 2) as non zero Real by A24;
A32: l * (v . 2) = v . 1 by XCMPLX_1:87, A24;
A33: l * (w . 2) = ((v . 1) * (w . 2)) / (v . 2) by XCMPLX_1:74
.= ((v . 2) * (w . 1)) / (v . 2) by A18, BKMODEL1:7, A14, A8
.= w . 1 by XCMPLX_1:89, A24 ;
per cases ( v . 2 = 1 / (sqrt (1 + (l ^2))) or v . 2 = (- 1) / (sqrt (1 + (l ^2))) ) by A32, A8, BKMODEL1:10;
suppose A34: v . 2 = 1 / (sqrt (1 + (l ^2))) ; :: thesis: x = P
per cases ( w . 2 = 1 / (sqrt (1 + (l ^2))) or w . 2 = (- 1) / (sqrt (1 + (l ^2))) ) by A33, A14, BKMODEL1:10;
suppose w . 2 = 1 / (sqrt (1 + (l ^2))) ; :: thesis: x = P
then ( w `1 = v . 1 & w `2 = v . 2 & w `3 = v . 3 ) by A8, A15, A34, A32, A33, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then ( w `1 = v `1 & w `2 = v `2 & w `3 = v `3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then v = |[(w `1),(w `2),(w `3)]| by EUCLID_5:3
.= w by EUCLID_5:3 ;
hence x = P by A8, A16; :: thesis: verum
end;
suppose A35: w . 2 = (- 1) / (sqrt (1 + (l ^2))) ; :: thesis: x = P
0 <= l ^2 by SQUARE_1:12;
then A36: (sqrt (1 + (l ^2))) ^2 = 1 + (l * l) by SQUARE_1:def 2;
((v . 1) * (w . 1)) + ((v . 2) * (w . 2)) = (((l * (1 / (sqrt (1 + (l ^2))))) * l) * ((- 1) / (sqrt (1 + (l ^2))))) + ((v . 2) * (w . 2)) by A34, A35, A32, A33
.= - 1 by A34, A35, A36, BKMODEL1:11 ;
hence x = P by A18; :: thesis: verum
end;
end;
end;
suppose A37: v . 2 = (- 1) / (sqrt (1 + (l ^2))) ; :: thesis: x = P
per cases ( w . 2 = 1 / (sqrt (1 + (l ^2))) or w . 2 = (- 1) / (sqrt (1 + (l ^2))) ) by A33, A14, BKMODEL1:10;
suppose A38: w . 2 = 1 / (sqrt (1 + (l ^2))) ; :: thesis: x = P
0 <= l ^2 by SQUARE_1:12;
then A39: (sqrt (1 + (l ^2))) ^2 = 1 + (l * l) by SQUARE_1:def 2;
((v . 1) * (w . 1)) + ((v . 2) * (w . 2)) = (((l * (1 / (sqrt (1 + (l ^2))))) * l) * ((- 1) / (sqrt (1 + (l ^2))))) + ((1 / (sqrt (1 + (l ^2)))) * ((- 1) / (sqrt (1 + (l ^2))))) by A37, A38, A32, A33
.= - 1 by A39, BKMODEL1:11 ;
hence x = P by A18; :: thesis: verum
end;
suppose w . 2 = (- 1) / (sqrt (1 + (l ^2))) ; :: thesis: x = P
then ( w `1 = v . 1 & w `2 = v . 2 & w `3 = v . 3 ) by A8, A15, A37, A32, A33, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then ( w `1 = v `1 & w `2 = v `2 & w `3 = v `3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then v = |[(w `1),(w `2),(w `3)]| by EUCLID_5:3
.= w by EUCLID_5:3 ;
hence x = P by A8, A16; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
hence x in {P} by TARSKI:def 1; :: thesis: verum
end;
hence (tangent P) /\ absolute = {P} by A1; :: thesis: verum