BKMODEL4: Beltrami-Klein model, Part {IV}

:: Beltrami-Klein model, Part {IV}
:: by Roland Coghetto
::
:: Received December 30, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

theorem Th25: :: BKMODEL4:1

for a, b being Real st a <> b holds
1 - (a / (a - b)) = - (b / (a - b))

proof end;

theorem :: BKMODEL4:2

for a, b being Real st 0 < a * b holds
0 < a / b

proof end;

theorem Th31: :: BKMODEL4:3

for a, b, c being Real st 0 <= a & a <= 1 & 0 < b * c holds
( 0 <= (a * c) / (((1 - a) * b) + (a * c)) & (a * c) / (((1 - a) * b) + (a * c)) <= 1 )

proof end;

theorem Th32: :: BKMODEL4:4

for a, b, c being Real st ((1 - a) * b) + (a * c) <> 0 holds
1 - ((a * c) / (((1 - a) * b) + (a * c))) = ((1 - a) * b) / (((1 - a) * b) + (a * c))

proof end;

theorem Th33: :: BKMODEL4:5

for a, b, c, d being Real st b <> 0 holds
(((a * b) / c) * d) / b = (a * d) / c

proof end;

theorem Th35: :: BKMODEL4:6

for u being Element of (TOP-REAL 3) holds u = |[(u . 1),(u . 2),(u . 3)]|

proof end;

theorem Th01: :: BKMODEL4:7

for P being Element of BK_model holds BK_to_REAL2 P in TarskiEuclid2Space

proof end;

definition

let P be POINT of BK-model-Plane;

func BK_to_T2 P -> POINT of TarskiEuclid2Space means :Def01: :: BKMODEL4:def 1
ex p being Element of BK_model st
( P = p & it = BK_to_REAL2 p );

existence

proof end;

uniqueness ;

end;

:: deftheorem Def01 defines BK_to_T2 BKMODEL4:def 1 :

definition

let P be POINT of TarskiEuclid2Space;
assume A1: Tn2TR P in inside_of_circle (0,0,1) ;

