let P1, P2 be Element of absolute ; ( not pole_infty P1 = pole_infty P2 or P1 = P2 or ex u being non zero Element of (TOP-REAL 3) st
( P1 = Dir u & P2 = Dir |[(- (u `1)),(- (u `2)),1]| & u `3 = 1 ) )
assume A1:
pole_infty P1 = pole_infty P2
; ( P1 = P2 or ex u being non zero Element of (TOP-REAL 3) st
( P1 = Dir u & P2 = Dir |[(- (u `1)),(- (u `2)),1]| & u `3 = 1 ) )
consider u1 being non zero Element of (TOP-REAL 3) such that
A2:
( P1 = Dir u1 & u1 . 3 = 1 & ((u1 . 1) ^2) + ((u1 . 2) ^2) = 1 & pole_infty P1 = Dir |[(- (u1 . 2)),(u1 . 1),0]| )
by Def03;
consider u2 being non zero Element of (TOP-REAL 3) such that
A3:
( P2 = Dir u2 & u2 . 3 = 1 & ((u2 . 1) ^2) + ((u2 . 2) ^2) = 1 & pole_infty P2 = Dir |[(- (u2 . 2)),(u2 . 1),0]| )
by Def03;
reconsider w1 = |[(- (u1 . 2)),(u1 . 1),0]| as non zero Element of (TOP-REAL 3) by A2, BKMODEL1:91;
reconsider w2 = |[(- (u2 . 2)),(u2 . 1),0]| as non zero Element of (TOP-REAL 3) by A3, BKMODEL1:91;
are_Prop w1,w2
by A1, A2, A3, ANPROJ_1:22;
then consider a being Real such that
a <> 0
and
A5:
w1 = a * w2
by ANPROJ_1:1;
a * w2 = |[(a * (- (u2 . 2))),(a * (u2 . 1)),(a * 0)]|
by EUCLID_5:8;
then A6:
( - (u1 . 2) = a * (- (u2 . 2)) & u1 . 1 = a * (u2 . 1) )
by A5, FINSEQ_1:78;
then A7: 1 =
((a * (u2 . 1)) * (a * (u2 . 1))) + ((a * (u2 . 2)) ^2)
by A2
.=
(a * a) * (((u2 . 1) * (u2 . 1)) + ((u2 . 2) * (u2 . 2)))
.=
a ^2
by A3
;
A8:
( a = 1 implies P1 = P2 )
proof
assume
a = 1
;
P1 = P2
then
(
u1 `1 = u2 . 1 &
u1 `2 = u2 . 2 &
u1 `3 = u2 . 3 )
by A2, A3, A6, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A9:
(
u1 `1 = u2 `1 &
u1 `2 = u2 `2 &
u1 `3 = u2 `3 )
by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
u1 =
|[(u1 `1),(u1 `2),(u1 `3)]|
by EUCLID_5:3
.=
u2
by A9, EUCLID_5:3
;
hence
P1 = P2
by A2, A3;
verum
end;
( a = - 1 implies ex u being non zero Element of (TOP-REAL 3) st
( P1 = Dir u & P2 = Dir |[(- (u `1)),(- (u `2)),1]| & u `3 = 1 ) )
proof
assume
a = - 1
;
ex u being non zero Element of (TOP-REAL 3) st
( P1 = Dir u & P2 = Dir |[(- (u `1)),(- (u `2)),1]| & u `3 = 1 )
then
(
u1 `1 = - (u2 . 1) &
u1 `2 = - (u2 . 2) &
u2 `3 = 1 )
by A3, A6, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A10:
(
u1 `1 = - (u2 `1) &
u1 `2 = - (u2 `2) &
u2 `3 = 1 )
by EUCLID_5:def 1, EUCLID_5:def 2;
take
u1
;
( P1 = Dir u1 & P2 = Dir |[(- (u1 `1)),(- (u1 `2)),1]| & u1 `3 = 1 )
thus
(
P1 = Dir u1 &
P2 = Dir |[(- (u1 `1)),(- (u1 `2)),1]| &
u1 `3 = 1 )
by A10, EUCLID_5:3, A3, A2, EUCLID_5:def 3;
verum
end;
hence
( P1 = P2 or ex u being non zero Element of (TOP-REAL 3) st
( P1 = Dir u & P2 = Dir |[(- (u `1)),(- (u `2)),1]| & u `3 = 1 ) )
by A7, A8, SQUARE_1:41; verum