BKMODEL3: Beltrami-Klein model, Part {III}

:: Beltrami-Klein model, Part {III}
:: by Roland Coghetto
::
:: Received December 30, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

theorem :: BKMODEL3:1

for x, y being Real st x * y < 0 holds
( 0 < x / (x - y) & x / (x - y) < 1 )

proof end;

theorem Th02: :: BKMODEL3:2

for a being non zero Real
for b, r being Real st r = sqrt ((a ^2) + (b ^2)) holds
( r is positive & ((a / r) ^2) + ((b / r) ^2) = 1 )

proof end;

theorem Th03: :: BKMODEL3:3

for a being non zero Real
for 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))

proof end;

theorem Th04: :: BKMODEL3:4

for a, b, c being Complex st a <> 0 holds
(((a ^2) * b) * c) / (a ^2) = b * c

proof end;

theorem Th05: :: BKMODEL3:5

for a, b, c being Complex st a <> 0 holds
((2 * ((a ^2) * b)) * c) / (a ^2) = (2 * b) * c

proof end;

theorem Th07: :: BKMODEL3:6

for a being Real st 1 < a holds
(1 / a) - 1 < 0

proof end;

theorem Th08: :: BKMODEL3:7

for a, b being Real st 0 < a & 1 < b holds
(a / b) - a < 0

proof end;

theorem Th09: :: BKMODEL3:8

for a being non zero Real
for 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

proof end;

theorem Th10: :: BKMODEL3:9

for a, b, c being Real st a * (- b) = c & a * c = b holds
( c = 0 & b = 0 )

proof end;

theorem :: BKMODEL3:10

for a being positive Real holds (sqrt a) / a = 1 / (sqrt a)

proof end;

registration

let a be non zero Real;
let b, c be Real;

cluster |[a,b,c]| -> non zero for Element of (TOP-REAL 3);

coherence

proof end;

cluster |[c,a,b]| -> non zero for Element of (TOP-REAL 3);

coherence

proof end;

cluster |[b,c,a]| -> non zero for Element of (TOP-REAL 3);

coherence

proof end;

end;

definition

let P be Element of real_projective_plane;
assume A0: P in absolute \/ BK_model ;

func # P -> non zero Element of (TOP-REAL 3) means :Def01: :: BKMODEL3:def 1
( Dir it = P & it . 3 = 1 );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def01 defines # BKMODEL3:def 1 :

theorem Th11: :: BKMODEL3:11

for P being Element of real_projective_plane ex Q being Element of BK_model st P <> Q

proof end;

theorem :: BKMODEL3:12

for P being Element of BK_model ex P1, P2 being Element of absolute st
( P1 <> P2 & P1,P,P2 are_collinear )

proof end;

theorem :: BKMODEL3:13

for P being Element of BK_model
for Q being Element of absolute ex R being Element of BK_model st
( P <> R & P,Q,R are_collinear )

proof end;

theorem Th12: :: BKMODEL3:14

for P being Element of BK_model
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 )

proof end;

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

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def02 defines line_homography BKMODEL3:def 2 :

theorem Th13: :: BKMODEL3:15

for N1, N2 being invertible Matrix of 3,F_Real
for l being Element of the Lines of (IncProjSp_of real_projective_plane) holds (line_homography N1) . ((line_homography N2) . l) = (line_homography (N1 * N2)) . l

proof end;

theorem Th14: :: BKMODEL3:16

for l being Element of the Lines of (IncProjSp_of real_projective_plane) holds (line_homography (1. (F_Real,3))) . l = l

proof end;

theorem Th15: :: BKMODEL3:17

for N being invertible Matrix of 3,F_Real
for l being Element of the Lines of (IncProjSp_of real_projective_plane) holds
( (line_homography N) . ((line_homography (N ~)) . l) = l & (line_homography (N ~)) . ((line_homography N) . l) = l )

proof end;

theorem :: BKMODEL3:18

for N being invertible Matrix of 3,F_Real
for l1, l2 being Element of the Lines of (IncProjSp_of real_projective_plane) st (line_homography N) . l1 = (line_homography N) . l2 holds
l1 = l2

