:: Beltrami-Klein model, Part {II}
:: by Roland Coghetto
::
:: Received March 27, 2018
:: Copyright (c) 2018-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 FVSUM_1, NAT_1, TREES_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, GROUP_1, MONOID_0, ANPROJ_9, TARSKI, XXREAL_0, PASCAL, INCPROJ,
ZFMISC_1, GROUP_2, SQUARE_1, JGRAPH_6, PROB_1, RVSUM_1, FINSEQ_1,
QC_LANG1, RELAT_2, MATRIXR1, MATRIXC1, MATRIX_3, FUNCT_3, CARD_3,
BKMODEL1, BKMODEL2, COLLSP;
notations FVSUM_1, RELSET_1, ORDINAL1, XCMPLX_0, PRE_TOPC, RVSUM_1, TARSKI,
GROUP_1, XBOOLE_0, RLVECT_1, COLLSP, EUCLID_5, PASCAL, XXREAL_0, INCPROJ,
DOMAIN_1, INCSP_1, ANPROJ_9, SQUARE_1, XREAL_0, JGRAPH_6, TOPREAL9,
ZFMISC_1, SUBSET_1, NUMBERS, FUNCT_1, FUNCT_2, FINSEQ_1, STRUCT_0,
ALGSTR_0, VECTSP_1, FINSEQ_2, EUCLID, ANPROJ_1, MATRIX_0, MATRIX_6,
LAPLACE, ANPROJ_8, GROUP_2, MATRIX_1, MATRIX_3, MATRIXR1, MATRIXR2,
MATRPROB, QUIN_1, BKMODEL1;
constructors REALSET1, MATRIXR2, FINSEQ_4, FVSUM_1, LAPLACE, MATRPROB,
GROUP_5, RELSET_1, MONOID_0, EUCLID_5, MATRIX13, ANPROJ_8, PASCAL,
INCPROJ, ANPROJ_9, SQUARE_1, TOPREAL9, BINOP_2, QUIN_1, BKMODEL1;
registrations SUBSET_1, RVSUM_1, FUNCT_1, MEMBERED, FINSEQ_1, ORDINAL1,
XXREAL_0, GROUP_2, 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, NUMBERS, MATRIX_0, TOPREAL9, QUIN_1;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
begin :: Beltrami-Cayley-Klein disk model
definition
func BK_model -> non empty Subset of ProjectiveSpace TOP-REAL 3 equals
:: BKMODEL2:def 1
negative_conic(1,1,-1,0,0,0);
end;
theorem :: BKMODEL2:1
BK_model misses absolute;
theorem :: BKMODEL2:2
for P being Element of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3 st
P = Dir u & P in BK_model holds u.3 <> 0;
definition
let P being Element of BK_model;
func BK_to_REAL2 P -> Element of inside_of_circle(0,0,1) means
:: BKMODEL2:def 2
ex u being non zero Element of TOP-REAL 3 st
Dir u = P & u.3 = 1 & it = |[u.1,u.2]|;
end;
definition
let Q being Element of inside_of_circle(0,0,1);
func REAL2_to_BK Q -> Element of BK_model means
:: BKMODEL2:def 3
ex P being Element of TOP-REAL 2 st P = Q & it = Dir |[P`1,P`2,1]|;
end;
theorem :: BKMODEL2:3
for P being Element of BK_model holds REAL2_to_BK BK_to_REAL2 P = P;
theorem :: BKMODEL2:4
for P,Q being Element of BK_model holds P = Q iff
BK_to_REAL2 P = BK_to_REAL2 Q;
theorem :: BKMODEL2:5
for Q being Element of inside_of_circle(0,0,1) holds
BK_to_REAL2 REAL2_to_BK Q = Q;
theorem :: BKMODEL2:6
for P,Q being Element of BK_model for P1,P2,P3 being Element of absolute st
P <> Q & P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear &
P,Q,P3 are_collinear holds P3 = P1 or P3 = P2;
theorem :: BKMODEL2:7
for P being Element of BK_model
for Q being Element of ProjectiveSpace TOP-REAL 3
for v being non zero Element of TOP-REAL 3 st P <> Q & Q = Dir v &
v.3 = 1 holds
ex P1 being Element of absolute st P,Q,P1 are_collinear;
theorem :: BKMODEL2:8
for P being Element of BK_model
for L being LINE of IncProjSp_of real_projective_plane
holds ex Q being Element of ProjectiveSpace TOP-REAL 3 st P <> Q & Q in L;
theorem :: BKMODEL2:9
for a,b,c,d,e being Real
for u,v,w being Element of TOP-REAL 3 st
u = |[a,b,e]| & v = |[c,d,0]| & w = |[ a + c, b + d, e ]| holds
|{u,v,w}| = 0;
theorem :: BKMODEL2:10
for a,b being Real for c being non zero Real holds
|[a,b,c]| is non zero Element of TOP-REAL 3;
theorem :: BKMODEL2:11
for u,v being Element of TOP-REAL 3 for a,b,c,d,e being Real st
u = |[a,b,c]| & v = |[d,e,0]| & are_Prop u,v holds c = 0;
theorem :: BKMODEL2:12
for P,Q,R being Element 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 <> 0 & v`3 = 0 &
w = |[u`1 + v`1,u`2 + v`2, u`3]| holds R <> P & R <> Q;
theorem :: BKMODEL2:13
for L being LINE of IncProjSp_of real_projective_plane
for P,Q being Element of ProjectiveSpace TOP-REAL 3 st
P <> Q & P in L & Q in L holds L = Line(P,Q);
theorem :: BKMODEL2:14
for L being LINE of IncProjSp_of real_projective_plane
for P,Q being Element of ProjectiveSpace TOP-REAL 3
for u,v being non zero Element of TOP-REAL 3 st
P in L & Q in L &
P = Dir u & Q = Dir v & u`3 <> 0 & v`3 = 0 holds
P <> Q &
Dir |[u`1 + v`1, u`2 + v`2, u`3]| in L;
theorem :: BKMODEL2:15
for u,v,w being Element of TOP-REAL 3 st v`3 = 0 &
w = |[u`1 + v`1,u`2 + v`2, u`3]| holds |{u,v,w}| = 0;
theorem :: BKMODEL2:16
for L being LINE of IncProjSp_of real_projective_plane
for P being Element of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3
st P = Dir u & P in L & u.3 <> 0 holds
ex Q being Element of ProjectiveSpace TOP-REAL 3 st
(ex v being non zero Element of TOP-REAL 3 st
Q = Dir v & Q in L & P <> Q & v.3 <> 0);
theorem :: BKMODEL2:17
for P being Element of BK_model
for L being LINE of IncProjSp_of real_projective_plane st P in L
holds ex Q being Element of ProjectiveSpace TOP-REAL 3 st
P <> Q & Q in L &
for u being non zero Element of TOP-REAL 3 st Q = Dir u holds u.3 <> 0;
theorem :: BKMODEL2:18
for u,v being non zero Element of TOP-REAL 3
for k being non zero Real st u = k * v holds
Dir u = Dir v;
theorem :: BKMODEL2:19
for P being Element of BK_model
for Q being Element of ProjectiveSpace TOP-REAL 3
st P <> Q holds ex P1 being Element of absolute st
P,Q,P1 are_collinear;
theorem :: BKMODEL2:20
for P,Q being Element of BK_model st P <> Q holds
ex P1,P2 being Element of absolute st P1 <> P2 &
P,Q,P1 are_collinear & P,Q,P2 are_collinear;
theorem :: BKMODEL2:21
for P,Q,R being Element of real_projective_plane
for u,v,w being non zero Element of TOP-REAL 3
for a,b,c,d being Real st P in BK_model &
Q in absolute & P = Dir u & Q = Dir v & R = Dir w &
u = |[a,b,1]| & v = |[c,d,1]| & w = |[ (a + c) / 2,(b + d) / 2,1 ]| holds
R in BK_model & R <> P & P,R,Q are_collinear;
theorem :: BKMODEL2:22
for P,Q being Element of real_projective_plane
st P in absolute & Q in BK_model
holds
ex R being Element of real_projective_plane st R in BK_model &
Q <> R & R,Q,P are_collinear;
theorem :: BKMODEL2:23
for L being LINE of IncProjSp_of real_projective_plane
for p ,q being POINT of IncProjSp_of real_projective_plane
for P,Q being Element of real_projective_plane st
p = P & q = Q &
P in BK_model & Q in absolute &
q on L & p on L holds
ex p1,p2 being POINT of IncProjSp_of real_projective_plane,
P1,P2 being Element of real_projective_plane st
p1 = P1 & p2 = P2 & P1 <> P2 &
P1 in absolute & P2 in absolute &
p1 on L & p2 on L;
theorem :: BKMODEL2:24
for P being Element of BK_model
for Q being Element of absolute holds
ex R being Element of absolute st Q <> R & Q,P,R are_collinear;
theorem :: BKMODEL2:25
for P being Element of BK_model
for u being non zero Element of TOP-REAL 3 st
P = Dir u & u.3 = 1 holds (u.1)^2 + (u.2)^2 < 1;
theorem :: BKMODEL2:26
for P1,P2 being Element of absolute
for Q being Element of BK_model
for u,v,w being non zero Element of TOP-REAL 3 st
Dir u = P1 & Dir v = P2 & Dir w = Q &
u.3 = 1 & v.3 = 1 & w.3 = 1 & v.1 = - u.1 & v.2 = - u.2 &
P1,Q,P2 are_collinear holds
ex a being Real st -1 < a < 1 & w.1 = a * u.1 & w.2 = a * u.2;
begin :: Tangent
definition
let P being Element of absolute;
func pole_infty P -> Element of real_projective_plane means
:: BKMODEL2:def 4
ex u being non zero Element of TOP-REAL 3 st P = Dir u & u.3 = 1 &
(u.1)^2 + (u.2)^2 = 1 & it = Dir |[- u.2,u.1,0]|;
end;
theorem :: BKMODEL2:27
for P being Element of absolute holds P <> pole_infty P;
theorem :: BKMODEL2:28
for P1,P2 being Element of absolute st pole_infty P1 = pole_infty P2
holds P1 = P2 or (ex u being non zero Element of TOP-REAL 3 st
P1 = Dir u & P2 = Dir |[-u`1,-u`2,1]| & u`3 = 1);
definition
let P being Element of absolute;
func tangent P -> LINE of real_projective_plane means
:: BKMODEL2:def 5
ex p being Element of real_projective_plane st p = P &
it = Line(p,pole_infty P);
end;
theorem :: BKMODEL2:29
for P being Element of absolute holds P in tangent P;
theorem :: BKMODEL2:30
for P being Element of absolute holds tangent P /\ absolute = {P};
theorem :: BKMODEL2:31
for P1,P2 being Element of absolute st tangent P1 = tangent P2 holds P1 = P2;
theorem :: BKMODEL2:32
for P,Q being Element of absolute holds
ex R being Element of real_projective_plane st
R in tangent P & R in tangent Q;
theorem :: BKMODEL2:33
for P1,P2 being Element of absolute st P1 <> P2 holds
ex P being Element of real_projective_plane st tangent P1 /\ tangent P2 = {P}
;
theorem :: BKMODEL2:34
for M being Matrix of 3,REAL
for P being Element of absolute
for Q being Element of real_projective_plane
for u,v being non zero Element of TOP-REAL 3
for fp,fq being FinSequence of REAL st
M = symmetric_3(1,1,-1,0,0,0) &
P = Dir u & Q = Dir v &
u = fp & v = fq &
Q in tangent P holds SumAll QuadraticForm(fq,M,fp) = 0;
theorem :: BKMODEL2:35
for P,Q,R being Element of absolute for P1,P2,P3,P4 being
Point of real_projective_plane st P,Q,R are_mutually_distinct &
P1 = P & P2 = Q & P3 = R & P4 in tangent P & P4 in tangent Q holds
not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear &
not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear;
theorem :: BKMODEL2:36
for P,Q being Element of absolute
for R being Element 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 & R in tangent P & R in tangent Q & u.3 = 1 & v.3 = 1 &
w.3 = 0 holds P = Q or (u.1 = -v.1 & u.2 = -v.2);
theorem :: BKMODEL2:37
for P being Element of absolute
for R being Element of real_projective_plane
for u being non zero Element of TOP-REAL 3 st
R in tangent P & R = Dir u & u.3 = 0 holds R = pole_infty P;
theorem :: BKMODEL2:38
for a being non zero Real
for N being invertible Matrix of 3,F_Real st N = symmetric_3(a,a,-a,0,0,0)
holds homography(N).:absolute = absolute;
theorem :: BKMODEL2:39
for ra being non zero Element of F_Real
for M,O being invertible Matrix of 3,F_Real st
O = symmetric_3(1,1,-1,0,0,0) & M = ra * O holds
homography(M).:absolute = absolute;
theorem :: BKMODEL2:40
for P being Element of absolute holds tangent P misses BK_model;
theorem :: BKMODEL2:41
for P,PP1,PP2 being Element of real_projective_plane
for P1,P2 being Element of absolute
for Q being Element of real_projective_plane st
P1 <> P2 & PP1 = P1 & PP2 = P2 &
P in BK_model & P,PP1,PP2 are_collinear &
Q in tangent P1 & Q in tangent P2 holds
ex R being Element of real_projective_plane st R in absolute &
P,Q,R are_collinear;
theorem :: BKMODEL2:42
for P,R,S being Element of real_projective_plane
for Q being Element of absolute st P in BK_model & R in tangent Q &
P,S,R are_collinear & R <> S holds Q <> S;
begin :: Sub-Group of K-isometry
definition
let h being Element of EnsHomography3;
pred h is_K-isometry means
:: BKMODEL2:def 6
ex N being invertible Matrix of 3,F_Real st
h = homography(N) & (homography(N)).:absolute = absolute;
end;
theorem :: BKMODEL2:43
for h being Element of EnsHomography3 st h = homography(1.(F_Real,3)) holds
h is_K-isometry;
definition
func EnsK-isometry -> non empty Subset of EnsHomography3 equals
:: BKMODEL2:def 7
{h where h is Element of EnsHomography3: h is_K-isometry};
end;
definition
func SubGroupK-isometry -> strict Subgroup of GroupHomography3 means
:: BKMODEL2:def 8
the carrier of it = EnsK-isometry;
end;
theorem :: BKMODEL2:44
for h being Element of EnsK-isometry
for N being invertible Matrix of 3,F_Real st
h = homography(N) holds homography(N).:absolute = absolute;
theorem :: BKMODEL2:45
homography(1.(F_Real,3)) = 1_GroupHomography3 &
homography(1.(F_Real,3)) = 1_SubGroupK-isometry;
theorem :: BKMODEL2:46
for N1,N2 being invertible Matrix of 3,F_Real
for h1,h2 being Element of SubGroupK-isometry st
h1 = homography(N1) & h2 = homography(N2) holds
h1 * h2 is Element of SubGroupK-isometry &
h1 * h2 = homography(N1 * N2);
theorem :: BKMODEL2:47
for N being invertible Matrix of 3,F_Real
for h being Element of SubGroupK-isometry st
h = homography(N) holds h" = homography(N~) &
homography(N~) is Element of SubGroupK-isometry;
theorem :: BKMODEL2:48
for s being Element of ProjectiveSpace TOP-REAL 3
for p,q,r being Element of absolute st p,q,r are_mutually_distinct &
s in tangent p /\ tangent q holds
ex N being invertible Matrix of 3,F_Real st
homography(N).:absolute = absolute &
(homography(N)).Dir101 = p &
(homography(N)).Dirm101 = q &
(homography(N)).Dir011 = r &
(homography(N)).Dir010 = s;
theorem :: BKMODEL2:49
for p1,q1,r1,p2,q2,r2 being Element of absolute
for s1,s2 being Element of real_projective_plane st
p1,q1,r1 are_mutually_distinct &
p2,q2,r2 are_mutually_distinct &
s1 in tangent p1 /\ tangent q1 &
s2 in tangent p2 /\ tangent q2
holds ex N being invertible Matrix of 3,F_Real st
homography(N).:absolute = absolute &
(homography(N)).p1 = p2 & (homography(N)).q1 = q2 &
(homography(N)).r1 = r2 & (homography(N)).s1 = s2;
theorem :: BKMODEL2:50
for p1,q1,r1,p2,q2,r2 being Element of absolute st
p1,q1,r1 are_mutually_distinct &
p2,q2,r2 are_mutually_distinct
holds ex N being invertible Matrix of 3,F_Real st
homography(N).:absolute = absolute &
(homography(N)).p1 = p2 & (homography(N)).q1 = q2 &
(homography(N)).r1 = r2;
theorem :: BKMODEL2:51
for CLSP being CollSp
for p,q,r,s being Element of CLSP st
Line(p,q) = Line(r,s) holds r,s,p are_collinear;
theorem :: BKMODEL2:52
for CLSP being CollSp
for p,q being Element of CLSP holds Line(p,q) = Line(q,p);
theorem :: BKMODEL2:53
for N being invertible Matrix of 3,F_Real
for p,q,r,s being Element of ProjectiveSpace TOP-REAL 3 st
Line(homography(N).p,homography(N).q) = Line(homography(N).r,homography(N).s)
holds p,q,r are_collinear & p,q,s are_collinear &
r,s,p are_collinear & r,s,q are_collinear;
theorem :: BKMODEL2:54
for N being invertible Matrix of 3,F_Real
for p,q,r,s,t,u,np,nq,nr,ns being Element of real_projective_plane st
p <> q & r <> s & np <> nq & nr <> ns &
p,q,t are_collinear & r,s,t are_collinear &
np = homography(N).p & nq = homography(N).q &
nr = homography(N).r & ns = homography(N).s &
np,nq,u are_collinear & nr,ns,u are_collinear holds
u = homography(N).t or Line(np,nq) = Line(nr,ns);
theorem :: BKMODEL2:55
for N being invertible Matrix of 3,F_Real
for p,q,r,s,t,u,np,nq,nr,ns being Element of real_projective_plane st
p <> q & r <> s & np <> nq & nr <> ns &
p,q,t are_collinear & r,s,t are_collinear &
np = homography(N).p & nq = homography(N).q &
nr = homography(N).r & ns = homography(N).s &
np,nq,u are_collinear & nr,ns,u are_collinear &
not p,q,r are_collinear holds u = homography(N).t;
theorem :: BKMODEL2:56
for p,q being Element of absolute
for a,b being Element of BK_model
holds ex N being invertible Matrix of 3,F_Real st
homography(N).:absolute = absolute &
(homography(N)).a = b & (homography(N)).p = q;
theorem :: BKMODEL2:57
for p,q,r,s being Element of absolute st
p,q,r are_mutually_distinct & q,p,s are_mutually_distinct
holds ex N being invertible Matrix of 3,F_Real st
homography(N).:absolute = absolute &
(homography(N)).p = q & (homography(N)).q = p &
(homography(N)).r = s &
(for t being Element of real_projective_plane st
t in tangent p /\ tangent q holds (homography(N)).t = t);
theorem :: BKMODEL2:58
for P,Q being Element of BK_model st P <> Q holds
ex P1,P2,P3,P4 being Element of absolute,
P5 being Element of ProjectiveSpace TOP-REAL 3 st
P1 <> P2 &
P,Q,P1 are_collinear & P,Q,P2 are_collinear &
P,P5,P3 are_collinear & Q,P5,P4 are_collinear &
P1,P2,P3 are_mutually_distinct &
P1,P2,P4 are_mutually_distinct &
P5 in tangent P1 /\ tangent P2;
theorem :: BKMODEL2:59
for P,Q being Element of BK_model st P <> Q holds
ex N being invertible Matrix of 3,F_Real st
(homography(N)).:absolute = absolute &
(homography(N)). P = Q & (homography(N)).Q = P &
(ex P1,P2 being Element of absolute st P1 <> P2 &
P,Q,P1 are_collinear & P,Q,P2 are_collinear &
homography(N).P1 = P2 & homography(N).P2 = P1);
begin :: Main lemmas
theorem :: BKMODEL2:60
for P,Q being Element of BK_model holds
ex h being Element of SubGroupK-isometry,
N being invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).P = Q &
homography(N).Q = P;
theorem :: BKMODEL2:61
for P,Q,R,S,T,U being Element of BK_model st
ex h1,h2 being Element of SubGroupK-isometry,
N1,N2 being invertible Matrix of 3,F_Real st
h1 = homography(N1) & h2 = homography(N2) &
homography(N1).P = R & homography(N1).Q = S &
homography(N2).R = T & homography(N2).S = U holds
ex h3 being Element of SubGroupK-isometry,
N3 being invertible Matrix of 3,F_Real st
h3 = homography(N3) & homography(N3).P = T &
homography(N3).Q = U;
theorem :: BKMODEL2:62
for P,Q,R being Element of BK_model, h being Element of SubGroupK-isometry,
N being invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).P = R & homography(N).Q = R holds
P = Q;