func T2_to_BK P -> POINT of BK-model-Plane means :Def02: :: BKMODEL4:def 2
ex u being non zero Element of (TOP-REAL 3) st
( it = Dir u & u `3 = 1 & Tn2TR P = |[(u `1),(u `2)]| );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def02 defines T2_to_BK BKMODEL4:def 2 :

theorem Th02: :: BKMODEL4:8

for P being POINT of BK-model-Plane holds Tn2TR (BK_to_T2 P) in inside_of_circle (0,0,1)

proof end;

theorem :: BKMODEL4:9

for P being POINT of BK-model-Plane holds T2_to_BK (BK_to_T2 P) = P

proof end;

theorem Th03: :: BKMODEL4:10

for P being POINT of TarskiEuclid2Space st Tn2TR P is Element of inside_of_circle (0,0,1) holds
BK_to_T2 (T2_to_BK P) = P

proof end;

theorem Th04: :: BKMODEL4:11

for P being Point of BK-model-Plane
for p being Element of BK_model st P = p holds
( BK_to_T2 P = BK_to_REAL2 p & Tn2TR (BK_to_T2 P) = BK_to_REAL2 p )

proof end;

theorem Th05: :: BKMODEL4:12

for P, Q, R being Point of BK-model-Plane
for P2, Q2, R2 being POINT of TarskiEuclid2Space st P2 = BK_to_T2 P & Q2 = BK_to_T2 Q & R2 = BK_to_T2 R holds
( between P,Q,R iff between P2,Q2,R2 )

proof end;

theorem Th06: :: BKMODEL4:13

for P, Q being Element of (TOP-REAL 2) holds
( not P <> Q or P . 1 <> Q . 1 or P . 2 <> Q . 2 )

proof end;

theorem Th07: :: BKMODEL4:14

for a, b being Real
for P, Q being Element of (TOP-REAL 2) st P <> Q & ((1 - a) * P) + (a * Q) = ((1 - b) * P) + (b * Q) holds
a = b

proof end;

theorem Th08: :: BKMODEL4:15

for P, Q being Point of BK-model-Plane st Tn2TR (BK_to_T2 P) = Tn2TR (BK_to_T2 Q) holds
P = Q

proof end;

definition

let P, Q, R be Point of BK-model-Plane;
assume that
A1: between P,Q,R and
A2: P <> R ;

func length (P,Q,R) -> Real means :Def03: :: BKMODEL4:def 3
( 0 <= it & it <= 1 & Tn2TR (BK_to_T2 Q) = ((1 - it) * (Tn2TR (BK_to_T2 P))) + (it * (Tn2TR (BK_to_T2 R))) );

existence

proof end;

uniqueness by A2, Th07, Th08;

end;

:: deftheorem Def03 defines length BKMODEL4:def 3 :

theorem Th09: :: BKMODEL4:16

for P, Q being Point of BK-model-Plane holds
( between P,P,Q & between P,Q,Q )

proof end;

theorem :: BKMODEL4:17

for P, Q being Point of BK-model-Plane st P <> Q holds
( length (P,P,Q) = 0 & length (P,Q,Q) = 1 )

proof end;

theorem :: BKMODEL4:18

for N being Matrix of 3,F_Real st N = <*<*2,0,(- 1)*>,<*0,(sqrt 3),0*>,<*1,0,(- 2)*>*> holds
( Det N = (- 3) * (sqrt 3) & N is invertible )

proof end;

theorem Th10: :: BKMODEL4:19

for a11, a12, a13, a21, a22, a23, a31, a32, a33, b11, b12, b13, b21, b22, b23, b31, b32, b33, ab11, ab12, ab13, ab21, ab22, ab23, ab31, ab32, ab33 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*>*> & ab11 = ((a11 * b11) + (a12 * b21)) + (a13 * b31) & ab12 = ((a11 * b12) + (a12 * b22)) + (a13 * b32) & ab13 = ((a11 * b13) + (a12 * b23)) + (a13 * b33) & ab21 = ((a21 * b11) + (a22 * b21)) + (a23 * b31) & ab22 = ((a21 * b12) + (a22 * b22)) + (a23 * b32) & ab23 = ((a21 * b13) + (a22 * b23)) + (a23 * b33) & ab31 = ((a31 * b11) + (a32 * b21)) + (a33 * b31) & ab32 = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & ab33 = ((a31 * b13) + (a32 * b23)) + (a33 * b33) holds
A * B = <*<*ab11,ab12,ab13*>,<*ab21,ab22,ab23*>,<*ab31,ab32,ab33*>*> by ANPROJ_9:6;

theorem Th11: :: BKMODEL4:20

for N1, N2 being Matrix of 3,F_Real st N1 = <*<*2,0,(- 1)*>,<*0,(sqrt 3),0*>,<*1,0,(- 2)*>*> & N2 = <*<*(2 / 3),0,(- (1 / 3))*>,<*0,(1 / (sqrt 3)),0*>,<*(1 / 3),0,(- (2 / 3))*>*> holds
N1 * N2 = <*<*1,0,0*>,<*0,1,0*>,<*0,0,1*>*>

proof end;

theorem Th12: :: BKMODEL4:21

for N1, N2 being Matrix of 3,F_Real st N2 = <*<*2,0,(- 1)*>,<*0,(sqrt 3),0*>,<*1,0,(- 2)*>*> & N1 = <*<*(2 / 3),0,(- (1 / 3))*>,<*0,(1 / (sqrt 3)),0*>,<*(1 / 3),0,(- (2 / 3))*>*> holds
N1 * N2 = <*<*1,0,0*>,<*0,1,0*>,<*0,0,1*>*>

proof end;

theorem Th13: :: BKMODEL4:22

proof end;

theorem Th14: :: BKMODEL4:23

for N being invertible Matrix of 3,F_Real st N = <*<*(2 / 3),0,(- (1 / 3))*>,<*0,(1 / (sqrt 3)),0*>,<*(1 / 3),0,(- (2 / 3))*>*> holds
(homography N) .: absolute c= absolute

proof end;

theorem :: BKMODEL4:24

for N being invertible Matrix of 3,F_Real st N = <*<*2,0,(- 1)*>,<*0,(sqrt 3),0*>,<*1,0,(- 2)*>*> holds
(homography N) .: absolute = absolute

proof end;

theorem Th15: :: BKMODEL4:25

for a, b, r being Real
for P, Q, R being Element of (TOP-REAL 2) st Q in LSeg (P,R) & P in inside_of_circle (a,b,r) & R in inside_of_circle (a,b,r) holds
Q in inside_of_circle (a,b,r)

proof end;

theorem Th16: :: BKMODEL4:26

for u, v being non zero Element of (TOP-REAL 3) st Dir u = Dir v & u . 3 <> 0 & u . 3 = v . 3 holds
u = v

proof end;

theorem Th17: :: BKMODEL4:27

for R being Element of (ProjectiveSpace (TOP-REAL 3))
for P, Q being Element of BK_model
for u, v, w being non zero Element of (TOP-REAL 3)
for r being Real st 0 <= r & r <= 1 & P = Dir u & Q = Dir v & R = Dir w & u . 3 = 1 & v . 3 = 1 & w = (r * u) + ((1 - r) * v) holds
R is Element of BK_model

proof end;

theorem Th18: :: BKMODEL4:28

for N being invertible Matrix of 3,F_Real
for n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real
for P, Q being Point of (ProjectiveSpace (TOP-REAL 3))
for u, v being non zero Element of (TOP-REAL 3) st N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & Q = Dir v & Q = (homography N) . P & u . 3 = 1 holds
ex a being non zero Real st
( v . 1 = a * (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) & v . 2 = a * (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) & v . 3 = a * (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) )

proof end;

theorem Th19: :: BKMODEL4:29

for N being invertible Matrix of 3,F_Real
for n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real
for P being Element of BK_model
for Q being Point of (ProjectiveSpace (TOP-REAL 3))
for u, v being non zero Element of (TOP-REAL 3) st N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & Q = Dir v & Q = (homography N) . P & u . 3 = 1 & v . 3 = 1 holds
( ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0 & v . 1 = (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) & v . 2 = (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) )

proof end;

theorem Th20: :: BKMODEL4:30

for N being invertible Matrix of 3,F_Real
for h being Element of SubGroupK-isometry
for n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real
for P being Element of BK_model
for u being non zero Element of (TOP-REAL 3) st h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & u . 3 = 1 holds
((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0

proof end;

theorem Th21: :: BKMODEL4:31

for N being invertible Matrix of 3,F_Real
for n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real
for P being Element of absolute
for Q being Point of (ProjectiveSpace (TOP-REAL 3))
for u, v being non zero Element of (TOP-REAL 3) st N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & Q = Dir v & Q = (homography N) . P & u . 3 = 1 & v . 3 = 1 holds
( ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0 & v . 1 = (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) & v . 2 = (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) )

proof end;

theorem Th22: :: BKMODEL4:32

proof end;

theorem Th23: :: BKMODEL4:33

proof end;

theorem Th24: :: BKMODEL4:34

for N being invertible Matrix of 3,F_Real
for h being Element of SubGroupK-isometry
for n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real
for P being Element of absolute
for u being non zero Element of (TOP-REAL 3) st h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & u . 3 = 1 holds
(homography N) . P = Dir |[((((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),((((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),1]|

proof end;

theorem Th26: :: BKMODEL4:35

for A being Subset of (TOP-REAL 3)
for B being non empty convex Subset of (TOP-REAL 2)
for r being Real
for x being Element of (TOP-REAL 3) st A = { x where x is Element of (TOP-REAL 3) : ( |[(x `1),(x `2)]| in B & x `3 = r ) } holds
( not A is empty & A is convex )