proof end;

definition

func EnsLineHomography3 -> set equals :: BKMODEL3:def 3
{ (line_homography N) where N is invertible Matrix of 3,F_Real : verum } ;

coherence ;

end;

:: deftheorem defines EnsLineHomography3 BKMODEL3:def 3 :

registration

cluster EnsLineHomography3 -> non empty ;

coherence

proof end;

end;

definition

let h1, h2 be Element of EnsLineHomography3 ;

func h1 (*) h2 -> Element of EnsLineHomography3 means :Def03: :: 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) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def03 defines (*) BKMODEL3:def 4 :

theorem Th16: :: BKMODEL3:19

for N1, N2 being invertible Matrix of 3,F_Real
for h1, h2 being Element of EnsLineHomography3 st h1 = line_homography N1 & h2 = line_homography N2 holds
line_homography (N1 * N2) = h1 (*) h2

proof end;

theorem Th17: :: BKMODEL3:20

for x, y, z being Element of EnsLineHomography3 holds (x (*) y) (*) z = x (*) (y (*) z)

proof end;

definition

func BinOpLineHomography3 -> BinOp of EnsLineHomography3 means :Def04: :: BKMODEL3:def 5
for h1, h2 being Element of EnsLineHomography3 holds it . (h1,h2) = h1 (*) h2;

existence from BINOP_1:sch 4();
uniqueness from BINOP_2:sch 2();

end;

:: deftheorem Def04 defines BinOpLineHomography3 BKMODEL3:def 5 :

definition

