:: Beltrami-Klein Model, {P}art {I}
:: by Roland Coghetto
::
:: Copyright (c) 2018-2021 Association of Mizar Users

theorem Th01: :: BKMODEL1:1
for u, v, w being Element of ()
for P1, P2, P3 being Element of () st not u is zero & not v is zero & not w is zero & P1 = Dir u & P2 = Dir v & P3 = Dir w holds
( P1,P2,P3 are_collinear iff |{u,v,w}| = 0 )
proof end;

Lem01: for a, b, c, d being Real st a <> 0 & b <> 0 & a * d = b * c holds
ex e being Real st
( e = d / b & e = c / a & c = e * a & d = e * b )

proof end;

Lem02: for a, b, c, d being Real st a <> 0 & b = 0 & a * d = b * c holds
ex e being Real st
( c = e * a & d = e * b )

proof end;

theorem :: BKMODEL1:2
for a, b, c, d being Real st ( a <> 0 or b <> 0 ) & a * d = b * c holds
ex e being Real st
( c = e * a & d = e * b )
proof end;

theorem :: BKMODEL1:3
for a, b, c being Real st (a ^2) + (b ^2) = 1 & ((c * a) ^2) + ((c * b) ^2) = 1 & not c = 1 holds
c = - 1
proof end;

theorem :: BKMODEL1:4
for a being Real
for u being Element of () holds (a * u) + ((- a) * u) = 0. ()
proof end;

theorem :: BKMODEL1:5
for a, b, c being Real st 0 <= a & c < 0 & delta (a,b,c) = 0 holds
a = 0
proof end;

theorem :: BKMODEL1:6
for S, T being Element of REAL 2 holds Sum (sqr (T - S)) = Sum (sqr (S - T))
proof end;

theorem :: BKMODEL1:7
for a, b, c, d being Real st (a ^2) + (b ^2) = 1 & (c ^2) + (d ^2) = 1 & (c * a) + (d * b) = 1 holds
b * c = a * d
proof end;

theorem :: BKMODEL1:8
for a, b being Real st (a ^2) + (b ^2) = 1 & a = 0 & not b = 1 holds
b = - 1
proof end;

Lem03: for a being Real holds 1 + (a ^2) <> 0
proof end;

theorem Th07: :: BKMODEL1:9
for a being Real holds 0 <= a ^2
proof end;

Lem04: for a, b being Real holds
( not a ^2 = 1 / b or a = 1 / (sqrt b) or a = (- 1) / (sqrt b) )

proof end;

theorem :: BKMODEL1:10
for a, b being Real holds
( not ((a * b) ^2) + (b ^2) = 1 or b = 1 / (sqrt (1 + (a ^2))) or b = (- 1) / (sqrt (1 + (a ^2))) )
proof end;

Lem05: for z being non zero Complex holds ((1 / z) ^2) * (z ^2) = 1
proof end;

theorem :: BKMODEL1:11
for a, b being Real st a <> 0 & b ^2 = 1 + (a * a) holds
(((a * (1 / b)) * a) * ((- 1) / b)) + ((1 / b) * ((- 1) / b)) = - 1
proof end;

theorem :: BKMODEL1:12
for a, b being Real holds (a ^2) * (1 / (b ^2)) = (a / b) ^2
proof end;

theorem Th11: :: BKMODEL1:13
for a, b being Real holds
( (a ^2) + (b ^2) = 1 iff |[a,b]| in circle (0,0,1) )
proof end;

theorem Th12: :: BKMODEL1:14
for a, b being Real
for g being positive Real holds
( (a ^2) + (b ^2) = g ^2 iff |[a,b]| in circle (0,0,g) )
proof end;

Lem06: for a, b, c being Real holds ((a * b) ^2) + ((a * c) ^2) = (a ^2) * ((b ^2) + (c ^2))
;

