:: 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 ();
coherence
for b1 being Element of () st b1 = |[a,b,c]| holds
not b1 is zero
proof end;
cluster |[c,a,b]| -> non zero for Element of ();
coherence
for b1 being Element of () st b1 = |[c,a,b]| holds
not b1 is zero
proof end;
cluster |[b,c,a]| -> non zero for Element of ();
coherence
for b1 being Element of () st b1 = |[b,c,a]| holds
not b1 is zero
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 () means :Def01: :: BKMODEL3:def 1
( Dir it = P & it . 3 = 1 );
existence
ex b1 being non zero Element of () st
( Dir b1 = P & b1 . 3 = 1 )
proof end;
uniqueness
for b1, b2 being non zero Element of () st Dir b1 = P & b1 . 3 = 1 & Dir b2 = P & b2 . 3 = 1 holds
b1 = b2
proof end;
end;

:: deftheorem Def01 defines # BKMODEL3:def 1 :
for P being Element of real_projective_plane st P in absolute \/ BK_model holds
for b2 being non zero Element of () holds
( b2 = # P iff ( Dir b2 = P & b2 . 3 = 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 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 , the Lines of means :Def02: :: BKMODEL3:def 2
for x being LINE of holds it . x = { (() . P) where P is POINT of : P on x } ;
existence
ex b1 being Function of the Lines of , the Lines of st
for x being LINE of holds b1 . x = { (() . P) where P is POINT of : P on x }
proof end;
uniqueness
for b1, b2 being Function of the Lines of , the Lines of st ( for x being LINE of holds b1 . x = { (() . P) where P is POINT of : P on x } ) & ( for x being LINE of holds b2 . x = { (() . P) where P is POINT of : P on x } ) holds
b1 = b2
proof end;
end;

:: deftheorem Def02 defines line_homography BKMODEL3:def 2 :
for N being invertible Matrix of 3,F_Real
for b2 being Function of the Lines of , the Lines of holds
( b2 = line_homography N iff for x being LINE of holds b2 . x = { (() . P) where P is POINT of : P on x } );

theorem Th13: :: BKMODEL3:15
for N1, N2 being invertible Matrix of 3,F_Real
for l being Element of the Lines of holds () . (() . l) = (line_homography (N1 * N2)) . l
proof end;

theorem Th14: :: BKMODEL3:16
for l being Element of the Lines of 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 holds
( () . ((line_homography (N ~)) . l) = l & (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 st () . l1 = () . l2 holds
l1 = l2
proof end;

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

:: deftheorem defines EnsLineHomography3 BKMODEL3:def 3 :
EnsLineHomography3 = { () where N is invertible Matrix of 3,F_Real : verum } ;

registration
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
ex b1 being Element of EnsLineHomography3 ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = line_homography N1 & h2 = line_homography N2 & b1 = line_homography (N1 * N2) )
proof end;
uniqueness
for b1, b2 being Element of EnsLineHomography3 st ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = line_homography N1 & h2 = line_homography N2 & b1 = line_homography (N1 * N2) ) & ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = line_homography N1 & h2 = line_homography N2 & b2 = line_homography (N1 * N2) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def03 defines (*) BKMODEL3:def 4 :
for h1, h2, b3 being Element of EnsLineHomography3 holds
( b3 = h1 (*) h2 iff ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = line_homography N1 & h2 = line_homography N2 & b3 = line_homography (N1 * N2) ) );

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
ex b1 being BinOp of EnsLineHomography3 st
for h1, h2 being Element of EnsLineHomography3 holds b1 . (h1,h2) = h1 (*) h2
from uniqueness
for b1, b2 being BinOp of EnsLineHomography3 st ( for h1, h2 being Element of EnsLineHomography3 holds b1 . (h1,h2) = h1 (*) h2 ) & ( for h1, h2 being Element of EnsLineHomography3 holds b2 . (h1,h2) = h1 (*) h2 ) holds
b1 = b2
from
end;

:: deftheorem Def04 defines BinOpLineHomography3 BKMODEL3:def 5 :
for b1 being BinOp of EnsLineHomography3 holds
( b1 = BinOpLineHomography3 iff for h1, h2 being Element of EnsLineHomography3 holds b1 . (h1,h2) = h1 (*) h2 );