func GroupLineHomography3 -> strict multMagma equals :: BKMODEL3:def 6
multMagma(# EnsLineHomography3,BinOpLineHomography3 #);

coherence ;

end;

:: deftheorem defines GroupLineHomography3 BKMODEL3:def 6 :

set GLH3 = GroupLineHomography3 ;

Lm1: now :: thesis:

let e be Element of GroupLineHomography3; :: thesis:
assume A1: e = line_homography (1. (F_Real,3)) ; :: thesis:
let h be Element of GroupLineHomography3; :: thesis:
reconsider h1 = h, h2 = e as Element of EnsLineHomography3 ;
consider N1, N2 being invertible Matrix of 3,F_Real such that
A2: h1 = line_homography N1 and
A3: h2 = line_homography N2 and
A4: h1 (*) h2 = line_homography (N1 * N2) by Def03;
line_homography (N1 * N2) = line_homography N1

proof

dom (line_homography (N1 * N2)) = the Lines of (IncProjSp_of real_projective_plane) by FUNCT_2:def 1;
then A5: dom (line_homography (N1 * N2)) = dom (line_homography N1) by FUNCT_2:def 1;
for x being object st x in dom (line_homography N1) holds
(line_homography (N1 * N2)) . x = (line_homography N1) . x

proof

let x be object ; :: thesis:
assume x in dom (line_homography N1) ; :: thesis:
then reconsider xf = x as Element of the Lines of (IncProjSp_of real_projective_plane) ;
(line_homography (N1 * N2)) . xf = (line_homography N1) . ((line_homography N2) . xf) by Th13
.= (line_homography N1) . xf by A1, A3, Th14 ;
hence (line_homography (N1 * N2)) . x = (line_homography N1) . x ; :: thesis:

end;

hence line_homography (N1 * N2) = line_homography N1 by A5, FUNCT_1:def 11; :: thesis:

end;

hence h * e = h by Def04, A2, A4; :: thesis:
consider N2, N1 being invertible Matrix of 3,F_Real such that
A6: h2 = line_homography N2 and
A7: h1 = line_homography N1 and
A8: h2 (*) h1 = line_homography (N2 * N1) by Def03;
line_homography (N2 * N1) = line_homography N1

proof

dom (line_homography (N2 * N1)) = the Lines of (IncProjSp_of real_projective_plane) by FUNCT_2:def 1;
then A9: dom (line_homography (N2 * N1)) = dom (line_homography N1) by FUNCT_2:def 1;
for x being object st x in dom (line_homography N1) holds
(line_homography (N2 * N1)) . x = (line_homography N1) . x

proof

let x be object ; :: thesis:
assume x in dom (line_homography N1) ; :: thesis:
then reconsider xf = x as Element of the Lines of (IncProjSp_of real_projective_plane) ;
(line_homography (N2 * N1)) . xf = (line_homography N2) . ((line_homography N1) . xf) by Th13
.= (line_homography N1) . xf by A1, A6, Th14 ;
hence (line_homography (N2 * N1)) . x = (line_homography N1) . x ; :: thesis:

end;

hence line_homography (N2 * N1) = line_homography N1 by A9, FUNCT_1:def 11; :: thesis:

end;

hence e * h = h by Def04, A7, A8; :: thesis:

end;

Lm2: now :: thesis:

let e, h, g be Element of GroupLineHomography3; :: thesis:
let N, Ng be invertible Matrix of 3,F_Real; :: thesis:
assume that
A1: h = line_homography N and
A2: g = line_homography Ng and
A3: Ng = N ~ and
A4: e = line_homography (1. (F_Real,3)) ; :: thesis:
reconsider h1 = h as Element of EnsLineHomography3 ;
A5: Ng is_reverse_of N by A3, MATRIX_6:def 4;
reconsider g1 = g as Element of EnsLineHomography3 ;
consider N1, N2 being invertible Matrix of 3,F_Real such that
A6: h1 = line_homography N1 and
A7: g1 = line_homography N2 and
A8: h1 (*) g1 = line_homography (N1 * N2) by Def03;
line_homography (N1 * N2) = line_homography (N * Ng)

proof

now :: thesis:

dom (line_homography (N1 * N2)) = the Lines of (IncProjSp_of real_projective_plane) by FUNCT_2:def 1;
hence dom (line_homography (N1 * N2)) = dom (line_homography (N * Ng)) by FUNCT_2:def 1; :: thesis:
thus for x being object st x in dom (line_homography (N1 * N2)) holds
(line_homography (N1 * N2)) . x = (line_homography (N * Ng)) . x :: thesis:

proof

let x be object ; :: thesis:
assume x in dom (line_homography (N1 * N2)) ; :: thesis:
then reconsider xf = x as Element of the Lines of (IncProjSp_of real_projective_plane) ;
(line_homography (N1 * N2)) . xf = (line_homography N) . ((line_homography Ng) . xf) by Th13, A6, A1, A7, A2
.= (line_homography (N * Ng)) . xf by Th13 ;
hence (line_homography (N1 * N2)) . x = (line_homography (N * Ng)) . x ; :: thesis:

end;

hence line_homography (N1 * N2) = line_homography (N * Ng) by FUNCT_1:def 11; :: thesis:

end;

then h1 (*) g1 = e by A4, A8, A5, MATRIX_6:def 2;
hence h * g = e by Def04; :: thesis:
consider N1, N2 being invertible Matrix of 3,F_Real such that
A9: g1 = line_homography N1 and
A10: h1 = line_homography N2 and
A11: g1 (*) h1 = line_homography (N1 * N2) by Def03;
line_homography (N1 * N2) = line_homography (Ng * N)

proof

now :: thesis:

dom (line_homography (N1 * N2)) = the Lines of (IncProjSp_of real_projective_plane) by FUNCT_2:def 1;
hence dom (line_homography (N1 * N2)) = dom (line_homography (Ng * N)) by FUNCT_2:def 1; :: thesis:
thus for x being object st x in dom (line_homography (N1 * N2)) holds
(line_homography (N1 * N2)) . x = (line_homography (Ng * N)) . x :: thesis:

proof

let x be object ; :: thesis:
assume x in dom (line_homography (N1 * N2)) ; :: thesis:
then reconsider xf = x as Element of the Lines of (IncProjSp_of real_projective_plane) ;
(line_homography (N1 * N2)) . xf = (line_homography Ng) . ((line_homography N) . xf) by Th13, A9, A1, A10, A2
.= (line_homography (Ng * N)) . xf by Th13 ;
hence (line_homography (N1 * N2)) . x = (line_homography (Ng * N)) . x ; :: thesis:

end;

hence line_homography (N1 * N2) = line_homography (Ng * N) by FUNCT_1:def 11; :: thesis:

end;

then g1 (*) h1 = e by A11, A5, A4, MATRIX_6:def 2;
hence g * h = e by Def04; :: thesis:

end;

set e = line_homography (1. (F_Real,3));

line_homography (1. (F_Real,3)) in EnsLineHomography3
;

then reconsider e = line_homography (1. (F_Real,3)) as Element of GroupLineHomography3 ;

registration

cluster GroupLineHomography3 -> non empty strict Group-like associative ;

coherence

proof end;

end;

theorem Th18: :: BKMODEL3:21

1_ GroupLineHomography3 = line_homography (1. (F_Real,3))

proof end;

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 "

proof end;

theorem Th19: :: BKMODEL3:23

for N being invertible Matrix of 3,F_Real
for P being Point of (ProjectiveSpace (TOP-REAL 3))
for l being LINE of (IncProjSp_of real_projective_plane) st (homography N) . P in l holds
P in (line_homography (N ~)) . l

proof end;

theorem :: BKMODEL3:24

for N being invertible Matrix of 3,F_Real
for P being Point of (ProjectiveSpace (TOP-REAL 3))
for l being LINE of (IncProjSp_of real_projective_plane) st P in (line_homography N) . l holds
(homography (N ~)) . P in l

proof end;

theorem Th20: :: BKMODEL3:25

for N being invertible Matrix of 3,F_Real
for P being Point of (ProjectiveSpace (TOP-REAL 3))
for l being LINE of (IncProjSp_of real_projective_plane) holds
( P in l iff (homography N) . P in (line_homography N) . l )

proof end;

theorem Th21: :: 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

proof end;

theorem Th22: :: BKMODEL3:27

for a being non zero Real
for b, c being Real holds a * |[(b / a),(c / a),1]| = |[b,c,a]|

proof end;

theorem Th23: :: 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

proof end;

theorem Th24: :: 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

proof end;

theorem Th25: :: BKMODEL3:30

for P being Element of absolute ex u being non zero Element of (TOP-REAL 3) st
( u . 3 = 1 & P = Dir u )

proof end;

theorem Th26: :: 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

proof end;

theorem Th27: :: 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

proof end;

theorem Th28: :: BKMODEL3:33

for a, b being Real st (a ^2) + (b ^2) <= 1 holds
Dir |[a,b,1]| in BK_model \/ absolute

proof end;

theorem Th29: :: BKMODEL3:34

for P being Point of (ProjectiveSpace (TOP-REAL 3)) st not P in BK_model \/ absolute holds
ex l being LINE of (IncProjSp_of real_projective_plane) st
( P in l & l misses absolute )

proof end;

theorem Th30: :: BKMODEL3:35

for P being Point of real_projective_plane
for h being Element of SubGroupK-isometry
for 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 )

proof end;

theorem Th31: :: BKMODEL3:36

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
(homography N) . P is Element of BK_model

proof end;

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 )

proof end;

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

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines BK-model-Betweenness BKMODEL3:def 7 :

definition

func BK-model-Equidistance -> Relation of [:BK_model,BK_model:],[:BK_model,BK_model:] means :Def05: :: 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 ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) . a = c & (homography N) . b = d ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def05 defines BK-model-Equidistance BKMODEL3:def 8 :

definition

func BK-model-Plane -> TarskiGeometryStruct equals :: BKMODEL3:def 9
TarskiGeometryStruct(# BK_model,BK-model-Betweenness,BK-model-Equidistance #);

coherence ;

end;

:: deftheorem defines BK-model-Plane BKMODEL3:def 9 :

theorem :: BKMODEL3:38

BK-model-Plane is satisfying_CongruenceSymmetry

proof end;

theorem :: BKMODEL3:39

BK-model-Plane is satisfying_CongruenceEquivalenceRelation

proof end;

theorem :: BKMODEL3:40

BK-model-Plane is satisfying_CongruenceIdentity

proof end;