let P be Element of real_projective_plane; ex Q being Element of BK_model st P <> Q
per cases
( # P = |[0,0,1]| or # P <> |[0,0,1]| )
;
suppose A1:
# P = |[0,0,1]|
;
ex Q being Element of BK_model st P <> Qreconsider u =
|[0,(1 / 2),1]| as non
zero Element of
(TOP-REAL 3) ;
reconsider Q =
Dir u as
Point of
(ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
now for v being Element of (TOP-REAL 3) st not v is zero & Q = Dir v holds
qfconic (1,1,(- 1),0,0,0,v) is negative let v be
Element of
(TOP-REAL 3);
( not v is zero & Q = Dir v implies qfconic (1,1,(- 1),0,0,0,v) is negative )assume
( not
v is
zero &
Q = Dir v )
;
qfconic (1,1,(- 1),0,0,0,v) is negative then
are_Prop u,
v
by ANPROJ_1:22;
then consider a being
Real such that A2:
a <> 0
and A3:
v = a * u
by ANPROJ_1:1;
v =
|[(a * 0),(a * (1 / 2)),(a * 1)]|
by A3, EUCLID_5:8
.=
|[0,(a / 2),a]|
;
then A4:
(
v . 1
= 0 &
v . 2
= a / 2 &
v . 3
= a )
by FINSEQ_1:45;
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
.=
(a ^2) * (- (3 / 4))
by A4
;
hence
qfconic (1,1,
(- 1),
0,
0,
0,
v) is
negative
by A2;
verum end; then
Q in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) is negative }
;
then reconsider Q =
Q as
Element of
BK_model by BKMODEL2:def 1;
reconsider Q9 =
Q as
Element of
real_projective_plane ;
take
Q
;
P <> Q
Q <> P
hence
P <> Q
;
verum end; suppose A8:
# P <> |[0,0,1]|
;
ex Q being Element of BK_model st P <> Qreconsider u =
|[0,0,1]| as non
zero Element of
(TOP-REAL 3) ;
reconsider Q =
Dir u as
Point of
(ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
now for v being Element of (TOP-REAL 3) st not v is zero & Q = Dir v holds
qfconic (1,1,(- 1),0,0,0,v) is negative let v be
Element of
(TOP-REAL 3);
( not v is zero & Q = Dir v implies qfconic (1,1,(- 1),0,0,0,v) is negative )assume
( not
v is
zero &
Q = Dir v )
;
qfconic (1,1,(- 1),0,0,0,v) is negative then
are_Prop u,
v
by ANPROJ_1:22;
then consider a being
Real such that A9:
a <> 0
and A10:
v = a * u
by ANPROJ_1:1;
v =
|[(a * 0),(a * 0),(a * 1)]|
by A10, EUCLID_5:8
.=
|[0,0,a]|
;
then A11:
(
v . 1
= 0 &
v . 2
= 0 &
v . 3
= a )
by FINSEQ_1:45;
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
.=
(a ^2) * (- 1)
by A11
;
hence
qfconic (1,1,
(- 1),
0,
0,
0,
v) is
negative
by A9;
verum end; then
Q in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) is negative }
;
then reconsider Q =
Q as
Element of
BK_model by BKMODEL2:def 1;
reconsider Q9 =
Q as
Element of
real_projective_plane ;
take
Q
;
P <> Q
Q <> P
hence
P <> Q
;
verum end;