definition
coherence ;
end;

:: deftheorem defines GroupLineHomography3 BKMODEL3:def 6 :

set GLH3 = GroupLineHomography3 ;

Lm1: now :: thesis: for e being Element of GroupLineHomography3 st e = line_homography (1. (F_Real,3)) holds
for h being Element of GroupLineHomography3 holds
( h * e = h & e * h = h )
let e be Element of GroupLineHomography3; :: thesis: ( e = line_homography (1. (F_Real,3)) implies for h being Element of GroupLineHomography3 holds
( h * e = h & e * h = h ) )

assume A1: e = line_homography (1. (F_Real,3)) ; :: thesis: for h being Element of GroupLineHomography3 holds
( h * e = h & e * h = h )

let h be Element of GroupLineHomography3; :: thesis: ( h * e = h & e * h = h )
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 by FUNCT_2:def 1;
then A5: dom (line_homography (N1 * N2)) = dom () by FUNCT_2:def 1;
for x being object st x in dom () holds
(line_homography (N1 * N2)) . x = () . x
proof
let x be object ; :: thesis: ( x in dom () implies (line_homography (N1 * N2)) . x = () . x )
assume x in dom () ; :: thesis: (line_homography (N1 * N2)) . x = () . x
then reconsider xf = x as Element of the Lines of ;
(line_homography (N1 * N2)) . xf = () . (() . xf) by Th13
.= () . xf by A1, A3, Th14 ;
hence (line_homography (N1 * N2)) . x = () . x ; :: thesis: verum
end;
hence line_homography (N1 * N2) = line_homography N1 by ; :: thesis: verum
end;
hence h * e = h by ; :: thesis: e * h = h
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 by FUNCT_2:def 1;
then A9: dom (line_homography (N2 * N1)) = dom () by FUNCT_2:def 1;
for x being object st x in dom () holds
(line_homography (N2 * N1)) . x = () . x
proof
let x be object ; :: thesis: ( x in dom () implies (line_homography (N2 * N1)) . x = () . x )
assume x in dom () ; :: thesis: (line_homography (N2 * N1)) . x = () . x
then reconsider xf = x as Element of the Lines of ;
(line_homography (N2 * N1)) . xf = () . (() . xf) by Th13
.= () . xf by A1, A6, Th14 ;
hence (line_homography (N2 * N1)) . x = () . x ; :: thesis: verum
end;
hence line_homography (N2 * N1) = line_homography N1 by ; :: thesis: verum
end;
hence e * h = h by ; :: thesis: verum
end;

Lm2: now :: thesis: for e, 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 ~ & e = line_homography (1. (F_Real,3)) holds
( h * g = e & g * h = e )
let e, h, g be Element of GroupLineHomography3; :: thesis: for N, Ng being invertible Matrix of 3,F_Real st h = line_homography N & g = line_homography Ng & Ng = N ~ & e = line_homography (1. (F_Real,3)) holds
( h * g = e & g * h = e )

