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

theorem Th01: :: BKMODEL1:1

for u, v, w being Element of (TOP-REAL 3)
for P1, P2, P3 being Element of (ProjectiveSpace (TOP-REAL 3)) 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 (TOP-REAL 3) holds (a * u) + ((- a) * u) = 0. (TOP-REAL 3)

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 (TOP-REAL 3) 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 (TOP-REAL 3) 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 (TOP-REAL 3)
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. (TOP-REAL 3) holds
N * uf = 0. (TOP-REAL 3)

proof end;

theorem Th32: :: BKMODEL1:36

for N being Matrix of 3,REAL
for uf being FinSequence of REAL
for u being Element of (TOP-REAL 3) st N is invertible & u = uf & not u is zero holds
N * uf <> 0. (TOP-REAL 3)

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 (ProjectiveSpace (TOP-REAL 3))
for u, v being non zero Element of (TOP-REAL 3)
for vfr, ufr being FinSequence of REAL st P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = vfr holds
(homography N) . 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 (ProjectiveSpace (TOP-REAL 3))
for u, v being non zero Element of (TOP-REAL 3)
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
(homography N) . 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 EUCLID_5:4, FINSEQ_1:78;

theorem :: BKMODEL1:42

for P, Q being Element of (TOP-REAL 2)
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 (TOP-REAL 3) st Dir u = Dir v & u . 3 = v . 3 & v . 3 <> 0 holds
u = v

proof end;

definition

func Dir101 -> Point of (ProjectiveSpace (TOP-REAL 3)) equals :: BKMODEL1:def 1
Dir |[1,0,1]|;

coherence
Dir |[1,0,1]| is Point of (ProjectiveSpace (TOP-REAL 3))

proof end;

end;

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

definition

func Dirm101 -> Point of (ProjectiveSpace (TOP-REAL 3)) equals :: BKMODEL1:def 2
Dir |[(- 1),0,1]|;

coherence
Dir |[(- 1),0,1]| is Point of (ProjectiveSpace (TOP-REAL 3))

proof end;

end;

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

definition

func Dir011 -> Point of (ProjectiveSpace (TOP-REAL 3)) equals :: BKMODEL1:def 3
Dir |[0,1,1]|;

coherence
Dir |[0,1,1]| is Point of (ProjectiveSpace (TOP-REAL 3))

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 PASCAL:def 3, ANPROJ_9:1;

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 * (1_Rmatrix 3) & M * O = ra * (1_Rmatrix 3) )

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 (TOP-REAL 3) st a * u = 0. (TOP-REAL 3) holds
u is zero

proof end;

theorem Th57: :: BKMODEL1:68

for u, v being non zero Element of (TOP-REAL 3)
for a, b being Real st ( a <> 0 or b <> 0 ) & (a * u) + (b * v) = 0. (TOP-REAL 3) 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 (ProjectiveSpace (TOP-REAL 3)) st P <> Q & (homography N) . P = Q & (homography N) . Q = P & P,Q,R are_collinear holds
(homography N) . ((homography N) . R) = R

proof end;

theorem :: BKMODEL1:70

for n being Nat
for u, v being Element of (TOP-REAL n)
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

ProjectiveSpace (TOP-REAL 3) is proper by ANPROJ_8:57;

definition

func real_projective_plane -> CollProjectivePlane equals :: BKMODEL1:def 4
ProjectiveSpace (TOP-REAL 3);

coherence
ProjectiveSpace (TOP-REAL 3) is CollProjectivePlane by ANPROJ_8:57;

end;

:: deftheorem defines real_projective_plane BKMODEL1:def 4 :
real_projective_plane = ProjectiveSpace (TOP-REAL 3);

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 (IncProjSp_of real_projective_plane) 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 (IncProjSp_of real_projective_plane)
for L being LINE of (IncProjSp_of real_projective_plane)
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