proof end;

theorem Th27: :: BKMODEL4:36

for n1, n2, n3 being Element of F_Real
for n, u being Element of (TOP-REAL 3) st n = <*n1,n2,n3*> & u . 3 = 1 holds
|(n,u)| = ((n1 * (u . 1)) + (n2 * (u . 2))) + n3

proof end;

theorem Th28: :: BKMODEL4:37

for A being non empty convex Subset of (TOP-REAL 3)
for n, u, v being Element of (TOP-REAL 3) st ( for w being Element of (TOP-REAL 3) st w in A holds
|(n,w)| <> 0 ) & u in A & v in A holds
0 < |(n,u)| * |(n,v)|

proof end;

theorem Th29: :: BKMODEL4:38

for n31, n32, n33 being Element of F_Real
for u, v being Element of (TOP-REAL 2) st u in inside_of_circle (0,0,1) & v in inside_of_circle (0,0,1) & ( for w being Element of (TOP-REAL 2) st w in inside_of_circle (0,0,1) holds
((n31 * (w . 1)) + (n32 * (w . 2))) + n33 <> 0 ) holds
0 < (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) * (((n31 * (v . 1)) + (n32 * (v . 2))) + n33)

proof end;

theorem Th30: :: BKMODEL4:39

for n31, n32, n33 being Element of F_Real
for u, v being Element of (TOP-REAL 2) st u in inside_of_circle (0,0,1) & v in circle (0,0,1) & ( for w being Element of (TOP-REAL 2) st w in closed_inside_of_circle (0,0,1) holds
((n31 * (w . 1)) + (n32 * (w . 2))) + n33 <> 0 ) holds
0 < (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) * (((n31 * (v . 1)) + (n32 * (v . 2))) + n33)