let N, Ng be invertible Matrix of 3,F_Real; :: thesis: ( h = line_homography N & g = line_homography Ng & Ng = N ~ & e = line_homography (1. (F_Real,3)) implies ( h * g = e & g * h = e ) )
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: ( h * g = e & g * h = e )
reconsider h1 = h as Element of EnsLineHomography3 ;
A5: Ng is_reverse_of N by ;
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)) = dom (line_homography (N * Ng)) & ( for x being object st x in dom (line_homography (N1 * N2)) holds
(line_homography (N1 * N2)) . x = (line_homography (N * Ng)) . x ) )
dom (line_homography (N1 * N2)) = the Lines of by FUNCT_2:def 1;
hence dom (line_homography (N1 * N2)) = dom (line_homography (N * Ng)) by FUNCT_2:def 1; :: thesis: for x being object st x in dom (line_homography (N1 * N2)) holds
(line_homography (N1 * N2)) . x = (line_homography (N * Ng)) . x

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: verum
proof
let x be object ; :: thesis: ( x in dom (line_homography (N1 * N2)) implies (line_homography (N1 * N2)) . x = (line_homography (N * Ng)) . x )
assume x in dom (line_homography (N1 * N2)) ; :: thesis: (line_homography (N1 * N2)) . x = (line_homography (N * Ng)) . x
then reconsider xf = x as Element of the Lines of ;
(line_homography (N1 * N2)) . xf = () . (() . 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: verum
end;
end;
hence line_homography (N1 * N2) = line_homography (N * Ng) by FUNCT_1:def 11; :: thesis: verum
end;
then h1 (*) g1 = e by ;
hence h * g = e by Def04; :: thesis: g * h = e
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)) = dom (line_homography (Ng * N)) & ( for x being object st x in dom (line_homography (N1 * N2)) holds
(line_homography (N1 * N2)) . x = (line_homography (Ng * N)) . x ) )
dom (line_homography (N1 * N2)) = the Lines of by FUNCT_2:def 1;
hence dom (line_homography (N1 * N2)) = dom (line_homography (Ng * N)) by FUNCT_2:def 1; :: thesis: for x being object st x in dom (line_homography (N1 * N2)) holds
(line_homography (N1 * N2)) . x = (line_homography (Ng * N)) . x

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: verum
proof
let x be object ; :: thesis: ( x in dom (line_homography (N1 * N2)) implies (line_homography (N1 * N2)) . x = (line_homography (Ng * N)) . x )
assume x in dom (line_homography (N1 * N2)) ; :: thesis: (line_homography (N1 * N2)) . x = (line_homography (Ng * N)) . x
then reconsider xf = x as Element of the Lines of ;
(line_homography (N1 * N2)) . xf = () . (() . 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: verum
end;
end;
hence line_homography (N1 * N2) = line_homography (Ng * N) by FUNCT_1:def 11; :: thesis: verum
end;
then g1 (*) h1 = e by ;
hence g * h = e by Def04; :: thesis: verum
end;

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

;

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

registration
coherence
proof end;
end;

theorem Th18: :: BKMODEL3:21
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 ()
for l being LINE of st () . 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 ()
for l being LINE of st P in () . 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 ()
for l being LINE of holds
( P in l iff () . P in () . l )
proof end;

theorem Th21: :: BKMODEL3:26
for u, v, w being non zero Element of () 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 () 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 () 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 () 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 () 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 () 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 () st not P in BK_model \/ absolute holds
ex l being LINE of 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 () . 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
() . 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 () st
( () . P = Dir u & u . 3 = 1 )
proof end;

definition
func BK-model-Betweenness -> Relation of ,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 ((),()) );
existence
ex b1 being Relation of ,BK_model st
for a, b, c being Element of BK_model holds
( [[a,b],c] in b1 iff BK_to_REAL2 b in LSeg ((),()) )
proof end;
uniqueness
for b1, b2 being Relation of ,BK_model st ( for a, b, c being Element of BK_model holds
( [[a,b],c] in b1 iff BK_to_REAL2 b in LSeg ((),()) ) ) & ( for a, b, c being Element of BK_model holds
( [[a,b],c] in b2 iff BK_to_REAL2 b in LSeg ((),()) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines BK-model-Betweenness BKMODEL3:def 7 :
for b1 being Relation of ,BK_model holds
( b1 = BK-model-Betweenness iff for a, b, c being Element of BK_model holds
( [[a,b],c] in b1 iff BK_to_REAL2 b in LSeg ((),()) ) );

definition
func BK-model-Equidistance -> Relation of , 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 & () . a = c & () . b = d ) );
existence
ex b1 being Relation of , st
for a, b, c, d being Element of BK_model holds
( [[a,b],[c,d]] in b1 iff ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & () . a = c & () . b = d ) )
proof end;
uniqueness
for b1, b2 being Relation of , st ( for a, b, c, d being Element of BK_model holds
( [[a,b],[c,d]] in b1 iff ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & () . a = c & () . b = d ) ) ) & ( for a, b, c, d being Element of BK_model holds
( [[a,b],[c,d]] in b2 iff ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & () . a = c & () . b = d ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def05 defines BK-model-Equidistance BKMODEL3:def 8 :
for b1 being Relation of , holds
( b1 = BK-model-Equidistance iff for a, b, c, d being Element of BK_model holds
( [[a,b],[c,d]] in b1 iff ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & () . a = c & () . b = d ) ) );

definition end;

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

theorem :: BKMODEL3:38
proof end;

theorem :: BKMODEL3:40
proof end;