IncProjSp_of real_projective_plane is IncProjectivePlane

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 (IncProjSp_of real_projective_plane)
for L being LINE of (IncProjSp_of real_projective_plane)
for p, q being Point of real_projective_plane
for u, v, w being non zero Element of (TOP-REAL 3) 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 (TOP-REAL 3)
for p, q being Element of (ProjectiveSpace (TOP-REAL 3)) 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 (TOP-REAL 3) st
( p = Dir u & q = Dir v & it = Dir (u <X> v) );

existence
ex b₁ being Point of real_projective_plane ex u, v being non zero Element of (TOP-REAL 3) st
( p = Dir u & q = Dir v & b₁ = Dir (u <X> v) )

proof end;

uniqueness
for b₁, b₂ being Point of real_projective_plane st ex u, v being non zero Element of (TOP-REAL 3) st
( p = Dir u & q = Dir v & b₁ = Dir (u <X> v) ) & ex u, v being non zero Element of (TOP-REAL 3) st
( p = Dir u & q = Dir v & b₂ = Dir (u <X> v) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def01 defines L2P BKMODEL1:def 5 :
for p, q being Point of real_projective_plane st p <> q holds
for b₃ being Point of real_projective_plane holds
( b₃ = L2P (p,q) iff ex u, v being non zero Element of (TOP-REAL 3) st
( p = Dir u & q = Dir v & b₃ = 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 (homography N) = ProjectivePoints (TOP-REAL 3)

proof end;

definition

let a, b, c, d, e, f be Real;

func negative_conic (a,b,c,d,e,f) -> Subset of (ProjectiveSpace (TOP-REAL 3)) equals :: BKMODEL1:def 6
{ 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 (a,b,c,d,e,f,u) is negative } ;

coherence
{ 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 (a,b,c,d,e,f,u) is negative } is Subset of (ProjectiveSpace (TOP-REAL 3))

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 (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) 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 (TOP-REAL 3) 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 (ProjectiveSpace (TOP-REAL 3)) equals :: BKMODEL1:def 7
conic (1,1,(- 1),0,0,0);

coherence
conic (1,1,(- 1),0,0,0) is non empty Subset of (ProjectiveSpace (TOP-REAL 3))

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 (TOP-REAL 3)
for O being Matrix of 3,REAL
for P being Element of (ProjectiveSpace (TOP-REAL 3))
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 (TOP-REAL 3)
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 (TOP-REAL 3)
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 (TOP-REAL 3)
for P being Point of (ProjectiveSpace (TOP-REAL 3)) 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 (ProjectiveSpace (TOP-REAL 3))
for u being non zero Element of (TOP-REAL 3) st P = Dir u & u . 3 = 1 holds
( |[(u . 1),(u . 2)]| in circle (0,0,1) iff P is Element of absolute ) by Th68, Th69;

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 (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & it = |[(u . 1),(u . 2)]| );

existence
ex b₁ being Element of circle (0,0,1) ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & b₁ = |[(u . 1),(u . 2)]| )

proof end;

uniqueness
for b₁, b₂ being Element of circle (0,0,1) st ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & b₁ = |[(u . 1),(u . 2)]| ) & ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & b₂ = |[(u . 1),(u . 2)]| ) holds
b₁ = b₂

proof end;

end;

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

theorem :: BKMODEL1:87

the carrier of (Tunit_circle 2) = circle (0,0,1)

proof end;

definition

let u be non zero Element of (TOP-REAL 2);
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 (TOP-REAL 2) 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 (TOP-REAL 3) st qfconic (1,1,(- 1),0,0,0,u) = 0 & u . 3 = 1 holds
|[(u . 1),(u . 2)]| in Sphere ((0. (TOP-REAL 2)),1)

proof end;

theorem :: BKMODEL1:89

for P being Element of absolute ex u being non zero Element of (TOP-REAL 3) 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 & (homography M) .: absolute = absolute holds
(homography N) .: absolute = absolute

proof end;