:: by Roland Coghetto

::

:: Received March 17, 2017

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

theorem Th02: :: ANPROJ_9:2

for ra being Element of F_Real

for N being Matrix of 3,F_Real holds ra * N = (ra * (1. (F_Real,3))) * N

for N being Matrix of 3,F_Real holds ra * N = (ra * (1. (F_Real,3))) * N

proof end;

theorem Th04: :: ANPROJ_9:3

for r being Real

for u being Element of (TOP-REAL 3) st r <> 0 & not u is zero holds

not r * u is zero

for u being Element of (TOP-REAL 3) st r <> 0 & not u is zero holds

not r * u is zero

proof end;

theorem Th05: :: ANPROJ_9:4

for a11, a12, a13, a21, a22, a23, a31, a32, a33 being Element of F_Real

for A being Matrix of 3,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> holds

( Line (A,1) = <*a11,a12,a13*> & Line (A,2) = <*a21,a22,a23*> & Line (A,3) = <*a31,a32,a33*> )

for A being Matrix of 3,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> holds

( Line (A,1) = <*a11,a12,a13*> & Line (A,2) = <*a21,a22,a23*> & Line (A,3) = <*a31,a32,a33*> )

proof end;

theorem Th06: :: ANPROJ_9:5

for a11, a12, a13, a21, a22, a23, a31, a32, a33 being Element of F_Real

for A being Matrix of 3,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> holds

( Col (A,1) = <*a11,a21,a31*> & Col (A,2) = <*a12,a22,a32*> & Col (A,3) = <*a13,a23,a33*> )

for A being Matrix of 3,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> holds

( Col (A,1) = <*a11,a21,a31*> & Col (A,2) = <*a12,a22,a32*> & Col (A,3) = <*a13,a23,a33*> )

proof end;

theorem Th07: :: ANPROJ_9:6

for a11, a12, a13, a21, a22, a23, a31, a32, a33, b11, b12, b13, b21, b22, b23, b31, b32, b33 being Element of F_Real

for A, B being Matrix of 3,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> & B = <*<*b11,b12,b13*>,<*b21,b22,b23*>,<*b31,b32,b33*>*> holds

A * B = <*<*(((a11 * b11) + (a12 * b21)) + (a13 * b31)),(((a11 * b12) + (a12 * b22)) + (a13 * b32)),(((a11 * b13) + (a12 * b23)) + (a13 * b33))*>,<*(((a21 * b11) + (a22 * b21)) + (a23 * b31)),(((a21 * b12) + (a22 * b22)) + (a23 * b32)),(((a21 * b13) + (a22 * b23)) + (a23 * b33))*>,<*(((a31 * b11) + (a32 * b21)) + (a33 * b31)),(((a31 * b12) + (a32 * b22)) + (a33 * b32)),(((a31 * b13) + (a32 * b23)) + (a33 * b33))*>*>

for A, B being Matrix of 3,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> & B = <*<*b11,b12,b13*>,<*b21,b22,b23*>,<*b31,b32,b33*>*> holds

A * B = <*<*(((a11 * b11) + (a12 * b21)) + (a13 * b31)),(((a11 * b12) + (a12 * b22)) + (a13 * b32)),(((a11 * b13) + (a12 * b23)) + (a13 * b33))*>,<*(((a21 * b11) + (a22 * b21)) + (a23 * b31)),(((a21 * b12) + (a22 * b22)) + (a23 * b32)),(((a21 * b13) + (a22 * b23)) + (a23 * b33))*>,<*(((a31 * b11) + (a32 * b21)) + (a33 * b31)),(((a31 * b12) + (a32 * b22)) + (a33 * b32)),(((a31 * b13) + (a32 * b23)) + (a33 * b33))*>*>

proof end;

theorem Th08: :: ANPROJ_9:7

for a11, a12, a13, a21, a22, a23, a31, a32, a33, b1, b2, b3 being Element of F_Real

for A being Matrix of 3,3,F_Real

for B being Matrix of 3,1,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> & B = <*<*b1*>,<*b2*>,<*b3*>*> holds

A * B = <*<*(((a11 * b1) + (a12 * b2)) + (a13 * b3))*>,<*(((a21 * b1) + (a22 * b2)) + (a23 * b3))*>,<*(((a31 * b1) + (a32 * b2)) + (a33 * b3))*>*>

for A being Matrix of 3,3,F_Real

