reconsider P = Q as Element of (TOP-REAL 2) ;
A1: |.(P - |[0,0]|).| =
|.(|[(P `1),(P `2)]| - |[0,0]|).|
by EUCLID:53
.=
|.|[((P `1) - 0),((P `2) - 0)]|.|
by EUCLID:62
.=
|.P.|
by EUCLID:53
;
1 ^2 = 1
;
then
|.P.| ^2 < 1
by TOPREAL9:45, A1, SQUARE_1:16;
then
((P `1) ^2) + ((P `2) ^2) < 1
by JGRAPH_3:1;
then A2:
(((P `1) ^2) + ((P `2) ^2)) - 1 < 1 - 1
by XREAL_1:14;
A3:
not |[(P `1),(P `2),1]| is zero
by EUCLID_5:4, FINSEQ_1:78;
then reconsider R = Dir |[(P `1),(P `2),1]| as Element of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
for u being Element of (TOP-REAL 3) st not u is zero & R = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) is negative
proof
let u be
Element of
(TOP-REAL 3);
( not u is zero & R = Dir u implies qfconic (1,1,(- 1),0,0,0,u) is negative )
assume that A4:
not
u is
zero
and A5:
R = Dir u
;
qfconic (1,1,(- 1),0,0,0,u) is negative
are_Prop u,
|[(P `1),(P `2),1]|
by A3, A4, A5, ANPROJ_1:22;
then consider k being
Real such that A6:
k <> 0
and A7:
u = k * |[(P `1),(P `2),1]|
by ANPROJ_1:1;
|[(P `1),(P `2),1]| . 1 =
|[(P `1),(P `2),1]| `1
by EUCLID_5:def 1
.=
P `1
by EUCLID_5:2
;
then A8:
u . 1
= k * (P `1)
by A7, RVSUM_1:44;
|[(P `1),(P `2),1]| . 2 =
|[(P `1),(P `2),1]| `2
by EUCLID_5:def 2
.=
P `2
by EUCLID_5:2
;
then A9:
u . 2
= k * (P `2)
by A7, RVSUM_1:44;
|[(P `1),(P `2),1]| . 3 =
|[(P `1),(P `2),1]| `3
by EUCLID_5:def 3
.=
1
by EUCLID_5:2
;
then A10:
u . 3
= k * 1
by A7, RVSUM_1:44;
A11:
qfconic (1,1,
(- 1),
0,
0,
0,
u) =
((((((1 * (u . 1)) * (u . 1)) + ((1 * (u . 2)) * (u . 2))) + (((- 1) * (u . 3)) * (u . 3))) + ((0 * (u . 1)) * (u . 2))) + ((0 * (u . 1)) * (u . 3))) + ((0 * (u . 2)) * 1)
by PASCAL:def 1
.=
(k ^2) * ((((P `1) ^2) + ((P `2) ^2)) - 1)
by A8, A9, A10
;
0 < k ^2
by A6, SQUARE_1:12;
hence
qfconic (1,1,
(- 1),
0,
0,
0,
u) is
negative
by A11, A2;
verum
end;
then
R 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 }
;
hence
ex b1 being Element of BK_model ex P being Element of (TOP-REAL 2) st
( P = Q & b1 = Dir |[(P `1),(P `2),1]| )
; verum