proof end;

theorem Th34: :: BKMODEL4:40

for l, r being Real
for u, v, w being Element of (TOP-REAL 3)
for n11, n12, n13, n21, n22, n23, n31, n32, n33, nu1, nu2, nu3, nv1, nv2, nv3, nw1, nw2, nw3 being Real st nu3 <> 0 & nv3 <> 0 & nw3 <> 0 & r = (l * nv3) / (((1 - l) * nu3) + (l * nv3)) & ((1 - l) * nu3) + (l * nv3) <> 0 & w = ((1 - l) * u) + (l * v) & nu1 = ((n11 * (u . 1)) + (n12 * (u . 2))) + n13 & nu2 = ((n21 * (u . 1)) + (n22 * (u . 2))) + n23 & nu3 = ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 & nv1 = ((n11 * (v . 1)) + (n12 * (v . 2))) + n13 & nv2 = ((n21 * (v . 1)) + (n22 * (v . 2))) + n23 & nv3 = ((n31 * (v . 1)) + (n32 * (v . 2))) + n33 & nw1 = ((n11 * (w . 1)) + (n12 * (w . 2))) + n13 & nw2 = ((n21 * (w . 1)) + (n22 * (w . 2))) + n23 & nw3 = ((n31 * (w . 1)) + (n32 * (w . 2))) + n33 holds
((1 - r) * |[(nu1 / nu3),(nu2 / nu3),1]|) + (r * |[(nv1 / nv3),(nv2 / nv3),1]|) = |[(nw1 / nw3),(nw2 / nw3),1]|

proof end;

theorem :: BKMODEL4:41

for N being invertible Matrix of 3,F_Real
for h being Element of SubGroupK-isometry
for n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real
for P being Element of BK_model st h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> holds
(homography N) . P = Dir |[((((n11 * ((BK_to_REAL2 P) `1)) + (n12 * ((BK_to_REAL2 P) `2))) + n13) / (((n31 * ((BK_to_REAL2 P) `1)) + (n32 * ((BK_to_REAL2 P) `2))) + n33)),((((n21 * ((BK_to_REAL2 P) `1)) + (n22 * ((BK_to_REAL2 P) `2))) + n23) / (((n31 * ((BK_to_REAL2 P) `1)) + (n32 * ((BK_to_REAL2 P) `2))) + n33)),1]|

proof end;

theorem Th36: :: BKMODEL4:42

for h being Element of SubGroupK-isometry
for N being invertible Matrix of 3,F_Real
for n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real
for u2 being Element of (TOP-REAL 2) st h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & u2 in inside_of_circle (0,0,1) holds
((n31 * (u2 . 1)) + (n32 * (u2 . 2))) + n33 <> 0

proof end;

Lem01: (0 ^2) + (0 ^2) = 0

proof end;

theorem Th37: :: BKMODEL4:43

for r being positive Real
for u being Element of (TOP-REAL 2) st u in circle (0,0,r) holds
not u is zero

proof end;

theorem Th38: :: BKMODEL4:44

for h being Element of SubGroupK-isometry
for N being invertible Matrix of 3,F_Real
for n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real
for u2 being Element of (TOP-REAL 2) st h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & u2 in closed_inside_of_circle (0,0,1) holds
((n31 * (u2 . 1)) + (n32 * (u2 . 2))) + n33 <> 0

proof end;

theorem Th39: :: BKMODEL4:45

for a, b, c, d, e, f, r being Real st ((1 - r) * |[a,b,1]|) + (r * |[c,d,1]|) = |[e,f,1]| holds
((1 - r) * |[a,b]|) + (r * |[c,d]|) = |[e,f]|

proof end;

theorem :: BKMODEL4:46

for P, Q, R, P9, Q9, R9 being POINT of BK-model-Plane
for p, q, r, p9, q9, r9 being Element of BK_model
for h being Element of SubGroupK-isometry
for N being invertible Matrix of 3,F_Real st h = homography N & between P,Q,R & P = p & Q = q & R = r & p9 = (homography N) . p & q9 = (homography N) . q & r9 = (homography N) . r & P9 = p9 & Q9 = q9 & R9 = r9 holds
between P9,Q9,R9

proof end;

definition

let P be Point of (ProjectiveSpace (TOP-REAL 3));