for B being Matrix of 3,1,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> & B = <*<*b1*>,<*b2*>,<*b3*>*> holds

A * B = <*<*(((a11 * b1) + (a12 * b2)) + (a13 * b3))*>,<*(((a21 * b1) + (a22 * b2)) + (a23 * b3))*>,<*(((a31 * b1) + (a32 * b2)) + (a33 * b3))*>*>

proof end;

Lem01: for a11, a12, a13, a21, a22, a23, a31, a32, a33, b11, b12, b13, b21, b22, b23, b31, b32, b33 being Element of F_Real

for A, B being Matrix of 3,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> & B = <*<*b11,b12,b13*>,<*b21,b22,b23*>,<*b31,b32,b33*>*> holds

( (A * B) . 1 = <*(((a11 * b11) + (a12 * b21)) + (a13 * b31)),(((a11 * b12) + (a12 * b22)) + (a13 * b32)),(((a11 * b13) + (a12 * b23)) + (a13 * b33))*> & (A * B) . 2 = <*(((a21 * b11) + (a22 * b21)) + (a23 * b31)),(((a21 * b12) + (a22 * b22)) + (a23 * b32)),(((a21 * b13) + (a22 * b23)) + (a23 * b33))*> & (A * B) . 3 = <*(((a31 * b11) + (a32 * b21)) + (a33 * b31)),(((a31 * b12) + (a32 * b22)) + (a33 * b32)),(((a31 * b13) + (a32 * b23)) + (a33 * b33))*> )

proof end;

theorem Th09: :: ANPROJ_9:8

for a, b, c being non zero Element of F_Real

for M1, M2 being Matrix of 3,F_Real st M1 = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> & M2 = <*<*(1 / a),0,0*>,<*0,(1 / b),0*>,<*0,0,(1 / c)*>*> holds

( M1 * M2 = 1. (F_Real,3) & M2 * M1 = 1. (F_Real,3) )

for M1, M2 being Matrix of 3,F_Real st M1 = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> & M2 = <*<*(1 / a),0,0*>,<*0,(1 / b),0*>,<*0,0,(1 / c)*>*> holds

( M1 * M2 = 1. (F_Real,3) & M2 * M1 = 1. (F_Real,3) )

proof end;

theorem Th10: :: ANPROJ_9:9

for a, b, c being non zero Element of F_Real holds <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> is invertible Matrix of 3,F_Real

proof end;

theorem :: ANPROJ_9:11

( |[1,0,0]| <> 0. (TOP-REAL 3) & |[0,1,0]| <> 0. (TOP-REAL 3) & |[0,0,1]| <> 0. (TOP-REAL 3) & |[1,1,1]| <> 0. (TOP-REAL 3) )

proof end;

Lem02: for i being Nat

for u being Element of (TOP-REAL 3)

for p1 being FinSequence of 1 -tuples_on REAL

for uf being FinSequence of F_Real

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & p1 = N * uf holds

p1 . i = <*((N * (<*uf*> @)) * (i,1))*>

proof end;

Lem03: for i being Nat

for r being Real

for u, v being Element of (TOP-REAL 3)

for pf, uf being FinSequence of F_Real

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & r <> 0 & v = r * u holds

(N * (<*uf*> @)) * (i,1) = (1 / r) * ((Line (N,i)) "*" pf)

proof end;

Lem04: for i being Nat

for r being Real

for u, v being Element of (TOP-REAL 3)

for p1 being FinSequence of 1 -tuples_on REAL

for pf, uf being FinSequence of F_Real

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u holds

(p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)

proof end;

Lem05: for i being Nat

for v being Element of (TOP-REAL 3)

for pf being FinSequence of F_Real

for N being Matrix of 3,F_Real st i in Seg 3 & pf = v holds

(Line (N,i)) "*" pf = ((N * pf) . i) . 1

proof end;

registration
end;

registration
end;

registration

let n be Nat;

let K be Field;

let N1, N2 be invertible Matrix of n,K;

coherence

N1 * N2 is invertible by MATRIX_6:36;

end;
let K be Field;

let N1, N2 be invertible Matrix of n,K;

coherence

N1 * N2 is invertible by MATRIX_6:36;

theorem Th14: :: ANPROJ_9:13

for N1, N2 being invertible Matrix of 3,F_Real

