:: Group of Homography in Real Projective Plane
:: by Roland Coghetto
::
:: Received March 17, 2017
:: Copyright (c) 2017-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies REAL_1, XCMPLX_0, ANPROJ_1, PENCIL_1, MCART_1, EUCLID_5,
ALGSTR_0, ARYTM_1, ARYTM_3, CARD_1, EUCLID, FINSEQ_1, FUNCT_1, FVSUM_1,
INCSP_1, MATRIX_1, NAT_1, NUMBERS, PRE_TOPC, QC_LANG1, RELAT_1, STRUCT_0,
SUBSET_1, SUPINF_2, TREES_1, VECTSP_1, XBOOLE_0, BINOP_1, EUCLID_8,
MATRIX_0, MATRIX_6, MESFUNC1, FINSEQ_2, ANPROJ_8, GROUP_1, MONOID_0,
ANPROJ_9;
notations RELSET_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, FUNCT_1,
BINOP_1, FINSEQ_1, FINSEQ_4, PRE_TOPC, RVSUM_1, EUCLID, ANPROJ_1, TARSKI,
FUNCT_2, VECTSP_1, MATRIX_0, MATRIX_1, MATRIX_3, MATRIX13, FVSUM_1,
GROUP_1, XBOOLE_0, STRUCT_0, ALGSTR_0, RLVECT_1, COLLSP, EUCLID_8,
EUCLID_5, FINSEQ_2, LAPLACE, MATRIX_6, ANPROJ_8;
constructors RELSET_1, BINOP_2, FINSEQ_4, MONOID_0, EUCLID_5, FVSUM_1,
MATRIX13, EUCLID_8, LAPLACE, ANPROJ_8, MATRPROB, MATRIX_3;
registrations XBOOLE_0, ANPROJ_1, FUNCT_1, STRUCT_0, VECTSP_1, REVROT_1,
MATRIX_0, RELSET_1, XREAL_0, MEMBERED, MONOID_0, EUCLID, VALUED_0,
FINSEQ_1, MATRIX_6, NUMBERS, RLVECT_1, MATRIX_3;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
definitions GROUP_1;
equalities VECTSP_1, ALGSTR_0, STRUCT_0;
expansions STRUCT_0;
theorems EUCLID_5, ANPROJ_1, ANPROJ_2, XREAL_0, EUCLID, MATRIXR2, XCMPLX_1,
RVSUM_1, MATRIX_0, FINSEQ_1, FINSEQ_3, EUCLID_8, LAPLACE, MATRIX_6,
MATRIXR1, MATRIX_3, FUNCT_1, FUNCT_2, ANPROJ_8, GROUP_1, MATRIX15,
MATRPROB;
schemes BINOP_1, BINOP_2;
begin :: Preliminaries
reserve i,n for Nat;
reserve r for Real;
reserve ra for Element of F_Real;
reserve a,b,c for non zero Element of F_Real;
reserve u,v for Element of TOP-REAL 3;
reserve p1 for FinSequence of (1-tuples_on REAL);
reserve pf,uf for FinSequence of F_Real;
reserve N for Matrix of 3,F_Real;
reserve K for Field;
reserve k for Element of K;
theorem Th01:
1.(F_Real,3) = <* <* 1,0,0 *>,
<* 0,1,0 *>,
<* 0,0,1 *> *>
proof
A1: len 1.(F_Real,3) = 3 by MATRIX_0:23;
1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1;
then (1.(F_Real,3)).1 = Line(1.(F_Real,3),1) &
(1.(F_Real,3)).2 = Line(1.(F_Real,3),2) &
(1.(F_Real,3)).3 = Line(1.(F_Real,3),3) by MATRIX_0:52;
hence thesis by A1,FINSEQ_1:45,ANPROJ_8:68;
end;
theorem Th02:
ra * N = (ra * 1.(F_Real,3)) * N
proof
width 1.(F_Real,3) = 3 by MATRIX_0:24; then
A1: width 1.(F_Real,3) = len N by MATRIX_0:24;
ra * N = ra * (1.(F_Real,3) * N) by MATRIX_3:18;
hence thesis by A1,MATRIX15:1;
end;
theorem Th04:
r <> 0 & u is non zero implies r * u is non zero
proof
assume that
A1: r <> 0 and
A2: u is non zero;
r * u <> 0.TOP-REAL 3
proof
assume
A3: r * u = 0.TOP-REAL 3;
u = 1 * u by RVSUM_1:52
.= (1/r * r) * u by A1,XCMPLX_1:87
.= 1/r * 0.TOP-REAL 3 by A3,RVSUM_1:49
.= 0.TOP-REAL 3;
hence contradiction by A2;
end;
hence thesis;
end;
theorem Th05:
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
let a11,a12,a13,a21,a22,a23,a31,a32,a33 be Element of F_Real;
let A be Matrix of 3,F_Real;
assume A = <* <* a11,a12,a13 *>, <* a21,a22,a23 *>, <* a31,a32,a33 *> *>;
then
A1: A.1 = <* a11,a12,a13 *> & A.2 = <* a21,a22,a23 *> &
A.3 = <* a31,a32,a33 *>;
1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1;
hence thesis by A1,MATRIX_0:52;
end;
theorem Th06:
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
let a11,a12,a13,a21,a22,a23,a31,a32,a33 be Element of F_Real;
let A be Matrix of 3,F_Real;
assume
A1: A = <* <* a11,a12,a13 *>, <* a21,a22,a23 *>, <* a31,a32,a33 *> *>;
|[ a11,a12,a13 ]| is Point of TOP-REAL 3 &
|[ a21,a22,a23 ]| is Point of TOP-REAL 3 &
|[ a31,a32,a33 ]| is Point of TOP-REAL 3;
then reconsider p = <* a11,a12,a13 *>, q = <* a21,a22,a23 *>,
r = <* a31,a32,a33 *> as Point of TOP-REAL 3;
p.1 = a11 & p.2 = a12 & p.3 = a13 & q.1 = a21 & q.2 = a22 & q.3 = a23 &
r.1 = a31 & r.2 = a32 & r.3 = a33;
then
A2: p`1 = a11 & p`2 = a12 & p`3 = a13 & q`1 = a21 & q`2 = a22 & q`3 = a23 &
r`1 = a31 & r`2 = a32 & r`3 = a33
by EUCLID_5:def 1,EUCLID_5:def 2,EUCLID_5:def 3;
A@ = <*<*p`1,q`1,r`1*>,<*p`2,q`2,r`2*>,<*p`3,q`3,r`3*>*>
by A1,ANPROJ_8:23; then
A3: Line(A@,1) = <* a11,a21,a31 *> & Line(A@,2) = <* a12,a22,a32 *> &
Line(A@,3) = <* a13,a23,a33 *> by A2,Th05;
A4: width A = 3 by MATRIX_0:24;
1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1;
hence thesis by A3,A4,MATRIX_0:59;
end;
theorem Th07:
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
let a11,a12,a13,a21,a22,a23,a31,a32,a33,
b11,b12,b13,b21,b22,b23,b31,b32,b33 be Element of F_Real;
let A,B be Matrix of 3,F_Real;
assume that
A1: A = <* <* a11,a12,a13 *>, <* a21,a22,a23 *>, <* a31,a32,a33 *> *> and
A2: B = <* <* b11,b12,b13 *>, <* b21,b22,b23 *>, <* b31,b32,b33 *> *>;
A3: width A = 3 & len B = 3 by MATRIX_0:23;
A4: [1,1] in Indices (A * B) & [1,2] in Indices (A * B) &
[1,3] in Indices (A * B) & [2,1] in Indices (A * B) &
[2,2] in Indices (A * B) & [2,3] in Indices (A * B) &
[3,1] in Indices (A * B) & [3,2] in Indices (A * B) &
[3,3] in Indices (A * B) by ANPROJ_8:1,MATRIX_0:23;
A5: Line(A,1) = <* a11,a12,a13 *> & Line(A,2) = <* a21,a22,a23 *> &
Line(A,3) = <* a31,a32,a33 *> by A1,Th05;
A6: Col(B,1) = <* b11,b21,b31 *> & Col(B,2) = <* b12,b22,b32 *> &
Col(B,3) = <* b13,b23,b33 *> by A2,Th06;
now
thus (A * B)*(1,1) = Line(A,1) "*" Col(B,1) by A3,A4,MATRIX_3:def 4
.= a11 * b11 + a12 * b21 + a13 * b31
by A5,A6,ANPROJ_8:7;
thus (A * B)*(1,2) = Line(A,1) "*" Col(B,2) by A3,A4,MATRIX_3:def 4
.= a11 * b12 + a12 * b22 + a13 * b32
by A5,A6,ANPROJ_8:7;
thus (A * B)*(1,3) = Line(A,1) "*" Col(B,3) by A3,A4,MATRIX_3:def 4
.= a11 * b13 + a12 * b23 + a13 * b33
by A5,A6,ANPROJ_8:7;
thus (A * B)*(2,1) = Line(A,2) "*" Col(B,1) by A3,A4,MATRIX_3:def 4
.= a21 * b11 + a22 * b21 + a23 * b31
by A5,A6,ANPROJ_8:7;
thus (A * B)*(2,2) = Line(A,2) "*" Col(B,2) by A3,A4,MATRIX_3:def 4
.= a21 * b12 + a22 * b22 + a23 * b32
by A5,A6,ANPROJ_8:7;
thus (A * B)*(2,3) = Line(A,2) "*" Col(B,3) by A3,A4,MATRIX_3:def 4
.= a21 * b13 + a22 * b23 + a23 * b33
by A5,A6,ANPROJ_8:7;
thus (A * B)*(3,1) = Line(A,3) "*" Col(B,1) by A3,A4,MATRIX_3:def 4
.= a31 * b11 + a32 * b21 + a33 * b31
by A5,A6,ANPROJ_8:7;
thus (A * B)*(3,2) = Line(A,3) "*" Col(B,2) by A3,A4,MATRIX_3:def 4
.= a31 * b12 + a32 * b22 + a33 * b32
by A5,A6,ANPROJ_8:7;
thus (A * B)*(3,3) = Line(A,3) "*" Col(B,3) by A3,A4,MATRIX_3:def 4
.= a31 * b13 + a32 * b23 + a33 * b33
by A5,A6,ANPROJ_8:7;
end;
hence thesis by MATRIXR2:37;
end;
theorem Th08:
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
let a11,a12,a13,a21,a22,a23,a31,a32,a33,b1,b2,b3 be Element of F_Real;
let A be Matrix of 3,3,F_Real;
let B be Matrix of 3,1,F_Real;
assume that
A1: A = <* <* a11,a12,a13 *>, <* a21,a22,a23 *>, <* a31,a32,a33 *> *> and
A2: B = <* <* b1 *>, <* b2 *>, <* b3 *> *>;
A3: width A = 3 & len B = 3 & len A = 3 & width B = 1 by MATRIX_0:23;
A4: len (A * B) = 3 & width (A * B) = 1 by A3,MATRIX_3:def 4;
A5: A * B is Matrix of 3,1,F_Real by A4,MATRIX_0:20;
then
A6: [1,1] in Indices (A * B) & [2,1] in Indices (A * B) &
[3,1] in Indices (A * B) by ANPROJ_8:2,MATRIX_0:23;
A7: Line(A,1) = <* a11,a12,a13 *> & Line(A,2) = <* a21,a22,a23 *> &
Line(A,3) = <* a31,a32,a33 *> by A1,Th05;
1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1; then
A8: 1 in dom B & 2 in dom B & 3 in dom B by FINSEQ_1:def 3,A3;
now
thus len Col(B,1) = 3 by A3,MATRIX_0:def 8;
[1,1] in Indices B by MATRIX_0:23,ANPROJ_8:2;
then consider p be FinSequence of F_Real such that
A9: p = B.1 and
A10: B*(1,1) = p.1 by MATRIX_0:def 5;
B*(1,1) = <*b1*>.1 by A9,A10,A2
.= b1;
hence Col(B,1).1 = b1 by A8,MATRIX_0:def 8;
[2,1] in Indices B by MATRIX_0:23,ANPROJ_8:2;
then consider p be FinSequence of F_Real such that
A11: p = B.2 and
A12: B*(2,1) = p.1 by MATRIX_0:def 5;
B*(2,1) = <*b2*>.1 by A11,A12,A2
.= b2;
hence Col(B,1).2 = b2 by A8,MATRIX_0:def 8;
[3,1] in Indices B by MATRIX_0:23,ANPROJ_8:2;
then consider p be FinSequence of F_Real such that
A13: p = B.3 and
A14: B*(3,1) = p.1 by MATRIX_0:def 5;
B*(3,1) = <*b3*>.1 by A13,A14,A2
.= b3;
hence Col(B,1).3 = b3 by A8,MATRIX_0:def 8;
end;
then
A15: Col(B,1) = <* b1,b2,b3 *> by FINSEQ_1:45;
now
thus (A * B)*(1,1) = Line(A,1) "*" Col(B,1) by A3,A6,MATRIX_3:def 4
.= a11 * b1 + a12 * b2 + a13 * b3 by A7,A15,ANPROJ_8:7;
thus (A * B)*(2,1) = Line(A,2) "*" Col(B,1) by A3,A6,MATRIX_3:def 4
.= a21 * b1 + a22 * b2 + a23 * b3 by A7,A15,ANPROJ_8:7;
thus (A * B)*(3,1) = Line(A,3) "*" Col(B,1) by A3,A6,MATRIX_3:def 4
.= a31 * b1 + a32 * b2 + a33 * b3 by A7,A15,ANPROJ_8:7;
end;
then
A16: Line(A * B,1) = <* a11 * b1 + a12 * b2 + a13 * b3 *> &
Line(A*B,2) = <* a21 * b1 + a22 * b2 + a23 * b3 *> &
Line(A*B,3) = <* a31 * b1 + a32 * b2 + a33 * b3 *> by A5,ANPROJ_8:90;
now
thus len (A * B) = 3 by A3,MATRIX_3:def 4;
1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1;
hence (A * B).1 = Line(A * B,1)&
(A * B).2 = Line(A * B,2)&
(A * B).3 = Line(A * B,3) by A5,MATRIX_0:52;
end;
hence thesis by A16,FINSEQ_1:45;
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
let a11,a12,a13,a21,a22,a23,a31,a32,a33,
b11,b12,b13,b21,b22,b23,b31,b32,b33 be Element of F_Real;
let A,B be Matrix of 3,F_Real;
assume that
A1: A = <* <* a11,a12,a13 *>, <* a21,a22,a23 *>, <* a31,a32,a33 *> *> and
A2: B = <* <* b11,b12,b13 *>, <* b21,b22,b23 *>, <* b31,b32,b33 *> *>;
now
now
thus len A = 3 by A1,FINSEQ_1:45;
width A = 3 & len B = 3 by MATRIX_0:23;
hence len (A * B) = len A by MATRIX_3:def 4;
end;
hence len (A * B) = 3;
thus 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 *> *> by A1,A2,Th07;
end;
hence thesis;
end;
theorem Th09:
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
let a,b,c be non zero Element of F_Real;
let M1,M2 be Matrix of 3,F_Real;
assume that
A1: M1 = <* <* a,0,0 *>, <* 0,b,0 *>, <* 0,0,c *> *> and
A2: M2 = <* <* (1/a),0,0 *>, <* 0,(1/b),0 *>, <* 0,0,(1/c) *> *>;
reconsider z = 0 as Element of F_Real;
reconsider ia = 1/a, ib = 1/b, ic = 1/c as Element of F_Real
by XREAL_0:def 1;
A4: M2 = <* <* ia,z,z *>, <* z,ib,z *>, <* z,z,ic *> *> by A2;
a is non zero; then
A5: a * ia = 1 & b * ib = 1 & c * ic = 1 by XCMPLX_1:106;
A6: len (M1 * M2) = 3 by MATRIX_0:23;
(M1 * M2).1 = <* a * ia + z * z + z * z, a * z + z * ib + z * z,
a * z + z * z + z * ic *> & (M1 * M2).2 = <* z * ia + b * z + z * z,
z * z + b * ib + z * z, z * z + b * z + z * ic *> &
(M1 * M2).3 = <* z * ia + z * z + c * z, z * z + z * ib + c * z,
z * z + z * z + c * ic *> by A1,A2,Lem01;
hence M1 * M2 = 1.(F_Real,3) by A6,A5,FINSEQ_1:45,Th01;
A7: len (M2 * M1) = 3 by MATRIX_0:23;
(M2 * M1).1 = <* ia * a + z * z + z * z, ia * z + z * b + z * z,
ia * z + z * z + z * c *> & (M2 * M1).2 = <* z * a + ib * z + z * z,
z * z + ib * b + z * z, z * z + ib * z + z * c *> &
(M2 * M1).3 = <* z * a + z * z + ic * z, z * z + z * b + ic * z,
z * z + z * z + ic * c *> by A1,A4,Lem01;
hence M2 * M1 = 1.(F_Real,3) by A7,A5,FINSEQ_1:45,Th01;
end;
theorem Th10:
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
let a,b,c be non zero Element of F_Real;
reconsider ia = 1/a, ib = 1/b, ic = 1/c as Element of F_Real
by XREAL_0:def 1;
reconsider M = <* <* a,0,0 *>,
<* 0,b,0 *>,
<* 0,0,c *> *>,
N = <* <* ia,0,0 *>,
<* 0,ib,0 *>,
<* 0,0,ic *> *> as Matrix of 3,F_Real by MATRIXR2:35;
now
thus N * M = 1.(F_Real,3) by Th09;
hence N * M = M * N by Th09;
end;
hence thesis by MATRIX_6:def 2,MATRIX_6:def 3;
end;
theorem Th11:
|[1,0,0]| is non zero &
|[0,1,0]| is non zero &
|[0,0,1]| is non zero &
|[1,1,1]| is non zero by EUCLID_5:4,FINSEQ_1:78;
theorem
|[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
|[1,0,0]| <> |[0,0,0]|
proof
assume |[1,0,0]| = |[0,0,0]|;
then 1 = |[0,0,0]|`1 by EUCLID_5:2;
hence thesis by EUCLID_5:2;
end;
hence |[1,0,0]| <> 0.TOP-REAL 3 by EUCLID_5:4;
|[0,1,0]| <> |[0,0,0]|
proof
assume |[0,1,0]| = |[0,0,0]|;
then 1 = |[0,0,0]|`2 by EUCLID_5:2;
hence thesis by EUCLID_5:2;
end;
hence |[0,1,0]| <> 0.TOP-REAL 3 by EUCLID_5:4;
|[0,0,1]| <> |[0,0,0]|
proof
assume |[0,0,1]| = |[0,0,0]|;
then 1 = |[0,0,0]|`3 by EUCLID_5:2;
hence thesis by EUCLID_5:2;
end;
hence |[0,0,1]| <> 0.TOP-REAL 3 by EUCLID_5:4;
|[1,1,1]| <> |[0,0,0]|
proof
assume |[1,1,1]| = |[0,0,0]|;
then 1 = |[0,0,0]|`1 by EUCLID_5:2;
hence thesis by EUCLID_5:2;
end;
hence |[1,1,1]| <> 0.TOP-REAL 3 by EUCLID_5:4;
end;
theorem Th13:
<e1> <> 0.TOP-REAL 3 &
<e2> <> 0.TOP-REAL 3 &
<e3> <> 0.TOP-REAL 3
proof
|[1,0,0]| <> |[0,0,0]|
proof
assume |[1,0,0]| = |[0,0,0]|;
then 1 = |[0,0,0]|`1 by EUCLID_5:2;
hence thesis by EUCLID_5:2;
end;
hence <e1> <> 0.TOP-REAL 3 by EUCLID_5:4,EUCLID_8:def 1;
|[0,1,0]| <> |[0,0,0]|
proof
assume |[0,1,0]| = |[0,0,0]|;
then 1 = |[0,0,0]|`2 by EUCLID_5:2;
hence thesis by EUCLID_5:2;
end;
hence <e2> <> 0.TOP-REAL 3 by EUCLID_5:4,EUCLID_8:def 2;
|[0,0,1]| <> |[0,0,0]|
proof
assume |[0,0,1]| = |[0,0,0]|;
then 1 = |[0,0,0]|`3 by EUCLID_5:2;
hence thesis by EUCLID_5:2;
end;
hence <e3> <> 0.TOP-REAL 3 by EUCLID_5:4,EUCLID_8:def 3;
end;
begin
Lem02:
i in Seg 3 & u = uf & p1 = N * uf implies p1.i = <* (N * <*uf*>@)*(i,1) *>
proof
assume that
A1: i in Seg 3 and
A2: u = uf and
A3: p1 = N * uf;
A4: N * (<*uf*>@) is Matrix of 3,1,F_Real by A2,FINSEQ_3:153,ANPROJ_8:91;
u in TOP-REAL 3;
then u in REAL 3 by EUCLID:22; then
A5: 3 = len uf by A2,EUCLID_8:50;
A6: i = 1 or ... or i = 3 by A1,FINSEQ_1:91;
p1 = N * (<*uf*>@) by A3,LAPLACE:def 9; then
p1.i = Line(N * (<*uf*>@),i) by A1,A4,MATRIX_0:52
.= <* (N * <*uf*>@)*(i,1) *> by A6,A5,ANPROJ_8:92;
hence thesis;
end;
Lem03:
i in Seg 3 & u = uf & pf = v & r <> 0 & v = r * u implies
(N * <*uf*>@)*(i,1) = (1/r) * (Line(N,i) "*" pf)
proof
assume that
A1: i in Seg 3 and
A2: u = uf and
A3: pf = v and
A4: r <> 0 and
A5: v = r * u;
set b = 1/r;
reconsider s1 = uf.1, s2 = uf.2, s3 = uf.3 as Element of F_Real
by XREAL_0:def 1;
u in TOP-REAL 3; then
A6: u in REAL 3 by EUCLID:22;
A7: width(<*uf*>) = len u by A2,ANPROJ_8:75
.= 3 by A6,EUCLID_8:50;
A8: width N = 3 by MATRIX_0:24
.= len (<*uf*>@) by MATRIX_0:def 6,A7;
N * (<*uf*>@) is Matrix of 3,1,F_Real by A2,FINSEQ_3:153,ANPROJ_8:91;
then
A9: [1,1] in Indices(N * <*uf*>@) & [2,1] in Indices(N * <*uf*>@) &
[3,1] in Indices(N * <*uf*>@) by MATRIX_0:23,ANPROJ_8:2;
reconsider t1 = v.1, t2 = v.2, t3 = v.3 as Element of F_Real
by XREAL_0:def 1;
A10: len N = 3 & width N = 3 by MATRIX_0:23;
A11:
now
thus len Line(N,1) = width N by MATRIX_0:def 7
.= 3 by MATRIX_0:23;
1 in Seg width N & 2 in Seg width N &
3 in Seg width N by A10,FINSEQ_1:1;
hence Line(N,1).1 = N*(1,1) &
Line(N,1).2 = N*(1,2) & Line(N,1).3 = N*(1,3) by MATRIX_0:def 7;
end;
A12:
now
thus len Line(N,2) = width N by MATRIX_0:def 7
.= 3 by MATRIX_0:23;
1 in Seg width N & 2 in Seg width N &
3 in Seg width N by A10,FINSEQ_1:1;
hence Line(N,2).1 = N*(2,1) &
Line(N,2).2 = N*(2,2) & Line(N,2).3 = N*(2,3) by MATRIX_0:def 7;
end;
A13:
now
thus len Line(N,3) = width N by MATRIX_0:def 7
.= 3 by MATRIX_0:23;
1 in Seg width N & 2 in Seg width N &
3 in Seg width N by A10,FINSEQ_1:1;
hence Line(N,3).1 = N*(3,1) &
Line(N,3).2 = N*(3,2) & Line(N,3).3 = N*(3,3) by MATRIX_0:def 7;
end;
3 = len uf by A2,A6,EUCLID_8:50; then
A14: uf = <* s1,s2,s3 *> by FINSEQ_1:45;
A15: i = 1 or ... or i = 3 by A1,FINSEQ_1:91;
A16: b * v = (1/r) * r * uf by A5,A2,RVSUM_1:49
.= 1 * uf by A4,XCMPLX_1:87
.= uf by RVSUM_1:52;
uf in TOP-REAL 3 by A2; then
A17: uf in REAL 3 by EUCLID:22;
v in TOP-REAL 3; then
A18: v in REAL 3 by EUCLID:22;
then |[ b * v.1, b * v.2, b * v.3]| = uf by A16,EUCLID_8:52
.= |[uf.1,uf.2,uf.3]| by A17,EUCLID_8:1;
then
A19: b * v.1 = uf.1 & b * v.2 = uf.2 & b * v.3 = uf.3 by FINSEQ_1:78;
A20: pf = <* t1,t2,t3 *> by A3,A18,EUCLID_8:1;
(N * <*uf*>@)*(i,1) = Line(N,i) "*" Col(<*uf*>@,1)
by A15,A8,A9,MATRIX_3:def 4
.= Line(N,i) "*" uf by ANPROJ_8:93
.= <* N*(i,1),N*(i,2),N*(i,3) *> "*" <* s1, s2, s3 *>
by A15,A11,A12,A13,FINSEQ_1:45,A14
.= N*(i,1) * s1 + N*(i,2) * s2 + N*(i,3) * s3
by ANPROJ_8:7
.= b * (N*(i,1) * t1 + N*(i,2) * t2 + N*(i,3) * t3)
by A19
.= b * (<* N*(i,1),N*(i,2),N*(i,3) *> "*"
<* t1, t2, t3 *>)
by ANPROJ_8:7
.= b * (Line(N,i) "*" pf)
by A15,A11,A12,A13,FINSEQ_1:45,A20;
hence thesis;
end;
Lem04:
i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u implies
(p1.i).1 = (1/r) * (Line(N,i) "*" pf)
proof
assume that
A1: i in Seg 3 and
A2: u = uf and
A3: pf = v and
A4: p1 = N * uf and
A5: r <> 0 and
A6: v = r * u;
set b = 1/r;
A7: p1.1 = <* (N * <*uf*>@)*(1,1) *> &
p1.2 = <* (N * <*uf*>@)*(2,1) *> & p1.3 = <* (N * <*uf*>@)*(3,1) *>
by A2,A4,FINSEQ_1:1,Lem02;
i = 1 or ... or i = 3 by A1,FINSEQ_1:91;
then (p1.i).1 = (N * <*uf*>@)*(i,1) by A7
.= b * (Line(N,i) "*" pf) by A1,A2,A3,A5,A6,Lem03;
hence thesis;
end;
Lem05:
i in Seg 3 & pf = v implies Line(N,i) "*" pf = ((N * pf).i).1
proof
assume that
A1: i in Seg 3 and
A2: pf = v;
A3: N * (<*pf*>@) is Matrix of 3,1,F_Real by A2,FINSEQ_3:153,ANPROJ_8:91;
v in TOP-REAL 3;
then v in REAL 3 by EUCLID:22; then
A4: 3 = len pf by A2,EUCLID_8:50;
v in TOP-REAL 3; then
A5: v in REAL 3 by EUCLID:22;
A6: width(<*pf*>) = len pf by ANPROJ_8:75
.= 3 by A2,A5,EUCLID_8:50;
A7: width N = 3 by MATRIX_0:24
.= len (<*pf*>@) by MATRIX_0:def 6,A6;
N * <*pf*>@ is Matrix of 3,1,F_Real by A2,FINSEQ_3:153,ANPROJ_8:91;
then
A8: [1,1] in Indices(N * <*pf*>@) &
[2,1] in Indices(N * <*pf*>@) & [3,1] in Indices(N * <*pf*>@)
by MATRIX_0:23,ANPROJ_8:2;
A9: i = 1 or ... or i = 3 by A1,FINSEQ_1:91;
(N * pf).i = (N * <*pf*>@).i by LAPLACE:def 9
.= Line(N * <*pf*>@,i) by A1,A3,MATRIX_0:52
.= <* (N * <*pf*>@)*(i,1) *> by A9,A4,ANPROJ_8:92;
then ((N * pf).i).1 = (N * <*pf*>@)*(i,1)
.= Line(N,i) "*" Col(<*pf*>@,1)
by A9,A7,A8,MATRIX_3:def 4;
hence thesis by ANPROJ_8:93;
end;
registration
let n be Nat;
cluster 1.(F_Real,n) -> invertible;
coherence;
end;
registration
let n be Nat;
let M be invertible Matrix of n,F_Real;
cluster M~ -> invertible;
coherence;
end;
registration
let n be Nat;
let K be Field;
let N1,N2 be invertible Matrix of n,K;
cluster N1 * N2 -> invertible;
coherence by MATRIX_6:36;
end;
begin :: Group of homography
reserve N,N1,N2 for invertible Matrix of 3,F_Real;
reserve P,P1,P2,P3 for Point of ProjectiveSpace TOP-REAL 3;
theorem Th14:
(homography(N1)).((homography(N2)).P) = (homography(N1 * N2)).P
proof
consider u12,v12 being Element of TOP-REAL 3,
u12f being FinSequence of F_Real,
p12 being FinSequence of (1-tuples_on REAL) such that
A1: P = Dir u12 and
A2: u12 is not zero and
A3: u12 = u12f and
A4: p12 = (N1 * N2) * u12f and
A5: v12 = M2F p12 and
A6: v12 is not zero and
A7: (homography(N1 * N2)).P = Dir v12 by ANPROJ_8:def 4;
consider u2,v2 being Element of TOP-REAL 3,
u2f being FinSequence of F_Real,
p2 being FinSequence of (1-tuples_on REAL) such that
A8: P = Dir u2 and
A9: u2 is not zero and
A10: u2 = u2f and
A11: p2 = N2 * u2f and
A12: v2 = M2F p2 and
A13: v2 is not zero and
A14: (homography(N2)).P = Dir v2 by ANPROJ_8:def 4;
consider u1,v1 being Element of TOP-REAL 3,
u1f being FinSequence of F_Real,
p1 being FinSequence of (1-tuples_on REAL) such that
A15: (homography(N2)).P = Dir u1 and
A16: u1 is not zero and
A17: u1 = u1f and
A18: p1 = N1 * u1f and
A19: v1 = M2F p1 and
A20: v1 is not zero and
A21: (homography(N1)).((homography(N2)).P) = Dir v1 by ANPROJ_8:def 4;
are_Prop u12,u2 by A1,A8,A2,A9,ANPROJ_1:22;
then consider a be Real such that
A22: a <> 0 and
A23: u2 = a * u12 by ANPROJ_1:1;
are_Prop v2,u1 by A14,A15,A16,A13,ANPROJ_1:22;
then consider b be Real such that
A24: b <> 0 and
A25: u1 = b * v2 by ANPROJ_1:1;
u1 in TOP-REAL 3; then
F2: u1 in REAL 3 by EUCLID:22;
width(<*u1f*>) = len u1 by A17,ANPROJ_8:75
.= 3 by F2,EUCLID_8:50;
then len ( <*u1f*>@ ) = width <*u1f*> by MATRIX_0:29
.= len u1 by ANPROJ_8:75,A17
.= 3 by F2,EUCLID_8:50; then
A26: width N1 = len (<*u1f*>@) by MATRIX_0:24;
A27: len (N1 * u1f) = len (N1 * (<*u1f*>@)) by LAPLACE:def 9
.= len N1 by A26,MATRIX_3:def 4
.= 3 by MATRIX_0:24;
A28: v1 = <* (N1 * <*u1f*>@)*(1,1),
(N1 * <*u1f*>@)*(2,1),
(N1 * <*u1f*>@)*(3,1) *>
proof
p1.1 = <* (N1 * <*u1f*>@)*(1,1) *> &
p1.2 = <* (N1 * <*u1f*>@)*(2,1) *> & p1.3 = <* (N1 * <*u1f*>@)*(3,1) *>
by A17,A18,FINSEQ_1:1,Lem02;
then (p1.1).1 = (N1 * <*u1f*>@)*(1,1) &
(p1.2).1 = (N1 * <*u1f*>@)*(2,1) & (p1.3).1 = (N1 * <*u1f*>@)*(3,1);
hence thesis by A19,A27,A18,ANPROJ_8:def 2;
end;
u2 in TOP-REAL 3; then
A29: u2 in REAL 3 by EUCLID:22;
width(<*u2f*>) = len u2 by A10,ANPROJ_8:75
.= 3 by A29,EUCLID_8:50;
then
len ( <*u2f*>@ ) = width <*u2f*> by MATRIX_0:29
.= len u2 by ANPROJ_8:75,A10
.= 3 by A29,EUCLID_8:50; then
A30: width N2 = len (<*u2f*>@) by MATRIX_0:24;
A31: len (N2 * u2f) = len (N2 * (<*u2f*>@)) by LAPLACE:def 9
.= len N2 by A30,MATRIX_3:def 4
.= 3 by MATRIX_0:24;
A32: v2 = <* (N2 * <*u2f*>@)*(1,1),
(N2 * <*u2f*>@)*(2,1),
(N2 * <*u2f*>@)*(3,1) *>
proof
p2.1 = <* (N2 * <*u2f*>@)*(1,1) *> &
p2.2 = <* (N2 * <*u2f*>@)*(2,1) *> & p2.3 = <* (N2 * <*u2f*>@)*(3,1) *>
by A10,A11,FINSEQ_1:1,Lem02;
then (p2.1).1 = (N2 * <*u2f*>@)*(1,1) &
(p2.2).1 = (N2 * <*u2f*>@)*(2,1) & (p2.3).1 = (N2 * <*u2f*>@)*(3,1);
hence thesis by A12,A31,A11,ANPROJ_8:def 2;
end;
u12 in TOP-REAL 3; then
A33: u12 in REAL 3 by EUCLID:22;
width(<*u12f*>) = len u12 by A3,ANPROJ_8:75
.= 3 by A33,EUCLID_8:50;
then
A34: len ( <*u12f*>@ ) = width <*u12f*> by MATRIX_0:29
.= len u12 by ANPROJ_8:75,A3
.= 3 by A33,EUCLID_8:50;
A35: width (N1 * N2) = len (<*u12f*>@) by MATRIX_0:24,A34;
A36: len ((N1 * N2) * u12f) = len ((N1 * N2) * (<*u12f*>@)) by LAPLACE:def 9
.= len (N1 * N2) by A35,MATRIX_3:def 4
.= 3 by MATRIX_0:24;
A37: v12 = <* ((N1*N2) * <*u12f*>@)*(1,1),
((N1*N2) * <*u12f*>@)*(2,1),
((N1*N2) * <*u12f*>@)*(3,1) *>
proof
p12.1 = <* ((N1 * N2) * <*u12f*>@)*(1,1) *> &
p12.2 = <* ((N1 * N2) * <*u12f*>@)*(2,1) *> &
p12.3 = <* ((N1 * N2) * <*u12f*>@)*(3,1) *>
by A3,A4,FINSEQ_1:1,Lem02;
then (p12.1).1 = ((N1 * N2) * <*u12f*>@)*(1,1) &
(p12.2).1 = ((N1 * N2) * <*u12f*>@)*(2,1) &
(p12.3).1 = ((N1 * N2) * <*u12f*>@)*(3,1);
hence thesis by A5,A36,A4,ANPROJ_8:def 2;
end;
reconsider v2f = v2 as FinSequence of F_Real by RVSUM_1:145;
reconsider invb = 1/b as Real;
A38: v2f = invb * u1
proof
invb * u1 = (invb * b) * v2f by A25,RVSUM_1:49
.= 1 * v2f by A24,XCMPLX_1:106
.= v2f by RVSUM_1:52;
hence thesis;
end;
1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1;
then
A39: (N1 * <*u1f*>@)*(1,1) = (1/invb) * (Line(N1,1) "*" v2f) &
(N1 * <*u1f*>@)*(2,1) = (1/invb) * (Line(N1,2) "*" v2f) &
(N1 * <*u1f*>@)*(3,1) = (1/invb) * (Line(N1,3) "*" v2f)
by A24,XCMPLX_1:50,A38,A17,Lem03;
A40: len Line(N1,1) = width N1 & len Line(N1,2) = width N1 &
len Line(N1,3) = width N1 by MATRIX_0:def 7;
width N1 = 3 by MATRIX_0:24;
then 1 in Seg width N1 & 2 in Seg width N1 &
3 in Seg width N1 by FINSEQ_1:1; then
A41: Line(N1,1).1 = N1*(1,1) & Line(N1,1).2 = N1*(1,2) &
Line(N1,1).3 = N1*(1,3) & Line(N1,2).1 = N1*(2,1) &
Line(N1,2).2 = N1*(2,2) & Line(N1,2).3 = N1*(2,3) &
Line(N1,3).1 = N1*(3,1) & Line(N1,3).2 = N1*(3,2) &
Line(N1,3).3 = N1*(3,3) by MATRIX_0:def 7; then
A42: Line(N1,1) = <* N1*(1,1),N1*(1,2),N1*(1,3) *> &
Line(N1,2) = <* N1*(2,1),N1*(2,2),N1*(2,3) *> &
Line(N1,3) = <* N1*(3,1),N1*(3,2),N1*(3,3) *>
by A40,MATRIX_0:24,FINSEQ_1:45;
A43: len Line(N1 * N2,1) = width (N1 * N2) &
len Line(N1 * N2,2) = width (N1 * N2) &
len Line(N1 * N2,3) = width (N1 * N2) by MATRIX_0:def 7;
width (N1 * N2) = 3 by MATRIX_0:24;
then 1 in Seg width (N1 * N2) & 2 in Seg width (N1 * N2) &
3 in Seg width (N1 * N2) by FINSEQ_1:1;
then
A44: Line(N1*N2,1).1 = (N1*N2)*(1,1) & Line(N1*N2,1).2 = (N1*N2)*(1,2) &
Line(N1*N2,1).3 = (N1*N2)*(1,3) & Line(N1*N2,2).1 = (N1*N2)*(2,1) &
Line(N1*N2,2).2 = (N1*N2)*(2,2) & Line(N1*N2,2).3 = (N1*N2)*(2,3) &
Line(N1*N2,3).1 = (N1*N2)*(3,1) & Line(N1*N2,3).2 = (N1*N2)*(3,2) &
Line(N1*N2,3).3 = (N1*N2)*(3,3) by MATRIX_0:def 7;
reconsider fa = a as Element of F_Real by XREAL_0:def 1;
A45: v1.1 = (N1 * <*u1f*>@)*(1,1) & v1.2 = (N1 * <*u1f*>@)*(2,1) &
v1.3 = (N1 * <*u1f*>@)*(3,1) by A28;
reconsider t1 = v2f.1, t2 = v2f.2, t3 = v2f.3 as Element of F_Real
by A32;
len v2f = 3 by A32,FINSEQ_1:45;
then
A46: v2f = <* t1,t2,t3 *> by FINSEQ_1:45;
N2 * <*u2f*>@ is Matrix of 3,1,F_Real by A10,FINSEQ_3:153,ANPROJ_8:91;
then
A47: [1,1] in Indices(N2 * <*u2f*>@) & [2,1] in Indices(N2 * <*u2f*>@) &
[3,1] in Indices(N2 * <*u2f*>@) by ANPROJ_8:2,MATRIX_0:23;
A48: t1 = (N2 * <*u2f*>@)*(1,1) by A32
.= Line(N2,1) "*" Col(<*u2f*>@,1) by A30,A47,MATRIX_3:def 4
.= Line(N2,1) "*" u2f by ANPROJ_8:93;
A49: t2 = (N2 * <*u2f*>@)*(2,1) by A32
.= Line(N2,2) "*" Col(<*u2f*>@,1) by A30,A47,MATRIX_3:def 4
.= Line(N2,2) "*" u2f by ANPROJ_8:93;
A50: t3 = (N2 * <*u2f*>@)*(3,1) by A32
.= Line(N2,3) "*" Col(<*u2f*>@,1) by A30,A47,MATRIX_3:def 4
.= Line(N2,3) "*" u2f by ANPROJ_8:93;
now
width N2 = 3 by MATRIX_0:23;
then 1 in Seg width N2 & 2 in Seg width N2 & 3 in Seg width N2
by FINSEQ_1:1;
hence Line(N2,1).1 = N2*(1,1) & Line(N2,1).2 = N2*(1,2) &
Line(N2,1).3 = N2*(1,3) & Line(N2,2).1 = N2*(2,1) &
Line(N2,2).2 = N2*(2,2) & Line(N2,2).3 = N2*(2,3) &
Line(N2,3).1 = N2*(3,1) & Line(N2,3).2 = N2*(3,2) &
Line(N2,3).3 = N2*(3,3) by MATRIX_0:def 7;
thus [1,1] in Indices N2 & [1,2] in Indices N2 &
[1,3] in Indices N2 & [2,1] in Indices N2 & [2,2] in Indices N2 &
[2,3] in Indices N2 & [3,1] in Indices N2 & [3,2] in Indices N2 &
[3,3] in Indices N2 by ANPROJ_8:1,MATRIX_0:23;
end;
then reconsider l11 = Line(N2,1).1,l12 = Line(N2,1).2,
l13 = Line(N2,1).3, l21 = Line(N2,2).1,l22 = Line(N2,2).2,
l23 = Line(N2,2).3, l31 = Line(N2,3).1,l32 = Line(N2,3).2,
l33 = Line(N2,3).3 as Element of F_Real;
reconsider ru121 = u12f.1,ru122 = u12f.2,
ru123 = u12f.3 as Element of F_Real by XREAL_0:def 1;
len Line(N2,1) = width N2 & len Line(N2,2) = width N2 &
len Line(N2,3) = width N2 by MATRIX_0:def 7;
then
A51: Line(N2,1) = <* l11,l12,l13 *> & Line(N2,2) = <* l21,l22,l23 *> &
Line(N2,3) = <* l31,l32,l33 *> by MATRIX_0:23,FINSEQ_1:45;
reconsider ru21 = u2.1,ru22 = u2.2,ru23 = u2.3 as Element of F_Real
by XREAL_0:def 1;
A52: ru21 = a * u12f.1 & ru22 = a * u12f.2 & ru23 = a * u12f.3
by A3,A23,RVSUM_1:44;
len u2 = 3 by A29,EUCLID_8:50;
then
A53: u2f = <* ru21,ru22,ru23 *> by A10,FINSEQ_1:45;
reconsider t121 = v12.1, t122 = v12.2, t123 = v12.3 as Element of F_Real
by A37;
reconsider v12f = v12 as FinSequence of F_Real by RVSUM_1:145;
width N1 = 3 by MATRIX_0:24; then
A54: width N1 = len N2 by MATRIX_0:24;
A55: [1,1] in Indices(N1*N2) & [1,2] in Indices(N1*N2) &
[1,3] in Indices(N1*N2) & [2,1] in Indices(N1*N2) &
[2,2] in Indices(N1*N2) & [2,3] in Indices(N1*N2) &
[3,1] in Indices(N1*N2) & [3,2] in Indices(N1*N2) &
[3,3] in Indices(N1*N2) by ANPROJ_8:1,MATRIX_0:23;
A56: width(N1*N2)=len(<*u12f*>@) by A34,MATRIX_0:24;
u12 in TOP-REAL 3;
then u12f in REAL 3 by EUCLID:22,A3; then
A57: len u12f = 3 by EUCLID_8:50;
(N1 * N2) * <*u12f*>@ is Matrix of 3,1,F_Real
by A3,FINSEQ_3:153,ANPROJ_8:91; then
A58: [1,1] in Indices((N1*N2) * <*u12f*>@) &
[2,1] in Indices((N1*N2) * <*u12f*>@) &
[3,1] in Indices((N1*N2) * <*u12f*>@) by MATRIX_0:23,ANPROJ_8:2;
A59: u12f = <* ru121,ru122,ru123 *> by A57,FINSEQ_1:45;
A60: Col(N2,1) = <* l11,l21,l31 *> & Col(N2,2) = <* l12,l22,l32 *> &
Col(N2,3) = <* l13,l23,l33 *>
proof
now
len N2 = 3 by MATRIX_0:24;
hence len Col(N2,1) = 3 & len Col(N2,2) = 3 & len Col(N2,3) = 3
by MATRIX_0:def 8;
len N2 = 3 & width N2 = 3 by MATRIX_0:24;
then dom N2 = Seg 3 & Seg width N2 = Seg 3 by FINSEQ_1:def 3;
then 1 in dom N2 & 2 in dom N2 & 3 in dom N2 &
1 in Seg width N2 & 2 in Seg width N2 & 3 in Seg width N2
by FINSEQ_1:1;
hence Col(N2,1).1 = l11 & Col(N2,2).1 = l12 & Col(N2,3).1 = l13 &
Col(N2,1).2 = l21 & Col(N2,2).2 = l22 & Col(N2,3).2 = l23 &
Col(N2,1).3 = l31 & Col(N2,2).3 = l32 & Col(N2,3).3 = l33
by MATRIX_0:42;
end;
hence thesis by FINSEQ_1:45;
end;
Dir v1 = Dir v12
proof
ex c be Real st c <> 0 & v1 = c * v12
proof
set c = a * b;
take c;
thus c <> 0 by A22,A24,XCMPLX_1:6;
A61:
now
thus (N1 * <*u1f*>@)*(1,1) = c * (((N1*N2) * <*u12f*>@)*(1,1))
proof
v1.1 = c * v12.1
proof
reconsider s1 = N1*(1,1),s2 = N1*(1,2),
s3 = N1*(1,3) as Element of F_Real;
A62: Line(N1,1) "*" v2f =
s1 * (<* l11,l12,l13 *> "*" <* ru21, ru22, ru23 *>) +
s2 * (<* l21,l22,l23 *> "*" <* ru21,ru22,ru23 *>) +
s3 * (<* l31,l32,l33 *> "*" <* ru21,ru22,ru23 *>)
by A51,A53,A48,A49,A50,A42,A46,ANPROJ_8:7
.= s1 * (l11 * ru21 + l12 * ru22
+ l13 * ru23) +
s2 * (Line(N2,2) "*" u2f)
+ s3 * (Line(N2,3) "*" u2f)
by A51,A53,ANPROJ_8:7
.= s1 * (l11 * ru21 + l12 * ru22
+ l13 * ru23) +
s2 * (l21 * ru21 + l22 * ru22 + l23 * ru23) +
s3 * (Line(N2,3) "*" u2f)
by A51,A53,ANPROJ_8:7
.= s1 * (l11 * ru21 + l12 * ru22
+ l13 * ru23) +
s2 * (l21 * ru21 + l22 * ru22 + l23 * ru23) +
s3 * (l31 * ru21 + l32 * ru22 + l33 * ru23)
by A51,A53,ANPROJ_8:7
.= a * ((s1 * l11 + s2 * l21 + s3 * l31)
* ru121 +
(s1 * l12 + s2 * l22 + s3 * l32) * ru122 +
(s1 * l13 + s2 * l23 + s3 * l33) * ru123)
by A52;
reconsider s121 = (N1*N2)*(1,1),s122 = (N1*N2)*(1,2),
s123 = (N1*N2)*(1,3) as Element of F_Real;
A63: t121 = ((N1*N2) * <*u12f*>@)*(1,1) by A37
.= Line(N1*N2,1) "*" Col(<*u12f*>@,1)
by A56,A58,MATRIX_3:def 4
.= Line(N1*N2,1) "*" u12f by ANPROJ_8:93
.= <* s121,s122,s123 *> "*" <* ru121,ru122,ru123 *>
by A59,A44,A43,MATRIX_0:24,FINSEQ_1:45
.= s121 * ru121 + s122 * ru122 + s123 * ru123 by ANPROJ_8:7;
now
thus s121 = Line(N1,1) "*" Col(N2,1) by A54,A55,MATRIX_3:def 4
.= <* s1,s2,s3 *> "*" Col(N2,1)
by A41,A40,MATRIX_0:24,FINSEQ_1:45
.= (s1 * l11 + s2 * l21 + s3 * l31) by A60,ANPROJ_8:7;
thus s122 = Line(N1,1) "*" Col(N2,2) by A54,A55,MATRIX_3:def 4
.= <* s1,s2,s3 *> "*" Col(N2,2)
by A41,A40,MATRIX_0:24,FINSEQ_1:45
.= (s1 * l12 + s2 * l22 + s3 * l32) by A60,ANPROJ_8:7;
thus s123 = Line(N1,1) "*" Col(N2,3) by A54,A55,MATRIX_3:def 4
.= <* s1,s2,s3 *> "*" Col(N2,3)
by A41,A40,MATRIX_0:24,FINSEQ_1:45
.= (s1 * l13 + s2 * l23 + s3 * l33) by A60,ANPROJ_8:7;
end;
then a * b * t121 = b * (Line(N1,1) "*" v2f) by A63,A62
.= (N1 * <*u1f*>@)*(1,1) by A39,XCMPLX_1:52
.= v1.1 by A28;
hence thesis;
end;
hence thesis by A45,A37;
end;
thus (N1 * <*u1f*>@)*(2,1) = c * (((N1*N2) * <*u12f*>@)*(2,1))
proof
v1.2 = c * v12.2
proof
reconsider s1 = N1*(2,1),s2 = N1*(2,2),
s3 = N1*(2,3) as Element of F_Real;
A64: Line(N1,2) "*" v2f =
s1 * (<* l11,l12,l13 *> "*" <* ru21, ru22, ru23 *>) +
s2 * (<* l21,l22,l23 *> "*" <* ru21,ru22,ru23 *>) +
s3 * (<* l31,l32,l33 *> "*" <* ru21,ru22,ru23 *>)
by A51,A53,A48,A49,A50,A42,A46,ANPROJ_8:7
.= s1 * (l11 * ru21 + l12 * ru22
+ l13 * ru23) +
s2 * (Line(N2,2) "*" u2f) +
s3 * (Line(N2,3) "*" u2f)
by A51,A53,ANPROJ_8:7
.= s1 * (l11 * ru21 + l12 * ru22
+ l13 * ru23) +
s2 * (l21 * ru21 + l22 * ru22 + l23 * ru23) +
s3 * (Line(N2,3) "*" u2f)
by A51,A53,ANPROJ_8:7
.= s1 * (l11 * ru21 + l12 * ru22
+ l13 * ru23) +
s2 * (l21 * ru21 + l22 * ru22 + l23 * ru23) +
s3 * (l31 * ru21 + l32 * ru22 + l33 * ru23)
by A51,A53,ANPROJ_8:7
.= a * ((s1 * l11 + s2 * l21 + s3 * l31)
* ru121 +
(s1 * l12 + s2 * l22 + s3 * l32) * ru122 +
(s1 * l13 + s2 * l23 + s3 * l33) * ru123)
by A52;
reconsider s121 = (N1*N2)*(2,1),s122 = (N1*N2)*(2,2),
s123 = (N1*N2)*(2,3) as Element of F_Real;
A65: t122 = ((N1*N2) * <*u12f*>@)*(2,1) by A37
.= Line(N1*N2,2) "*" Col(<*u12f*>@,1)
by A56,A58,MATRIX_3:def 4
.= Line(N1*N2,2) "*" u12f by ANPROJ_8:93
.= <* s121,s122,s123 *> "*" <* ru121,ru122,ru123 *>
by A59,A44,A43,MATRIX_0:24,FINSEQ_1:45
.= s121 * ru121 + s122 * ru122 + s123 * ru123
by ANPROJ_8:7;
now
thus s121 = Line(N1,2) "*" Col(N2,1) by A54,A55,MATRIX_3:def 4
.= <* s1,s2,s3 *> "*" Col(N2,1)
by A41,A40,MATRIX_0:24,FINSEQ_1:45
.= (s1 * l11 + s2 * l21 + s3 * l31) by A60,ANPROJ_8:7;
thus s122 = Line(N1,2) "*" Col(N2,2) by A54,A55,MATRIX_3:def 4
.= <* s1,s2,s3 *> "*" Col(N2,2)
by A41,A40,MATRIX_0:24,FINSEQ_1:45
.= (s1 * l12 + s2 * l22 + s3 * l32) by A60,ANPROJ_8:7;
thus s123 = Line(N1,2) "*" Col(N2,3) by A54,A55,MATRIX_3:def 4
.= <* s1,s2,s3 *> "*" Col(N2,3)
by A41,A40,MATRIX_0:24,FINSEQ_1:45
.= (s1 * l13 + s2 * l23 + s3 * l33) by A60,ANPROJ_8:7;
end;
then a * b * t122 = b * (Line(N1,2) "*" v2f) by A65,A64
.= (N1 * <*u1f*>@)*(2,1) by A39,XCMPLX_1:52
.= v1.2 by A28;
hence thesis;
end;
hence thesis by A45,A37;
end;
thus (N1 * <*u1f*>@)*(3,1) = c * (((N1*N2) * <*u12f*>@)*(3,1))
proof
v1.3 = c * v12.3
proof
reconsider s1 = N1*(3,1),s2 = N1*(3,2),
s3 = N1*(3,3) as Element of F_Real;
A66: Line(N1,3) "*" v2f =
s1 * (<* l11,l12,l13 *> "*" <* ru21, ru22, ru23 *>) +
s2 * (<* l21,l22,l23 *> "*" <* ru21,ru22,ru23 *>) +
s3 * (<* l31,l32,l33 *> "*" <* ru21,ru22,ru23 *>)
by A51,A53,A48,A49,A50,A42,A46,ANPROJ_8:7
.= s1 * (l11 * ru21 + l12 * ru22
+ l13 * ru23) +
s2 * (Line(N2,2) "*" u2f) +
s3 * (Line(N2,3) "*" u2f)
by A51,A53,ANPROJ_8:7
.= s1 * (l11 * ru21 + l12 * ru22
+ l13 * ru23) +
s2 * (l21 * ru21 + l22 * ru22 + l23 * ru23) +
s3 * (Line(N2,3) "*" u2f)
by A51,A53,ANPROJ_8:7
.= s1 * (l11 * ru21 + l12 * ru22
+ l13 * ru23) +
s2 * (l21 * ru21 + l22 * ru22 + l23 * ru23) +
s3 * (l31 * ru21 + l32 * ru22 + l33 * ru23)
by A51,A53,ANPROJ_8:7
.= a * ((s1 * l11 + s2 * l21 + s3 * l31)
* ru121 +
(s1 * l12 + s2 * l22 + s3 * l32) * ru122 +
(s1 * l13 + s2 * l23 + s3 * l33) * ru123)
by A52;
reconsider s121 = (N1*N2)*(3,1),s122 = (N1*N2)*(3,2),
s123 = (N1*N2)*(3,3) as Element of F_Real;
A67: t123 = ((N1*N2) * <*u12f*>@)*(3,1) by A37
.= Line(N1*N2,3) "*" Col(<*u12f*>@,1)
by A56,A58,MATRIX_3:def 4
.= Line(N1*N2,3) "*" u12f by ANPROJ_8:93
.= <* s121,s122,s123 *> "*" <* ru121,ru122,ru123 *>
by A59,A44,A43,MATRIX_0:24,FINSEQ_1:45
.= s121 * ru121 + s122 * ru122 + s123 * ru123 by ANPROJ_8:7;
now
thus s121 = Line(N1,3) "*" Col(N2,1) by A54,A55,MATRIX_3:def 4
.= <* s1,s2,s3 *> "*" Col(N2,1)
by A41,A40,MATRIX_0:24,FINSEQ_1:45
.= (s1 * l11 + s2 * l21 + s3 * l31) by A60,ANPROJ_8:7;
thus s122 = Line(N1,3) "*" Col(N2,2) by A54,A55,MATRIX_3:def 4
.= <* s1,s2,s3 *> "*" Col(N2,2)
by A41,A40,MATRIX_0:24,FINSEQ_1:45
.= (s1 * l12 + s2 * l22 + s3 * l32) by A60,ANPROJ_8:7;
thus s123 = Line(N1,3) "*" Col(N2,3) by A54,A55,MATRIX_3:def 4
.= <* s1,s2,s3 *> "*" Col(N2,3)
by A41,A40,MATRIX_0:24,FINSEQ_1:45
.= (s1 * l13 + s2 * l23 + s3 * l33) by A60,ANPROJ_8:7;
end;
then a * b * t123 = b * (Line(N1,3) "*" v2f) by A67,A66
.= (N1 * <*u1f*>@)*(3,1) by A39,XCMPLX_1:52
.= v1.3 by A28;
hence thesis;
end;
hence thesis by A45,A37;
end;
end;
<* c * (((N1*N2) * <*u12f*>@)*(1,1)),
c * (((N1*N2) * <*u12f*>@)*(2,1)),
c * (((N1*N2) * <*u12f*>@)*(3,1)) *>
= c * |[ (((N1*N2) * <*u12f*>@)*(1,1)),
(((N1*N2) * <*u12f*>@)*(2,1)),
(((N1*N2) * <*u12f*>@)*(3,1)) ]| by EUCLID_5:8
.= c * <* ((N1*N2) * <*u12f*>@)*(1,1),
((N1*N2) * <*u12f*>@)*(2,1),
((N1*N2) * <*u12f*>@)*(3,1) *>;
hence thesis by A28,A37,A61;
end;
then are_Prop v1,v12 by ANPROJ_1:1;
hence thesis by A6,A20,ANPROJ_1:22;
end;
hence thesis by A7,A21;
end;
theorem Th15:
(homography(1.(F_Real,3))).P = P
proof
consider u,v being Element of TOP-REAL 3,
uf being FinSequence of F_Real,
p being FinSequence of (1-tuples_on REAL) such that
A1: P = Dir u and
u is not zero and
A3: u = uf and
A4: p = 1.(F_Real,3) * uf and
A5: v = M2F p and
v is not zero and
A7: (homography(1.(F_Real,3))).P = Dir v by ANPROJ_8:def 4;
u in TOP-REAL 3; then
A8: uf in REAL 3 by A3,EUCLID:22; then
A9: len uf = 3 by EUCLID_8:50;
A10: 1.(F_Real,3) * uf = 1.(F_Real,3) * <*uf*>@ by LAPLACE:def 9
.= <*uf*>@ by A8,EUCLID_8:50,ANPROJ_8:99;
reconsider ur = uf as FinSequence of REAL;
p = F2M ur by A4,A8,A10,EUCLID_8:50,ANPROJ_8:88;
hence thesis by A1,A3,A5,A7,A9,ANPROJ_8:86;
end;
theorem Th16:
(homography(N)).((homography(N~)).P) = P &
(homography(N~)).((homography(N)).P) = P
proof
A1: N~ is_reverse_of N by MATRIX_6:def 4;
thus (homography(N)).((homography(N~)).P) = (homography(N * N~)).P
by Th14
.= (homography(1.(F_Real,3))).P
by A1,MATRIX_6:def 2
.= P by Th15;
thus (homography(N~)).((homography(N)).P) = (homography(N~ * N)).P
by Th14
.= (homography(1.(F_Real,3))).P
by A1,MATRIX_6:def 2
.= P by Th15;
end;
theorem
(homography(N)).P1 = (homography(N)).P2 implies P1 = P2
proof
assume
A1: (homography(N)).P1 = (homography(N)).P2;
P1 = (homography(N~)).((homography(N)).P1) by Th16
.= P2 by A1,Th16;
hence thesis;
end;
Lem06:
len uf = 3 implies (a * 1.(F_Real,3)) * <*uf*>@ = a * <*uf*>@
proof
assume
A1: len uf = 3;
width <*uf*> = 3 by A1,MATRIX_0:23;
then len (<*uf*>@) = 3 by MATRIX_0:29;
then width 1.(F_Real,3) = len (<*uf*>@) by MATRIX_0:23;
then (a * 1.(F_Real,3)) * <*uf*>@ = a * ((1.(F_Real,3) * <*uf*>@))
by MATRIX15:1;
hence thesis by A1,ANPROJ_8:99;
end;
theorem Th17:
for a being non zero Element of F_Real st
a * 1.(F_Real,3) = N holds (homography(N)).P = P
proof
let a be non zero Element of F_Real;
assume
A1: a * 1.(F_Real,3) = N;
set aN = N;
consider u,v being Element of TOP-REAL 3,
uf being FinSequence of F_Real, p being FinSequence of (1-tuples_on REAL)
such that
A2: P = Dir u and
A3: u is not zero and
A4: u = uf and
A5: p = aN * uf and
A6: v = M2F p and
A7: v is not zero and
A8: (homography(aN)).P = Dir v by ANPROJ_8:def 4;
u in TOP-REAL 3; then
A9: uf in REAL 3 by A4,EUCLID:22;
A10: aN * <*uf*>@ is Matrix of 3,1,F_Real by A4,FINSEQ_3:153,ANPROJ_8:91;
p = aN * <*uf*>@ by A5,LAPLACE:def 9; then
A11: len p = 3 by A10,MATRIX_0:23;
A12: p = aN * <*uf*>@ by A5,LAPLACE:def 9
.= a * <*uf*>@ by A1,A9,EUCLID_8:50,Lem06;
A13: v = <* ((a * <*uf*>@).1).1,((a * <*uf*>@).2).1,((a * <*uf*>@).3).1 *>
by A6,A12,A11,ANPROJ_8:def 2;
now
1.(F_Real,3) * (<*uf*>@) is (3,1)-size by A9,EUCLID_8:50,ANPROJ_8:91;
then
A14: <*uf*>@ is (3,1)-size by A9,EUCLID_8:50,ANPROJ_8:99;
A15: [1,1] in Indices (<*uf*>@) & [2,1] in Indices (<*uf*>@) &
[3,1] in Indices (<*uf*>@) by A14,MATRIX_0:23,ANPROJ_8:2;
then
A16: (a * <*uf*>@)*(1,1) = a * ((<*uf*>@)*(1,1)) &
(a * <*uf*>@)*(2,1) = a * ((<*uf*>@)*(2,1)) &
(a * <*uf*>@)*(3,1) = a * ((<*uf*>@)*(3,1)) by MATRIX_3:def 5;
A17: <*uf*>@ = <* <*uf.1*>, <*uf.2*>, <*uf.3*> *>
by A9,EUCLID_8:50,ANPROJ_8:77;
A18: len (<*uf*>@) = 3 & width (<*uf*>@) = 1 by A14,MATRIX_0:23;
A19: len (a * <*uf*>@) = len (<*uf*>@) &
width (a * <*uf*>@) = width (<*uf*>@) by MATRIX_3:def 5;
a * <*uf*>@ is Matrix of 3,1,F_Real by MATRIX_0:20,A19,A18;
then
A20: [1,1] in Indices(a * <*uf*>@) & [2,1] in Indices(a * <*uf*>@) &
[3,1] in Indices(a * <*uf*>@) by ANPROJ_8:2,MATRIX_0:23;
(<*uf*>@)*(1,1) = ((<*uf*>@).1).1 by A15,MATRPROB:14
.= (<*uf.1*>).1 by A17
.= uf.1;
hence ((a * <*uf*>@).1).1 = a * u.1 by A4,A20,MATRPROB:14,A16;
(<*uf*>@)*(2,1) = ((<*uf*>@).2).1 by A15,MATRPROB:14
.= (<*uf.2*>).1 by A17
.= uf.2;
hence ((a * <*uf*>@).2).1 = a * u.2 by A4,A20,MATRPROB:14,A16;
(<*uf*>@)*(3,1) = ((<*uf*>@).3).1 by A15,MATRPROB:14
.= (<*uf.3*>).1 by A17
.= uf.3;
hence ((a * <*uf*>@).3).1 = a * u.3 by A4,A20,MATRPROB:14,A16;
end;
then
A21: v = <* a * u`1,a * u.2,a * u.3 *> by A13,EUCLID_5:def 1
.= <* a * u`1,a * u`2,a * u.3 *> by EUCLID_5:def 2
.= <* a * u`1,a * u`2,a * u`3 *> by EUCLID_5:def 3
.= a * |[u`1,u`2,u`3]| by EUCLID_5:8
.= a * u by EUCLID_5:3;
a is non zero;
then are_Prop v,u by A21,ANPROJ_1:1;
hence thesis by A2,A3,A7,A8,ANPROJ_1:22;
end;
definition
func EnsHomography3 -> set equals
the set of all homography(N) where N is invertible Matrix of 3,F_Real;
coherence;
end;
registration
cluster EnsHomography3 -> non empty;
coherence
proof
homography(1.(F_Real,3)) in EnsHomography3;
hence thesis;
end;
end;
definition
let h1,h2 be Element of EnsHomography3;
func h1 (*) h2 -> Element of EnsHomography3 means
:Def01:
ex N1,N2 being invertible Matrix of 3,F_Real st h1 = homography(N1) &
h2 = homography(N2) & it = homography(N1 * N2);
existence
proof
h1 in the set of all homography(N) where
N is invertible Matrix of 3,F_Real;
then consider N1 be invertible Matrix of 3,F_Real such that
A1: h1 = homography(N1);
h2 in the set of all homography(N) where
N is invertible Matrix of 3,F_Real;
then consider N2 be invertible Matrix of 3,F_Real such that
A2: h2 = homography(N2);
homography(N1 * N2) in EnsHomography3;
hence thesis by A1,A2;
end;
uniqueness
proof
let H1,H2 be Element of EnsHomography3 such that
A3: ex N1,N2 being invertible Matrix of 3,F_Real st h1 = homography(N1) &
h2 = homography(N2) & H1 = homography(N1 * N2) and
A4: ex N1,N2 being invertible Matrix of 3,F_Real st h1 = homography(N1) &
h2 = homography(N2) & H2 = homography(N1 * N2);
consider NA1,NA2 being invertible Matrix of 3,F_Real such that
A5: h1 = homography(NA1) and
A6: h2 = homography(NA2) and
A7: H1 = homography(NA1 * NA2) by A3;
consider NB1,NB2 being invertible Matrix of 3,F_Real such that
A8: h1 = homography(NB1) and
A9: h2 = homography(NB2) and
A10: H2 = homography(NB1 * NB2) by A4;
reconsider fH1 = H1,fH2 = H2 as Function of ProjectiveSpace TOP-REAL 3,
ProjectiveSpace TOP-REAL 3 by A7,A10;
now
dom fH1 = the carrier of ProjectiveSpace TOP-REAL 3 by FUNCT_2:def 1;
hence dom fH1 = dom fH2 by FUNCT_2:def 1;
thus for x be object st x in dom fH1 holds fH1.x = fH2.x
proof
let x be object;
assume x in dom fH1;
then reconsider P = x as Element of ProjectiveSpace TOP-REAL 3;
fH1.x = (homography(NB1)).((homography(NB2)).P)
by A5,A6,A7,A8,A9,Th14
.= fH2.x by A10,Th14;
hence thesis;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
end;
theorem Th18:
for h1,h2 being Element of EnsHomography3 st
h1 = homography(N1) & h2 = homography(N2) holds
homography(N1 * N2) = h1 (*) h2
proof
let h1,h2 be Element of EnsHomography3;
assume that
A1: h1 = homography(N1) and
A2: h2 = homography(N2);
consider M1,M2 being invertible Matrix of 3,F_Real such that
A3: h1 = homography(M1) and
A4: h2 = homography(M2) and
A5: h1 (*) h2 = homography(M1 * M2) by Def01;
reconsider h12 = h1 (*) h2 as
Function of ProjectiveSpace TOP-REAL 3,ProjectiveSpace TOP-REAL 3 by A5;
now
dom homography(N1 * N2) = the carrier of ProjectiveSpace TOP-REAL 3
by FUNCT_2:def 1;
hence dom homography(N1 * N2) = dom h12 by FUNCT_2:def 1;
thus for x be object st x in dom homography(N1 * N2) holds
(homography(N1 * N2)).x = h12.x
proof
let x be object;
assume x in dom homography(N1 * N2);
then reconsider xf = x as Element of ProjectiveSpace TOP-REAL 3;
(homography(N1 * N2)).xf = (homography(N1)).((homography(N2)).xf)
by Th14
.= h12.xf by A3,A4,A5,A1,A2,Th14;
hence thesis;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
theorem Ta1:
for x,y,z being Element of EnsHomography3 holds
(x (*) y) (*) z = x (*) (y (*) z)
proof
let x,y,z be Element of EnsHomography3;
x in EnsHomography3;
then consider Nx be invertible Matrix of 3,F_Real such that
A2: x = homography(Nx);
y in EnsHomography3;
then consider Ny be invertible Matrix of 3,F_Real such that
A3: y = homography(Ny);
z in EnsHomography3;
then consider Nz be invertible Matrix of 3,F_Real such that
A4: z = homography(Nz);
A5: width Nx = 3 & len Ny = 3 & width Ny = 3 & len Nz = 3 by MATRIX_0:24;
y (*) z = homography(Ny * Nz) by A3,A4,Th18; then
A6: (x (*) (y (*) z)) = homography(Nx * (Ny * Nz)) by A2,Th18
.= homography((Nx * Ny) * Nz) by A5,MATRIX_3:33;
x (*) y = homography(Nx * Ny) by A2,A3,Th18;
hence thesis by A6,A4,Th18;
end;
definition
func BinOpHomography3 -> BinOp of EnsHomography3 means
:Def02:
for h1,h2 being Element of EnsHomography3 holds it.(h1,h2) = h1 (*) h2;
existence from BINOP_1:sch 4;
uniqueness from BINOP_2:sch 2;
end;
definition
func GroupHomography3 -> strict multMagma equals
multMagma(# EnsHomography3, BinOpHomography3 #);
coherence;
end;
set GH3 = GroupHomography3;
Lm1: now
let e be Element of GH3 such that
A1: e = homography(1.(F_Real,3));
let h be Element of GH3;
reconsider h1 = h,h2 = e as Element of EnsHomography3;
consider N1,N2 be 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 be object st x in dom homography(N1) holds
(homography(N1 * N2)).x = (homography(N1)).x
proof
let x be object;
assume x in dom homography(N1);
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 thesis;
end;
hence thesis by A14,FUNCT_1:def 11;
end;
hence h * e = h by Def02,A10,A12;
consider N2,N1 be 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 be object st x in dom homography(N1) holds
(homography(N2 * N1)).x = (homography(N1)).x
proof
let x be object;
assume x in dom homography(N1);
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 thesis;
end;
hence thesis by A18,FUNCT_1:def 11;
end;
hence e * h = h by Def02,A16,A17;
end;
Lm2:
now
let e,h,g be Element of GH3;
let N,Ng be invertible Matrix of 3,F_Real such that
A9: h = homography(N) and
B1: g = homography(Ng) and
B2: Ng = N~ and
B3: e = homography(1.(F_Real,3));
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 be 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
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;
thus for x be object st x in dom homography(N1 * N2) holds
(homography(N1 * N2)).x = (homography(N * Ng)).x
proof
let x be object;
assume x in dom homography(N1 * N2);
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 thesis;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
then h1 (*) g1 = e by B3,A21,A23,MATRIX_6:def 2;
hence h*g = e by Def02;
consider N1,N2 be 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
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;
thus for x be object st x in dom homography(N1 * N2) holds
(homography(N1 * N2)).x = (homography(Ng * N)).x
proof
let x be object;
assume x in dom homography(N1 * N2);
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 thesis;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
then g1 (*) h1 = e by A29,A23,B3,MATRIX_6:def 2;
hence g*h = e by Def02;
end;
set e = homography(1.(F_Real,3));
e in EnsHomography3;
then reconsider e as Element of GH3;
registration
cluster GroupHomography3 -> non empty associative Group-like;
coherence
proof
thus GH3 is non empty;
thus GH3 is associative
proof
let x,y,z be Element of GH3;
reconsider xf=x,yf=y,zf=z as Element of EnsHomography3;
A7: x * y = xf (*) yf by Def02;
A8: (x * y) * z = (xf (*) yf) (*) zf by Def02,A7;
y * z = yf (*) zf by Def02;
then x * (y * z) = xf (*) (yf (*) zf) by Def02;
hence thesis by A8,Ta1;
end;
take e;
let h be Element of GH3;
thus h * e = h & e * h = h by Lm1;
h in EnsHomography3;
then consider N be invertible Matrix of 3,F_Real such that
A9: h = homography(N);
reconsider Ng = N~ as invertible Matrix of 3,F_Real;
homography(Ng) in EnsHomography3;
then reconsider g = homography(Ng) as Element of GH3;
take g;
thus thesis by A9,Lm2;
end;
end;
theorem Ta2:
1_GroupHomography3 = homography(1.(F_Real,3))
proof
for h being Element of GH3 holds h * e = h & e * h = h by Lm1;
hence thesis by GROUP_1:4;
end;
theorem
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
let h,g be Element of GH3;
let N,Ng be invertible Matrix of 3,F_Real;
assume h = homography(N) & g = homography(Ng) & Ng = N~;
then h * g = 1_GH3 & g * h = 1_GH3 by Lm2,Ta2;
hence g = h" by GROUP_1:def 5;
end;
begin
definition
func Dir100 -> Point of ProjectiveSpace TOP-REAL 3 equals Dir |[1,0,0]|;
coherence by Th11,ANPROJ_1:26;
func Dir010 -> Point of ProjectiveSpace TOP-REAL 3 equals Dir |[0,1,0]|;
coherence by Th11,ANPROJ_1:26;
func Dir001 -> Point of ProjectiveSpace TOP-REAL 3 equals Dir |[0,0,1]|;
coherence by Th11,ANPROJ_1:26;
func Dir111 -> Point of ProjectiveSpace TOP-REAL 3 equals Dir |[1,1,1]|;
coherence by Th11,ANPROJ_1:26;
end;
theorem
Dir100 <> Dir010 &
Dir100 <> Dir001 &
Dir100 <> Dir111 &
Dir010 <> Dir001 &
Dir010 <> Dir111 &
Dir001 <> Dir111
proof
assume
A1: Dir100 = Dir010 or Dir100 = Dir001 or Dir100 = Dir111 or Dir010 = Dir001
or Dir010 = Dir111 or Dir001 = Dir111;
consider u100 be Element of TOP-REAL 3 such that
A2: u100 = |[1,0,0]| and
A3: Dir100 = Dir u100;
consider u010 be Element of TOP-REAL 3 such that
A4: u010 = |[0,1,0]| and
A5: Dir010 = Dir u010;
consider u001 be Element of TOP-REAL 3 such that
A6: u001 = |[0,0,1]| and
A7: Dir001 = Dir u001;
consider u111 be Element of TOP-REAL 3 such that
A8: u111 = |[1,1,1]| and
A9: Dir111 = Dir u111;
per cases by A1;
suppose
A10: Dir100 = Dir010;
u100 is not zero & u010 is not zero by A2,A4,EUCLID_5:4,FINSEQ_1:78;
then are_Prop u100, u010 by A3,A5,A10,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A12: u100 = a * u010 by ANPROJ_1:1;
|[1,0,0]| = |[a * 0,a * 1 ,0]| by A2,A4,A12,EUCLID_5:8
.= |[0,a,0]|;
then 1 = |[0,a,0]|`1 by EUCLID_5:2;
hence thesis by EUCLID_5:2;
end;
suppose
A13: Dir100 = Dir001;
u100 is not zero & u001 is not zero by A2,A6,EUCLID_5:4,FINSEQ_1:78;
then are_Prop u100, u001 by A13,A3,A7,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A15: u100 = a * u001 by ANPROJ_1:1;
|[1,0,0]| = |[a * 0,a * 0 ,a * 1]| by A2,A6,A15,EUCLID_5:8
.= |[0,0,a]|;
then 1 = |[0,0,a]|`1 by EUCLID_5:2;
hence thesis by EUCLID_5:2;
end;
suppose
A16: Dir100 = Dir111;
u100 is not zero & u111 is not zero by A2,A8,EUCLID_5:4,FINSEQ_1:78;
then are_Prop u100, u111 by A16,A3,A9,ANPROJ_1:22;
then consider a be Real such that
A17: a <> 0 and
A18: u100 = a * u111 by ANPROJ_1:1;
|[1,0,0]| = |[a * 1,a * 1 ,a * 1]| by A2,A8,A18,EUCLID_5:8
.= |[a,a,a]|;
then 0 = |[a,a,a]|`2 by EUCLID_5:2;
hence thesis by A17,EUCLID_5:2;
end;
suppose
A19: Dir010 = Dir001;
u010 is not zero & u001 is not zero by A4,A6,EUCLID_5:4,FINSEQ_1:78;
then are_Prop u010, u001 by A5,A7,A19,ANPROJ_1:22;
then consider a be Real such that
A20: a <> 0 and
A21: u010 = a * u001 by ANPROJ_1:1;
|[0,1,0]| = |[a * 0,a * 0 ,a * 1]| by A4,A6,A21,EUCLID_5:8
.= |[0,0,a]|;
then 0 = |[0,0,a]|`3 by EUCLID_5:2;
hence thesis by A20,EUCLID_5:2;
end;
suppose
A22: Dir010 = Dir111;
u010 is not zero & u111 is not zero by A4,A8,EUCLID_5:4,FINSEQ_1:78;
then are_Prop u010, u111 by A22,A5,A9,ANPROJ_1:22;
then consider a be Real such that
A23: a <> 0 and
A24: u010 = a * u111 by ANPROJ_1:1;
|[0,1,0]| = |[a * 1,a * 1 ,a]| by A4,A8,A24,EUCLID_5:8
.= |[a,a,a]|;
then 0 = |[a,a,a]|`1 by EUCLID_5:2;
hence thesis by A23,EUCLID_5:2;
end;
suppose
A25: Dir001 = Dir111;
u001 is not zero & u111 is not zero by A6,A8,EUCLID_5:4,FINSEQ_1:78;
then are_Prop u001, u111 by A7,A9,A25,ANPROJ_1:22;
then consider a be Real such that
A26: a <> 0 and
A27: u001 = a * u111 by ANPROJ_1:1;
|[0,0,1]| = |[a * 1,a * 1 ,a]| by A6,A8,A27,EUCLID_5:8
.= |[a,a,a]|;
then 0 = |[a,a,a]|`1 by EUCLID_5:2;
hence thesis by A26,EUCLID_5:2;
end;
end;
registration
let a be non zero Element of F_Real;
let N;
cluster a * N -> invertible for Matrix of 3,F_Real;
coherence
proof
consider N2 be Matrix of 3,F_Real such that
A1: N is_reverse_of N2 by MATRIX_6:def 3;
reconsider b = 1/a as Element of F_Real by XREAL_0:def 1;
A2: 1_(F_Real) = 1.F_Real;
a is non zero; then
A3: (b * a) * (N2 * N) = 1.F_Real * (N2 * N) by XCMPLX_1:106
.= N2 * N;
now
A4: width N2 = 3 & width N = 3 by MATRIX_0:23; then
A5: width N2 = len N & width N = len N2 by MATRIX_0:23;
A6: width N2 = len (a * N) & width N = len (b * N2) by A4,MATRIX_0:23;
hence (b * N2) * (a * N) = b * (N2 * (a * N)) by MATRIX15:1
.= b * (a * (N2 * N)) by A5,MATRIXR1:22
.= (b * a) * (N2 * N) by MATRIX15:2
.= (a * b) * (N * N2) by A1,MATRIX_6:def 2
.= a * (b * (N * N2)) by MATRIX15:2
.= a * (N * (b * N2)) by A5,MATRIXR1:22
.= (a * N) * (b * N2) by A6,MATRIX15:1;
thus (b * N2) * (a * N) = b * (N2 * (a * N)) by A6,MATRIX15:1
.= b * (a * (N2 * N)) by A5,MATRIXR1:22
.= N2 * N by A3,MATRIX15:2
.= 1.(F_Real,3) by A1,MATRIX_6:def 2;
end;
hence thesis by MATRIX_6:def 2,MATRIX_6:def 3;
end;
end;
theorem
for a being non zero Element of F_Real
holds (homography(a*N1)).P = (homography(N1)).P
proof
let a be non zero Element of F_Real;
set M = a * 1.(F_Real,3);
thus (homography(a*N1)).P = (homography(M * N1)).P by Th02
.= (homography(M)).((homography(N1)).P) by Th14
.= (homography(N1)).(P) by Th17;
end;
theorem Th20:
not P1,P2,P3 are_collinear implies
ex N being invertible Matrix of 3,F_Real st
(homography(N)).P1 = Dir100 &
(homography(N)).P2 = Dir010 &
(homography(N)).P3 = Dir001
proof
assume
A1: not P1,P2,P3 are_collinear;
consider u1 be Element of TOP-REAL 3 such that
A2: u1 is not zero and
A3: P1 = Dir u1 by ANPROJ_1:26;
consider u2 be Element of TOP-REAL 3 such that
A4: u2 is not zero and
A5: P2 = Dir u2 by ANPROJ_1:26;
consider u3 be Element of TOP-REAL 3 such that
A6: u3 is not zero and
A7: P3 = Dir u3 by ANPROJ_1:26;
A8: |{u1,u2,u3}| <> 0 by ANPROJ_8:43,A1,A2,A3,A4,A5,A6,A7,ANPROJ_2:23;
reconsider pf = u1,qf = u2,rf = u3 as FinSequence of F_Real by RVSUM_1:145;
consider N being Matrix of 3,F_Real such that
A9: N is invertible and
A10: N * pf = F2M <e1> and
A11: N * qf = F2M <e2> and
A12: N * rf = F2M <e3> by A8,ANPROJ_8:94;
reconsider N as invertible Matrix of 3,F_Real by A9;
A13: len <e1> = 3 & len <e2> = 3 & len <e3> = 3 by EUCLID_8:50;
take N;
thus (homography(N)).P1 = Dir100
proof
consider nu1,nv1 being Element of TOP-REAL 3,
u1f being FinSequence of F_Real,
p1 being FinSequence of (1-tuples_on REAL) such that
A14: P1 = Dir nu1 and
A15: nu1 is not zero and
A16: nu1 = u1f and
A17: p1 = N * u1f and
A18: nv1 = M2F p1 and
A19: nv1 is not zero and
A20: (homography(N)).P1 = Dir nv1 by ANPROJ_8:def 4;
are_Prop u1,nu1 by A2,A3,A14,A15,ANPROJ_1:22;
then consider a be Real such that
A21: a <> 0 and
A22: u1 = a * nu1 by ANPROJ_1:1;
reconsider b = 1/a as Real;
nu1 in TOP-REAL 3; then
A23: nu1 in REAL 3 by EUCLID:22;
width(<*u1f*>) = len nu1 by A16,ANPROJ_8:75
.= 3 by A23,EUCLID_8:50; then
A24: len ( <*u1f*>@ ) = width <*u1f*> by MATRIX_0:29
.= len nu1 by ANPROJ_8:75,A16
.= 3 by A23,EUCLID_8:50;
A25: width N = len (<*u1f*>@) by MATRIX_0:24,A24;
A26: len (N * u1f) = len (N * (<*u1f*>@)) by LAPLACE:def 9
.= len N by A25,MATRIX_3:def 4
.= 3 by MATRIX_0:24;
len <e1> = 3 by EUCLID_8:def 1,FINSEQ_1:45; then
A27: F2M <e1> = <* <* <e1>.1 *>, <* <e1>.2 *>, <* <e1>.3 *> *>
by ANPROJ_8:def 1;
reconsider s1 = u1f.1, s2 = u1f.2, s3 = u1f.3 as Element of F_Real
by XREAL_0:def 1;
reconsider t1 = u1.1, t2 = u1.2, t3 = u1.3 as Element of F_Real
by XREAL_0:def 1;
A28: (N * pf).1 = <* <e1>.1 *> & (N * pf).2 = <* <e1>.2 *> &
(N * pf).3 = <* <e1>.3 *> by A10,A27;
A29: ((N * pf).1).1 = |[1,0,0]|.1 by A28,EUCLID_8:def 1
.= |[1,0,0]|`1 by EUCLID_5:def 1
.= 1 by EUCLID_5:2;
A30: ((N * pf).2).1 = |[1,0,0]|.2 by A28,EUCLID_8:def 1
.= |[1,0,0]|`2 by EUCLID_5:def 2
.= 0 by EUCLID_5:2;
A31: ((N * pf).3).1 = |[1,0,0]|.3 by A28,EUCLID_8:def 1
.= |[1,0,0]|`3 by EUCLID_5:def 3
.= 0 by EUCLID_5:2;
p1.1 = <* (N * <*u1f*>@)*(1,1) *> & p1.2 = <* (N * <*u1f*>@)*(2,1) *> &
p1.3 = <* (N * <*u1f*>@)*(3,1) *> by A16,A17,FINSEQ_1:1,Lem02;
then reconsider p111 = (p1.1).1, p121 = (p1.2).1,
p131 = (p1.3).1 as Real;
A32: p111 = b * (Line(N,1) "*" pf) & p121 = b * (Line(N,2) "*" pf) &
p131 = b * (Line(N,3) "*" pf) by FINSEQ_1:1,A16,A17,A21,A22,Lem04;
A33: a * p1 = N * pf
proof
consider pp1,pp2,pp3 be Real such that
A34: pp1 = (p1.1).1 and
A35: pp2 = (p1.2).1 and
A36: pp3 = (p1.3).1 and
A37: a * p1 = <* <* a * pp1 *>, <* a * pp2 *>, <* a * pp3 *> *>
by A17,A26,ANPROJ_8:def 3;
now
thus len (N * pf) = 3 by A10,A13,ANPROJ_8:78;
thus (N * pf).1 = <* a * pp1 *>
proof
Line(N,1) "*" pf = ((N * pf).1).1 by FINSEQ_1:1,Lem05;
then len ((N * pf).1) = 1 & ((N * pf).1).1 = a * p111
by A28,FINSEQ_1:40,A29,A32,A21,XCMPLX_1:87;
hence thesis by A34,FINSEQ_1:40;
end;
thus (N * pf).2 = <* a * pp2 *>
proof
Line(N,2) "*" pf = ((N * pf).2).1 by FINSEQ_1:1,Lem05;
hence thesis by A35,A28,A30,A32;
end;
Line(N,3) "*" pf = ((N * pf).3).1 by FINSEQ_1:1,Lem05;
hence (N * pf).3 = <* a * pp3 *> by A36,A28,A32,A31;
end;
hence thesis by A37,FINSEQ_1:45;
end;
len <e1> = 3 by EUCLID_8:50; then
A38: <e1> = M2F F2M <e1> by ANPROJ_8:86
.= a * nv1 by A18,A33,A10,A26,A17,ANPROJ_8:83;
nv1 is non zero & a * nv1 is non zero & are_Prop nv1,a * nv1
by A19,A21,Th04,ANPROJ_1:1;
hence thesis by A38,EUCLID_8:def 1,ANPROJ_1:22,A20;
end;
thus (homography(N)).P2 = Dir010
proof
consider nu2,nv2 being Element of TOP-REAL 3,
u2f being FinSequence of F_Real,
p2 being FinSequence of (1-tuples_on REAL) such that
A39: P2 = Dir nu2 and
A40: nu2 is not zero and
A41: nu2 = u2f and
A42: p2 = N * u2f and
A43: nv2 = M2F p2 and
A44: nv2 is not zero and
A45: (homography(N)).P2 = Dir nv2 by ANPROJ_8:def 4;
are_Prop u2,nu2 by A4,A5,A39,A40,ANPROJ_1:22;
then consider a be Real such that
A46: a <> 0 and
A47: u2 = a * nu2 by ANPROJ_1:1;
reconsider b = 1/a as Real;
nu2 in TOP-REAL 3; then
A48: nu2 in REAL 3 by EUCLID:22;
width(<*u2f*>) = len nu2 by A41,ANPROJ_8:75
.= 3 by A48,EUCLID_8:50;
then
A49: len ( <*u2f*>@ ) = width <*u2f*> by MATRIX_0:29
.= len nu2 by ANPROJ_8:75,A41
.= 3 by A48,EUCLID_8:50;
A50: width N = len (<*u2f*>@) by MATRIX_0:24,A49;
A51: len (N * u2f) = len (N * (<*u2f*>@)) by LAPLACE:def 9
.= len N by A50,MATRIX_3:def 4
.= 3 by MATRIX_0:24;
len <e2> = 3 by EUCLID_8:def 2,FINSEQ_1:45; then
A52: F2M <e2> = <* <* <e2>.1 *>, <* <e2>.2 *>, <* <e2>.3 *> *>
by ANPROJ_8:def 1;
reconsider s1 = u2f.1, s2 = u2f.2, s3 = u2f.3 as Element of F_Real
by XREAL_0:def 1;
reconsider t1 = u2.1, t2 = u2.2, t3 = u2.3 as Element of F_Real
by XREAL_0:def 1;
A53: (N * qf).1 = <* <e2>.1 *> & (N * qf).2 = <* <e2>.2 *> &
(N * qf).3 = <* <e2>.3 *> by A11,A52;
A54: ((N * qf).1).1 = |[0,1,0]|.1 by A53,EUCLID_8:def 2
.= |[0,1,0]|`1 by EUCLID_5:def 1
.= 0 by EUCLID_5:2;
A55: ((N * qf).2).1 = |[0,1,0]|.2 by A53,EUCLID_8:def 2
.= |[0,1,0]|`2 by EUCLID_5:def 2
.= 1 by EUCLID_5:2;
A56: ((N * qf).3).1 = |[0,1,0]|.3 by A53,EUCLID_8:def 2
.= |[0,1,0]|`3 by EUCLID_5:def 3
.= 0 by EUCLID_5:2;
p2.1 = <* (N * <*u2f*>@)*(1,1) *> &
p2.2 = <* (N * <*u2f*>@)*(2,1) *> & p2.3 = <* (N * <*u2f*>@)*(3,1) *>
by A41,A42,FINSEQ_1:1,Lem02;
then reconsider p211 = (p2.1).1, p221 = (p2.2).1,
p231 = (p2.3).1 as Real;
A57: p211 = b * (Line(N,1) "*" qf) & p221 = b * (Line(N,2) "*" qf) &
p231 = b * (Line(N,3) "*" qf) by FINSEQ_1:1,A41,A42,A46,A47,Lem04;
A58: a * p2 = N * qf
proof
consider pp1,pp2,pp3 be Real such that
A59: pp1 = (p2.1).1 and
A60: pp2 = (p2.2).1 and
A61: pp3 = (p2.3).1 and
A62: a * p2 = <* <* a * pp1 *>, <* a * pp2 *>, <* a * pp3 *> *>
by A42,A51,ANPROJ_8:def 3;
now
thus len (N * qf) = 3 by A11,A13,ANPROJ_8:78;
Line(N,1) "*" qf = ((N * qf).1).1 by FINSEQ_1:1,Lem05;
hence (N * qf).1 = <* a * pp1 *> by A59,A53,A57,A54;
thus (N * qf).2 = <* a * pp2 *>
proof
Line(N,2) "*" qf = ((N * qf).2).1 by FINSEQ_1:1,Lem05;
then len ((N * qf).2) = 1 & ((N * qf).2).1 = a * p221
by A53,FINSEQ_1:40,A55,A57,A46,XCMPLX_1:87;
hence thesis by A60,FINSEQ_1:40;
end;
Line(N,3) "*" qf = ((N * qf).3).1 by FINSEQ_1:1,Lem05;
hence (N * qf).3 = <* a * pp3 *> by A61,A53,A57,A56;
end;
hence thesis by A62,FINSEQ_1:45;
end;
len <e2> = 3 by EUCLID_8:50; then
A63: <e2> = M2F F2M <e2> by ANPROJ_8:86
.= a * nv2 by A43,A58,A11,A51,A42,ANPROJ_8:83;
nv2 is non zero & a * nv2 is non zero & are_Prop nv2,a * nv2
by A44,A46,Th04,ANPROJ_1:1;
hence thesis by A63,EUCLID_8:def 2,ANPROJ_1:22,A45;
end;
thus (homography(N)).P3 = Dir001
proof
consider nu3,nv3 being Element of TOP-REAL 3,
u3f being FinSequence of F_Real,
p3 being FinSequence of (1-tuples_on REAL) such that
A64: P3 = Dir nu3 and
A65: nu3 is not zero and
A66: nu3 = u3f and
A67: p3 = N * u3f and
A68: nv3 = M2F p3 and
A69: nv3 is not zero and
A70: (homography(N)).P3 = Dir nv3 by ANPROJ_8:def 4;
are_Prop u3,nu3 by A6,A7,A64,A65,ANPROJ_1:22;
then consider a be Real such that
A71: a <> 0 and
A72: u3 = a * nu3 by ANPROJ_1:1;
reconsider b = 1/a as Real;
nu3 in TOP-REAL 3; then
A73: nu3 in REAL 3 by EUCLID:22;
width(<*u3f*>) = len nu3 by A66,ANPROJ_8:75
.= 3 by A73,EUCLID_8:50;
then
A74: len ( <*u3f*>@ ) = width <*u3f*> by MATRIX_0:29
.= len nu3 by ANPROJ_8:75,A66
.= 3 by A73,EUCLID_8:50;
A75: width N = len (<*u3f*>@) by MATRIX_0:24,A74;
A76: len (N * u3f) = len (N * (<*u3f*>@)) by LAPLACE:def 9
.= len N by A75,MATRIX_3:def 4
.= 3 by MATRIX_0:24;
len <e3> = 3 by EUCLID_8:def 3,FINSEQ_1:45; then
A77: F2M <e3> = <* <* <e3>.1 *>, <* <e3>.2 *>, <* <e3>.3 *> *>
by ANPROJ_8:def 1;
reconsider s1 = u3f.1, s2 = u3f.2, s3 = u3f.3 as Element of F_Real
by XREAL_0:def 1;
reconsider t1 = u3.1, t2 = u3.2, t3 = u3.3 as Element of F_Real
by XREAL_0:def 1;
A78: (N * rf).1 = <* <e3>.1 *> & (N * rf).2 = <* <e3>.2 *> &
(N * rf).3 = <* <e3>.3 *> by A12,A77;
A79: ((N * rf).1).1 = |[0,0,1]|.1 by A78,EUCLID_8:def 3
.= |[0,0,1]|`1 by EUCLID_5:def 1
.= 0 by EUCLID_5:2;
A80: ((N * rf).2).1 = |[0,0,1]|.2 by A78,EUCLID_8:def 3
.= |[0,0,1]|`2 by EUCLID_5:def 2
.= 0 by EUCLID_5:2;
A81: ((N * rf).3).1 = |[0,0,1]|.3 by A78,EUCLID_8:def 3
.= |[0,0,1]|`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
p3.1 = <* (N * <*u3f*>@)*(1,1) *> &
p3.2 = <* (N * <*u3f*>@)*(2,1) *> & p3.3 = <* (N * <*u3f*>@)*(3,1) *>
by A66,A67,FINSEQ_1:1,Lem02;
then reconsider p311 = (p3.1).1, p321 = (p3.2).1,
p331 = (p3.3).1 as Real;
A82: p311 = b * (Line(N,1) "*" rf) &
p321 = b * (Line(N,2) "*" rf) & p331 = b * (Line(N,3) "*" rf)
by FINSEQ_1:1,A66,A67,A71,A72,Lem04;
A83: a * p3 = N * rf
proof
consider pp1,pp2,pp3 be Real such that
A84: pp1 = (p3.1).1 and
A85: pp2 = (p3.2).1 and
A86: pp3 = (p3.3).1 and
A87: a * p3 = <* <* a * pp1 *>, <* a * pp2 *>, <* a * pp3 *> *>
by A67,A76,ANPROJ_8:def 3;
now
thus len (N * rf) = 3 by A12,A13,ANPROJ_8:78;
Line(N,1) "*" rf = ((N * rf).1).1 by FINSEQ_1:1,Lem05;
hence (N * rf).1 = <* a * pp1 *> by A84,A78,A82,A79;
Line(N,2) "*" rf = ((N * rf).2).1 by FINSEQ_1:1,Lem05;
hence (N * rf).2 = <* a * pp2 *> by A85,A78,A82,A80;
thus (N * rf).3 = <* a * pp3 *>
proof
Line(N,3) "*" rf = ((N * rf).3).1 by FINSEQ_1:1,Lem05;
then len ((N * rf).3) = 1 & ((N * rf).3).1 = a * p331
by A78,FINSEQ_1:40,A81,A82,A71,XCMPLX_1:87;
hence thesis by A86,FINSEQ_1:40;
end;
end;
hence thesis by A87,FINSEQ_1:45;
end;
len <e3> = 3 by EUCLID_8:50; then
A88: <e3> = M2F F2M <e3> by ANPROJ_8:86
.= a * nv3 by A68,A83,A12,A76,A67,ANPROJ_8:83;
nv3 is non zero & a * nv3 is non zero & are_Prop nv3,a * nv3
by A69,A71,Th04,ANPROJ_1:1;
hence thesis by A88,EUCLID_8:def 3,ANPROJ_1:22,A70;
end;
end;
theorem Th21:
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
let a,b,c be non zero Element of F_Real;
assume
A1: N = <* <* a,0,0 *>, <* 0,b,0 *>, <* 0,0,c *> *>;
thus (homography(N)).Dir100 = Dir100
proof
consider u,v being Element of TOP-REAL 3,
uf being FinSequence of F_Real,
p being FinSequence of (1-tuples_on REAL) such that
A2: Dir100 = Dir u and
A3: u is not zero and
A4: u = uf and
A5: p = N * uf and
A6: v = M2F p and
A7: v is not zero and
A8: (homography(N)).Dir100 = Dir v by ANPROJ_8:def 4;
|[1,0,0]| is not zero by EUCLID_8:def 1,Th13;
then are_Prop u, |[1,0,0]| by A2,A3,ANPROJ_1:22;
then consider d be Real such that
d <> 0 and
A9: u = d * |[1,0,0]| by ANPROJ_1:1;
A10: u = |[d * 1, d * 0,d * 0]| by A9,EUCLID_5:8
.= |[d,0,0]|;
then u`1 = d & u`2 = 0 & u`3 = 0 by EUCLID_5:2; then
A11: uf.1 = d & uf.2 = 0 & uf.3 = 0
by A4,EUCLID_5:def 1,EUCLID_5:def 2,EUCLID_5:def 3;
u in TOP-REAL 3;
then u in REAL 3 by EUCLID:22; then
A12: <*uf*>@ = <* <* d *>,<* 0 *>, <* 0 *> *>
by A11,A4,EUCLID_8:50,ANPROJ_8:77;
then reconsider Mu = <*uf*>@ as Matrix of 3,1,F_Real by ANPROJ_8:4;
reconsider z = 0 as Element of F_Real;
reconsider d as Element of F_Real by XREAL_0:def 1;
A13: p = N * Mu by A5,LAPLACE:def 9
.= <* <* a * d + z * z + z * z *>,
<* z * d + b * z + z * z *>,
<* z * d + z * z + c * z *> *> by A1,A12,Th08
.= <* <* a * d *>, <* 0 *>, <* 0 *> *>;
v = |[ a * d, 0, 0 ]|
proof
A14: <* a * d *>.1 = a * d & <* 0 *>.1 = 0;
A15: p.1 = <* a * d *> & p.2 = <* 0 *> & p.3 = <* 0 *>
by A13;
len p = 3 by A13,FINSEQ_1:45;
hence thesis by A14,A15,A6,ANPROJ_8:def 2;
end;
then
A16: v = |[ a * d, a * 0, a * 0]|
.= a * u by A10,EUCLID_5:8;
a is non zero;
then are_Prop v,u by A16,ANPROJ_1:1;
hence thesis by A2,A3,A7,A8,ANPROJ_1:22;
end;
thus (homography(N)).Dir010 = Dir010
proof
consider u,v being Element of TOP-REAL 3,
uf being FinSequence of F_Real,
p being FinSequence of (1-tuples_on REAL)
such that
A17: Dir010 = Dir u and
A18: u is not zero and
A19: u = uf and
A20: p = N * uf and
A21: v = M2F p and
A22: v is not zero and
A23: (homography(N)).Dir010 = Dir v by ANPROJ_8:def 4;
|[0,1,0]| is not zero by EUCLID_8:def 2,Th13;
then are_Prop u, |[0,1,0]| by A17,A18,ANPROJ_1:22;
then consider d be Real such that
d <> 0 and
A24: u = d * |[0,1,0]| by ANPROJ_1:1;
A25: u = |[d * 0, d * 1,d * 0]| by A24,EUCLID_5:8
.= |[0,d,0]|;
then u`1 = 0 & u`2 = d & u`3 = 0 by EUCLID_5:2; then
A26: uf.1 = 0 & uf.2 = d & uf.3 = 0
by A19,EUCLID_5:def 1,EUCLID_5:def 2,EUCLID_5:def 3;
u in TOP-REAL 3;
then u in REAL 3 by EUCLID:22; then
A27: <*uf*>@ = <* <* 0 *>,<* d *>, <* 0 *> *>
by A26,A19,EUCLID_8:50,ANPROJ_8:77;
reconsider Mu = <*uf*>@ as Matrix of 3,1,F_Real by A27,ANPROJ_8:4;
reconsider z = 0 as Element of F_Real;
reconsider d as Element of F_Real by XREAL_0:def 1;
A28: p = N * Mu by A20,LAPLACE:def 9
.= <* <* a * z + z * d + z * z *>,
<* z * z + b * d + z * z *>,
<* z * d + z * z + c * z *> *> by A1,A27,Th08
.= <* <* 0 *>, <* b * d *>, <* 0 *> *>;
v = |[ 0, b * d, 0 ]|
proof
A29: <* 0 *>.1 = 0 & <* b * d *>.1 = b * d;
A30: p.1 = <* 0 *> & p.2 = <* b * d *> & p.3 = <* 0 *>
by A28;
len p = 3 by A28,FINSEQ_1:45;
hence thesis by A29,A30,A21,ANPROJ_8:def 2;
end;
then
A31: v = |[ b * 0, b * d, b * 0]|
.= b * u by A25,EUCLID_5:8;
b is non zero;
then are_Prop v,u by A31,ANPROJ_1:1;
hence thesis by A17,A18,A22,A23,ANPROJ_1:22;
end;
thus (homography(N)).Dir001 = Dir001
proof
consider u,v being Element of TOP-REAL 3,
uf being FinSequence of F_Real,
p being FinSequence of (1-tuples_on REAL) such that
A31BIS: Dir001 = Dir u and
A32: u is not zero and
A33: u = uf and
A34: p = N * uf and
A35: v = M2F p and
A36: v is not zero and
A37: (homography(N)).Dir001 = Dir v by ANPROJ_8:def 4;
|[0,0,1]| is not zero by EUCLID_8:def 3,Th13;
then are_Prop u, |[0,0,1]| by A31BIS,A32,ANPROJ_1:22;
then consider d be Real such that
d <> 0 and
A38: u = d * |[0,0,1]| by ANPROJ_1:1;
A39: u = |[d * 0, d * 0,d * 1]| by A38,EUCLID_5:8
.= |[0,0,d]|;
then u`1 = 0 & u`2 = 0 & u`3 = d by EUCLID_5:2; then
A40: uf.1 = 0 & uf.2 = 0 & uf.3 = d
by A33,EUCLID_5:def 1,EUCLID_5:def 2,EUCLID_5:def 3;
u in TOP-REAL 3;
then u in REAL 3 by EUCLID:22; then
A41: <*uf*>@ = <* <* 0 *>,<* 0 *>, <* d *> *>
by A40,A33,EUCLID_8:50,ANPROJ_8:77;
reconsider Mu = <*uf*>@ as Matrix of 3,1,F_Real by A41,ANPROJ_8:4;
reconsider z = 0 as Element of F_Real;
reconsider d as Element of F_Real by XREAL_0:def 1;
A42: p = N * Mu by A34,LAPLACE:def 9
.= <* <* a * z + z * z + z * d *>,
<* z * z + b * z + z * d *>,
<* z * z + z * z + c * d *> *> by A1,A41,Th08
.= <* <* 0 *>, <* 0 *>, <* c * d *> *>;
v = |[ 0, 0, c * d ]|
proof
A43: <* c * d *>.1 = c * d & <* 0 *>.1 = 0;
A44: p.3 = <* c * d *> & p.2 = <* 0 *> & p.1 = <* 0 *>
by A42;
len p = 3 by A42,FINSEQ_1:45;
hence thesis by A43,A44,A35,ANPROJ_8:def 2;
end;
then
A45: v = |[ c * 0, c * 0, c * d]|
.= c * u by A39,EUCLID_5:8;
c is non zero;
then are_Prop v,u by A45,ANPROJ_1:1;
hence thesis by A31BIS,A32,A36,A37,ANPROJ_1:22;
end;
end;
theorem Th22:
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
let P be Point of ProjectiveSpace TOP-REAL 3;
consider u be Element of TOP-REAL 3 such that
A1: u is non zero and
A2: P = Dir u by ANPROJ_1:26;
A3: u = |[u`1,u`2,u`3]| by EUCLID_5:3
.= |[u.1,u`2,u`3]| by EUCLID_5:def 1
.= |[u.1,u.2,u`3]| by EUCLID_5:def 2
.= |[u.1,u.2,u.3]| by EUCLID_5:def 3;
reconsider a = u.1,b = u.2,c = u.3 as Element of F_Real by XREAL_0:def 1;
take a,b,c;
thus P = Dir |[a,b,c]| by A2,A3;
thus a <> 0 or b <> 0 or c <> 0 by A1,A3,EUCLID_5:4;
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
let a,b,c be Element of F_Real;
let P be Point of ProjectiveSpace TOP-REAL 3;
assume that
A1: P = Dir |[a,b,c]| and
A2: a <> 0 or b <> 0 or c <> 0;
thus not (Dir100,Dir010,P are_collinear) implies c <> 0
proof
assume
A3: not Dir100,Dir010,P are_collinear;
assume
A4: c = 0;
A5: |[a,b,c]| is not zero by A2,EUCLID_5:4,FINSEQ_1:78;
A6: not |[1,0,0]|,|[0,1,0]|,|[a,b,c]| are_LinDep
by A3,ANPROJ_2:23,Th11,A5,A1;
(-a) * |[1,0,0]| + (-b) * |[0,1,0]| + 1 * |[a,b,c]|
= |[ (-a) * 1, (-a) * 0,(-a) * 0]| + (-b) * |[0,1,0]| + 1 * |[a,b,c]|
by EUCLID_5:8
.= |[ (-a), 0,0]| + |[(-b) * 0,(-b) * 1,(-b) * 0]| + 1 * |[a,b,c]|
by EUCLID_5:8
.= |[ (-a), 0,0]| + |[0,(-b),0]| + |[1 * a,1 * b,1 * c]| by EUCLID_5:8
.= |[ (-a) + 0, 0 + (-b),0 + 0]| + |[a,b,c]| by EUCLID_5:6
.= |[(-a) + a,(-b) + b,0 + c]| by EUCLID_5:6
.= 0.TOP-REAL 3 by A4,EUCLID_5:4;
hence contradiction by A6,ANPROJ_1:def 2;
end;
thus not (Dir100,Dir001,P are_collinear) implies b <> 0
proof
assume
A7: not Dir100,Dir001,P are_collinear;
assume
A8: b = 0;
A9: |[a,b,c]| is not zero by A2,EUCLID_5:4,FINSEQ_1:78;
A10: not |[1,0,0]|,|[0,0,1]|,|[a,b,c]| are_LinDep
by A7,ANPROJ_2:23,Th11,A9,A1;
(-a) * |[1,0,0]| + (-c) * |[0,0,1]| + 1 * |[a,b,c]|
= |[ (-a) * 1, (-a) * 0,(-a) * 0]| + (-c) * |[0,0,1]| + 1 * |[a,b,c]|
by EUCLID_5:8
.= |[ (-a), 0,0]| + |[(-c) * 0,(-c) * 0,(-c) * 1]| + 1 * |[a,b,c]|
by EUCLID_5:8
.= |[ (-a), 0,0]| + |[0,0,(-c)]| + |[1 * a,1 * b,1 * c]| by EUCLID_5:8
.= |[ (-a) + 0, 0 + 0,0 + (-c)]| + |[a,b,c]| by EUCLID_5:6
.= |[(-a) + a,0 + b,(-c) + c]| by EUCLID_5:6
.= 0.TOP-REAL 3 by A8,EUCLID_5:4;
hence contradiction by A10,ANPROJ_1:def 2;
end;
thus not (Dir010,Dir001,P are_collinear) implies a <> 0
proof
assume
A11: not Dir010,Dir001,P are_collinear;
assume
A12: a = 0;
A13: |[a,b,c]| is not zero by A2,EUCLID_5:4,FINSEQ_1:78;
A14: not |[0,1,0]|,|[0,0,1]|,|[a,b,c]| are_LinDep
by A11,ANPROJ_2:23,Th11,A13,A1;
(-b) * |[0,1,0]| + (-c) * |[0,0,1]| + 1 * |[a,b,c]|
= |[ (-b) * 0, (-b) * 1,(-b) * 0]| + (-c) * |[0,0,1]| + 1 * |[a,b,c]|
by EUCLID_5:8
.= |[ 0, (-b),0]| + |[(-c) * 0,(-c) * 0,(-c) * 1]| + 1 * |[a,b,c]|
by EUCLID_5:8
.= |[ 0,(-b),0]| + |[0,0,(-c)]| + |[1 * a,1 * b,1 * c]| by EUCLID_5:8
.= |[ 0 + 0, (-b) + 0,0 + (-c)]| + |[a,b,c]| by EUCLID_5:6
.= |[0 + a,(-b) + b,(-c) + c]| by EUCLID_5:6
.= 0.TOP-REAL 3 by A12,EUCLID_5:4;
hence contradiction by A14,ANPROJ_1:def 2;
end;
end;
theorem Th23:
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
let P be Point of ProjectiveSpace TOP-REAL 3;
assume that
A1: not (Dir100,Dir010,P are_collinear) and
A2: not (Dir100,Dir001,P are_collinear) and
A3: not (Dir010,Dir001,P are_collinear);
consider a,b,c being Element of F_Real such that
A4: P = Dir |[a,b,c]| and
A5: (a <> 0 or b <> 0 or c <> 0) by Th22;
a is non zero & b is non zero & c is non zero by A1,A2,A3,A4,A5,Lem07;
then reconsider a,b,c as non zero Element of F_Real;
take a,b,c;
thus thesis by A4;
end;
theorem Th24:
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
let a,b,c,ia,ib,ic be non zero Element of F_Real;
let P be Point of ProjectiveSpace TOP-REAL 3;
let N be invertible Matrix of 3,F_Real;
assume that
A1: P = Dir |[a,b,c]| and
A2: ia = 1/a and
A3: ib = 1/b and
A4: ic = 1/c and
A5: N = <* <* ia,0,0 *>,<* 0,ib,0 *>,<* 0,0,ic *> *>;
consider u,v being Element of TOP-REAL 3,
uf being FinSequence of F_Real,
p being FinSequence of (1-tuples_on REAL) such that
A15: P = Dir u and
A16: u is not zero and
A17: u = uf and
A18: p = N * uf and
A19: v = M2F p and
A20: v is not zero and
A21: (homography(N)).P = Dir v by ANPROJ_8:def 4;
|[a,b,c]| is non zero
proof
assume |[a,b,c]| is zero;
then a is zero & b is zero & c is zero by EUCLID_5:4,FINSEQ_1:78;
hence thesis;
end;
then are_Prop u,|[a,b,c]| by A1,A15,A16,ANPROJ_1:22;
then consider d be Real such that
A22: d <> 0 and
A23: u = d * |[a,b,c]| by ANPROJ_1:1;
A24: u = <* d * a, d * b, d * c *> by A23,EUCLID_5:8;
A25: uf.1 = d * a & uf.2 = d * b & uf.3 = d * c by A24,A17;
u in TOP-REAL 3;
then u in REAL 3 by EUCLID:22; then
A26: <*uf*>@ = <* <* d * a *>,<* d * b *>, <* d * c *> *>
by A25,A17,EUCLID_8:50,ANPROJ_8:77;
reconsider Mu = <*uf*>@ as Matrix of 3,1,F_Real by A26,ANPROJ_8:4;
reconsider z = 0, da = d * a,db = d * b,dc = d * c as Element of F_Real
by XREAL_0:def 1;
A27: p = N * Mu by A18,LAPLACE:def 9
.= <* <* ia * da + z * db + z * dc *>,
<* z * da + ib * db + z * dc *>,
<* z * da + z * db + ic * dc *> *> by A26,A5,Th08
.= <* <* ia * da *>, <* ib * db *>, <* ic * dc *> *>;
A28: v = |[ ia * da, ib * db, ic * dc ]|
proof
A29: <* ia * da *>.1 = ia * da & <* ib * db *>.1 = ib * db &
<* ic * dc *>.1 = ic * dc;
A30: p.1 = <* ia * da *> & p.2 = <* ib * db *> & p.3 = <* ic * dc *>
by A27;
len p = 3 by A27,FINSEQ_1:45;
hence thesis by A29,A30,A19,ANPROJ_8:def 2;
end;
A31: a is non zero & b is non zero & c is non zero;
now
thus ia * da = (1/a) * a * d by A2
.= 1 * d by A31,XCMPLX_1:106
.= d;
thus ib * db = (1/b) * b * d by A3
.= 1 * d by A31,XCMPLX_1:106
.= d;
thus ic * dc = (1/c) * c * d by A4
.= 1 * d by A31,XCMPLX_1:106
.= d;
end;
then v = |[ d * 1,d * 1, d * 1]| by A28
.= d * |[1,1,1]| by EUCLID_5:8;
then are_Prop v,|[1,1,1]| by A22,ANPROJ_1:1;
hence thesis by Th11,A20,ANPROJ_1:22,A21;
end;
theorem Th25:
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
let P be Point of ProjectiveSpace TOP-REAL 3;
assume that
A1: not (Dir100,Dir010,P are_collinear) and
A2: not (Dir100,Dir001,P are_collinear) and
A3: not (Dir010,Dir001,P are_collinear);
consider a,b,c being non zero Element of F_Real such that
A4: P = Dir |[a,b,c]| by Th23,A1,A2,A3;
reconsider ia = 1/a, ib = 1/b, ic = 1/c as Element of F_Real
by XREAL_0:def 1;
ia is non zero & ib is non zero & ic is non zero by XCMPLX_1:50;
then reconsider ia,ib,ic as non zero Element of F_Real;
take ia,ib,ic;
thus thesis by A4,Th24;
end;
theorem Th26:
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
let P1,P2,P3,P4 be Point of ProjectiveSpace TOP-REAL 3;
assume that
A1: not (P1,P2,P3 are_collinear) and
A2: not (P1,P2,P4 are_collinear) and
A3: not (P1,P3,P4 are_collinear) and
A4: not (P2,P3,P4 are_collinear);
consider N1 being invertible Matrix of 3,F_Real such that
A5: (homography(N1)).P1 = Dir100 and
A6: (homography(N1)).P2 = Dir010 and
A7: (homography(N1)).P3 = Dir001 by A1,Th20;
set Q1 = (homography(N1)).P1, Q2 = (homography(N1)).P2,
Q3 = (homography(N1)).P3, Q4 = (homography(N1)).P4;
not (Q1,Q2,Q3 are_collinear) & not (Q1,Q2,Q4 are_collinear) &
not (Q1,Q3,Q4 are_collinear) & not (Q2,Q3,Q4 are_collinear)
by A1,A2,A3,A4,ANPROJ_8:102;
then consider a,b,c being non zero Element of F_Real such that
A8: for N2 being invertible Matrix of 3,F_Real st
N2 = <* <* a,0,0 *>,<* 0,b,0 *>,<* 0,0,c *> *> holds
(homography(N2)).Q4 = Dir111 by A5,A6,A7,Th25;
reconsider N2 = <* <* a,0,0 *>,<* 0,b,0 *>,<* 0,0,c *> *> as
invertible Matrix of 3,F_Real by Th10;
reconsider N = N2 * N1 as invertible Matrix of 3,F_Real;
take N;
now
thus Dir100 = (homography(N2)).Q1 by A5,Th21
.= (homography(N2 * N1)).P1 by Th14;
thus Dir010 = (homography(N2)).Q2 by A6,Th21
.= (homography(N2 * N1)).P2 by Th14;
thus Dir001 = (homography(N2)).Q3 by A7,Th21
.= (homography(N2 * N1)).P3 by Th14;
thus Dir111 = (homography(N2)).Q4 by A8
.= (homography(N2 * N1)).P4 by Th14;
end;
hence thesis;
end;
theorem
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
let P1,P2,P3,P4,Q1,Q2,Q3,Q4 be Point of ProjectiveSpace TOP-REAL 3;
assume that
A1: not (P1,P2,P3 are_collinear) & not (P1,P2,P4 are_collinear) &
not (P1,P3,P4 are_collinear) & not (P2,P3,P4 are_collinear) and
A2: not (Q1,Q2,Q3 are_collinear) & not (Q1,Q2,Q4 are_collinear) &
not (Q1,Q3,Q4 are_collinear) & not (Q2,Q3,Q4 are_collinear);
consider N1 being invertible Matrix of 3,F_Real such that
A3: (homography(N1)).P1 = Dir100 & (homography(N1)).P2 = Dir010 &
(homography(N1)).P3 = Dir001 & (homography(N1)).P4 = Dir111 by A1,Th26;
consider N2 being invertible Matrix of 3,F_Real such that
A4: (homography(N2)).Q1 = Dir100 & (homography(N2)).Q2 = Dir010 &
(homography(N2)).Q3 = Dir001 & (homography(N2)).Q4 = Dir111 by A2,Th26;
reconsider N = (N2~) * N1 as invertible Matrix of 3,F_Real;
take N;
thus Q1 = (homography(N2~)).((homography(N1)).P1) by A3,A4,Th16
.= (homography(N)).P1 by Th14;
thus Q2 = (homography(N2~)).((homography(N1)).P2) by A3,A4,Th16
.= (homography(N)).P2 by Th14;
thus Q3 = (homography(N2~)).((homography(N1)).P3) by A3,A4,Th16
.= (homography(N)).P3 by Th14;
thus Q4 = (homography(N2~)).((homography(N1)).P4) by A3,A4,Th16
.= (homography(N)).P4 by Th14;
end;