:: Homography in $\mathbbRP^2$
:: by Roland Coghetto
::
:: Received October 18, 2016
:: Copyright (c) 2016-2018 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 SETWISEO, MSSUBFAM, REAL_1, XCMPLX_0, ANPROJ_1, ZFMISC_1,
PENCIL_1, MCART_1, EUCLID_5, ALGSTR_0, ARYTM_1, ARYTM_3, CARD_1, CARD_3,
CLASSES1, EUCLID, FINSEQ_1, FUNCT_1, FVSUM_1, INCSP_1, LMOD_7, MATRIX_1,
MATRIX_3, MATRIX13, MATRLIN2, NAT_1, NUMBERS, PRE_TOPC, QC_LANG1,
RANKNULL, RELAT_1, RLSUB_1, RLVECT_1, RLVECT_3, RVSUM_1, STRUCT_0,
SUBSET_1, SUPINF_2, TARSKI, TREES_1, VECTSP_1, VECTSP10, XBOOLE_0,
XXREAL_0, DUALSP01, BINOP_1, ANPROJ_2, EUCLID_8, COMPLEX1, SQUARE_1,
MATRIX_0, MATRIX_6, MESFUNC1, MATRIXR1, MATRIXR2, FINSEQ_2, ANPROJ_8,
FUNCSDOM;
notations XBOOLE_0, RELSET_1, ENUMSET1, ZFMISC_1, SQUARE_1, SUBSET_1,
ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, FUNCT_1, BINOP_1, FINSEQ_1,
FINSEQ_4, FINSEQOP, PRE_TOPC, RVSUM_1, EUCLID, DOMAIN_1, ANPROJ_1,
TARSKI, CARD_1, XXREAL_0, FUNCT_2, RLVECT_3, VECTSP_1, MATRIX_0,
MATRIX_1, MATRIX_3, VECTSP_4, VECTSP_7, MATRIX13, FVSUM_1, RANKNULL,
GROUP_1, MATRTOP1, DUALSP01, STRUCT_0, ALGSTR_0, RLVECT_1, SETWOP_2,
ANPROJ_2, COLLSP, EUCLID_8, EUCLID_5, FINSEQ_2, LAPLACE, MATRIXR1,
MATRIXR2, MATRIX_6;
constructors RELSET_1, SQUARE_1, BINOP_2, FINSEQ_4, MONOID_0, EUCLID_5,
ANPROJ_1, FVSUM_1, MATRIX13, MATRTOP1, RANKNULL, REALSET1, RLVECT_3,
VECTSP10, NORMSP_3, FINSOP_1, ANPROJ_2, EUCLID_8, MATRIX_6, LAPLACE,
MATRIXR2;
registrations XBOOLE_0, ANPROJ_1, FUNCT_1, MATRTOP1, PRVECT_1, STRUCT_0,
VECTSP_1, REVROT_1, MATRIX_0, RELSET_1, NUMBERS, XREAL_0, MEMBERED,
MONOID_0, EUCLID, VALUED_0, FINSEQ_2, RVSUM_1, FINSEQ_1, ANPROJ_2,
MATRIX_6;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
begin :: Preliminaries
reserve a,b,c,d,e,f for Real,
k,m for Nat,
D for non empty set,
V for non trivial RealLinearSpace,
u,v,w for Element of V,
p,q,r for Element of ProjectiveSpace(V);
theorem :: ANPROJ_8:1
[1,1] in [:Seg 3,Seg 3:] & [1,2] in [:Seg 3,Seg 3:] &
[1,3] in [:Seg 3,Seg 3:] & [2,1] in [:Seg 3,Seg 3:] &
[2,2] in [:Seg 3,Seg 3:] & [2,3] in [:Seg 3,Seg 3:] &
[3,1] in [:Seg 3,Seg 3:] & [3,2] in [:Seg 3,Seg 3:] &
[3,3] in [:Seg 3,Seg 3:];
theorem :: ANPROJ_8:2
[1,1] in [:Seg 3,Seg 1:] & [2,1] in [:Seg 3,Seg 1:] &
[3,1] in [:Seg 3,Seg 1:];
theorem :: ANPROJ_8:3
[1,1] in [:Seg 1,Seg 3:] & [1,2] in [:Seg 1,Seg 3:] &
[1,3] in [:Seg 1,Seg 3:];
theorem :: ANPROJ_8:4
<* <* a *>, <* b *>, <* c *> *> is Matrix of 3,1,F_Real;
theorem :: ANPROJ_8:5
for N being Matrix of 3,1,F_Real st N = <* <* a *>, <* b *>, <* c *> *>
holds Col(N,1) = <* a,b,c *>;
theorem :: ANPROJ_8:6
for K being non empty multMagma
for a1,a2,a3,b1,b2,b3 being Element of K holds
mlt(<*a1,a2,a3*>,<*b1,b2,b3*>) = <*a1*b1,a2*b2,a3*b3*>;
theorem :: ANPROJ_8:7
for K being commutative associative left_unital Abelian
add-associative right_zeroed right_complementable non empty doubleLoopStr for
a1,a2,a3,b1,b2,b3 being Element of K holds
<*a1,a2,a3*> "*" <*b1,b2,b3*> = a1*b1 + a2*b2 + a3*b3;
theorem :: ANPROJ_8:8
for M being Matrix of 3,F_Real
for N being Matrix of 3,1,F_Real st N = <* <* 0 *>, <* 0 *>, <* 0 *> *> holds
M * N = <* <* 0 *>, <* 0 *>, <* 0 *> *>;
theorem :: ANPROJ_8:9
u,v,w are_LinDep iff
(u = v or u = w or v = w or {u,v,w} is linearly-dependent);
theorem :: ANPROJ_8:10
p,q,r are_collinear iff ex u,v,w st p = Dir(u) & q = Dir(v) & r = Dir(w) &
u is not zero & v is not zero & w is not zero & (u = v or u = w or v = w or
{u,v,w} is linearly-dependent);
theorem :: ANPROJ_8:11
p,q,r are_collinear iff ex u,v,w st p = Dir(u) & q = Dir(v) & r = Dir(w) &
u is not zero & v is not zero & w is not zero & ex a,b,c st
a*u + b*v + c*w = 0.V & (a<>0 or b<>0 or c <>0);
theorem :: ANPROJ_8:12
for u,v,w being Element of V st a <> 0 &
a * u + b * v + c * w = 0.V holds u = ((-b)/a) * v + ((-c)/a) * w;
theorem :: ANPROJ_8:13
a <> 0 & a * b + c * d + e * f = 0 implies b = - (c/a) * d - (e/a) * f;
theorem :: ANPROJ_8:14
for u,v,w being Point of TOP-REAL 3 st
ex a,b,c st a*u + b*v + c*w = 0.(TOP-REAL 3) & a<>0 holds |{u,v,w}| = 0;
theorem :: ANPROJ_8:15
for n being Nat holds dom 1_Rmatrix(n) = Seg n;
theorem :: ANPROJ_8:16
for A being Matrix of F_Real holds MXR2MXF MXF2MXR A = A;
theorem :: ANPROJ_8:17
for A,B being Matrix of F_Real for RA,RB being Matrix of REAL st
A = RA & B = RB holds A * B = RA * RB;
theorem :: ANPROJ_8:18
for n being Nat for M being Matrix of n,REAL
for N being Matrix of n,F_Real st M = N holds
M is invertible iff N is invertible;
reserve o,p,q,r,s,t for Point of TOP-REAL 3,
M for Matrix of 3,F_Real;
theorem :: ANPROJ_8:19
for p1,p2,p3,q1,q2,q3,r1,r2,r3 being Real holds
<*<*p1,p2,p3*>,<*q1,q2,q3*>,<*r1,r2,r3*>*> is Matrix of 3,F_Real;
theorem :: ANPROJ_8:20
for p1,p2,p3,q1,q2,q3,r1,r2,r3 being Real holds
M = <*<*p1,q1,r1*>,<*p2,q2,r2*>,<*p3,q3,r3*>*> implies
M*(1,1) = p1 & M*(1,2) = q1 & M*(1,3) = r1 &
M*(2,1) = p2 & M*(2,2) = q2 & M*(2,3) = r2 &
M*(3,1) = p3 & M*(3,2) = q3 & M*(3,3) = r3;
theorem :: ANPROJ_8:21
M = <*p,q,r*> implies
M*(1,1) = p`1 & M*(1,2) = p`2 & M*(1,3) = p`3 &
M*(2,1) = q`1 & M*(2,2) = q`2 & M*(2,3) = q`3 &
M*(3,1) = r`1 & M*(3,2) = r`2 & M*(3,3) = r`3;
theorem :: ANPROJ_8:22
for p1,p2,p3,q1,q2,q3,r1,r2,r3 being Real holds
M = <*<*p1,q1,r1*>,<*p2,q2,r2*>,<*p3,q3,r3*>*> implies
M@ = <*<*p1,p2,p3*>,<*q1,q2,q3*>,<*r1,r2,r3*>*>;
theorem :: ANPROJ_8:23
M = <* p,q,r *> implies
M@ = <*<*p`1,q`1,r`1*>,<*p`2,q`2,r`2*>,<*p`3,q`3,r`3*>*>;
theorem :: ANPROJ_8:24
lines M = {Line(M,1),Line(M,2),Line(M,3)};
theorem :: ANPROJ_8:25
M = <*<*p`1,p`2,p`3*>,<*q`1,q`2,q`3*>,<*r`1,r`2,r`3*>*> implies
Line(M,1) = p & Line(M,2) = q & Line(M,3) = r;
theorem :: ANPROJ_8:26
for x be object holds x in lines M@ iff
ex i be Nat st i in Seg 3 & x = Col(M,i);
begin :: Grassman-Pl\{?}ucker relation
theorem :: ANPROJ_8:27
|{ p,q,r }| = p`1 * q`2 * r`3 - p`3*q`2*r`1 - p`1*q`3*r`2 + p`2*q`3*r`1 -
p`2*q`1*r`3 + p`3*q`1*r`2;
::$N Grassmann-Pl\{?}ucker-Relation in rank 3
theorem :: ANPROJ_8:28
|{p,q,r}| * |{p,s,t}| - |{p,q,s}| * |{p,r,t}| + |{p,q,t}| * |{p,r,s}| = 0;
theorem :: ANPROJ_8:29
|{ p,q,r }| = - |{ p,r,q }|;
theorem :: ANPROJ_8:30
|{ p,q,r }| = - |{ q,p,r }|;
theorem :: ANPROJ_8:31
|{ a * p, q, r }| = a * |{ p, q, r }|;
theorem :: ANPROJ_8:32
|{ p, a * q, r }| = a * |{ p, q, r }|;
theorem :: ANPROJ_8:33
|{ p, q, a * r }| = a * |{ p, q, r }|;
theorem :: ANPROJ_8:34
M = <*<*p`1,q`1,r`1*>,<*p`2,q`2,r`2*>,<*p`3,q`3,r`3*>*> implies
|{ p,q,r }| = Det M;
theorem :: ANPROJ_8:35
M = <*<*p`1,p`2,p`3*>,<*q`1,q`2,q`3*>,<*r`1,r`2,r`3*>*> implies
|{ p,q,r }| = Det M;
theorem :: ANPROJ_8:36
for M being Matrix of k,F_Real holds
Det M = 0.F_Real iff the_rank_of M < k;
theorem :: ANPROJ_8:37
for M being Matrix of k,F_Real holds
the_rank_of M < k iff
lines M is linearly-dependent or not M is without_repeated_line;
theorem :: ANPROJ_8:38
for M being Matrix of k,m,F_Real holds
Mx2Tran M is Function of RLSp2RVSp(TOP-REAL k),RLSp2RVSp(TOP-REAL m);
theorem :: ANPROJ_8:39
for M being Matrix of k,F_Real holds
Mx2Tran M is linear-transformation of
RLSp2RVSp(TOP-REAL k),RLSp2RVSp(TOP-REAL k);
theorem :: ANPROJ_8:40
M = <*<*p`1,p`2,p`3*>,<*q`1,q`2,q`3*>,<*r`1,r`2,r`3*>*> &
the_rank_of M < 3 implies ex a,b,c st a*p + b*q + c*r = 0.(TOP-REAL 3) &
(a<>0 or b<>0 or c <>0);
theorem :: ANPROJ_8:41
(a*p + b*q + c*r = 0.(TOP-REAL 3) & (a <> 0 or b <> 0 or c <> 0))
implies |{p,q,r}| = 0;
theorem :: ANPROJ_8:42
|{p,q,r}| = 0 implies ex a,b,c st a*p + b*q + c*r = 0.(TOP-REAL 3) &
(a<>0 or b<>0 or c <>0);
theorem :: ANPROJ_8:43
p,q,r are_LinDep iff |{p,q,r}| = 0;
begin :: Some properties about the cross product
theorem :: ANPROJ_8:44
|(p,p q)| = 0;
theorem :: ANPROJ_8:45
|(p,q p)| = 0;
theorem :: ANPROJ_8:46
|{ o, p, (o p) (q r) }| = 0 &
|{ q, r, (o p) (q r) }| = 0;
theorem :: ANPROJ_8:47
o,p, (o p) (q r) are_LinDep &
q,r, (o p) (q r) are_LinDep;
theorem :: ANPROJ_8:48
0.TOP-REAL 3 p = 0.TOP-REAL 3 & p 0.TOP-REAL 3 = 0.TOP-REAL 3;
theorem :: ANPROJ_8:49
|{p,q,0.TOP-REAL 3}| = 0;
theorem :: ANPROJ_8:50
p q = 0.TOP-REAL 3 & r = |[1,1,1]| implies p,q,r are_LinDep;
theorem :: ANPROJ_8:51
p is not zero & q is not zero &
p q = 0.TOP-REAL 3 implies are_Prop p,q;
theorem :: ANPROJ_8:52
for p,q,r,s be non zero Point of TOP-REAL 3 st
(p q) (r s) is zero holds
are_Prop p,q or are_Prop r,s or are_Prop p q,r s;
theorem :: ANPROJ_8:53
|{ p, q, p q }| = |(q,q)| * |(p,p)| - |(q,p)| * |(p,q)|;
theorem :: ANPROJ_8:54
|(p q, p q)| = |(q,q)| * |(p,p)| - |(q,p)| * |(p,q)|;
theorem :: ANPROJ_8:55
p is non zero & |(p,q)| = 0 & |(p,r)| = 0 & |(p,s)| = 0 implies |{q,r,s}| = 0
;
theorem :: ANPROJ_8:56
|{ p, q, p q }| = |. p q .|^2;
theorem :: ANPROJ_8:57
ProjectiveSpace TOP-REAL 3 is CollProjectivePlane;
begin :: Real projective plane and homography
theorem :: ANPROJ_8:58
for u,v,w,x being Element of TOP-REAL 3 st
u is not zero & x is not zero &
Dir u = Dir x holds |{u,v,w}| = 0 iff |{x,v,w}| = 0;
theorem :: ANPROJ_8:59
for u,v,w,x being Element of TOP-REAL 3 st
v is not zero & x is not zero & Dir v = Dir x holds
|{u,v,w}| = 0 iff |{u,x,w}| = 0;
theorem :: ANPROJ_8:60
for u,v,w,x being Element of TOP-REAL 3 st
w is not zero & x is not zero & Dir w = Dir x holds
|{u,v,w}| = 0 iff |{u,v,x}| = 0;
theorem :: ANPROJ_8:61
(1_Rmatrix(3)).1 = & (1_Rmatrix(3)).2 = &
(1_Rmatrix(3)).3 = ;
theorem :: ANPROJ_8:62
Base_FinSeq(3,1) = & Base_FinSeq(3,2) = &
Base_FinSeq(3,3) = ;
theorem :: ANPROJ_8:63
for pr being FinSequence of D st len pr = 3 holds
Col(<*pr*>,1) = <* pr.1 *> &
Col(<*pr*>,2) = <* pr.2 *> & Col(<*pr*>,3) = <* pr.3 *>;
theorem :: ANPROJ_8:64
Col(<**>,1) = <* 1 *> &
Col(<**>,2) = <* 0 *> &
Col(<**>,3) = <* 0 *>;
theorem :: ANPROJ_8:65
Col(<**>,1) = <* 0 *> &
Col(<**>,2) = <* 1 *> &
Col(<**>,3) = <* 0 *>;
theorem :: ANPROJ_8:66
Col(<**>,1) = <* 0 *> &
Col(<**>,2) = <* 0 *> &
Col(<**>,3) = <* 1 *>;
theorem :: ANPROJ_8:67
Col(1.(F_Real,3),1) = <* 1,0,0 *> &
Col(1.(F_Real,3),2) = <* 0,1,0 *> &
Col(1.(F_Real,3),3) = <* 0,0,1 *>;
theorem :: ANPROJ_8:68
Line(1.(F_Real,3),1) = <* 1,0,0 *> &
Line(1.(F_Real,3),2) = <* 0,1,0 *> &
Line(1.(F_Real,3),3) = <* 0,0,1 *>;
theorem :: ANPROJ_8:69
<**>@ = <* <* 1 *>, <* 0 *> , <* 0 *> *> &
<**>@ = <* <* 0 *>, <* 1 *> , <* 0 *> *> &
<**>@ = <* <* 0 *>, <* 0 *> , <* 1 *> *>;
reserve pf for FinSequence of D;
theorem :: ANPROJ_8:70
for pf being FinSequence of D holds
k in dom pf implies <*pf*>*(1,k) = pf.k;
theorem :: ANPROJ_8:71
k in dom pf implies Col(<*pf*>,k) = <*pf.k*>;
theorem :: ANPROJ_8:72
for pr being Element of REAL 3 st
pf = pr holds MXR2MXF ColVec2Mx pr = <*pf*>@;
reserve PQR for Matrix of 3,F_Real;
theorem :: ANPROJ_8:73
PQR = <*<*p`1,p`2,p`3*>,<*q`1,q`2,q`3*>,<*r`1,r`2,r`3*>*> implies
Line(PQR,1) = p & Line(PQR,2) = q & Line(PQR,3) = r;
theorem :: ANPROJ_8:74
PQR = <*<*p`1,p`2,p`3*>,<*q`1,q`2,q`3*>,<*r`1,r`2,r`3*>*> implies
Col(PQR,1) = <*p`1,q`1,r`1*> & Col(PQR,2) = <*p`2,q`2,r`2*> &
Col(PQR,3) = <*p`3,q`3,r`3*>;
theorem :: ANPROJ_8:75
width <*pf*> = len pf;
theorem :: ANPROJ_8:76
len pf = 3 implies Line(<*pf*>@,1) = <* pf.1 *> &
Line(<*pf*>@,2) = <* pf.2 *> & Line(<*pf*>@,3) = <* pf.3 *>;
theorem :: ANPROJ_8:77
len pf = 3 implies <*pf*>@ = <* <* pf.1 *>, <* pf.2 *>, <* pf.3 *> *>;
definition
let D;
let p be FinSequence of D;
assume
len p = 3;
func F2M p -> FinSequence of 1-tuples_on D equals
:: ANPROJ_8:def 1
<* <*p.1*>, <*p.2*> , <*p.3*> *>;
end;
theorem :: ANPROJ_8:78
for p being FinSequence of REAL st len p = 3 holds len F2M p = 3;
theorem :: ANPROJ_8:79
for p being FinSequence of REAL st len p = 3 holds
p is 3-element FinSequence of REAL;
theorem :: ANPROJ_8:80
for p being FinSequence of REAL st p = |[0,0,0]| holds
F2M p = <* <* 0 *>, <* 0 *>, <* 0 *> *>;
theorem :: ANPROJ_8:81
len pf = 3 implies
<* Col(<*pf*>,1), Col(<*pf*>,2), Col(<*pf*>,3) *> = F2M pf;
definition
let D;
let p be FinSequence of 1-tuples_on D;
assume
len p = 3;
func M2F p -> FinSequence of D equals
:: ANPROJ_8:def 2
<* (p.1).1, (p.2).1, (p.3).1 *>;
end;
theorem :: ANPROJ_8:82
for p being FinSequence of 1-tuples_on REAL st len p = 3 holds
M2F p is Point of TOP-REAL 3;
definition
let p be FinSequence of 1-tuples_on REAL;
let a be Real;
assume
len p = 3;
func a * p -> FinSequence of 1-tuples_on REAL means
:: ANPROJ_8:def 3
ex p1,p2,p3 be Real st p1 = (p.1).1 & p2 = (p.2).1 & p3 = (p.3).1 &
it = <* <* a * p1 *>, <* a * p2 *> , <* a * p3 *> *>;
end;
theorem :: ANPROJ_8:83
for p being FinSequence of 1-tuples_on REAL st
len p = 3 holds M2F (a * p) = a * (M2F p);
theorem :: ANPROJ_8:84
for p being FinSequence of 1-tuples_on REAL st len p = 3 holds
<* <*(p.1).1*>, <*(p.2).1*> , <*(p.3).1*> *> = p;
theorem :: ANPROJ_8:85
for p being FinSequence of 1-tuples_on REAL st len p = 3 holds
F2M M2F p = p;
theorem :: ANPROJ_8:86
for p being FinSequence of REAL st len p = 3 holds M2F F2M p = p;
theorem :: ANPROJ_8:87
<**>@ = F2M & <**>@ = F2M & <**>@ = F2M ;
theorem :: ANPROJ_8:88
for p being FinSequence of D st len p = 3 holds
<*p*>@ = F2M p;
theorem :: ANPROJ_8:89
Line(<*pf*>,1) = pf;
theorem :: ANPROJ_8:90
for M being Matrix of 3,1,D holds Line(M,1) = <* M*(1,1) *> &
Line(M,2) = <* M*(2,1) *> & Line(M,3) = <* M*(3,1) *>;
reserve R for Ring;
theorem :: ANPROJ_8:91
for N being Matrix of 3,R
for p being FinSequence of R st len p = 3 holds
N * (<*p*>@) is (3,1)-size;
theorem :: ANPROJ_8:92
for pf being FinSequence of R
for N being Matrix of 3,R st
len pf = 3 holds
Line(N * (<*pf*>@),1) = <* (N * (<*pf*>@))*(1,1) *> &
Line(N * (<*pf*>@),2) = <* (N * (<*pf*>@))*(2,1) *> &
Line(N * (<*pf*>@),3) = <* (N * (<*pf*>@))*(3,1) *>;
theorem :: ANPROJ_8:93
Col(<*pf*>@,1) = pf;
theorem :: ANPROJ_8:94
for pf,qf,rf being FinSequence of F_Real st p = pf & q = qf & r = rf &
|{p,q,r}| <> 0 holds ex M being Matrix of 3,F_Real st M is invertible &
M * pf = F2M & M * qf = F2M & M * rf = F2M ;
theorem :: ANPROJ_8:95
for pf,qf,rf being FinSequence of F_Real
for pt,qt,rt being FinSequence of 1-tuples_on REAL
st PQR = <*<*p`1,q`1,r`1*>,<*p`2,q`2,r`2*>,<*p`3,q`3,r`3*>*> &
p = pf & q = qf & r = rf &
pt = M * pf & qt = M * qf & rt = M * rf
holds (M * PQR)@ = <* M2F pt,M2F qt, M2F rt *>;
theorem :: ANPROJ_8:96
for pt,qt,rt being FinSequence of 1-tuples_on REAL
st M = <* M2F pt,M2F qt,M2F rt*> & Det M = 0 & M2F pt = p &
M2F qt = q & M2F rt = r holds |{ p,q,r }| = 0;
theorem :: ANPROJ_8:97
for pm,qm,rm being Point of TOP-REAL 3
for pt,qt,rt being FinSequence of 1-tuples_on REAL
for pf,qf,rf being FinSequence of F_Real st
M is invertible &
p = pf & q = qf & r = rf &
pt = M * pf & qt = M * qf & rt = M * rf &
M2F pt = pm & M2F qt = qm & M2F rt = rm holds
|{ p,q,r }| = 0 iff |{ pm,qm,rm }| = 0;
theorem :: ANPROJ_8:98
0 < m implies
for M being Matrix of m,1,F_Real holds M is FinSequence of 1-tuples_on REAL;
theorem :: ANPROJ_8:99
for uf being FinSequence of F_Real st len uf = 3 holds
<*uf*>@ = 1.(F_Real,3) * (<*uf*>@);
theorem :: ANPROJ_8:100
for u being Element of TOP-REAL 3
for uf being FinSequence of F_Real
st u = uf & <*uf*>@ = <* <* 0 *>, <* 0 *>, <* 0 *> *>
holds u = 0.TOP-REAL 3;
theorem :: ANPROJ_8:101
for N being invertible Matrix of 3,F_Real
for u,mu being Element of TOP-REAL 3
for uf being FinSequence of F_Real
for ut being FinSequence of 1-tuples_on REAL st
u is non zero & u = uf & ut = N * uf & mu = M2F ut holds
mu is non zero;
definition
let N be invertible Matrix of 3,F_Real;
func homography(N) -> Function of ProjectiveSpace TOP-REAL 3,
ProjectiveSpace TOP-REAL 3 means
:: ANPROJ_8:def 4
for x being Point of ProjectiveSpace TOP-REAL 3 holds
ex u,v being Element of TOP-REAL 3,
uf being FinSequence of F_Real,
p being FinSequence of 1-tuples_on REAL
st x = Dir u & u is not zero & u = uf & p = N * uf & v = M2F p &
v is not zero & it.x = Dir v;
end;
theorem :: ANPROJ_8:102
for N being invertible Matrix of 3,F_Real
for p,q,r being Point of ProjectiveSpace TOP-REAL 3 holds
p,q,r are_collinear iff
homography(N).p, homography(N).q, homography(N).r are_collinear;