for P being Point of (ProjectiveSpace (TOP-REAL 3)) holds (homography N1) . ((homography N2) . P) = (homography (N1 * N2)) . P

for P being Point of (ProjectiveSpace (TOP-REAL 3)) holds (homography N1) . ((homography N2) . P) = (homography (N1 * N2)) . P

proof end;

theorem Th16: :: ANPROJ_9:15

for N being invertible Matrix of 3,F_Real

for P being Point of (ProjectiveSpace (TOP-REAL 3)) holds

( (homography N) . ((homography (N ~)) . P) = P & (homography (N ~)) . ((homography N) . P) = P )

for P being Point of (ProjectiveSpace (TOP-REAL 3)) holds

( (homography N) . ((homography (N ~)) . P) = P & (homography (N ~)) . ((homography N) . P) = P )

proof end;

theorem :: ANPROJ_9:16

for N being invertible Matrix of 3,F_Real

for P1, P2 being Point of (ProjectiveSpace (TOP-REAL 3)) st (homography N) . P1 = (homography N) . P2 holds

P1 = P2

for P1, P2 being Point of (ProjectiveSpace (TOP-REAL 3)) st (homography N) . P1 = (homography N) . P2 holds

P1 = P2

proof end;

Lem06: for a being non zero Element of F_Real

for uf being FinSequence of F_Real st len uf = 3 holds

(a * (1. (F_Real,3))) * (<*uf*> @) = a * (<*uf*> @)

proof end;

theorem Th17: :: ANPROJ_9:17

for N being invertible Matrix of 3,F_Real

for P being Point of (ProjectiveSpace (TOP-REAL 3))

for a being non zero Element of F_Real st a * (1. (F_Real,3)) = N holds

(homography N) . P = P

for P being Point of (ProjectiveSpace (TOP-REAL 3))

for a being non zero Element of F_Real st a * (1. (F_Real,3)) = N holds

(homography N) . P = P

proof end;

definition

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

end;

func EnsHomography3 -> set equals :: ANPROJ_9:def 1

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

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

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

:: deftheorem defines EnsHomography3 ANPROJ_9:def 1 :

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

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

registration
end;

definition

let h1, h2 be Element of EnsHomography3 ;

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

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

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

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

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

b_{1} = b_{2}

end;
func h1 (*) h2 -> Element of EnsHomography3 means :Def01: :: ANPROJ_9:def 2

ex N1, N2 being invertible Matrix of 3,F_Real st

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

existence ex N1, N2 being invertible Matrix of 3,F_Real st

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

ex b

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

proof end;

uniqueness for b

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

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

b

proof end;

:: deftheorem Def01 defines (*) ANPROJ_9:def 2 :

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

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

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

for h1, h2, b

