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