:: 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
for b1 being Element of (TOP-REAL 3) st b1 = |[a,b,c]| holds
not b1 is zero
proof end;
cluster |[c,a,b]| -> non zero for Element of (TOP-REAL 3);
coherence
for b1 being Element of (TOP-REAL 3) st b1 = |[c,a,b]| holds
not b1 is zero
proof end;
cluster |[b,c,a]| -> non zero for Element of (TOP-REAL 3);
coherence
for b1 being Element of (TOP-REAL 3) 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 (TOP-REAL 3) means :Def01: :: BKMODEL3:def 1
( Dir it = P & it . 3 = 1 );
existence
ex b1 being non zero Element of (TOP-REAL 3) st
( Dir b1 = P & b1 . 3 = 1 )
proof end;
uniqueness
for b1, b2 being non zero Element of (TOP-REAL 3) 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 (TOP-REAL 3) 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 (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
ex b1 being Function of the Lines of (IncProjSp_of real_projective_plane), the Lines of (IncProjSp_of real_projective_plane) st
for x being LINE of (IncProjSp_of real_projective_plane) holds b1 . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x }
proof end;
uniqueness
for b1, b2 being Function of the Lines of (IncProjSp_of real_projective_plane), the Lines of (IncProjSp_of real_projective_plane) st ( for x being LINE of (IncProjSp_of real_projective_plane) holds b1 . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } ) & ( for x being LINE of (IncProjSp_of real_projective_plane) holds b2 . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : 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 (IncProjSp_of real_projective_plane), the Lines of (IncProjSp_of real_projective_plane) holds
( b2 = line_homography N iff for x being LINE of (IncProjSp_of real_projective_plane) holds b2 . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : 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 (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
{ (line_homography N) where N is invertible Matrix of 3,F_Real : verum } is set
;
end;

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

registration
cluster EnsLineHomography3 -> non empty ;
coherence
not EnsLineHomography3 is empty
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 BINOP_1:sch 4();
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 BINOP_2:sch 2();
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
func GroupLineHomography3 -> strict multMagma equals :: BKMODEL3:def 6
multMagma(# EnsLineHomography3,BinOpLineHomography3 #);
coherence
multMagma(# EnsLineHomography3,BinOpLineHomography3 #) is strict multMagma
;
end;

:: deftheorem defines GroupLineHomography3 BKMODEL3:def 6 :
GroupLineHomography3 = multMagma(# EnsLineHomography3,BinOpLineHomography3 #);

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 (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: ( x in dom (line_homography N1) implies (line_homography (N1 * N2)) . x = (line_homography N1) . x )
assume x in dom (line_homography N1) ; :: thesis: (line_homography (N1 * N2)) . x = (line_homography N1) . x
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: verum
end;
hence line_homography (N1 * N2) = line_homography N1 by A5, FUNCT_1:def 11; :: thesis: verum
end;
hence h * e = h by Def04, A2, A4; :: 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 (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: ( x in dom (line_homography N1) implies (line_homography (N2 * N1)) . x = (line_homography N1) . x )
assume x in dom (line_homography N1) ; :: thesis: (line_homography (N2 * N1)) . x = (line_homography N1) . x
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: verum
end;
hence line_homography (N2 * N1) = line_homography N1 by A9, FUNCT_1:def 11; :: thesis: verum
end;
hence e * h = h by Def04, A7, A8; :: 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 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)) = 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 (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: 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 (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: 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 A4, A8, A5, MATRIX_6:def 2;
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 (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: 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 (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: 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 A11, A5, A4, MATRIX_6:def 2;
hence g * h = e by Def04; :: thesis: verum
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
( not GroupLineHomography3 is empty & GroupLineHomography3 is associative & GroupLineHomography3 is Group-like )
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
ex b1 being Relation of [:BK_model,BK_model:],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 ((BK_to_REAL2 a),(BK_to_REAL2 c)) )
proof end;
uniqueness
for b1, b2 being Relation of [:BK_model,BK_model:],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 ((BK_to_REAL2 a),(BK_to_REAL2 c)) ) ) & ( for a, b, c being Element of BK_model holds
( [[a,b],c] in b2 iff BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c)) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines BK-model-Betweenness BKMODEL3:def 7 :
for b1 being Relation of [:BK_model,BK_model:],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 ((BK_to_REAL2 a),(BK_to_REAL2 c)) ) );

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
ex b1 being Relation of [:BK_model,BK_model:],[:BK_model,BK_model:] 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 & (homography N) . a = c & (homography N) . b = d ) )
proof end;
uniqueness
for b1, b2 being Relation of [:BK_model,BK_model:],[:BK_model,BK_model:] 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 & (homography N) . a = c & (homography N) . 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 & (homography N) . a = c & (homography N) . b = d ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def05 defines BK-model-Equidistance BKMODEL3:def 8 :
for b1 being Relation of [:BK_model,BK_model:],[:BK_model,BK_model:] 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 & (homography N) . a = c & (homography N) . b = d ) ) );

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

:: deftheorem defines BK-model-Plane BKMODEL3:def 9 :
BK-model-Plane = TarskiGeometryStruct(# BK_model,BK-model-Betweenness,BK-model-Equidistance #);

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;