( b

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

theorem Th18: :: ANPROJ_9:18

for N1, N2 being invertible Matrix of 3,F_Real

for h1, h2 being Element of EnsHomography3 st h1 = homography N1 & h2 = homography N2 holds

homography (N1 * N2) = h1 (*) h2

for h1, h2 being Element of EnsHomography3 st h1 = homography N1 & h2 = homography N2 holds

homography (N1 * N2) = h1 (*) h2

proof end;

definition

ex b_{1} being BinOp of EnsHomography3 st

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

uniqueness

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

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

end;

func BinOpHomography3 -> BinOp of EnsHomography3 means :Def02: :: ANPROJ_9:def 3

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

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

ex b

for h1, h2 being Element of EnsHomography3 holds b

uniqueness

for b

b

:: deftheorem Def02 defines BinOpHomography3 ANPROJ_9:def 3 :

for b_{1} being BinOp of EnsHomography3 holds

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

for b

( b

definition

multMagma(# EnsHomography3,BinOpHomography3 #) is strict multMagma ;

end;

func GroupHomography3 -> strict multMagma equals :: ANPROJ_9:def 4

multMagma(# EnsHomography3,BinOpHomography3 #);

coherence multMagma(# EnsHomography3,BinOpHomography3 #);

multMagma(# EnsHomography3,BinOpHomography3 #) is strict multMagma ;

:: deftheorem defines GroupHomography3 ANPROJ_9:def 4 :

GroupHomography3 = multMagma(# EnsHomography3,BinOpHomography3 #);

GroupHomography3 = multMagma(# EnsHomography3,BinOpHomography3 #);

set GH3 = GroupHomography3 ;

Lm1: now :: thesis: for e being Element of GroupHomography3 st e = homography (1. (F_Real,3)) holds

for h being Element of GroupHomography3 holds

( h * e = h & e * h = h )

for h being Element of GroupHomography3 holds

( h * e = h & e * h = h )

let e be Element of GroupHomography3; :: thesis: ( e = homography (1. (F_Real,3)) implies for h being Element of GroupHomography3 holds

( h * e = h & e * h = h ) )

assume A1: e = homography (1. (F_Real,3)) ; :: thesis: for h being Element of GroupHomography3 holds

( h * e = h & e * h = h )

let h be Element of GroupHomography3; :: thesis: ( h * e = h & e * h = h )

reconsider h1 = h, h2 = e as Element of EnsHomography3 ;

consider N1, N2 being invertible Matrix of 3,F_Real such that

A10: h1 = homography N1 and

A11: h2 = homography N2 and

A12: h1 (*) h2 = homography (N1 * N2) by Def01;

homography (N1 * N2) = homography N1

consider N2, N1 being invertible Matrix of 3,F_Real such that

A15: h2 = homography N2 and

A16: h1 = homography N1 and

A17: h2 (*) h1 = homography (N2 * N1) by Def01;

homography (N2 * N1) = homography N1

end;
( h * e = h & e * h = h ) )

assume A1: e = homography (1. (F_Real,3)) ; :: thesis: for h being Element of GroupHomography3 holds

( h * e = h & e * h = h )

let h be Element of GroupHomography3; :: thesis: ( h * e = h & e * h = h )

reconsider h1 = h, h2 = e as Element of EnsHomography3 ;

consider N1, N2 being invertible Matrix of 3,F_Real such that

A10: h1 = homography N1 and

A11: h2 = homography N2 and

A12: h1 (*) h2 = homography (N1 * N2) by Def01;

homography (N1 * N2) = homography N1

proof

hence
h * e = h
by Def02, A10, A12; :: thesis: e * h = h
dom (homography (N1 * N2)) = the carrier of (ProjectiveSpace (TOP-REAL 3))
by FUNCT_2:def 1;

then A14: dom (homography (N1 * N2)) = dom (homography N1) by FUNCT_2:def 1;

for x being object st x in dom (homography N1) holds

(homography (N1 * N2)) . x = (homography N1) . x

end;
then A14: dom (homography (N1 * N2)) = dom (homography N1) by FUNCT_2:def 1;

for x being object st x in dom (homography N1) holds

(homography (N1 * N2)) . x = (homography N1) . x

proof

hence
homography (N1 * N2) = homography N1
by A14, FUNCT_1:def 11; :: thesis: verum
let x be object ; :: thesis: ( x in dom (homography N1) implies (homography (N1 * N2)) . x = (homography N1) . x )

assume x in dom (homography N1) ; :: thesis: (homography (N1 * N2)) . x = (homography N1) . x

then reconsider xf = x as Point of (ProjectiveSpace (TOP-REAL 3)) ;

(homography (N1 * N2)) . xf = (homography N1) . ((homography N2) . xf) by Th14

.= (homography N1) . xf by A1, A11, Th15 ;

hence (homography (N1 * N2)) . x = (homography N1) . x ; :: thesis: verum

end;
assume x in dom (homography N1) ; :: thesis: (homography (N1 * N2)) . x = (homography N1) . x

then reconsider xf = x as Point of (ProjectiveSpace (TOP-REAL 3)) ;

(homography (N1 * N2)) . xf = (homography N1) . ((homography N2) . xf) by Th14

.= (homography N1) . xf by A1, A11, Th15 ;

hence (homography (N1 * N2)) . x = (homography N1) . x ; :: thesis: verum

consider N2, N1 being invertible Matrix of 3,F_Real such that

A15: h2 = homography N2 and

A16: h1 = homography N1 and

A17: h2 (*) h1 = homography (N2 * N1) by Def01;

homography (N2 * N1) = homography N1

proof

hence
e * h = h
by Def02, A16, A17; :: thesis: verum
dom (homography (N2 * N1)) = the carrier of (ProjectiveSpace (TOP-REAL 3))
by FUNCT_2:def 1;

then A18: dom (homography (N2 * N1)) = dom (homography N1) by FUNCT_2:def 1;

for x being object st x in dom (homography N1) holds

(homography (N2 * N1)) . x = (homography N1) . x

end;
then A18: dom (homography (N2 * N1)) = dom (homography N1) by FUNCT_2:def 1;

for x being object st x in dom (homography N1) holds

(homography (N2 * N1)) . x = (homography N1) . x

proof

hence
homography (N2 * N1) = homography N1
by A18, FUNCT_1:def 11; :: thesis: verum
let x be object ; :: thesis: ( x in dom (homography N1) implies (homography (N2 * N1)) . x = (homography N1) . x )

assume x in dom (homography N1) ; :: thesis: (homography (N2 * N1)) . x = (homography N1) . x

then reconsider xf = x as Point of (ProjectiveSpace (TOP-REAL 3)) ;

(homography (N2 * N1)) . xf = (homography N2) . ((homography N1) . xf) by Th14

.= (homography N1) . xf by A1, A15, Th15 ;

hence (homography (N2 * N1)) . x = (homography N1) . x ; :: thesis: verum

end;
assume x in dom (homography N1) ; :: thesis: (homography (N2 * N1)) . x = (homography N1) . x

then reconsider xf = x as Point of (ProjectiveSpace (TOP-REAL 3)) ;

(homography (N2 * N1)) . xf = (homography N2) . ((homography N1) . xf) by Th14

.= (homography N1) . xf by A1, A15, Th15 ;

hence (homography (N2 * N1)) . x = (homography N1) . x ; :: thesis: verum

Lm2: now :: thesis: for e, h, g being Element of GroupHomography3

for N, Ng being invertible Matrix of 3,F_Real st h = homography N & g = homography Ng & Ng = N ~ & e = homography (1. (F_Real,3)) holds

( h * g = e & g * h = e )

for N, Ng being invertible Matrix of 3,F_Real st h = homography N & g = homography Ng & Ng = N ~ & e = homography (1. (F_Real,3)) holds

( h * g = e & g * h = e )

let e, h, g be Element of GroupHomography3; :: thesis: for N, Ng being invertible Matrix of 3,F_Real st h = homography N & g = homography Ng & Ng = N ~ & e = homography (1. (F_Real,3)) holds

( h * g = e & g * h = e )

let N, Ng be invertible Matrix of 3,F_Real; :: thesis: ( h = homography N & g = homography Ng & Ng = N ~ & e = homography (1. (F_Real,3)) implies ( h * g = e & g * h = e ) )

assume that

A9: h = homography N and

B1: g = homography Ng and

B2: Ng = N ~ and

B3: e = homography (1. (F_Real,3)) ; :: thesis: ( h * g = e & g * h = e )

reconsider h1 = h as Element of EnsHomography3 ;

A23: Ng is_reverse_of N by B2, MATRIX_6:def 4;

reconsider g1 = g as Element of EnsHomography3 ;

consider N1, N2 being invertible Matrix of 3,F_Real such that

A19: h1 = homography N1 and

A20: g1 = homography N2 and

A21: h1 (*) g1 = homography (N1 * N2) by Def01;

homography (N1 * N2) = homography (N * Ng)

hence h * g = e by Def02; :: thesis: g * h = e

consider N1, N2 being invertible Matrix of 3,F_Real such that

A27: g1 = homography N1 and

A28: h1 = homography N2 and

A29: g1 (*) h1 = homography (N1 * N2) by Def01;

homography (N1 * N2) = homography (Ng * N)

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

end;
( h * g = e & g * h = e )

let N, Ng be invertible Matrix of 3,F_Real; :: thesis: ( h = homography N & g = homography Ng & Ng = N ~ & e = homography (1. (F_Real,3)) implies ( h * g = e & g * h = e ) )

assume that

A9: h = homography N and

B1: g = homography Ng and

B2: Ng = N ~ and

B3: e = homography (1. (F_Real,3)) ; :: thesis: ( h * g = e & g * h = e )

reconsider h1 = h as Element of EnsHomography3 ;

A23: Ng is_reverse_of N by B2, MATRIX_6:def 4;

reconsider g1 = g as Element of EnsHomography3 ;

consider N1, N2 being invertible Matrix of 3,F_Real such that

A19: h1 = homography N1 and

A20: g1 = homography N2 and

A21: h1 (*) g1 = homography (N1 * N2) by Def01;

homography (N1 * N2) = homography (N * Ng)

proof

end;

then
h1 (*) g1 = e
by B3, A21, A23, MATRIX_6:def 2;
now :: thesis: ( dom (homography (N1 * N2)) = dom (homography (N * Ng)) & ( for x being object st x in dom (homography (N1 * N2)) holds

(homography (N1 * N2)) . x = (homography (N * Ng)) . x ) )

hence
homography (N1 * N2) = homography (N * Ng)
by FUNCT_1:def 11; :: thesis: verum(homography (N1 * N2)) . x = (homography (N * Ng)) . x ) )

dom (homography (N1 * N2)) = the carrier of (ProjectiveSpace (TOP-REAL 3))
by FUNCT_2:def 1;

hence dom (homography (N1 * N2)) = dom (homography (N * Ng)) by FUNCT_2:def 1; :: thesis: for x being object st x in dom (homography (N1 * N2)) holds

(homography (N1 * N2)) . x = (homography (N * Ng)) . x

thus for x being object st x in dom (homography (N1 * N2)) holds

(homography (N1 * N2)) . x = (homography (N * Ng)) . x :: thesis: verum

end;
hence dom (homography (N1 * N2)) = dom (homography (N * Ng)) by FUNCT_2:def 1; :: thesis: for x being object st x in dom (homography (N1 * N2)) holds

(homography (N1 * N2)) . x = (homography (N * Ng)) . x

thus for x being object st x in dom (homography (N1 * N2)) holds

(homography (N1 * N2)) . x = (homography (N * Ng)) . x :: thesis: verum

proof

let x be object ; :: thesis: ( x in dom (homography (N1 * N2)) implies (homography (N1 * N2)) . x = (homography (N * Ng)) . x )

assume x in dom (homography (N1 * N2)) ; :: thesis: (homography (N1 * N2)) . x = (homography (N * Ng)) . x

then reconsider xf = x as Point of (ProjectiveSpace (TOP-REAL 3)) ;

(homography (N1 * N2)) . xf = (homography N) . ((homography Ng) . xf) by Th14, A19, A9, A20, B1

.= (homography (N * Ng)) . xf by Th14 ;

hence (homography (N1 * N2)) . x = (homography (N * Ng)) . x ; :: thesis: verum

end;
assume x in dom (homography (N1 * N2)) ; :: thesis: (homography (N1 * N2)) . x = (homography (N * Ng)) . x

then reconsider xf = x as Point of (ProjectiveSpace (TOP-REAL 3)) ;

(homography (N1 * N2)) . xf = (homography N) . ((homography Ng) . xf) by Th14, A19, A9, A20, B1

.= (homography (N * Ng)) . xf by Th14 ;

hence (homography (N1 * N2)) . x = (homography (N * Ng)) . x ; :: thesis: verum

hence h * g = e by Def02; :: thesis: g * h = e

consider N1, N2 being invertible Matrix of 3,F_Real such that

A27: g1 = homography N1 and

A28: h1 = homography N2 and

A29: g1 (*) h1 = homography (N1 * N2) by Def01;

homography (N1 * N2) = homography (Ng * N)

proof

end;

then
g1 (*) h1 = e
by A29, A23, B3, MATRIX_6:def 2;
now :: thesis: ( dom (homography (N1 * N2)) = dom (homography (Ng * N)) & ( for x being object st x in dom (homography (N1 * N2)) holds

(homography (N1 * N2)) . x = (homography (Ng * N)) . x ) )

hence
homography (N1 * N2) = homography (Ng * N)
by FUNCT_1:def 11; :: thesis: verum(homography (N1 * N2)) . x = (homography (Ng * N)) . x ) )

dom (homography (N1 * N2)) = the carrier of (ProjectiveSpace (TOP-REAL 3))
by FUNCT_2:def 1;

hence dom (homography (N1 * N2)) = dom (homography (Ng * N)) by FUNCT_2:def 1; :: thesis: for x being object st x in dom (homography (N1 * N2)) holds

(homography (N1 * N2)) . x = (homography (Ng * N)) . x

thus for x being object st x in dom (homography (N1 * N2)) holds

(homography (N1 * N2)) . x = (homography (Ng * N)) . x :: thesis: verum

end;
hence dom (homography (N1 * N2)) = dom (homography (Ng * N)) by FUNCT_2:def 1; :: thesis: for x being object st x in dom (homography (N1 * N2)) holds

(homography (N1 * N2)) . x = (homography (Ng * N)) . x

thus for x being object st x in dom (homography (N1 * N2)) holds

(homography (N1 * N2)) . x = (homography (Ng * N)) . x :: thesis: verum

proof

let x be object ; :: thesis: ( x in dom (homography (N1 * N2)) implies (homography (N1 * N2)) . x = (homography (Ng * N)) . x )

assume x in dom (homography (N1 * N2)) ; :: thesis: (homography (N1 * N2)) . x = (homography (Ng * N)) . x

then reconsider xf = x as Point of (ProjectiveSpace (TOP-REAL 3)) ;

(homography (N1 * N2)) . xf = (homography Ng) . ((homography N) . xf) by Th14, A27, A9, A28, B1

.= (homography (Ng * N)) . xf by Th14 ;

hence (homography (N1 * N2)) . x = (homography (Ng * N)) . x ; :: thesis: verum

end;
assume x in dom (homography (N1 * N2)) ; :: thesis: (homography (N1 * N2)) . x = (homography (Ng * N)) . x

then reconsider xf = x as Point of (ProjectiveSpace (TOP-REAL 3)) ;

(homography (N1 * N2)) . xf = (homography Ng) . ((homography N) . xf) by Th14, A27, A9, A28, B1

.= (homography (Ng * N)) . xf by Th14 ;

hence (homography (N1 * N2)) . x = (homography (Ng * N)) . x ; :: thesis: verum

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

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

homography (1. (F_Real,3)) in EnsHomography3

;

then reconsider e = homography (1. (F_Real,3)) as Element of GroupHomography3 ;

registration

coherence

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

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

proof end;

theorem :: ANPROJ_9:21

for h, g being Element of GroupHomography3

for N, Ng being invertible Matrix of 3,F_Real st h = homography N & g = homography Ng & Ng = N ~ holds

g = h "

for N, Ng being invertible Matrix of 3,F_Real st h = homography N & g = homography Ng & Ng = N ~ holds

g = h "

proof end;

definition

coherence

Dir |[1,0,0]| is Point of (ProjectiveSpace (TOP-REAL 3)) by Th11, ANPROJ_1:26;

coherence

Dir |[0,1,0]| is Point of (ProjectiveSpace (TOP-REAL 3)) by Th11, ANPROJ_1:26;

coherence

Dir |[0,0,1]| is Point of (ProjectiveSpace (TOP-REAL 3)) by Th11, ANPROJ_1:26;

coherence

Dir |[1,1,1]| is Point of (ProjectiveSpace (TOP-REAL 3)) by Th11, ANPROJ_1:26;

end;
Dir |[1,0,0]| is Point of (ProjectiveSpace (TOP-REAL 3)) by Th11, ANPROJ_1:26;

coherence

Dir |[0,1,0]| is Point of (ProjectiveSpace (TOP-REAL 3)) by Th11, ANPROJ_1:26;

coherence

Dir |[0,0,1]| is Point of (ProjectiveSpace (TOP-REAL 3)) by Th11, ANPROJ_1:26;

coherence

Dir |[1,1,1]| is Point of (ProjectiveSpace (TOP-REAL 3)) by Th11, ANPROJ_1:26;

theorem :: ANPROJ_9:22

( Dir100 <> Dir010 & Dir100 <> Dir001 & Dir100 <> Dir111 & Dir010 <> Dir001 & Dir010 <> Dir111 & Dir001 <> Dir111 )

proof end;

registration

let a be non zero Element of F_Real;

let N be invertible Matrix of 3,F_Real;

coherence

for b_{1} being Matrix of 3,F_Real st b_{1} = a * N holds

b_{1} is invertible

end;
let N be invertible Matrix of 3,F_Real;

coherence

for b

b

proof end;

theorem :: ANPROJ_9:23

for N1 being invertible Matrix of 3,F_Real

for P being Point of (ProjectiveSpace (TOP-REAL 3))

for a being non zero Element of F_Real holds (homography (a * N1)) . P = (homography N1) . P

for P being Point of (ProjectiveSpace (TOP-REAL 3))

for a being non zero Element of F_Real holds (homography (a * N1)) . P = (homography N1) . P

proof end;

theorem Th20: :: ANPROJ_9:24

for P1, P2, P3 being Point of (ProjectiveSpace (TOP-REAL 3)) st not P1,P2,P3 are_collinear holds

ex N being invertible Matrix of 3,F_Real st

( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 )

ex N being invertible Matrix of 3,F_Real st

( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 )

proof end;

theorem Th21: :: ANPROJ_9:25

for N being invertible Matrix of 3,F_Real

for a, b, c being non zero Element of F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds

( (homography N) . Dir100 = Dir100 & (homography N) . Dir010 = Dir010 & (homography N) . Dir001 = Dir001 )

for a, b, c being non zero Element of F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds

( (homography N) . Dir100 = Dir100 & (homography N) . Dir010 = Dir010 & (homography N) . Dir001 = Dir001 )

proof end;

theorem Th22: :: ANPROJ_9:26

for P being Point of (ProjectiveSpace (TOP-REAL 3)) ex a, b, c being Element of F_Real st

( P = Dir |[a,b,c]| & ( a <> 0 or b <> 0 or c <> 0 ) )

( P = Dir |[a,b,c]| & ( a <> 0 or b <> 0 or c <> 0 ) )

proof end;

Lem07: for a, b, c being Element of F_Real

for P being Point of (ProjectiveSpace (TOP-REAL 3)) st P = Dir |[a,b,c]| & ( a <> 0 or b <> 0 or c <> 0 ) holds

( ( not Dir100 , Dir010 ,P are_collinear implies c <> 0 ) & ( not Dir100 , Dir001 ,P are_collinear implies b <> 0 ) & ( not Dir010 , Dir001 ,P are_collinear implies a <> 0 ) )

proof end;

theorem Th23: :: ANPROJ_9:27

for P being Point of (ProjectiveSpace (TOP-REAL 3)) st not Dir100 , Dir010 ,P are_collinear & not Dir100 , Dir001 ,P are_collinear & not Dir010 , Dir001 ,P are_collinear holds

ex a, b, c being non zero Element of F_Real st P = Dir |[a,b,c]|

ex a, b, c being non zero Element of F_Real st P = Dir |[a,b,c]|

proof end;

theorem Th24: :: ANPROJ_9:28

for a, b, c, ia, ib, ic being non zero Element of F_Real

for P being Point of (ProjectiveSpace (TOP-REAL 3))

for N being invertible Matrix of 3,F_Real st P = Dir |[a,b,c]| & ia = 1 / a & ib = 1 / b & ic = 1 / c & N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> holds

(homography N) . P = Dir |[1,1,1]|

for P being Point of (ProjectiveSpace (TOP-REAL 3))

for N being invertible Matrix of 3,F_Real st P = Dir |[a,b,c]| & ia = 1 / a & ib = 1 / b & ic = 1 / c & N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> holds

(homography N) . P = Dir |[1,1,1]|

proof end;

theorem Th25: :: ANPROJ_9:29

for P being Point of (ProjectiveSpace (TOP-REAL 3)) st not Dir100 , Dir010 ,P are_collinear & not Dir100 , Dir001 ,P are_collinear & not Dir010 , Dir001 ,P are_collinear holds

ex a, b, c being non zero Element of F_Real st

for N being invertible Matrix of 3,F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds

(homography N) . P = Dir111

ex a, b, c being non zero Element of F_Real st

for N being invertible Matrix of 3,F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds

(homography N) . P = Dir111

proof end;

theorem Th26: :: ANPROJ_9:30

for P1, P2, P3, P4 being Point of (ProjectiveSpace (TOP-REAL 3)) st not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear holds

ex N being invertible Matrix of 3,F_Real st

( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 & (homography N) . P4 = Dir111 )

ex N being invertible Matrix of 3,F_Real st

( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 & (homography N) . P4 = Dir111 )

proof end;

theorem :: ANPROJ_9:31

for P1, P2, P3, P4, Q1, Q2, Q3, Q4 being Point of (ProjectiveSpace (TOP-REAL 3)) st not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear & not Q1,Q2,Q3 are_collinear & not Q1,Q2,Q4 are_collinear & not Q1,Q3,Q4 are_collinear & not Q2,Q3,Q4 are_collinear holds

ex N being invertible Matrix of 3,F_Real st

( (homography N) . P1 = Q1 & (homography N) . P2 = Q2 & (homography N) . P3 = Q3 & (homography N) . P4 = Q4 )

ex N being invertible Matrix of 3,F_Real st

( (homography N) . P1 = Q1 & (homography N) . P2 = Q2 & (homography N) . P3 = Q3 & (homography N) . P4 = Q4 )

proof end;