attr P is point_at_infty means :Def04: :: BKMODEL4:def 4
ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u `3 = 0 );

end;

:: deftheorem Def04 defines point_at_infty BKMODEL4:def 4 :

theorem Th40: :: BKMODEL4:47

for P being Point of (ProjectiveSpace (TOP-REAL 3)) st ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u `3 <> 0 ) holds
not P is point_at_infty

proof end;

registration

cluster point_at_infty for Element of the carrier of (ProjectiveSpace (TOP-REAL 3));

existence

proof end;

cluster non point_at_infty for Element of the carrier of (ProjectiveSpace (TOP-REAL 3));

correctness

proof end;

end;

definition

let P be non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3));

func RP3_to_REAL2 P -> Element of REAL 2 means :Def05: :: BKMODEL4:def 5
ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u `3 = 1 & it = |[(u `1),(u `2)]| );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def05 defines RP3_to_REAL2 BKMODEL4:def 5 :

definition

let P be non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3));

func RP3_to_T2 P -> Point of TarskiEuclid2Space equals :: BKMODEL4:def 6
RP3_to_REAL2 P;

coherence

proof end;

end;

:: deftheorem defines RP3_to_T2 BKMODEL4:def 6 :

theorem Th41: :: BKMODEL4:48

for P, Q, R, P9, Q9, R9 being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3))
for h being Element of SubGroupK-isometry
for N being invertible Matrix of 3,F_Real st h = homography N & P in BK_model & Q in BK_model & R in absolute & P9 = (homography N) . P & Q9 = (homography N) . Q & R9 = (homography N) . R & between RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R holds
between RP3_to_T2 P9, RP3_to_T2 Q9, RP3_to_T2 R9

proof end;

theorem Th42: :: BKMODEL4:49

for a, b, c being Real
for u, v, w being Element of (TOP-REAL 3) st a <> 0 & (a + b) + c = 0 & ((a * u) + (b * v)) + (c * w) = 0. (TOP-REAL 3) holds
u in Line (v,w)

proof end;

theorem Th43: :: BKMODEL4:50

for P, Q, R being non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3))
for u, v, w being non zero Element of (TOP-REAL 3) st P = Dir u & Q = Dir v & R = Dir w & u `3 = 1 & v `3 = 1 & w `3 = 1 holds
( P,Q,R are_collinear iff u,v,w are_collinear )

proof end;

theorem Th44: :: BKMODEL4:51

for u, v, w being Element of (TOP-REAL 3) st u in LSeg (v,w) holds
|[(u `1),(u `2)]| in LSeg (|[(v `1),(v `2)]|,|[(w `1),(w `2)]|)

proof end;

theorem Th45: :: BKMODEL4:52

for u, v, w being Element of (TOP-REAL 2) st u in LSeg (v,w) holds
|[(u `1),(u `2),1]| in LSeg (|[(v `1),(v `2),1]|,|[(w `1),(w `2),1]|)

proof end;

theorem Th46: :: BKMODEL4:53

for P, Q, R being non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3)) holds
( P,Q,R are_collinear iff Collinear RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R )

proof end;

theorem :: BKMODEL4:54

for u, v, w being Element of (TOP-REAL 2) st u,v,w are_collinear holds
|[(u `1),(u `2),1]|,|[(v `1),(v `2),1]|,|[(w `1),(w `2),1]| are_collinear

proof end;

theorem Th47: :: BKMODEL4:55

for P, Q, P1 being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st P in BK_model & Q in BK_model & P1 in absolute holds
not between RP3_to_T2 Q, RP3_to_T2 P1, RP3_to_T2 P

proof end;

definition

func Dir001 -> non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) equals :: BKMODEL4:def 7
Dir |[0,0,1]|;

coherence

proof end;

end;

:: deftheorem defines Dir001 BKMODEL4:def 7 :

definition

func Dir101 -> non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) equals :: BKMODEL4:def 8
Dir |[1,0,1]|;

coherence

proof end;

end;

:: deftheorem defines Dir101 BKMODEL4:def 8 :

theorem :: BKMODEL4:56

for P, Q being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st P in absolute & Q in absolute holds
RP3_to_T2 Dir001, RP3_to_T2 P equiv RP3_to_T2 Dir001, RP3_to_T2 Q

proof end;

theorem Th48: :: BKMODEL4:57

