:: by Roland Coghetto

::

:: Received December 30, 2019

:: Copyright (c) 2019-2021 Association of Mizar Users

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 )

( 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))

1 - ((a * c) / (((1 - a) * b) + (a * c))) = ((1 - a) * b) / (((1 - a) * b) + (a * c))

proof end;

definition

let P be POINT of BK-model-Plane;

ex b_{1} being POINT of TarskiEuclid2Space ex p being Element of BK_model st

( P = p & b_{1} = BK_to_REAL2 p )

for b_{1}, b_{2} being POINT of TarskiEuclid2Space st ex p being Element of BK_model st

( P = p & b_{1} = BK_to_REAL2 p ) & ex p being Element of BK_model st

( P = p & b_{2} = BK_to_REAL2 p ) holds

b_{1} = b_{2}
;

end;
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 ex p being Element of BK_model st

( P = p & it = BK_to_REAL2 p );

ex b

( P = p & b

proof end;

uniqueness for b

( P = p & b

( P = p & b

b

:: deftheorem Def01 defines BK_to_T2 BKMODEL4:def 1 :

for P being POINT of BK-model-Plane

for b_{2} being POINT of TarskiEuclid2Space holds

( b_{2} = BK_to_T2 P iff ex p being Element of BK_model st

( P = p & b_{2} = BK_to_REAL2 p ) );

for P being POINT of BK-model-Plane

for b

( b

( P = p & b

definition

let P be POINT of TarskiEuclid2Space;

assume A1: Tn2TR P in inside_of_circle (0,0,1) ;

ex b_{1} being POINT of BK-model-Plane ex u being non zero Element of (TOP-REAL 3) st

( b_{1} = Dir u & u `3 = 1 & Tn2TR P = |[(u `1),(u `2)]| )

for b_{1}, b_{2} being POINT of BK-model-Plane st ex u being non zero Element of (TOP-REAL 3) st

( b_{1} = Dir u & u `3 = 1 & Tn2TR P = |[(u `1),(u `2)]| ) & ex u being non zero Element of (TOP-REAL 3) st

( b_{2} = Dir u & u `3 = 1 & Tn2TR P = |[(u `1),(u `2)]| ) holds

b_{1} = b_{2}

end;
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 ex u being non zero Element of (TOP-REAL 3) st

( it = Dir u & u `3 = 1 & Tn2TR P = |[(u `1),(u `2)]| );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def02 defines T2_to_BK BKMODEL4:def 2 :

for P being POINT of TarskiEuclid2Space st Tn2TR P in inside_of_circle (0,0,1) holds

for b_{2} being POINT of BK-model-Plane holds

( b_{2} = T2_to_BK P iff ex u being non zero Element of (TOP-REAL 3) st

( b_{2} = Dir u & u `3 = 1 & Tn2TR P = |[(u `1),(u `2)]| ) );

for P being POINT of TarskiEuclid2Space st Tn2TR P in inside_of_circle (0,0,1) holds

for b

( b

( b

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

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 )

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 )

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 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

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;

definition

let P, Q, R be Point of BK-model-Plane;

assume that

A1: between P,Q,R and

A2: P <> R ;

ex b_{1} being Real st

( 0 <= b_{1} & b_{1} <= 1 & Tn2TR (BK_to_T2 Q) = ((1 - b_{1}) * (Tn2TR (BK_to_T2 P))) + (b_{1} * (Tn2TR (BK_to_T2 R))) )

for b_{1}, b_{2} being Real st 0 <= b_{1} & b_{1} <= 1 & Tn2TR (BK_to_T2 Q) = ((1 - b_{1}) * (Tn2TR (BK_to_T2 P))) + (b_{1} * (Tn2TR (BK_to_T2 R))) & 0 <= b_{2} & b_{2} <= 1 & Tn2TR (BK_to_T2 Q) = ((1 - b_{2}) * (Tn2TR (BK_to_T2 P))) + (b_{2} * (Tn2TR (BK_to_T2 R))) holds

b_{1} = b_{2}
by A2, Th07, Th08;

end;
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 ( 0 <= it & it <= 1 & Tn2TR (BK_to_T2 Q) = ((1 - it) * (Tn2TR (BK_to_T2 P))) + (it * (Tn2TR (BK_to_T2 R))) );

ex b

( 0 <= b

proof end;

uniqueness for b

b

:: deftheorem Def03 defines length BKMODEL4:def 3 :

for P, Q, R being Point of BK-model-Plane st between P,Q,R & P <> R holds

for b_{4} being Real holds

( b_{4} = length (P,Q,R) iff ( 0 <= b_{4} & b_{4} <= 1 & Tn2TR (BK_to_T2 Q) = ((1 - b_{4}) * (Tn2TR (BK_to_T2 P))) + (b_{4} * (Tn2TR (BK_to_T2 R))) ) );

for P, Q, R being Point of BK-model-Plane st between P,Q,R & P <> R holds

for b

( b

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 )

( 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;

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*>*>

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*>*>

N1 * N2 = <*<*1,0,0*>,<*0,1,0*>,<*0,0,1*>*>

proof end;

theorem Th13: :: BKMODEL4:22

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 is_reverse_of N2

N1 is_reverse_of N2

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

(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

(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)

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

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

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) )

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) )

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

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) )

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

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

((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0

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

((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0

proof end;

theorem Th23: :: BKMODEL4:33

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

(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]|

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

(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 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]|

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 )

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

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)|

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)

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)

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]|

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]|

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

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

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

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]|

((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

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;

:: deftheorem Def04 defines point_at_infty BKMODEL4:def 4 :

for P being Point of (ProjectiveSpace (TOP-REAL 3)) holds

( P is point_at_infty iff ex u being non zero Element of (TOP-REAL 3) st

( P = Dir u & u `3 = 0 ) );

for P being Point of (ProjectiveSpace (TOP-REAL 3)) holds

( P is point_at_infty iff ex u being non zero Element of (TOP-REAL 3) st

( P = Dir u & u `3 = 0 ) );

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

( P = Dir u & u `3 <> 0 ) holds

not P is point_at_infty

proof end;

registration

existence

ex b_{1} being Point of (ProjectiveSpace (TOP-REAL 3)) st b_{1} is point_at_infty

existence

not for b_{1} being Point of (ProjectiveSpace (TOP-REAL 3)) holds b_{1} is point_at_infty ;

end;
ex b

proof end;

correctness existence

not for b

proof end;

definition

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

ex b_{1} being Element of REAL 2 ex u being non zero Element of (TOP-REAL 3) st

( P = Dir u & u `3 = 1 & b_{1} = |[(u `1),(u `2)]| )

for b_{1}, b_{2} being Element of REAL 2 st ex u being non zero Element of (TOP-REAL 3) st

( P = Dir u & u `3 = 1 & b_{1} = |[(u `1),(u `2)]| ) & ex u being non zero Element of (TOP-REAL 3) st

( P = Dir u & u `3 = 1 & b_{2} = |[(u `1),(u `2)]| ) holds

b_{1} = b_{2}

end;
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 ex u being non zero Element of (TOP-REAL 3) st

( P = Dir u & u `3 = 1 & it = |[(u `1),(u `2)]| );

ex b

( P = Dir u & u `3 = 1 & b

proof end;

uniqueness for b

( P = Dir u & u `3 = 1 & b

( P = Dir u & u `3 = 1 & b

b

proof end;

:: deftheorem Def05 defines RP3_to_REAL2 BKMODEL4:def 5 :

for P being non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3))

for b_{2} being Element of REAL 2 holds

( b_{2} = RP3_to_REAL2 P iff ex u being non zero Element of (TOP-REAL 3) st

( P = Dir u & u `3 = 1 & b_{2} = |[(u `1),(u `2)]| ) );

for P being non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3))

for b

( b

( P = Dir u & u `3 = 1 & b

definition

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

coherence

RP3_to_REAL2 P is Point of TarskiEuclid2Space

end;
coherence

RP3_to_REAL2 P is Point of TarskiEuclid2Space

proof end;

:: deftheorem defines RP3_to_T2 BKMODEL4:def 6 :

for P being non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3)) holds RP3_to_T2 P = RP3_to_REAL2 P;

for P being non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3)) holds RP3_to_T2 P = RP3_to_REAL2 P;

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

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)

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 )

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)]|)

|[(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]|)

|[(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 )

( 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

|[(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

not between RP3_to_T2 Q, RP3_to_T2 P1, RP3_to_T2 P

proof end;

definition

Dir |[0,0,1]| is non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3))
end;

func Dir001 -> non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) equals :: BKMODEL4:def 7

Dir |[0,0,1]|;

coherence Dir |[0,0,1]|;

Dir |[0,0,1]| is non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3))

proof end;

definition

Dir |[1,0,1]| is non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3))
end;

func Dir101 -> non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) equals :: BKMODEL4:def 8

Dir |[1,0,1]|;

coherence Dir |[1,0,1]|;

Dir |[1,0,1]| is non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3))

proof end;

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

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

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

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

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

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)

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)

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)

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

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

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

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

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

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 p, RP3_to_T2 q, RP3_to_T2 r

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 p, RP3_to_T2 q, RP3_to_T2 r

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

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 )

( between q,a,x & a,x equiv b,c )

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;

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;