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