:: Beltrami-Klein model, Part {III}
:: 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 TREES_1, MATRIX_6, 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, GROUP_1, MONOID_0, TARSKI,
XXREAL_0, PASCAL, INCPROJ, ZFMISC_1, SQUARE_1, JGRAPH_6, FINSEQ_1,
FUNCT_3, BKMODEL1, BKMODEL2, BKMODEL3, PBOOLE, BINOP_1, RLTOPSP1,
GTARSKI1;
notations BINOP_1, RELSET_1, ORDINAL1, XCMPLX_0, PRE_TOPC, TARSKI, GROUP_1,
XBOOLE_0, RLVECT_1, COLLSP, EUCLID_5, PASCAL, XXREAL_0, INCPROJ,
DOMAIN_1, INCSP_1, SQUARE_1, XREAL_0, JGRAPH_6, ZFMISC_1, SUBSET_1,
FUNCT_1, FUNCT_2, FINSEQ_1, STRUCT_0, ALGSTR_0, VECTSP_1, EUCLID,
ANPROJ_1, MATRIX_0, MATRIX_6, ANPROJ_8, MATRIX_1, MATRIX_3, QUIN_1,
BKMODEL1, BKMODEL2, RLTOPSP1, GTARSKI1;
constructors REALSET1, RELSET_1, MONOID_0, EUCLID_5, MATRIX13, ANPROJ_8,
PASCAL, SQUARE_1, QUIN_1, BKMODEL2, GTARSKI2;
registrations SUBSET_1, ORDINAL1, XXREAL_0, XBOOLE_0, ANPROJ_1, STRUCT_0,
VECTSP_1, REVROT_1, RELSET_1, XREAL_0, MONOID_0, EUCLID, VALUED_0,
MATRIX_6, ANPROJ_2, ANPROJ_9, SQUARE_1, XCMPLX_0, QUIN_1, TOPREALC;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
begin :: Preliminaries
theorem :: BKMODEL3:1
for x,y being Real st x * y < 0 holds 0 < x / (x - y) < 1;
theorem :: BKMODEL3:2
for a being non zero Real, b, r being Real
st r = sqrt (a^2 + b^2) holds
r is positive & (a / r)^2 + (b / r)^2 = 1;
theorem :: BKMODEL3:3
for a being non zero Real,
b,c,d,e being Real st
a * b = c - d * e holds
b^2 = (c^2/a^2) - 2 * ((c * d) / (a * a)) * e + (d^2 / a^2) * e^2;
theorem :: BKMODEL3:4
for a,b,c being Complex st a <> 0 holds (a^2 * b) * c / a^2 = b * c;
theorem :: BKMODEL3:5
for a,b,c being Complex st a <> 0 holds 2 * (a^2 * b) * c / a^2 = 2 * b * c;
theorem :: BKMODEL3:6
for a being Real st 1 < a holds 1 / a - 1 < 0;
theorem :: BKMODEL3:7
for a,b being Real st 0 < a & 1 < b holds a / b - a < 0;
theorem :: BKMODEL3:8
for a being non zero Real,
b,c,d being Real st
a^2 + c^2 = b^2 & 1 < b^2 holds
not ((b^2)^2 / a^2) - 2 * ((b^2 * c) / (a * a)) * d
+ (c^2 / a^2) * d^2 + d^2 = 1;
theorem :: BKMODEL3:9
for a,b,c being Real st a * (- b) = c & a * c = b holds
c = 0 & b = 0;
theorem :: BKMODEL3:10
for a being positive Real holds (sqrt a) / a = 1 / sqrt a;
registration
let a be non zero Real;
let b,c be Real;
cluster |[a,b,c]| -> non zero for Element of TOP-REAL 3;
cluster |[c,a,b]| -> non zero for Element of TOP-REAL 3;
cluster |[b,c,a]| -> non zero for Element of TOP-REAL 3;
end;
definition
let P be Element of real_projective_plane;
assume
P in absolute \/ BK_model;
func #P -> non zero Element of TOP-REAL 3 means
:: BKMODEL3:def 1
Dir it = P & it.3 = 1;
end;
theorem :: BKMODEL3:11
for P being Element of real_projective_plane holds
ex Q being Element of BK_model st P <> Q;
reserve P for Element of BK_model;
theorem :: BKMODEL3:12
ex P1,P2 being Element of absolute st
P1 <> P2 & P1,P,P2 are_collinear;
theorem :: BKMODEL3:13
for Q being Element of absolute holds
ex R being Element of BK_model st P <> R & P,Q,R are_collinear;
theorem :: BKMODEL3:14
for L being LINE of IncProjSp_of real_projective_plane
st P in L holds ex P1,P2 being Element of absolute st P1 <> P2 &
P1 in L & P2 in L;
definition
let N be invertible Matrix of 3,F_Real;
func line_homography(N) -> Function of
the Lines of IncProjSp_of real_projective_plane,
the Lines of IncProjSp_of real_projective_plane means
:: BKMODEL3:def 2
for x being LINE of IncProjSp_of real_projective_plane holds
it.x = {homography(N).P where
P is POINT of IncProjSp_of real_projective_plane : P on x};
end;
reserve N,N1,N2 for invertible Matrix of 3,F_Real;
reserve l,l1,l2 for Element of the Lines of IncProjSp_of real_projective_plane;
theorem :: BKMODEL3:15
(line_homography(N1)).((line_homography(N2)).l)
= (line_homography(N1 * N2)).l;
theorem :: BKMODEL3:16
(line_homography(1.(F_Real,3))).l = l;
theorem :: BKMODEL3:17
(line_homography(N)).((line_homography(N~)).l) = l &
(line_homography(N~)).((line_homography(N)).l) = l;
theorem :: BKMODEL3:18
(line_homography(N)).l1 = (line_homography(N)).l2 implies l1 = l2;
definition
func EnsLineHomography3 -> set equals
:: BKMODEL3:def 3
the set of all line_homography(N) where N is invertible Matrix of 3,F_Real;
end;
registration
cluster EnsLineHomography3 -> non empty;
end;
definition
let h1,h2 be Element of EnsLineHomography3;
func h1 (*) h2 -> Element of EnsLineHomography3 means
:: BKMODEL3:def 4
ex N1,N2 being invertible Matrix of 3,F_Real st h1 = line_homography(N1) &
h2 = line_homography(N2) & it = line_homography(N1 * N2);
end;
theorem :: BKMODEL3:19
for h1,h2 being Element of EnsLineHomography3 st
h1 = line_homography(N1) & h2 = line_homography(N2) holds
line_homography(N1 * N2) = h1 (*) h2;
theorem :: BKMODEL3:20
for x,y,z being Element of EnsLineHomography3 holds
(x (*) y) (*) z = x (*) (y (*) z);
definition
func BinOpLineHomography3 -> BinOp of EnsLineHomography3 means
:: BKMODEL3:def 5
for h1,h2 being Element of EnsLineHomography3 holds it.(h1,h2) = h1 (*) h2;
end;
definition
func GroupLineHomography3 -> strict multMagma equals
:: BKMODEL3:def 6
multMagma(# EnsLineHomography3, BinOpLineHomography3 #);
end;
registration
cluster GroupLineHomography3 -> non empty associative Group-like;
end;
theorem :: BKMODEL3:21
1_GroupLineHomography3 = line_homography(1.(F_Real,3));
theorem :: BKMODEL3:22
for h,g being Element of GroupLineHomography3
for N,Ng being invertible Matrix of 3,F_Real st
h = line_homography(N) & g = line_homography(Ng) & Ng = N~
holds g = h";
reserve P for Point of ProjectiveSpace TOP-REAL 3,
l for LINE of IncProjSp_of real_projective_plane;
theorem :: BKMODEL3:23
homography(N).P in l implies P in (line_homography(N~)).l;
theorem :: BKMODEL3:24
P in (line_homography(N)).l implies homography(N~).P in l;
theorem :: BKMODEL3:25
P in l iff homography(N).P in (line_homography(N)).l;
theorem :: BKMODEL3:26
for u,v,w being non zero Element of TOP-REAL 3 st
u`3 = 1 & v`1 = - u`2 & v`2 = u`1 & v`3 = 0 &
w`3 = 1 & |{ u,v,w }| = 0 holds
(u`1)^2 + (u`2)^2 - (u`1) * (w`1) - (u`2) * (w`2) = 0;
theorem :: BKMODEL3:27
for a being non zero Real
for b,c being Real holds a * |[b / a,c / a,1]| = |[b,c,a]|;
theorem :: BKMODEL3:28
for u,v,w being non zero Element of TOP-REAL 3 st
u`1 <> 0 & u`3 = 1 & v`1 = - u`2 & v`2 = u`1 & v`3 = 0 &
w`3 = 1 & |{ u,v,w }| = 0 & 1 < (u`1)^2 + (u`2)^2 holds
(w`1)^2 + (w`2)^2 <> 1;
theorem :: BKMODEL3:29
for u,v,w being non zero Element of TOP-REAL 3 st
u`2 <> 0 & u`3 = 1 & v`1 = - u`2 & v`2 = u`1 & v`3 = 0 &
w`3 = 1 & |{ u,v,w }| = 0 & 1 < (u`1)^2 + (u`2)^2 holds
(w`1)^2 + (w`2)^2 <> 1;
theorem :: BKMODEL3:30
for P being Element of absolute holds
ex u being non zero Element of TOP-REAL 3 st u.3 = 1 & P = Dir u;
theorem :: BKMODEL3:31
for a,b,c,d being Real
for u,v being non zero Element of TOP-REAL 3 st u = |[a,b,1]| &
v = |[c,d,0]| holds Dir u <> Dir v;
theorem :: BKMODEL3:32
for u being non zero Element of TOP-REAL 3 st
(u.1)^2 + (u.2)^2 < 1 & u.3 = 1 holds Dir u is Element of BK_model;
theorem :: BKMODEL3:33
for a,b being Real st a^2 + b^2 <= 1 holds
Dir |[a,b,1]| in BK_model \/ absolute;
theorem :: BKMODEL3:34
not P in BK_model \/ absolute implies (ex l st P in l &
l misses absolute);
theorem :: BKMODEL3:35
for P being Point of real_projective_plane
for h being Element of SubGroupK-isometry,
N being invertible Matrix of 3,F_Real st h = homography(N) holds
P is Element of absolute iff homography(N).P is Element of absolute;
theorem :: BKMODEL3:36
for P being Element of BK_model
for h being Element of SubGroupK-isometry,
N being invertible Matrix of 3,F_Real st
h = homography(N) holds homography(N).P is Element of BK_model;
theorem :: BKMODEL3:37
for P 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) holds
ex u being non zero Element of TOP-REAL 3 st homography(N).P = Dir u &
u.3 = 1;
begin :: Beltrami-Klein model
definition
func BK-model-Betweenness -> Relation of
[: BK_model,BK_model:],BK_model means
:: BKMODEL3:def 7
for a,b,c being Element of BK_model holds [[a,b],c] in it iff
BK_to_REAL2 b in LSeg(BK_to_REAL2 a,BK_to_REAL2 c);
end;
definition
func BK-model-Equidistance -> Relation of [: BK_model,BK_model :],
[: BK_model,BK_model :] means
:: BKMODEL3:def 8
for a,b,c,d being Element of BK_model holds [[a,b],[c,d]] in it iff
ex h being Element of SubGroupK-isometry st
ex N being invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).a = c & homography(N).b = d;
end;
definition
func BK-model-Plane -> TarskiGeometryStruct equals
:: BKMODEL3:def 9
TarskiGeometryStruct(# BK_model, BK-model-Betweenness,
BK-model-Equidistance #);
end;
begin :: CongruenceSymmetry
theorem :: BKMODEL3:38
BK-model-Plane is satisfying_CongruenceSymmetry;
begin :: CongruenceEquivalenceRelation
theorem :: BKMODEL3:39
BK-model-Plane is satisfying_CongruenceEquivalenceRelation;
begin :: CongruenceIdentity
theorem :: BKMODEL3:40
BK-model-Plane is satisfying_CongruenceIdentity;