:: Beltrami-Klein model, Part {IV}
:: by Roland Coghetto
::
:: Received December 30, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NAT_1, MATRIX_6, FINSEQ_2, COMPLEX1, REAL_1, XCMPLX_0, ANPROJ_1,
PENCIL_1, MCART_1, EUCLID_5, ALGSTR_0, ARYTM_1, ARYTM_3, CARD_1, EUCLID,
FUNCT_1, INCSP_1, MATRIX_1, NUMBERS, PRE_TOPC, RELAT_1, STRUCT_0,
SUBSET_1, SUPINF_2, VECTSP_1, XBOOLE_0, MESFUNC1, ANPROJ_8, ANPROJ_9,
TARSKI, XXREAL_0, PASCAL, SQUARE_1, JGRAPH_6, RVSUM_1, FINSEQ_1,
MATRIX_3, BKMODEL1, BKMODEL2, BKMODEL3, RLTOPSP1, GTARSKI1, GTARSKI2,
METRIC_1, EUCLID12, CONVEX1, XXREAL_1, ALGSTR_4, BKMODEL4;
notations RELSET_1, ORDINAL1, XCMPLX_0, PRE_TOPC, RVSUM_1, TARSKI, XBOOLE_0,
RLVECT_1, COLLSP, EUCLID_5, PASCAL, XXREAL_0, ANPROJ_9, SQUARE_1,
XREAL_0, JGRAPH_6, SUBSET_1, NUMBERS, FUNCT_1, FUNCT_2, FINSEQ_1,
STRUCT_0, ALGSTR_0, VECTSP_1, FINSEQ_2, EUCLID, ANPROJ_1, MATRIX_6,
LAPLACE, ANPROJ_8, MATRIX_1, MATRIX_3, BKMODEL1, BKMODEL2, RLTOPSP1,
GTARSKI1, METRIC_1, EUCLID12, XXREAL_1, GTARSKI2, BKMODEL3;
constructors REALSET1, FINSEQ_4, LAPLACE, MATRPROB, RELSET_1, MONOID_0,
EUCLID_5, MATRIX13, ANPROJ_8, PASCAL, SQUARE_1, BINOP_2, GTARSKI2,
EUCLID12, CONVEX1, XXREAL_1, BKMODEL3;
registrations MEMBERED, ORDINAL1, XXREAL_0, XBOOLE_0, ANPROJ_1, STRUCT_0,
VECTSP_1, REVROT_1, RELSET_1, XREAL_0, MONOID_0, EUCLID, VALUED_0,
MATRIX_6, SQUARE_1, XCMPLX_0, NUMBERS, TOPREAL9, TOPREALC, GTARSKI2,
RLTOPSP1, CONVEX1, BKMODEL3;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
begin :: Preliminaries
theorem :: BKMODEL4:1
for a,b being Real st a <> b holds 1 - (a / (a - b)) = - b / (a - b);
theorem :: BKMODEL4:2
for a,b being Real st 0 < a * b holds 0 < a / b;
theorem :: BKMODEL4:3
for a,b,c being Real st 0 <= a <= 1 & 0 < b * c holds
0 <= (a * c) / ((1 - a) * b + a * c) <= 1;
theorem :: 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);
theorem :: BKMODEL4:5
for a,b,c,d being Real st b <> 0 holds
a * b / c * d / b = a * d / c;
theorem :: BKMODEL4:6
for u being Element of TOP-REAL 3 holds u = |[u.1,u.2,u.3]|;
theorem :: BKMODEL4:7
for P being Element of BK_model holds BK_to_REAL2 P in TarskiEuclid2Space;
definition
let P be POINT of BK-model-Plane;
func BK_to_T2 P -> POINT of TarskiEuclid2Space means
:: BKMODEL4:def 1
ex p be Element of BK_model st P = p &
it = BK_to_REAL2 p;
end;
definition
let P be POINT of TarskiEuclid2Space;
assume
Tn2TR P in inside_of_circle(0,0,1);
func T2_to_BK P -> POINT of BK-model-Plane means
:: BKMODEL4:def 2
ex u be non zero Element of TOP-REAL 3 st
it = Dir u & u`3 = 1 & Tn2TR P = |[u`1,u`2]|;
end;
theorem :: BKMODEL4:8
for P being POINT of BK-model-Plane holds
Tn2TR BK_to_T2 P in inside_of_circle(0,0,1);
theorem :: BKMODEL4:9
for P being POINT of BK-model-Plane holds T2_to_BK BK_to_T2 P = P;
theorem :: 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;
theorem :: 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;
theorem :: 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;
theorem :: BKMODEL4:13
for P,Q being Element of TOP-REAL 2 st P <> Q holds
P.1 <> Q.1 or P.2 <> Q.2;
theorem :: 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;
theorem :: 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;
definition
let P,Q,R be Point of BK-model-Plane;
assume that
between P,Q,R and
P <> R;
func length(P,Q,R) -> Real means
:: BKMODEL4:def 3
0 <= it <= 1 &
Tn2TR BK_to_T2 Q = (1 - it) * Tn2TR BK_to_T2 P + it * Tn2TR BK_to_T2 R;
end;
theorem :: BKMODEL4:16
for P,Q being Point of BK-model-Plane holds
between P,P,Q & between P,Q,Q;
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;
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;
theorem :: 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 *> *>;
theorem :: 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 *> *>;
theorem :: 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 *> *>;
theorem :: 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;
theorem :: 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;
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;
theorem :: 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);
theorem :: 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;
theorem :: 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 <= 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;
theorem :: 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);
theorem :: 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);
theorem :: 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;
theorem :: 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);
theorem :: 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;
theorem :: 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 ]|;
theorem :: 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 ]|;
theorem :: BKMODEL4:35
for A being Subset of TOP-REAL 3
for B being convex non empty 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 A is non empty convex;
theorem :: 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;
theorem :: BKMODEL4:37
for A being convex non empty 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 )|;
theorem :: 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);
theorem :: 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 be 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);
theorem :: 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]|;
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 ]|;
theorem :: 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;
theorem :: BKMODEL4:43
for r being positive Real
for u being Element of TOP-REAL 2 st u in circle(0,0,r)
holds u is non zero;
theorem :: 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
;
theorem :: 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]|;
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;
definition
let P be Point of ProjectiveSpace TOP-REAL 3;
attr P is point_at_infty means
:: BKMODEL4:def 4
ex u being non zero Element of TOP-REAL 3 st
P = Dir u & u`3 = 0;
end;
theorem :: 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 P is non point_at_infty;
registration
cluster point_at_infty for Point of ProjectiveSpace TOP-REAL 3;
cluster non point_at_infty for Point of ProjectiveSpace TOP-REAL 3;
end;
definition
let P being non point_at_infty Point of ProjectiveSpace TOP-REAL 3;
func RP3_to_REAL2 P -> Element of REAL 2 means
:: 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]|;
end;
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;
end;
theorem :: 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;
theorem :: 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);
theorem :: 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;
theorem :: 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]| );
theorem :: 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]|);
theorem :: 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;
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;
theorem :: 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 :::& P,Q,P1 are_collinear
holds
not between RP3_to_T2 Q,RP3_to_T2 P1,RP3_to_T2 P;
definition
func Dir001 -> non point_at_infty Element of
ProjectiveSpace TOP-REAL 3 equals
:: BKMODEL4:def 7
Dir |[0,0,1]|;
end;
definition
func Dir101 -> non point_at_infty Element of
ProjectiveSpace TOP-REAL 3 equals
:: BKMODEL4:def 8
Dir |[1,0,1]|;
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;
theorem :: 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;
theorem :: 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;
theorem :: 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;
theorem :: 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;
theorem :: 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);
theorem :: 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);
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);
theorem :: 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
;
theorem :: 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;
theorem :: 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
holds between RP3_to_T2 Q,RP3_to_T2 P,RP3_to_T2 P1 or
between RP3_to_T2 Q,RP3_to_T2 P,RP3_to_T2 P2;
theorem :: 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);
theorem :: 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);
theorem :: BKMODEL4:69
Dir |[1,0,1]| is Element of absolute;
theorem :: BKMODEL4:70
for a,b being POINT of BK-model-Plane holds a,a equiv b,b;
theorem :: BKMODEL4:71
for P being Element of BK_model holds
P is non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
theorem :: BKMODEL4:72
for P being Element of absolute holds
P is non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
theorem :: 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;
theorem :: BKMODEL4:74
for a, q, b, c being POINT of BK-model-Plane holds
ex x being POINT of BK-model-Plane st between q,a,x & a,x equiv b,c;
theorem :: BKMODEL4:75
for P,Q being POINT of BK-model-Plane st BK_to_T2 P = BK_to_T2 Q holds P = Q;
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);
begin :: SegmentConstruction
theorem :: BKMODEL4:77
BK-model-Plane is satisfying_SegmentConstruction;
begin :: BetweennessIdentity
theorem :: BKMODEL4:78
BK-model-Plane is satisfying_BetweennessIdentity;
begin :: Pasch
theorem :: BKMODEL4:79
BK-model-Plane is satisfying_Pasch;