theorem Th13: :: BKMODEL1:15
for a, b being Real st a <> 0 & - 1 < a & a < 1 & b = (2 + (sqrt (delta ((a * a),(- 2),1)))) / ((2 * a) * a) holds
(((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0
proof end;

Lem07: for a being Real st - 1 < a & a < 1 holds
ex b being Real st (((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0

proof end;

theorem :: BKMODEL1:16
for a, b, c being Real st (a ^2) + (b ^2) = 1 & - 1 < c & c < 1 holds
ex d, e, f being Real st
( e = ((d * c) * a) + ((1 - d) * (- b)) & f = ((d * c) * b) + ((1 - d) * a) & (e ^2) + (f ^2) = d ^2 )
proof end;

theorem :: BKMODEL1:17
for a, b, c, d being Real st (a ^2) + (b ^2) < 1 & (c ^2) + (d ^2) = 1 holds
(((a + c) / 2) ^2) + (((b + d) / 2) ^2) < 1
proof end;

Lem08: for a, b, c being Real st 0 <= a & c <= 0 holds
0 <= delta (a,b,c)

proof end;

theorem :: BKMODEL1:18
for b being Real
for S, T being Element of REAL 2 st |.S.| ^2 <= 1 holds
0 <= delta ((Sum (sqr (T - S))),b,((Sum (sqr S)) - 1))
proof end;

theorem :: BKMODEL1:19
for a, b being Real st (a ^2) + (b ^2) is negative holds
( a = 0 & b = 0 )
proof end;

theorem :: BKMODEL1:20
for a, b, c, d being Real
for u, v, w being Element of () st u = |[a,b,1]| & v = |[c,d,1]| & w = |[((a + c) / 2),((b + d) / 2),1]| holds
|{u,v,w}| = 0
proof end;

theorem Th19: :: BKMODEL1:21
for a being Real
for u, v being Element of () holds
( a * |(u,v)| = |((a * u),v)| & a * |(u,v)| = |(u,(a * v))| )
proof end;

theorem :: BKMODEL1:22
for M being Matrix of 3,F_Real st M = symmetric_3 (0,0,0,0,0,0) holds
Det M = 0. F_Real
proof end;

Lem09: for a11, a12, a13, a21, a22, a23, a31, a32, a33, b11, b12, b13, b21, b22, b23, b31, b32, b33 being Element of F_Real
for A, B being Matrix of 3,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> & B = <*<*b11,b12,b13*>,<*b21,b22,b23*>,<*b31,b32,b33*>*> holds
( (A * B) * (1,1) = ((a11 * b11) + (a12 * b21)) + (a13 * b31) & (A * B) * (1,2) = ((a11 * b12) + (a12 * b22)) + (a13 * b32) & (A * B) * (1,3) = ((a11 * b13) + (a12 * b23)) + (a13 * b33) & (A * B) * (2,1) = ((a21 * b11) + (a22 * b21)) + (a23 * b31) & (A * B) * (2,2) = ((a21 * b12) + (a22 * b22)) + (a23 * b32) & (A * B) * (2,3) = ((a21 * b13) + (a22 * b23)) + (a23 * b33) & (A * B) * (3,1) = ((a31 * b11) + (a32 * b21)) + (a33 * b31) & (A * B) * (3,2) = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & (A * B) * (3,3) = ((a31 * b13) + (a32 * b23)) + (a33 * b33) )

proof end;

theorem :: BKMODEL1:23
for a, b, c being Element of F_Real
for M, N being Matrix of 3,F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds
( ((M @) * (N * M)) * (1,1) = (((a * (M * (1,1))) * (M * (1,1))) + ((b * (M * (2,1))) * (M * (2,1)))) + ((c * (M * (3,1))) * (M * (3,1))) & ((M @) * (N * M)) * (1,2) = (((a * (M * (1,1))) * (M * (1,2))) + ((b * (M * (2,1))) * (M * (2,2)))) + ((c * (M * (3,1))) * (M * (3,2))) & ((M @) * (N * M)) * (1,3) = (((a * (M * (1,1))) * (M * (1,3))) + ((b * (M * (2,1))) * (M * (2,3)))) + ((c * (M * (3,1))) * (M * (3,3))) & ((M @) * (N * M)) * (2,1) = (((a * (M * (1,2))) * (M * (1,1))) + ((b * (M * (2,2))) * (M * (2,1)))) + ((c * (M * (3,2))) * (M * (3,1))) & ((M @) * (N * M)) * (2,2) = (((a * (M * (1,2))) * (M * (1,2))) + ((b * (M * (2,2))) * (M * (2,2)))) + ((c * (M * (3,2))) * (M * (3,2))) & ((M @) * (N * M)) * (2,3) = (((a * (M * (1,2))) * (M * (1,3))) + ((b * (M * (2,2))) * (M * (2,3)))) + ((c * (M * (3,2))) * (M * (3,3))) & ((M @) * (N * M)) * (3,1) = (((a * (M * (1,3))) * (M * (1,1))) + ((b * (M * (2,3))) * (M * (2,1)))) + ((c * (M * (3,3))) * (M * (3,1))) & ((M @) * (N * M)) * (3,2) = (((a * (M * (1,3))) * (M * (1,2))) + ((b * (M * (2,3))) * (M * (2,2)))) + ((c * (M * (3,3))) * (M * (3,2))) & ((M @) * (N * M)) * (3,3) = (((a * (M * (1,3))) * (M * (1,3))) + ((b * (M * (2,3))) * (M * (2,3)))) + ((c * (M * (3,3))) * (M * (3,3))) )
proof end;

theorem :: BKMODEL1:24
for m, n being Nat
for M being Matrix of m,F_Real
for N being Matrix of m,n,F_Real st m > 0 holds
M * N is Matrix of m,n,F_Real
proof end;

theorem :: BKMODEL1:25
for D being non empty set
for M being Matrix of 1,D holds M @ = M
proof end;

theorem Th23: :: BKMODEL1:26
for D being non empty set
for A being Matrix of 1,3,D holds A @ is 3,1 -size
proof end;

theorem Th24: :: BKMODEL1:27
for D being non empty set
for d1, d2, d3 being Element of D holds <*<*d1,d2,d3*>*> is Matrix of 1,3,D
proof end;

theorem Th25: :: BKMODEL1:28
for D being non empty set
for d1, d2, d3 being Element of D holds <*<*d1*>,<*d2*>,<*d3*>*> is Matrix of 3,1,D
proof end;

theorem Th26: :: BKMODEL1:29
for D being non empty set
for A being Matrix of 1,3,D holds A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>*>
proof end;

theorem Th27: :: BKMODEL1:30
for D being non empty set
for B being Matrix of 3,1,D holds B = <*<*(B * (1,1))*>,<*(B * (2,1))*>,<*(B * (3,1))*>*>
proof end;

theorem :: BKMODEL1:31
for D being non empty set
for A being Matrix of 1,3,D holds A @ = <*<*(A * (1,1))*>,<*(A * (1,2))*>,<*(A * (1,3))*>*>
proof end;

theorem :: BKMODEL1:32
for D being non empty set
for A being Matrix of 1,3,D ex d1, d2, d3 being Element of D st A = <*<*d1,d2,d3*>*>
proof end;

theorem :: BKMODEL1:33
for p being FinSequence of 1 -tuples_on REAL st len p = 3 holds
ColVec2Mx (M2F p) = p
proof end;

theorem Th30: :: BKMODEL1:34
for M being Matrix of 3,F_Real
for MR being Matrix of 3,REAL
for v being Element of ()
for uf being FinSequence of F_Real
for ufr being FinSequence of REAL
for p being FinSequence of 1 -tuples_on REAL st p = M * uf & v = M2F p & len uf = 3 & uf = ufr & MR = M holds
v = MR * ufr
proof end;

theorem Th31: :: BKMODEL1:35
for N being Matrix of 3,REAL
for uf being FinSequence of REAL st uf = 0. () holds
N * uf = 0. ()
proof end;

theorem Th32: :: BKMODEL1:36
for N being Matrix of 3,REAL
for uf being FinSequence of REAL
for u being Element of () st N is invertible & u = uf & not u is zero holds
N * uf <> 0. ()
proof end;

theorem :: BKMODEL1:37
for N being invertible Matrix of 3,F_Real
for NR being Matrix of 3,REAL
for P, Q being Element of ()
for u, v being non zero Element of ()
for vfr, ufr being FinSequence of REAL st P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = vfr holds
() . P = Q
proof end;

theorem Th33: :: BKMODEL1:38
for N being invertible Matrix of 3,F_Real
for NR being Matrix of 3,REAL
for P, Q being Element of ()
for u, v being non zero Element of ()
for vfr, ufr being FinSequence of REAL
for a being non zero Real st P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = a * vfr holds
() . P = Q
proof end;

theorem Th34: :: BKMODEL1:39
for a, b being Element of F_Real
for p being FinSequence of REAL
for M being Matrix of 3,REAL st len p = 3 holds
|((a * p),(M * (b * p)))| = (a * b) * |(p,(M * p))|
proof end;

theorem Th35: :: BKMODEL1:40
for a, b being Element of F_Real
for p being FinSequence of REAL
for M being Matrix of 3,REAL st len p = 3 holds
SumAll (QuadraticForm ((a * p),M,(b * p))) = (a * b) * (SumAll (QuadraticForm (p,M,p)))
proof end;

theorem Th36: :: BKMODEL1:41
for a, b being Real holds not |[a,b,1]| is zero by ;

theorem :: BKMODEL1:42
for P, Q being Element of ()
for r being Real holds
( P in Sphere (Q,r) iff P in circle ((Q . 1),(Q . 2),r) )
proof end;

theorem Th37: :: BKMODEL1:43
for u, v being non zero Element of () st Dir u = Dir v & u . 3 = v . 3 & v . 3 <> 0 holds
u = v
proof end;

definition
func Dir101 -> Point of () equals :: BKMODEL1:def 1
Dir |[1,0,1]|;
coherence
Dir |[1,0,1]| is Point of ()
proof end;
end;

:: deftheorem defines Dir101 BKMODEL1:def 1 :
Dir101 = Dir |[1,0,1]|;

definition
func Dirm101 -> Point of () equals :: BKMODEL1:def 2
Dir |[(- 1),0,1]|;
coherence
Dir |[(- 1),0,1]| is Point of ()
proof end;
end;

:: deftheorem defines Dirm101 BKMODEL1:def 2 :
Dirm101 = Dir |[(- 1),0,1]|;

definition
func Dir011 -> Point of () equals :: BKMODEL1:def 3
Dir |[0,1,1]|;
coherence
Dir |[0,1,1]| is Point of ()
proof end;
end;

:: deftheorem defines Dir011 BKMODEL1:def 3 :
Dir011 = Dir |[0,1,1]|;

theorem :: BKMODEL1:44
( not Dir101 , Dirm101 , Dir011 are_collinear & not Dir101 , Dirm101 , Dir010 are_collinear & not Dir101 , Dir011 , Dir010 are_collinear & not Dirm101 , Dir011 , Dir010 are_collinear )
proof end;

theorem :: BKMODEL1:45
symmetric_3 (1,1,1,0,0,0) = 1. (F_Real,3) by ;

theorem Th39: :: BKMODEL1:46
for r, a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
r * M = <*<*(r * a),(r * b),(r * c)*>,<*(r * d),(r * e),(r * f)*>,<*(r * g),(r * h),(r * i)*>*>
proof end;

theorem Th40: :: BKMODEL1:47
for a being Real
for ra2 being Element of F_Real st ra2 = a * a holds
(symmetric_3 (a,a,(- a),0,0,0)) * (symmetric_3 (a,a,(- a),0,0,0)) = ra2 * (1. (F_Real,3))
proof end;

theorem Th41: :: BKMODEL1:48
for a being non zero Real holds (symmetric_3 (a,a,(- a),0,0,0)) * (symmetric_3 ((1 / a),(1 / a),(- (1 / a)),0,0,0)) = 1. (F_Real,3)
proof end;

theorem Th42: :: BKMODEL1:49
for a being non zero Real holds (symmetric_3 ((1 / a),(1 / a),(- (1 / a)),0,0,0)) * (symmetric_3 (a,a,(- a),0,0,0)) = 1. (F_Real,3)
proof end;

theorem Th43: :: BKMODEL1:50
(symmetric_3 (1,1,(- 1),0,0,0)) * (symmetric_3 (1,1,(- 1),0,0,0)) = 1. (F_Real,3)
proof end;

theorem :: BKMODEL1:51
for a being non zero Real
for N being Matrix of 3,F_Real st N = symmetric_3 (a,a,(- a),0,0,0) holds
N is invertible
proof end;

theorem Th44: :: BKMODEL1:52
( symmetric_3 (1,1,(- 1),0,0,0) is invertible Matrix of 3,F_Real & (symmetric_3 (1,1,(- 1),0,0,0)) ~ = symmetric_3 (1,1,(- 1),0,0,0) )
proof end;

theorem :: BKMODEL1:53
for N being invertible Matrix of 3,F_Real
for N1 being Matrix of 3,F_Real
for M, NR being Matrix of 3,REAL st M = symmetric_3 (1,1,(- 1),0,0,0) & N1 = M & NR = MXF2MXR (N ~) holds
((N @) * N1) * N = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~))
proof end;

theorem Th46: :: BKMODEL1:54
for n being Nat
for a being Element of F_Real
for ra being Real
for A being Matrix of n,F_Real
for rA being Matrix of n,REAL st a = ra & A = rA holds
a * A = ra * rA
proof end;

theorem Th47: :: BKMODEL1:55
for n being Nat
for a being Element of F_Real
for A, B being Matrix of n,F_Real st n > 0 holds
(a * A) * B = a * (A * B)
proof end;

theorem Th48: :: BKMODEL1:56
for a being Element of F_Real holds symmetric_3 (a,a,(- a),0,0,0) = a * (symmetric_3 (1,1,(- 1),0,0,0))
proof end;

theorem Th49: :: BKMODEL1:57
for a being Element of F_Real
for M being Matrix of 3,F_Real st M = symmetric_3 (a,a,(- a),0,0,0) holds
(M * M) * M = ((a * a) * a) * (symmetric_3 (1,1,(- 1),0,0,0))
proof end;

theorem Th50: :: BKMODEL1:58
for n being Nat
for a being Real
for M being Matrix of n,REAL
for x being FinSequence of REAL st n > 0 & len x = n holds
M * (a * x) = (a * M) * x
proof end;

theorem Th51: :: BKMODEL1:59
for n being Nat
for a being Real
for M being Matrix of n,REAL
for x being FinSequence of REAL st n > 0 & len x = n holds
a * (M * x) = (a * M) * x
proof end;

theorem Th52: :: BKMODEL1:60
for n being Nat
for N being Matrix of n,REAL st N is invertible holds
( N @ is invertible & Inv (N @) = (Inv N) @ )
proof end;

theorem Th53: :: BKMODEL1:61
for ra being non zero Real
for N, O, M being Matrix of 3,3,REAL st N is invertible & M = ra * O & M = ((N @) * O) * N holds
(((Inv N) @) * O) * (Inv N) = (1 / ra) * O
proof end;

theorem Th54: :: BKMODEL1:62
for ra being Real
for M, N being Matrix of 3,F_Real
for MR, NR being Matrix of 3,REAL st MR = M & NR = N & N is symmetric & MR = ra * NR holds
M is symmetric
proof end;

theorem Th55: :: BKMODEL1:63
for ra being Real
for O, M being Matrix of 3,REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & M = ra * O holds
( O * M = ra * () & M * O = ra * () )
proof end;

theorem :: BKMODEL1:64
for ra being Real
for O, M being Matrix of 3,REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & M = ra * O holds
((((M @) * O) @) * O) * ((M @) * O) = (ra ^2) * O
proof end;

theorem :: BKMODEL1:65
for O, N being Matrix of 3,REAL holds ((((N @) * O) @) * O) * ((N @) * O) = ((O @) * ((N * O) * (N @))) * O
proof end;

theorem :: BKMODEL1:66
for NR, MR being Matrix of 3,REAL
for p1, p2, p3 being FinSequence of REAL st p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & NR * p1 = MR * p1 & NR * p2 = MR * p2 & NR * p3 = MR * p3 holds
NR = MR
proof end;

theorem Th56: :: BKMODEL1:67
for a being non zero Real
for u being Element of () st a * u = 0. () holds
u is zero
proof end;

theorem Th57: :: BKMODEL1:68
for u, v being non zero Element of ()
for a, b being Real st ( a <> 0 or b <> 0 ) & (a * u) + (b * v) = 0. () holds
are_Prop u,v
proof end;

theorem :: BKMODEL1:69
for N being invertible Matrix of 3,F_Real
for P, Q, R being Point of () st P <> Q & () . P = Q & () . Q = P & P,Q,R are_collinear holds
() . (() . R) = R
proof end;

theorem :: BKMODEL1:70
for n being Nat
for u, v being Element of ()
for a, b being Real st ((1 - a) * u) + (a * v) = ((1 - b) * v) + (b * u) holds
(1 - (a + b)) * u = (1 - (a + b)) * v
proof end;

theorem :: BKMODEL1:71

definition
coherence by ANPROJ_8:57;
end;

:: deftheorem defines real_projective_plane BKMODEL1:def 4 :

theorem :: BKMODEL1:72
for L being Element of ProjectiveLines real_projective_plane ex p, q being Point of real_projective_plane st
( p <> q & L = Line (p,q) )
proof end;

theorem Th60: :: BKMODEL1:73
for L being LINE of ex p, q being Point of real_projective_plane st
( p <> q & L = Line (p,q) )
proof end;

theorem Th61: :: BKMODEL1:74
for R being POINT of
for L being LINE of
for p, q, r being Point of real_projective_plane st R = r & L = Line (p,q) holds
( R on L iff p,q,r are_collinear )
proof end;

theorem Th62: :: BKMODEL1:75
proof end;

theorem :: BKMODEL1:76
for L1, L2 being LINE of real_projective_plane holds L1 meets L2
proof end;

theorem :: BKMODEL1:77
for R being POINT of
for L being LINE of
for p, q being Point of real_projective_plane
for u, v, w being non zero Element of () st p = Dir u & q = Dir v & R = Dir w & L = Line (p,q) holds
( R on L iff |{u,v,w}| = 0 )
proof end;

theorem Th64: :: BKMODEL1:78
for u, v being non zero Element of ()
for p, q being Element of () st p <> q & p = Dir u & q = Dir v holds
not u <X> v is zero
proof end;

definition
let p, q be Point of real_projective_plane;
assume A1: p <> q ;
func L2P (p,q) -> Point of real_projective_plane means :Def01: :: BKMODEL1:def 5
ex u, v being non zero Element of () st
( p = Dir u & q = Dir v & it = Dir (u <X> v) );
existence
ex b1 being Point of real_projective_plane ex u, v being non zero Element of () st
( p = Dir u & q = Dir v & b1 = Dir (u <X> v) )
proof end;
uniqueness
for b1, b2 being Point of real_projective_plane st ex u, v being non zero Element of () st
( p = Dir u & q = Dir v & b1 = Dir (u <X> v) ) & ex u, v being non zero Element of () st
( p = Dir u & q = Dir v & b2 = Dir (u <X> v) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def01 defines L2P BKMODEL1:def 5 :
for p, q being Point of real_projective_plane st p <> q holds
for b3 being Point of real_projective_plane holds
( b3 = L2P (p,q) iff ex u, v being non zero Element of () st
( p = Dir u & q = Dir v & b3 = Dir (u <X> v) ) );

theorem :: BKMODEL1:79
for p, q being Point of real_projective_plane st p <> q holds
( L2P (q,p) = L2P (p,q) & p <> L2P (p,q) )
proof end;

theorem :: BKMODEL1:80
for N being invertible Matrix of 3,F_Real holds dom () = ProjectivePoints ()
proof end;

definition
let a, b, c, d, e, f be Real;
func negative_conic (a,b,c,d,e,f) -> Subset of () equals :: BKMODEL1:def 6
{ P where P is Point of () : for u being Element of () st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) is negative
}
;
coherence
{ P where P is Point of () : for u being Element of () st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) is negative
}
is Subset of ()
proof end;
end;

:: deftheorem defines negative_conic BKMODEL1:def 6 :
for a, b, c, d, e, f being Real holds negative_conic (a,b,c,d,e,f) = { P where P is Point of () : for u being Element of () st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) is negative
}
;

theorem :: BKMODEL1:81
for a, b, c, d, e, f being Real
for u1, u2 being non zero Element of () st Dir u1 = Dir u2 & qfconic (a,b,c,d,e,f,u1) is negative holds
qfconic (a,b,c,d,e,f,u2) is negative
proof end;

definition
func absolute -> non empty Subset of () equals :: BKMODEL1:def 7
conic (1,1,(- 1),0,0,0);
coherence
conic (1,1,(- 1),0,0,0) is non empty Subset of ()
proof end;
end;

:: deftheorem defines absolute BKMODEL1:def 7 :
absolute = conic (1,1,(- 1),0,0,0);

theorem Th66: :: BKMODEL1:82
for u being non zero Element of ()
for O being Matrix of 3,REAL
for P being Element of ()
for p being FinSequence of REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & u = p holds
( P in absolute iff SumAll (QuadraticForm (p,O,p)) = 0 )
proof end;

theorem Th67: :: BKMODEL1:83
for u being non zero Element of ()
for P being Element of absolute st P = Dir u holds
u . 3 <> 0
proof end;

theorem Th68: :: BKMODEL1:84
for u being non zero Element of ()
for P being Element of absolute st P = Dir u & u . 3 = 1 holds
|[(u . 1),(u . 2)]| in circle (0,0,1)
proof end;

theorem Th69: :: BKMODEL1:85
for u being non zero Element of ()
for P being Point of () st P = Dir u & u . 3 = 1 & |[(u . 1),(u . 2)]| in circle (0,0,1) holds
P is Element of absolute
proof end;

theorem :: BKMODEL1:86
for P being Point of ()
for u being non zero Element of () st P = Dir u & u . 3 = 1 holds
( |[(u . 1),(u . 2)]| in circle (0,0,1) iff P is Element of absolute ) by ;

definition
let P be Element of absolute ;
func absolute_to_REAL2 P -> Element of circle (0,0,1) means :: BKMODEL1:def 8
ex u being non zero Element of () st
( P = Dir u & u . 3 = 1 & it = |[(u . 1),(u . 2)]| );
existence
ex b1 being Element of circle (0,0,1) ex u being non zero Element of () st
( P = Dir u & u . 3 = 1 & b1 = |[(u . 1),(u . 2)]| )
proof end;
uniqueness
for b1, b2 being Element of circle (0,0,1) st ex u being non zero Element of () st
( P = Dir u & u . 3 = 1 & b1 = |[(u . 1),(u . 2)]| ) & ex u being non zero Element of () st
( P = Dir u & u . 3 = 1 & b2 = |[(u . 1),(u . 2)]| ) holds
b1 = b2
proof end;
end;

:: deftheorem defines absolute_to_REAL2 BKMODEL1:def 8 :
for P being Element of absolute
for b2 being Element of circle (0,0,1) holds
( b2 = absolute_to_REAL2 P iff ex u being non zero Element of () st
( P = Dir u & u . 3 = 1 & b2 = |[(u . 1),(u . 2)]| ) );

theorem :: BKMODEL1:87
the carrier of () = circle (0,0,1)
proof end;

definition
let u be non zero Element of ();
assume A1: u in circle (0,0,1) ;
func REAL2_to_absolute u -> Element of absolute equals :: BKMODEL1:def 9
Dir |[(u . 1),(u . 2),1]|;
coherence
Dir |[(u . 1),(u . 2),1]| is Element of absolute
proof end;
end;

:: deftheorem defines REAL2_to_absolute BKMODEL1:def 9 :
for u being non zero Element of () st u in circle (0,0,1) holds
REAL2_to_absolute u = Dir |[(u . 1),(u . 2),1]|;

theorem Th70: :: BKMODEL1:88
for u being Element of () st qfconic (1,1,(- 1),0,0,0,u) = 0 & u . 3 = 1 holds
|[(u . 1),(u . 2)]| in Sphere ((0. ()),1)
proof end;

theorem :: BKMODEL1:89
for P being Element of absolute ex u being non zero Element of () st
( ((u . 1) ^2) + ((u . 2) ^2) = 1 & u . 3 = 1 & P = Dir u )
proof end;

theorem :: BKMODEL1:90
for P being Element of absolute ex Q being Element of absolute st P <> Q
proof end;

theorem :: BKMODEL1:91
for a, b being Real st (a ^2) + (b ^2) = 1 holds
not |[(- b),a,0]| is zero
proof end;

theorem :: BKMODEL1:92
for P, Q, R being Element of absolute st P,Q,R are_mutually_distinct holds
not P,Q,R are_collinear
proof end;

theorem :: BKMODEL1:93
for ra being non zero Real
for O, N, M being invertible Matrix of 3,F_Real st O = symmetric_3 (1,1,(- 1),0,0,0) & M = symmetric_3 (ra,ra,(- ra),0,0,0) & M = ((N @) * O) * N & () .: absolute = absolute holds
() .: absolute = absolute
proof end;