:: Group of Homography in Real Projective Plane
:: by Roland Coghetto
::
:: Received March 17, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users


theorem Th01: :: ANPROJ_9:1
1. (F_Real,3) = <*<*1,0,0*>,<*0,1,0*>,<*0,0,1*>*>
proof end;

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
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
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*> )
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*> )
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))*>*>
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))*>*>
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) )
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 Th11: :: ANPROJ_9:10
( not |[1,0,0]| is zero & not |[0,1,0]| is zero & not |[0,0,1]| is zero & not |[1,1,1]| is zero ) by EUCLID_5:4, FINSEQ_1:78;

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;

theorem Th13: :: ANPROJ_9:12
( <e1> <> 0. (TOP-REAL 3) & <e2> <> 0. (TOP-REAL 3) & <e3> <> 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
let n be Nat;
cluster 1. (F_Real,n) -> invertible ;
coherence
1. (F_Real,n) is invertible ;
end;

registration
let n be Nat;
let M be invertible Matrix of n,F_Real;
cluster M ~ -> invertible ;
coherence
M ~ is invertible ;
end;

registration
let n be Nat;
let K be Field;
let N1, N2 be invertible Matrix of n,K;
cluster N1 * N2 -> invertible ;
coherence
N1 * N2 is invertible by MATRIX_6:36;
end;

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

theorem Th15: :: ANPROJ_9:14
for P being Point of (ProjectiveSpace (TOP-REAL 3)) holds (homography (1. (F_Real,3))) . P = 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 )
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
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
proof end;

definition
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 } is set ;
end;

:: deftheorem defines EnsHomography3 ANPROJ_9:def 1 :
EnsHomography3 = { (homography N) where N is invertible Matrix of 3,F_Real : verum } ;

registration
cluster EnsHomography3 -> non empty ;
coherence
not EnsHomography3 is empty
proof end;
end;

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

:: deftheorem Def01 defines (*) ANPROJ_9:def 2 :
for h1, h2, b3 being Element of EnsHomography3 holds
( b3 = h1 (*) h2 iff ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = homography N1 & h2 = homography N2 & b3 = homography (N1 * N2) ) );

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

theorem Ta1: :: ANPROJ_9:19
for x, y, z being Element of EnsHomography3 holds (x (*) y) (*) z = x (*) (y (*) z)
proof end;

definition
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
ex b1 being BinOp of EnsHomography3 st
for h1, h2 being Element of EnsHomography3 holds b1 . (h1,h2) = h1 (*) h2 from BINOP_1:sch 4();
uniqueness
for b1, b2 being BinOp of EnsHomography3 st ( for h1, h2 being Element of EnsHomography3 holds b1 . (h1,h2) = h1 (*) h2 ) & ( for h1, h2 being Element of EnsHomography3 holds b2 . (h1,h2) = h1 (*) h2 ) holds
b1 = b2 from BINOP_2:sch 2();
end;

:: deftheorem Def02 defines BinOpHomography3 ANPROJ_9:def 3 :
for b1 being BinOp of EnsHomography3 holds
( b1 = BinOpHomography3 iff for h1, h2 being Element of EnsHomography3 holds b1 . (h1,h2) = h1 (*) h2 );

definition
func GroupHomography3 -> strict multMagma equals :: ANPROJ_9:def 4
 multMagma(# EnsHomography3,BinOpHomography3 #);
coherence
multMagma(# EnsHomography3,BinOpHomography3 #) is strict multMagma ;
end;

:: deftheorem defines GroupHomography3 ANPROJ_9:def 4 :
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 )
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
proof
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
proof
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;
hence homography (N1 * N2) = homography N1 by A14, FUNCT_1:def 11; :: thesis: verum
end;
hence h * e = h by Def02, A10, A12; :: thesis: e * h = h
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
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
proof
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;
hence homography (N2 * N1) = homography N1 by A18, FUNCT_1:def 11; :: thesis: verum
end;
hence e * h = h by Def02, A16, A17; :: thesis: verum
end;

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 )
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)
proof
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 ) )
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
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;
end;
hence homography (N1 * N2) = homography (N * Ng) by FUNCT_1:def 11; :: thesis: verum
end;
then h1 (*) g1 = e by B3, A21, A23, MATRIX_6:def 2;
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
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 ) )
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
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;
end;
hence homography (N1 * N2) = homography (Ng * N) by FUNCT_1:def 11; :: thesis: verum
end;
then g1 (*) h1 = e by A29, A23, B3, MATRIX_6:def 2;
hence g * h = e by Def02; :: thesis: verum
end;

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
cluster GroupHomography3 -> non empty strict Group-like associative ;
coherence
( not GroupHomography3 is empty & GroupHomography3 is associative & GroupHomography3 is Group-like )
proof end;
end;

theorem Ta2: :: ANPROJ_9:20
1_ GroupHomography3 = homography (1. (F_Real,3))
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 "
proof end;

definition
func Dir100 -> Point of (ProjectiveSpace (TOP-REAL 3)) equals :: ANPROJ_9:def 5
 Dir |[1,0,0]|;
coherence
Dir |[1,0,0]| is Point of (ProjectiveSpace (TOP-REAL 3)) by Th11, ANPROJ_1:26;
func Dir010 -> Point of (ProjectiveSpace (TOP-REAL 3)) equals :: ANPROJ_9:def 6
 Dir |[0,1,0]|;
coherence
Dir |[0,1,0]| is Point of (ProjectiveSpace (TOP-REAL 3)) by Th11, ANPROJ_1:26;
func Dir001 -> Point of (ProjectiveSpace (TOP-REAL 3)) equals :: ANPROJ_9:def 7
 Dir |[0,0,1]|;
coherence
Dir |[0,0,1]| is Point of (ProjectiveSpace (TOP-REAL 3)) by Th11, ANPROJ_1:26;
func Dir111 -> Point of (ProjectiveSpace (TOP-REAL 3)) equals :: ANPROJ_9:def 8
 Dir |[1,1,1]|;
coherence
Dir |[1,1,1]| is Point of (ProjectiveSpace (TOP-REAL 3)) by Th11, ANPROJ_1:26;
end;

:: deftheorem defines Dir100 ANPROJ_9:def 5 :
Dir100 = Dir |[1,0,0]|;

:: deftheorem defines Dir010 ANPROJ_9:def 6 :
Dir010 = Dir |[0,1,0]|;

:: deftheorem defines Dir001 ANPROJ_9:def 7 :
Dir001 = Dir |[0,0,1]|;

:: deftheorem defines Dir111 ANPROJ_9:def 8 :
Dir111 = Dir |[1,1,1]|;

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;
cluster a * N -> invertible for Matrix of 3,F_Real;
coherence
for b1 being Matrix of 3,F_Real st b1 = a * N holds
b1 is invertible
proof end;
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
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 )
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 )
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 ) )
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]|
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]|
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
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 )
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 )
proof end;