:: by Roland Coghetto

::

:: Received December 30, 2019

:: Copyright (c) 2019-2021 Association of Mizar Users

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 )

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

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

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;

registration

let a be non zero Real;

let b, c be Real;

coherence

for b_{1} being Element of (TOP-REAL 3) st b_{1} = |[a,b,c]| holds

not b_{1} is zero

for b_{1} being Element of (TOP-REAL 3) st b_{1} = |[c,a,b]| holds

not b_{1} is zero

for b_{1} being Element of (TOP-REAL 3) st b_{1} = |[b,c,a]| holds

not b_{1} is zero

end;
let b, c be Real;

coherence

for b

not b

proof end;

coherence for b

not b

proof end;

coherence for b

not b

proof end;

definition

let P be Element of real_projective_plane;

assume A0: P in absolute \/ BK_model ;

ex b_{1} being non zero Element of (TOP-REAL 3) st

( Dir b_{1} = P & b_{1} . 3 = 1 )

for b_{1}, b_{2} being non zero Element of (TOP-REAL 3) st Dir b_{1} = P & b_{1} . 3 = 1 & Dir b_{2} = P & b_{2} . 3 = 1 holds

b_{1} = b_{2}

end;
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 ( Dir it = P & it . 3 = 1 );

ex b

( Dir b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def01 defines # BKMODEL3:def 1 :

for P being Element of real_projective_plane st P in absolute \/ BK_model holds

for b_{2} being non zero Element of (TOP-REAL 3) holds

( b_{2} = # P iff ( Dir b_{2} = P & b_{2} . 3 = 1 ) );

for P being Element of real_projective_plane st P in absolute \/ BK_model holds

for b

( b

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 )

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

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 )

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;

ex b_{1} 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 b_{1} . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x }

for b_{1}, b_{2} 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 b_{1} . 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 b_{2} . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } ) holds

b_{1} = b_{2}

end;
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 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 } ;

ex b

for x being LINE of (IncProjSp_of real_projective_plane) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def02 defines line_homography BKMODEL3:def 2 :

for N being invertible Matrix of 3,F_Real

for b_{2} being Function of the Lines of (IncProjSp_of real_projective_plane), the Lines of (IncProjSp_of real_projective_plane) holds

( b_{2} = line_homography N iff for x being LINE of (IncProjSp_of real_projective_plane) holds b_{2} . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } );

for N being invertible Matrix of 3,F_Real

for b

( b

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

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 )

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

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

{ (line_homography N) where N is invertible Matrix of 3,F_Real : verum } is set ;

end;

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

{ (line_homography N) where N is invertible Matrix of 3,F_Real : verum } is set ;

:: deftheorem defines EnsLineHomography3 BKMODEL3:def 3 :

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

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

registration
end;

definition

let h1, h2 be Element of EnsLineHomography3 ;

ex b_{1} being Element of EnsLineHomography3 ex N1, N2 being invertible Matrix of 3,F_Real st

( h1 = line_homography N1 & h2 = line_homography N2 & b_{1} = line_homography (N1 * N2) )

for b_{1}, b_{2} being Element of EnsLineHomography3 st ex N1, N2 being invertible Matrix of 3,F_Real st

( h1 = line_homography N1 & h2 = line_homography N2 & b_{1} = line_homography (N1 * N2) ) & ex N1, N2 being invertible Matrix of 3,F_Real st

( h1 = line_homography N1 & h2 = line_homography N2 & b_{2} = line_homography (N1 * N2) ) holds

b_{1} = b_{2}

end;
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 N1, N2 being invertible Matrix of 3,F_Real st

( h1 = line_homography N1 & h2 = line_homography N2 & it = line_homography (N1 * N2) );

ex b