for P, Q, R being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3))
for u, v, w being non zero Element of (TOP-REAL 3) st P in absolute & Q in absolute & P <> Q & P = Dir u & Q = Dir v & R = Dir w & u `3 = 1 & v `3 = 1 & w = |[(((u `1) + (v `1)) / 2),(((u `2) + (v `2)) / 2),1]| holds
R in BK_model

proof end;

theorem Th49: :: BKMODEL4:58

for R1, R2 being Point of TarskiEuclid2Space st Tn2TR R1 in circle (0,0,1) & Tn2TR R2 in circle (0,0,1) & R1 <> R2 holds
ex P being Element of BK-model-Plane st between R1, BK_to_T2 P,R2

proof end;

theorem Th50: :: BKMODEL4:59

for P, Q being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st RP3_to_T2 P = RP3_to_T2 Q holds
P = Q

proof end;

theorem Th51: :: BKMODEL4:60

for R1, R2 being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st R1 in absolute & R2 in absolute & R1 <> R2 holds
ex P being Element of BK-model-Plane st between RP3_to_T2 R1, BK_to_T2 P, RP3_to_T2 R2

proof end;

theorem Th52: :: BKMODEL4:61

for P, Q, R being Point of TarskiEuclid2Space st between P,Q,R & Tn2TR P in inside_of_circle (0,0,1) & Tn2TR R in inside_of_circle (0,0,1) holds
Tn2TR Q in inside_of_circle (0,0,1)

proof end;

theorem Th53: :: BKMODEL4:62

for P being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st P in absolute holds
RP3_to_REAL2 P in circle (0,0,1)

proof end;

theorem :: BKMODEL4:63

for P being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st P in BK_model holds
RP3_to_REAL2 P in inside_of_circle (0,0,1)

proof end;

theorem Th54: :: BKMODEL4:64

for P being non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3))
for Q being Element of BK_model st P = Q holds
RP3_to_REAL2 P = BK_to_REAL2 Q

proof end;

theorem Th55: :: BKMODEL4:65

for P, Q, R1, R2 being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st P <> Q & P in BK_model & R1 in absolute & R2 in absolute & between RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R1 & between RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R2 holds
R1 = R2

proof end;

theorem Th56: :: BKMODEL4:66

for P, Q, P1, P2 being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st P <> Q & P in BK_model & Q in BK_model & P1 in absolute & P2 in absolute & P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & not between RP3_to_T2 Q, RP3_to_T2 P, RP3_to_T2 P1 holds
between RP3_to_T2 Q, RP3_to_T2 P, RP3_to_T2 P2

proof end;

theorem Th57: :: BKMODEL4:67

for P, Q being Element of BK_model st P <> Q holds
ex R being Element of absolute st
for p, q, r being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st p = P & q = Q & r = R holds
between RP3_to_T2 q, RP3_to_T2 p, RP3_to_T2 r

proof end;

theorem Th58: :: BKMODEL4:68

proof end;

theorem Th59: :: BKMODEL4:69

Dir |[1,0,1]| is Element of absolute

proof end;

theorem Th60: :: BKMODEL4:70

for a, b being POINT of BK-model-Plane holds a,a equiv b,b

proof end;

theorem Th61: :: BKMODEL4:71

for P being Element of BK_model holds P is non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3))

proof end;

theorem Th62: :: BKMODEL4:72

for P being Element of absolute holds P is non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3))

proof end;

theorem Th63: :: BKMODEL4:73

for P being Element of BK_model
for P9 being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st P = P9 holds
RP3_to_REAL2 P9 = BK_to_REAL2 P

proof end;

theorem Th64: :: BKMODEL4:74

for a, q, b, c being POINT of BK-model-Plane ex x being POINT of BK-model-Plane st
( between q,a,x & a,x equiv b,c )

proof end;

theorem Th65: :: BKMODEL4:75

for P, Q being POINT of BK-model-Plane st BK_to_T2 P = BK_to_T2 Q holds
P = Q

proof end;

theorem :: BKMODEL4:76

for a, b, r being Real
for P, Q, R being Element of (TOP-REAL 2) st P in inside_of_circle (a,b,r) & R in inside_of_circle (a,b,r) holds
LSeg (P,R) c= inside_of_circle (a,b,r) by Th15;

theorem :: BKMODEL4:77

BK-model-Plane is satisfying_SegmentConstruction by Th64;

theorem :: BKMODEL4:78

BK-model-Plane is satisfying_BetweennessIdentity

proof end;

theorem :: BKMODEL4:79

BK-model-Plane is satisfying_Pasch

proof end;