( h1 = line_homography N1 & h2 = line_homography N2 & b

proof end;

uniqueness for b

( h1 = line_homography N1 & h2 = line_homography N2 & b

( h1 = line_homography N1 & h2 = line_homography N2 & b

b

proof end;

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

for h1, h2, b_{3} being Element of EnsLineHomography3 holds

( b_{3} = h1 (*) h2 iff ex N1, N2 being invertible Matrix of 3,F_Real st

( h1 = line_homography N1 & h2 = line_homography N2 & b_{3} = line_homography (N1 * N2) ) );

for h1, h2, b

( b

( h1 = line_homography N1 & h2 = line_homography N2 & b

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

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;

definition

ex b_{1} being BinOp of EnsLineHomography3 st

for h1, h2 being Element of EnsLineHomography3 holds b_{1} . (h1,h2) = h1 (*) h2
from BINOP_1:sch 4();

uniqueness

for b_{1}, b_{2} being BinOp of EnsLineHomography3 st ( for h1, h2 being Element of EnsLineHomography3 holds b_{1} . (h1,h2) = h1 (*) h2 ) & ( for h1, h2 being Element of EnsLineHomography3 holds b_{2} . (h1,h2) = h1 (*) h2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 2();

end;

func BinOpLineHomography3 -> BinOp of EnsLineHomography3 means :Def04: :: BKMODEL3:def 5

for h1, h2 being Element of EnsLineHomography3 holds it . (h1,h2) = h1 (*) h2;

existence for h1, h2 being Element of EnsLineHomography3 holds it . (h1,h2) = h1 (*) h2;

ex b

for h1, h2 being Element of EnsLineHomography3 holds b

uniqueness

for b

b

:: deftheorem Def04 defines BinOpLineHomography3 BKMODEL3:def 5 :

for b_{1} being BinOp of EnsLineHomography3 holds

( b_{1} = BinOpLineHomography3 iff for h1, h2 being Element of EnsLineHomography3 holds b_{1} . (h1,h2) = h1 (*) h2 );

for b

( b

definition

multMagma(# EnsLineHomography3,BinOpLineHomography3 #) is strict multMagma ;

end;

func GroupLineHomography3 -> strict multMagma equals :: BKMODEL3:def 6

multMagma(# EnsLineHomography3,BinOpLineHomography3 #);

coherence multMagma(# EnsLineHomography3,BinOpLineHomography3 #);

multMagma(# EnsLineHomography3,BinOpLineHomography3 #) is strict multMagma ;

:: deftheorem defines GroupLineHomography3 BKMODEL3:def 6 :

GroupLineHomography3 = multMagma(# EnsLineHomography3,BinOpLineHomography3 #);

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 )

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

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

end;
( 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

hence
h * e = h
by Def04, A2, A4; :: thesis: e * h = h
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

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

hence
line_homography (N1 * N2) = line_homography N1
by A5, FUNCT_1:def 11; :: thesis: verum
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;
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

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

hence
e * h = h
by Def04, A7, A8; :: thesis: verum
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

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

hence
line_homography (N2 * N1) = line_homography N1
by A9, FUNCT_1:def 11; :: thesis: verum
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;
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

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 )

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)

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)

hence g * h = e by Def04; :: thesis: verum

end;
( 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

end;

then
h1 (*) g1 = e
by A4, A8, A5, MATRIX_6:def 2;
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 ) )

hence
line_homography (N1 * N2) = line_homography (N * Ng)
by FUNCT_1:def 11; :: thesis: verum(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

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

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

end;

then
g1 (*) h1 = e
by A11, A5, A4, MATRIX_6:def 2;
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 ) )

hence
line_homography (N1 * N2) = line_homography (Ng * N)
by FUNCT_1:def 11; :: thesis: verum(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

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

hence g * h = e by Def04; :: thesis: verum

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

coherence

( not GroupLineHomography3 is empty & GroupLineHomography3 is associative & GroupLineHomography3 is Group-like )

end;
( not GroupLineHomography3 is empty & GroupLineHomography3 is associative & GroupLineHomography3 is Group-like )

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 "

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

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

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 )

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

((((u `1) ^2) + ((u `2) ^2)) - ((u `1) * (w `1))) - ((u `2) * (w `2)) = 0

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

((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

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

( 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

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

Dir u is Element of BK_model

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 )

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 )

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

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 )

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

ex b_{1} being Relation of [:BK_model,BK_model:],BK_model st

for a, b, c being Element of BK_model holds

( [[a,b],c] in b_{1} iff BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c)) )

for b_{1}, b_{2} being Relation of [:BK_model,BK_model:],BK_model st ( for a, b, c being Element of BK_model holds

( [[a,b],c] in b_{1} 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 b_{2} iff BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c)) ) ) holds

b_{1} = b_{2}
end;

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

ex b

for a, b, c being Element of BK_model holds

( [[a,b],c] in b

proof end;

uniqueness for b

( [[a,b],c] in b

( [[a,b],c] in b

b

proof end;

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

for b_{1} being Relation of [:BK_model,BK_model:],BK_model holds

( b_{1} = BK-model-Betweenness iff for a, b, c being Element of BK_model holds

( [[a,b],c] in b_{1} iff BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c)) ) );

for b

( b

( [[a,b],c] in b

definition

ex b_{1} 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 b_{1} 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 b_{1}, b_{2} 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 b_{1} 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 b_{2} 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

b_{1} = b_{2}
end;

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

ex b

for a, b, c, d being Element of BK_model holds

( [[a,b],[c,d]] in b

( h = homography N & (homography N) . a = c & (homography N) . b = d ) )

proof end;

uniqueness for b

( [[a,b],[c,d]] in b

( 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 b

( h = homography N & (homography N) . a = c & (homography N) . b = d ) ) ) holds

b

proof end;

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

for b_{1} being Relation of [:BK_model,BK_model:],[:BK_model,BK_model:] holds

( b_{1} = BK-model-Equidistance iff for a, b, c, d being Element of BK_model holds

( [[a,b],[c,d]] in b_{1} 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 b

( b

( [[a,b],[c,d]] in b

( h = homography N & (homography N) . a = c & (homography N) . b = d ) ) );

definition

TarskiGeometryStruct(# BK_model,BK-model-Betweenness,BK-model-Equidistance #) is TarskiGeometryStruct ;

end;

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

TarskiGeometryStruct(# BK_model,BK-model-Betweenness,BK-model-Equidistance #) is TarskiGeometryStruct ;

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

BK-model-Plane = TarskiGeometryStruct(# BK_model,BK-model-Betweenness,BK-model-Equidistance #);

BK-model-Plane = TarskiGeometryStruct(# BK_model,BK-model-Betweenness,BK-model-Equidistance #);