:: Homography in $\mathbbRP^2$
:: by Roland Coghetto
::
:: Received October 18, 2016
:: Copyright (c) 2016-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 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, GROUP_1;
notations GCD_1, 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 VECTSP_2, GCD_1, 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, FINSEQOP,
MATRIX_3;
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, RING_2, VECTSP_2;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
definitions TARSKI;
equalities VECTSP_1, ALGSTR_0;
expansions TARSKI, XBOOLE_0, VECTSP_1, STRUCT_0;
theorems MOD_2, VECTSP_4, MATRIX_9, EUCLID_4, EUCLID_5, ANPROJ_1, ANPROJ_2,
MATRTOP2, RLVECT_4, STRUCT_0, XREAL_0, RLVECT_1, EUCLID, MATRIXR2,
FINSEQ_2, XCMPLX_1, RVSUM_1, XXREAL_0, MATRIX_0, MATRIX13, MATRTOP1,
MATRIX_7, RANKNULL, DUALSP01, FINSEQ_1, FINSEQ_3, ENUMSET1, MATRLIN2,
FVSUM_1, FINSOP_1, COLLSP, EUCLID_8, EUCLID_2, LAPLACE, MATRIX_6,
MATRIXR1, MATRIX_3, ZFMISC_1, FUNCT_1, FINSEQ_5, TARSKI, MATRIX_1,
VECTSP_1, FUNCT_2, EUCLID_9, CARD_1;
schemes FUNCT_2;
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 Th1:
[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:]
proof
1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1;
hence thesis by ZFMISC_1:87;
end;
theorem Th2:
[1,1] in [:Seg 3,Seg 1:] & [2,1] in [:Seg 3,Seg 1:] &
[3,1] in [:Seg 3,Seg 1:]
proof
1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 & 1 in Seg 1 by FINSEQ_1:1;
hence thesis by ZFMISC_1:87;
end;
theorem Th3:
[1,1] in [:Seg 1,Seg 3:] & [1,2] in [:Seg 1,Seg 3:] &
[1,3] in [:Seg 1,Seg 3:]
proof
1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 & 1 in Seg 1 by FINSEQ_1:1;
hence thesis by ZFMISC_1:87;
end;
theorem
<* <* a *>, <* b *>, <* c *> *> is Matrix of 3,1,F_Real
proof
rng <* a *> c= REAL;
then reconsider p = <* a *> as FinSequence of REAL by FINSEQ_1:def 4;
rng <* b *> c= REAL;
then reconsider q = <* b *> as FinSequence of REAL by FINSEQ_1:def 4;
rng <* c *> c= REAL;
then reconsider r = <* c *> as FinSequence of REAL by FINSEQ_1:def 4;
len p = 1 & len q = 1 & len r = 1 by FINSEQ_1:40;
hence thesis by MATRIXR2:34;
end;
theorem Th4:
for N being Matrix of 3,1,F_Real st N = <* <* a *>, <* b *>, <* c *> *>
holds Col(N,1) = <* a,b,c *>
proof
let N be Matrix of 3,1,F_Real;
assume
A1: N = <* <* a *>, <* b *>, <* c *> *>; then
A2: len N = 3 & N.1 = <* a *> & N.2 = <* b *> & N.3 = <* c *>
by FINSEQ_1:45; then
A3: dom N = Seg 3 by FINSEQ_1:def 3;
A4: len Col(N,1) = len N by MATRIX_0:def 8
.= 3 by A1,FINSEQ_1:45;
[1,1] in Indices N by MATRIX_0:23,Th2;
then consider p1 be FinSequence of F_Real such that
A5: p1 = N.1 and
A6: N*(1,1) = p1.1 by MATRIX_0:def 5;
[2,1] in Indices N by MATRIX_0:23,Th2;
then consider p2 be FinSequence of F_Real such that
A8: p2 = N.2 and
A9: N*(2,1) = p2.1 by MATRIX_0:def 5;
A10: N*(2,1) = b by A2,A8,A9;
[3,1] in Indices N by MATRIX_0:23,Th2;
then consider p3 be FinSequence of F_Real such that
A11: p3 = N.3 and
A12: N*(3,1) = p3.1 by MATRIX_0:def 5;
A13: N*(3,1) = c by A2,A11,A12;
Col(N,1).1 = N*(1,1) &
Col(N,1).2 = N*(2,1) &
Col(N,1).3 = N*(3,1) by A3,FINSEQ_1:1,MATRIX_0:def 8;
hence thesis by A10,A13,A4,A2,A5,A6,FINSEQ_1:45;
end;
theorem Th5:
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*>
proof
let K be non empty multMagma;
let a1,a2,a3,b1,b2,b3 be Element of K;
thus mlt(<*a1,a2,a3*>,<*b1,b2,b3*>)
= (the multF of K).:(<*a1,a2,a3*>,<*b1,b2,b3*>) by FVSUM_1:def 7
.= <*a1*b1,a2*b2,a3*b3*> by FINSEQ_2:76;
end;
theorem Th6:
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
proof
let K be commutative associative left_unital Abelian add-associative
right_zeroed right_complementable non empty doubleLoopStr;
let a1,a2,a3,b1,b2,b3 be Element of K;
set p = <*a1,a2,a3*>, q = <*b1,b2,b3*>;
Sum(mlt(p,q)) = (the addF of K) $$ mlt(p,q) by FVSUM_1:def 8
.= (the addF of K) $$ <*a1*b1,a2*b2,a3*b3*> by Th5
.= a1*b1 + a2*b2 + a3*b3 by FINSOP_1:14;
hence thesis by FVSUM_1:def 9;
end;
theorem Th7:
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 *> *>
proof
let M be Matrix of 3,F_Real;
let N be Matrix of 3,1,F_Real;
assume
A1: N = <* <* 0 *>, <* 0 *>, <* 0 *> *>;
A2: len M = 3 & width M = 3 by MATRIX_0:23;
A3: len N = 3 & width N = 1 by MATRIX_0:23;
width M = len N by A3,MATRIX_0:23; then
A4A: len(M * N) = len M & width(M * N) = width N by MATRIX_3:def 4; then
A4: len(M * N) = 3 & width(M * N) = 1 by MATRIX_0:23; then
A5: M * N is Matrix of 3,1,F_Real by MATRIX_0:20;
now
thus len Line(M,1) = width M by MATRIX_0:def 7
.= 3 by MATRIX_0:23;
1 in Seg width M & 2 in Seg width M &
3 in Seg width M by A2,FINSEQ_1:1;
hence Line(M,1).1 = M*(1,1) &
Line(M,1).2 = M*(1,2) & Line(M,1).3 = M*(1,3) by MATRIX_0:def 7;
end;
then
A6: Line(M,1) = <* M*(1,1),M*(1,2),M*(1,3) *> by FINSEQ_1:45;
reconsider ze = 0 as Element of F_Real;
<* M*(1,1),M*(1,2),M*(1,3) *> "*" <* ze,ze,ze *> =
M*(1,1) * ze + M*(1,2) * ze + M*(1,3) * ze by Th6; then
A7: Line(M,1) "*" Col(N,1) = 0 by A1,Th4,A6;
now
A8: 1 in Seg 3 by FINSEQ_1:1;
len Line(M * N,1) = width (M * N) by MATRIX_0:def 7
.= 1 by A4A,MATRIX_0:23; then
A9: Line(M * N,1) = <* (Line(M * N,1)).1 *> by FINSEQ_1:40;
2 in Seg 3 by FINSEQ_1:1; then
A10: (M * N).2 = Line(M * N,2) by A5,MATRIX_0:52;
A11: len Line(M * N,2) = width (M * N) by MATRIX_0:def 7
.= 1 by A4A,MATRIX_0:23;
3 in Seg 3 by FINSEQ_1:1; then
A12: (M * N).3 = Line(M * N,3) by A5,MATRIX_0:52;
A13: len Line(M * N,3) = width (M * N) by MATRIX_0:def 7
.= 1 by A4A,MATRIX_0:23;
(Line(M * N,1)).1 = 0
proof
A14: [1,1] in Indices(M * N) by A5,MATRIX_0:23,Th2;
1 in Seg width (M * N) by A4,FINSEQ_1:1; then
(Line(M * N,1)).1 = (M * N)*(1,1) by MATRIX_0:def 7
.= 0 by A7,A14,A2,A3,MATRIX_3:def 4;
hence thesis;
end;
hence (M * N).1 = <* 0 *> by A9,A8,A5,MATRIX_0:52;
now
thus len Line(M,2) = width M by MATRIX_0:def 7
.= 3 by MATRIX_0:23;
1 in Seg width M & 2 in Seg width M &
3 in Seg width M by A2,FINSEQ_1:1;
hence Line(M,2).1 = M*(2,1) & Line(M,2).2 = M*(2,2) &
Line(M,2).3 = M*(2,3) by MATRIX_0:def 7;
end;
then
A15: Line(M,2) = <* M*(2,1),M*(2,2),M*(2,3) *> by FINSEQ_1:45;
reconsider ze = 0 as Element of F_Real;
<* M*(2,1),M*(2,2),M*(2,3) *> "*" <* ze,ze,ze *>
= M*(2,1) * ze + M*(2,2) * ze + M*(2,3) * ze by Th6; then
A16: Line(M,2) "*" Col(N,1) = 0 by A1,Th4,A15;
(Line(M * N,2)).1 = 0
proof
A17: [2,1] in Indices(M * N) by A5,MATRIX_0:23,Th2;
1 in Seg width (M * N) by A4,FINSEQ_1:1;
then (Line(M * N,2)).1 = (M * N)*(2,1) by MATRIX_0:def 7
.= 0 by A16,A17,A2,A3,MATRIX_3:def 4;
hence thesis;
end;
hence (M * N).2 = <* 0 *> by FINSEQ_1:40,A10,A11;
now
thus len Line(M,3) = width M by MATRIX_0:def 7
.= 3 by MATRIX_0:23;
1 in Seg width M & 2 in Seg width M &
3 in Seg width M by A2,FINSEQ_1:1;
hence Line(M,3).1 = M*(3,1) & Line(M,3).2 = M*(3,2) &
Line(M,3).3 = M*(3,3) by MATRIX_0:def 7;
end;
then
A18: Line(M,3) = <* M*(3,1),M*(3,2),M*(3,3) *> by FINSEQ_1:45;
reconsider ze = 0 as Element of F_Real;
<* M*(3,1),M*(3,2),M*(3,3) *> "*" <* ze,ze,ze *> =
M*(3,1) * ze + M*(3,2) * ze + M*(3,3) * ze by Th6; then
A19: Line(M,3) "*" Col(N,1) = 0 by A1,Th4,A18;
(Line(M * N,3)).1 = 0
proof
A20: [3,1] in Indices(M * N) by A5,MATRIX_0:23,Th2;
1 in Seg width (M * N) by A4,FINSEQ_1:1; then
(Line(M * N,3)).1 = (M * N)*(3,1) by MATRIX_0:def 7
.= 0 by A20,A2,A3,MATRIX_3:def 4,A19;
hence thesis;
end;
hence (M * N).3 = <* 0 *> by A13,FINSEQ_1:40,A12;
end;
hence thesis by A4A,MATRIX_0:23,FINSEQ_1:45;
end;
theorem Th8:
u,v,w are_LinDep iff
(u = v or u = w or v = w or {u,v,w} is linearly-dependent)
proof
hereby
assume u,v,w are_LinDep;
then ex a,b,c st a*u + b*v + c*w = 0.V & (a<>0 or b<>0 or c <>0)
by ANPROJ_1:def 2;
hence u = v or u = w or v = w or {u,v,w} is linearly-dependent
by RLVECT_4:7;
end;
assume u = v or u = w or v = w or {u,v,w} is linearly-dependent;
then ex a,b,c st a * u + b * v + c * w = 0.V &
(a <> 0 or b <> 0 or c <> 0) by RLVECT_4:7;
hence u,v,w are_LinDep by ANPROJ_1:def 2;
end;
theorem Th9:
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)
proof
hereby
assume p,q,r are_collinear;
then consider u,v,w such that
A1: p = Dir(u) & q = Dir(v) & r =
Dir(w) & u is not zero & v is not zero & w is not zero &
u,v,w are_LinDep by ANPROJ_2:23;
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) by A1,Th8;
hence 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);
end;
given u,v,w such that
A2: 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);
p = Dir(u) & q = Dir(v) & r = Dir(w) & u is not zero & v is not zero &
w is not zero & u,v,w are_LinDep by Th8,A2;
hence p,q,r are_collinear by ANPROJ_2:23;
end;
theorem
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)
proof
hereby
assume p,q,r are_collinear;
then consider u,v,w such that
A1: p = Dir(u) & q = Dir(v) & r =
Dir(w) & u is not zero & v is not zero & w is not zero &
u,v,w are_LinDep by ANPROJ_2:23;
take u,v,w;
thus 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) by A1,ANPROJ_1:def 2;
end;
given u,v,w such that
A2: 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);
p = Dir(u) & q = Dir(v) & r = Dir(w) & u is not zero & v is not zero &
w is not zero & u,v,w are_LinDep by A2,ANPROJ_1:def 2;
hence p,q,r are_collinear by ANPROJ_2:23;
end;
theorem Th10:
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
proof
let u,v,w be Element of V;
assume that
A1: a <> 0 and
A2: a * u + b * v + c * w = 0.V;
a*u + (b*v+c*w)=0.V by RLVECT_1:def 3,A2; then
A3: -(b*v+c*w) = a*u by RLVECT_1:6;
a*u = 1 *(-(b*v+c*w)) by A3,RLVECT_1:def 8
.= (a*(1/a))*(-(b*v+c*w)) by A1,XCMPLX_1:106
.= a*((1/a)*(-(b*v+c*w))) by RLVECT_1:def 7;
then u = (1/a)*(-(b*v+c*w)) by A1,RLVECT_1:36
.= (1/a) * ((-1) * (b*v+c*w)) by RLVECT_1:16
.= (1/a) * ((-1) * (b*v) + (-1)* (c*w)) by RLVECT_1:def 5
.= (1/a) * ((-1) * (b*v)) + (1/a)*((-1)*(c*w)) by RLVECT_1:def 5
.= ((1/a) * (-1)) * (b*v) + (1/a)*((-1)*(c*w)) by RLVECT_1:def 7
.= ((-1/a) * b) * v + (1/a)*((-1)*(c*w)) by RLVECT_1:def 7
.= ((-1) / a)* b * v + (1/a)*((-1)*(c*w)) by XCMPLX_1:187
.= ((-1) * b /a) * v + (1/a)*((-1)*(c*w)) by XCMPLX_1:74
.= ((-b) /a) * v + ((1/a)*(-1))*(c*w) by RLVECT_1:def 7
.= ((-b) /a) * v + ((-1/a)*c)*w by RLVECT_1:def 7
.= ((-b) /a) * v + (((-1)/a)*c)*w by XCMPLX_1:187
.= ((-b) /a) * v + ((-1)*c/a)*w by XCMPLX_1:74
.= ((-b) /a) * v + ((-c)/a)*w;
hence thesis;
end;
theorem Th11:
a <> 0 & a * b + c * d + e * f = 0 implies b = - (c/a) * d - (e/a) * f
proof
assume that
A1: a <> 0 and
A2: a * b + c * d + e * f = 0;
b = ((- c) * d + (-e) * f) / a by A1,A2,XCMPLX_1:89
.= (- c) * d / a + (-e) * f / a by XCMPLX_1:62
.= (- c) / a * d + (-e) * f / a by XCMPLX_1:74
.= (- c) / a * d + (-e) / a * f by XCMPLX_1:74
.= (- (c / a)) * d + (-e) / a * f by XCMPLX_1:187
.= (- (c / a)) * d + (-(e / a)) * f by XCMPLX_1:187;
hence thesis;
end;
theorem Th12:
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
proof
let u,v,w be Point of TOP-REAL 3;
assume
A4: ex a,b,c st a*u + b*v + c*w = 0.(TOP-REAL 3) & a<>0;
consider a,b,c such that
B1: a*u + b*v + c*w = 0.(TOP-REAL 3) and
B2: a <> 0 by A4;
reconsider u1 = u,v1 = v,w1= w as Element of REAL 3 by EUCLID:22;
reconsider vw = v <X> w as Element of REAL 3 by EUCLID:22;
|{u,v,w}| = |{((-b)/a) * v + ((-c)/a) * w,v,w}| by B1,B2,Th10
.= |( ((-b)/a) * v + ((-c)/a) * w,v <X> w )| by EUCLID_5:def 5
.= ((-b)/a) * |(v1,vw)| + ((-c)/a) * |(w1,vw)| by EUCLID_4:27
.= ((-b)/a) * |{v,v,w}| + ((-c)/a) * |(w1,vw)| by EUCLID_5:def 5
.= ((-b)/a) * |{v,v,w}| + ((-c)/a) * |{w,v,w}| by EUCLID_5:def 5
.= ((-b)/a) * 0 + ((-c)/a) * |{w,v,w}| by EUCLID_5:31
.= ((-b)/a) * 0 + ((-c)/a) * 0 by EUCLID_5:31
.= 0;
hence thesis;
end;
theorem Th13:
for n being Nat holds dom 1_Rmatrix(n) = Seg n
proof
let n be Nat;
len 1_Rmatrix(n) = n by MATRIX_0:24;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th14:
for A being Matrix of F_Real holds MXR2MXF MXF2MXR A = A
proof
let A be Matrix of F_Real;
MXR2MXF MXF2MXR A = MXF2MXR A by MATRIXR1:def 1;
hence thesis by MATRIXR1:def 2;
end;
theorem Th15:
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
proof
let A,B be Matrix of F_Real;
let RA,RB be Matrix of REAL;
assume that
A1: A = RA and
A2: B = RB;
RA * RB = MXF2MXR (MXR2MXF RA * MXR2MXF RB) by MATRIXR1:def 6
.= MXF2MXR (A * MXR2MXF RB) by A1,MATRIXR1:def 1
.= MXF2MXR (A * B) by A2,MATRIXR1:def 1;
then MXR2MXF (RA * RB) = A * B by Th14;
hence thesis by MATRIXR1:def 1;
end;
theorem
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
proof
let n be Nat;
let M be Matrix of n,REAL;
let N be Matrix of n,F_Real;
assume
A1: M = N;
A2: 1.(F_Real,n) = MXF2MXR 1.(F_Real,n) by MATRIXR1:def 2
.= 1_Rmatrix(n) by MATRIXR2:def 2;
hereby
assume M is invertible;
then consider B be Matrix of n,REAL such that
A3: B * M = 1_Rmatrix(n) and
A4: M * B = 1_Rmatrix(n) by MATRIXR2:def 5;
reconsider C = B as Matrix of n,F_Real;
A5: B * M = C * N by A1,Th15;
C is_reverse_of N
proof
C * N = N * C by A1,A3,A4,A5,Th15;
hence thesis by A2,A3,A1,Th15,MATRIX_6:def 2;
end;
hence N is invertible by MATRIX_6:def 3;
end;
assume N is invertible;
then consider N2 be Matrix of n,F_Real such that
A6: N is_reverse_of N2 by MATRIX_6:def 3;
reconsider M2 = N2 as Matrix of n,REAL;
now
take M2;
A7: M2 * M = N2 * N by A1,Th15
.= 1.(F_Real,n) by A6,MATRIX_6:def 2;
hence M2 * M = 1_Rmatrix(n) by A2;
M2 * M = N2 * N by A1,Th15
.= N * N2 by A6,MATRIX_6:def 2
.= M * M2 by A1,Th15;
hence M * M2 = 1_Rmatrix(n) by A7,A2;
end;
hence M is invertible by MATRIXR2:def 5;
end;
reserve o,p,q,r,s,t for Point of TOP-REAL 3,
M for Matrix of 3,F_Real;
theorem Th16:
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
proof
let p1,p2,p3,q1,q2,q3,r1,r2,r3 be Real;
reconsider P1 = p1,P2 = p2,P3 = p3,
Q1 = q1,Q2 = q2,Q3 = q3,
R1 = r1,R2 = r2,R3 = r3 as Element of F_Real by XREAL_0:def 1;
<*<*P1,P2,P3*>,<*Q1,Q2,Q3*>,<*R1,R2,R3*>*> is Matrix of 3,F_Real
by MATRIXR2:35;
hence thesis;
end;
theorem Th17:
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
proof
let p1,p2,p3,q1,q2,q3,r1,r2,r3 be Real;
assume M = <*<*p1,q1,r1*>,<*p2,q2,r2*>,<*p3,q3,r3*>*>; then
A1: M.1 = <*p1,q1,r1*> & M.2 = <*p2,q2,r2*> &
M.3 = <*p3,q3,r3*>;
A2: [1,1] in Indices M & [1,2] in Indices M & [1,3] in Indices M &
[2,1] in Indices M & [2,2] in Indices M &
[2,3] in Indices M &[3,1] in Indices M & [3,2] in Indices M &
[3,3] in Indices M by MATRIX_0:24,Th1;
then ex s be FinSequence of F_Real st s = M.1 & M*(1,1) = s.1
by MATRIX_0:def 5;
hence M*(1,1) = p1 by A1;
ex s be FinSequence of F_Real st s = M.1 & M*(1,2) = s.2
by A2,MATRIX_0:def 5;
hence M*(1,2) = q1 by A1;
ex s be FinSequence of F_Real st s = M.1 & M*(1,3) = s.3
by A2,MATRIX_0:def 5;
hence M*(1,3) = r1 by A1;
ex s be FinSequence of F_Real st s = M.2 & M*(2,1) = s.1
by A2,MATRIX_0:def 5;
hence M*(2,1) = p2 by A1;
ex s be FinSequence of F_Real st s = M.2 & M*(2,2) = s.2
by A2,MATRIX_0:def 5;
hence M*(2,2) = q2 by A1;
ex s be FinSequence of F_Real st s = M.2 & M*(2,3) = s.3
by A2,MATRIX_0:def 5;
hence M*(2,3) = r2 by A1;
ex s be FinSequence of F_Real st s = M.3 & M*(3,1) = s.1
by A2,MATRIX_0:def 5;
hence M*(3,1) = p3 by A1;
ex s be FinSequence of F_Real st s = M.3 & M*(3,2) = s.2
by A2,MATRIX_0:def 5;
hence M*(3,2) = q3 by A1;
ex s be FinSequence of F_Real st s = M.3 & M*(3,3) = s.3
by A2,MATRIX_0:def 5;
hence M*(3,3) = r3 by A1;
end;
theorem Th18:
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
proof
assume M = <*p,q,r*>;
then M.1 = p & M.2 = q & M.3 = r; then
A1: M.1 = <*p`1,p`2,p`3*> & M.2 = <*q`1,q`2,q`3*> & M.3 = <*r`1,r`2,r`3*>
by EUCLID_5:3;
A2: [1,1] in Indices M & [1,2] in Indices M & [1,3] in Indices M &
[2,1] in Indices M & [2,2] in Indices M &
[2,3] in Indices M &[3,1] in Indices M & [3,2] in Indices M &
[3,3] in Indices M by MATRIX_0:24,Th1;
then ex s be FinSequence of F_Real st s = M.1 & M*(1,1) = s.1
by MATRIX_0:def 5;
hence M*(1,1) = p`1 by A1;
ex s be FinSequence of F_Real st s = M.1 & M*(1,2) = s.2
by A2,MATRIX_0:def 5;
hence M*(1,2) = p`2 by A1;
ex s be FinSequence of F_Real st s = M.1 & M*(1,3) = s.3
by A2,MATRIX_0:def 5;
hence M*(1,3) = p`3 by A1;
ex s be FinSequence of F_Real st s = M.2 & M*(2,1) = s.1
by A2,MATRIX_0:def 5;
hence M*(2,1) = q`1 by A1;
ex s be FinSequence of F_Real st s = M.2 & M*(2,2) = s.2
by A2,MATRIX_0:def 5;
hence M*(2,2) = q`2 by A1;
ex s be FinSequence of F_Real st s = M.2 & M*(2,3) = s.3
by A2,MATRIX_0:def 5;
hence M*(2,3) = q`3 by A1;
ex s be FinSequence of F_Real st s = M.3 & M*(3,1) = s.1
by A2,MATRIX_0:def 5;
hence M*(3,1) = r`1 by A1;
ex s be FinSequence of F_Real st s = M.3 & M*(3,2) = s.2
by A2,MATRIX_0:def 5;
hence M*(3,2) = r`2 by A1;
ex s be FinSequence of F_Real st s = M.3 & M*(3,3) = s.3
by A2,MATRIX_0:def 5;
hence M*(3,3) = r`3 by A1;
end;
theorem Th19:
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*>*>
proof
let p1,p2,p3,q1,q2,q3,r1,r2,r3 be Real;
assume
A1: M = <*<*p1,q1,r1*>,<*p2,q2,r2*>,<*p3,q3,r3*>*>;
Indices M = [:Seg 3,Seg 3:] by MATRIX_0:24; then
A2: M@*(1,1) = M*(1,1) & M@*(1,2) = M*(2,1) & M@*(1,3) = M*(3,1) &
M@*(2,1) = M*(1,2) & M@*(2,2) = M*(2,2) & M@*(2,3) = M*(3,2) &
M@*(3,1) = M*(1,3) & M@*(3,2) = M*(2,3) & M@*(3,3) = M*(3,3)
by MATRIX_0:def 6,Th1;
M*(1,1) = p1 & M*(2,1) = p2 & M*(3,1) = p3 &
M*(1,2) = q1 & M*(2,2) = q2 & M*(3,2) = q3 &
M*(1,3) = r1 & M*(2,3) = r2 & M*(3,3) = r3 by A1,Th17;
hence thesis by A2,MATRIXR2:37;
end;
theorem Th20:
M = <* p,q,r *> implies
M@ = <*<*p`1,q`1,r`1*>,<*p`2,q`2,r`2*>,<*p`3,q`3,r`3*>*>
proof
assume
A1: M = <* p,q,r *>;
Indices M = [:Seg 3,Seg 3:] by MATRIX_0:24; then
A2: M@*(1,1) = M*(1,1) & M@*(1,2) = M*(2,1) & M@*(1,3) = M*(3,1) &
M@*(2,1) = M*(1,2) & M@*(2,2) = M*(2,2) & M@*(2,3) = M*(3,2) &
M@*(3,1) = M*(1,3) & M@*(3,2) = M*(2,3) & M@*(3,3) = M*(3,3)
by MATRIX_0:def 6,Th1;
M*(1,1) = p`1 & M*(2,1) = q`1 & M*(3,1) = r`1 &
M*(1,2) = p`2 & M*(2,2) = q`2 & M*(3,2) = r`2 &
M*(1,3) = p`3 & M*(2,3) = q`3 & M*(3,3) = r`3 by A1,Th18;
hence thesis by A2,MATRIXR2:37;
end;
theorem Th21:
lines M = {Line(M,1),Line(M,2),Line(M,3)}
proof
A1: lines M c= {Line(M,1),Line(M,2),Line(M,3)}
proof
let x be object;
assume x in lines M;
then consider i be Nat such that
A2: i in Seg 3 and
A3: x = Line(M,i) by MATRIX13:103;
i = 1 or i = 2 or i = 3 by A2,FINSEQ_3:1,ENUMSET1:def 1;
hence thesis by A3,ENUMSET1:def 1;
end;
{Line(M,1),Line(M,2),Line(M,3)} c= lines M
proof
let x be object;
assume x in {Line(M,1),Line(M,2),Line(M,3)}; then
A4: x = Line(M,1) or x = Line(M,2) or x = Line(M,3) by ENUMSET1:def 1;
1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1;
hence thesis by A4,MATRIX13:103;
end;
hence thesis by A1;
end;
theorem Th22:
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
proof
assume
A1: M = <*<*p`1,p`2,p`3*>,<*q`1,q`2,q`3*>,<*r`1,r`2,r`3*>*>;
1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1;
then Line(M,1) = M.1 & Line(M,2) = M.2 & Line(M,3) = M.3 by MATRIX_0:52;
then Line(M,1) = <*p`1,p`2,p`3*> & Line(M,2) = <*q`1,q`2,q`3*> &
Line(M,3) = <*r`1,r`2,r`3*> by A1;
hence thesis by EUCLID_5:3;
end;
theorem
for x be object holds x in lines M@ iff
ex i be Nat st i in Seg 3 & x = Col(M,i)
proof
let x be object;
hereby
assume x in lines M@;
then consider i be Nat such that
A1: i in Seg 3 and
A2: x = Line( M@ ,i) by MATRIX13:103;
i in Seg width M by A1,MATRIX_0:24;
then x = Col(M,i) by A2,MATRIX_0:59;
hence ex i be Nat st i in Seg 3 & x = Col(M,i) by A1;
end;
given i be Nat such that
A3: i in Seg 3 and
A4: x = Col(M,i);
i in Seg width M by A3,MATRIX_0:24;
then x = Line(M@,i) by A4,MATRIX_0:59;
hence x in lines M@ by A3,MATRIX13:103;
end;
begin :: Grassman-Pl\{?}ucker relation
theorem Th23:
|{ 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
proof
A1: p = |[ p`1,p`2,p`3 ]| by EUCLID_5:3;
A2: q <X> r = |[ (q`2 * r`3) - (q`3 * r`2) , (q`3 * r`1) - (q`1 * r`3) ,
(q`1 * r`2) - (q`2 * r`1) ]| by EUCLID_5:def 4;
|( p, q <X> r )| = p`1*((q`2 * r`3) - (q`3 * r`2))+p`2*((q`3 * r`1) -
(q`1 * r`3))+ p`3*((q`1 * r`2) - (q`2 * r`1)) by A1,A2,EUCLID_5:30;
hence thesis by EUCLID_5:def 5;
end;
::$N Grassmann-Pl\{?}ucker-Relation in rank 3
theorem
|{p,q,r}| * |{p,s,t}| - |{p,q,s}| * |{p,r,t}| + |{p,q,t}| * |{p,r,s}| = 0
proof
A1: |{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 by Th23;
A2: |{p,s,t}| = p`1 * s`2 * t`3 - p`3 * s`2 * t`1 - p`1 * s`3 * t`2 +
p`2 * s`3 * t`1 - p`2 * s`1 * t`3 + p`3 * s`1 * t`2 by Th23;
A3: |{p,q,s}| = p`1 * q`2 * s`3 - p`3 * q`2 * s`1 - p`1 * q`3 * s`2 +
p`2 * q`3 * s`1 - p`2 * q`1 * s`3 + p`3 * q`1 * s`2 by Th23;
A4: |{p,r,t}| = p`1 * r`2 * t`3 - p`3 * r`2 * t`1 - p`1 * r`3 * t`2 +
p`2 * r`3 * t`1 - p`2 * r`1 * t`3 + p`3 * r`1 * t`2 by Th23;
A5: |{p,q,t}| = p`1 * q`2 * t`3 - p`3 * q`2 * t`1 - p`1 * q`3 * t`2 +
p`2 * q`3 * t`1 - p`2 * q`1 * t`3 + p`3 * q`1 * t`2 by Th23;
|{p,r,s}| = p`1 * r`2 * s`3 - p`3 * r`2 * s`1 - p`1 * r`3 * s`2 +
p`2 * r`3 * s`1 - p`2 * r`1 * s`3 + p`3 * r`1 * s`2 by Th23;
hence thesis by A1,A2,A3,A4,A5;
end;
theorem Th24:
|{ p,q,r }| = - |{ p,r,q }|
proof
A1: |{ 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 by Th23;
|{ p,r,q }| = p`1 * r`2 * q`3 - p`3*r`2*q`1 - p`1*r`3*q`2 +
p`2*r`3*q`1 - p`2*r`1*q`3 + p`3*r`1*q`2 by Th23;
hence thesis by A1;
end;
theorem Th25:
|{ p,q,r }| = - |{ q,p,r }|
proof
A1: |{ 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 by Th23;
|{ q,p,r }| = q`1 * p`2 * r`3 - q`3*p`2*r`1 - q`1*p`3*r`2 + q`2*p`3*r`1 -
q`2*p`1*r`3 + q`3*p`1*r`2 by Th23;
hence thesis by A1;
end;
theorem Th26:
|{ a * p, q, r }| = a * |{ p, q, r }|
proof
|{ a * p,q , r }| = (a * p)`1 * q`2 * r`3 - (a * p)`3*q`2*r`1 -
(a * p)`1*q`3*r`2 + (a * p)`2*q`3*r`1 -
(a * p)`2*q`1*r`3 + (a * p)`3*q`1*r`2 by Th23
.= a * p`1 * q`2 * r`3 - (a * p)`3*q`2*r`1 -
(a * p)`1*q`3*r`2 + (a * p)`2*q`3*r`1 -
(a * p)`2*q`1*r`3 + (a * p)`3*q`1*r`2 by EUCLID_5:9
.= a * p`1 * q`2 * r`3 - a * p`3*q`2*r`1 -
(a * p)`1*q`3*r`2 + (a * p)`2*q`3*r`1 -
(a * p)`2*q`1*r`3 + (a * p)`3*q`1*r`2 by EUCLID_5:9
.= a * p`1 * q`2 * r`3 - a * p`3*q`2*r`1 -
a * p`1*q`3*r`2 + (a * p)`2*q`3*r`1 -
(a * p)`2*q`1*r`3 + (a * p)`3*q`1*r`2 by EUCLID_5:9
.= a * p`1 * q`2 * r`3 - a * p`3*q`2*r`1 -
a * p`1*q`3*r`2 + a * p`2*q`3*r`1 -
(a * p)`2*q`1*r`3 + (a * p)`3*q`1*r`2 by EUCLID_5:9
.= a * p`1 * q`2 * r`3 - a * p`3*q`2*r`1 -
a * p`1*q`3*r`2 + a * p`2*q`3*r`1 -
a * p`2*q`1*r`3 + (a * p)`3*q`1*r`2 by EUCLID_5:9
.= a * p`1 * q`2 * r`3 - a * p`3*q`2*r`1 -
a * p`1*q`3*r`2 + a * p`2*q`3*r`1 -
a * p`2*q`1*r`3 + a * p`3*q`1*r`2 by EUCLID_5:9
.= a * (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)
.= a * |{ p,q,r }| by Th23;
hence thesis;
end;
theorem Th27:
|{ p, a * q, r }| = a * |{ p, q, r }|
proof
|{p, a * q , r }| = - |{ a *q, p,r}| by Th25
.= - (a * |{q,p,r}|) by Th26
.= - (a * (- |{p,q,r}|)) by Th25;
hence thesis;
end;
theorem Th28:
|{ p, q, a * r }| = a * |{ p, q, r }|
proof
|{p, q , a * r }| = - |{ p, a * r,q}| by Th24
.= - (a * |{p,r,q}|) by Th27
.= - (a * (- |{p,q,r}|)) by Th24;
hence thesis;
end;
theorem
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
proof
assume M = <*<*p`1,q`1,r`1*>,<*p`2,q`2,r`2*>,<*p`3,q`3,r`3*>*>; then
A1: M@ = <*<*p`1,p`2,p`3*>,<*q`1,q`2,q`3*>,<*r`1,r`2,r`3*>*> by Th19;
A2: p = |[ p`1,p`2,p`3 ]| by EUCLID_5:3;
A3: q <X> r = |[ (q`2 * r`3) - (q`3 * r`2) , (q`3 * r`1) - (q`1 * r`3) ,
(q`1 * r`2) - (q`2 * r`1) ]| by EUCLID_5:def 4;
A4: |( p, q <X> r )| = p`1*((q`2 * r`3) - (q`3 * r`2))+p`2*((q`3 * r`1) -
(q`1 * r`3))+ p`3*((q`1 * r`2) - (q`2 * r`1)) by A2,A3,EUCLID_5:30;
reconsider p1 = p`1,p2 = p`2,p3 = p`3,
q1 = q`1,q2 = q`2,q3 = q`3,
r1 = r`1,r2 = r`2,r3 = r`3 as Element of F_Real
by XREAL_0:def 1;
Det M = Det M@ by MATRIX_7:37
.= p1*q2*r3 - p3*q2*r1 - p1*q3*r2
+ p2*q3*r1 - p2*q1*r3 + p3*q1*r2
by A1,MATRIX_9:46;
hence thesis by A4,EUCLID_5:def 5;
end;
theorem Th29:
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
proof
assume
A1: M = <*<*p`1,p`2,p`3*>,<*q`1,q`2,q`3*>,<*r`1,r`2,r`3*>*>;
A2: p = |[ p`1,p`2,p`3 ]| by EUCLID_5:3;
A3: q <X> r = |[ (q`2 * r`3) - (q`3 * r`2) , (q`3 * r`1) - (q`1 * r`3) ,
(q`1 * r`2) - (q`2 * r`1) ]| by EUCLID_5:def 4;
A4: |( p, q <X> r )| = p`1*((q`2 * r`3) - (q`3 * r`2))+p`2*((q`3 * r`1) -
(q`1 * r`3))+ p`3*((q`1 * r`2) - (q`2 * r`1)) by A2,A3,EUCLID_5:30;
reconsider p1 = p`1,p2 = p`2,p3 = p`3,
q1 = q`1,q2 = q`2,q3 = q`3,
r1 = r`1,r2 = r`2,r3 = r`3 as Element of F_Real
by XREAL_0:def 1;
Det M = p1*q2*r3 - p3*q2*r1 - p1*q3*r2 + p2*q3*r1 - p2*q1*r3 + p3*q1*r2
by A1,MATRIX_9:46;
hence thesis by A4,EUCLID_5:def 5;
end;
theorem Th30:
for M being Matrix of k,F_Real holds
Det M = 0.F_Real iff the_rank_of M < k
proof
let M be Matrix of k,F_Real;
A1: Det M = 0.F_Real iff the_rank_of M <> k by MATRIX13:83;
A2: the_rank_of M <= len M by MATRIX13:74;
len M = k by MATRIX_0:def 2;
hence thesis by A1,A2,XXREAL_0:1;
end;
theorem Th31:
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
proof
let M be Matrix of k,F_Real;
A1: the_rank_of M = k iff lines M is linearly-independent &
M is without_repeated_line by MATRIX13:121;
A2: the_rank_of M <= len M by MATRIX13:74;
len M = k by MATRIX_0:def 2;
hence thesis by A1,A2,XXREAL_0:1;
end;
theorem Th32:
for M being Matrix of k,m,F_Real holds
Mx2Tran M is Function of RLSp2RVSp(TOP-REAL k),RLSp2RVSp(TOP-REAL m)
proof
let M be Matrix of k,m,F_Real;
RLSp2RVSp(TOP-REAL k) =
ModuleStr (# the carrier of TOP-REAL k, the addF of TOP-REAL k,
the ZeroF of TOP-REAL k, MultF_Real*(TOP-REAL k) #) &
RLSp2RVSp(TOP-REAL m) =
ModuleStr (# the carrier of TOP-REAL m, the addF of TOP-REAL m,
the ZeroF of TOP-REAL m, MultF_Real*(TOP-REAL m) #) by DUALSP01:def 2;
hence thesis;
end;
theorem Th33:
for M being Matrix of k,F_Real holds
Mx2Tran M is linear-transformation of
RLSp2RVSp(TOP-REAL k),RLSp2RVSp(TOP-REAL k)
proof
let M be Matrix of k,F_Real;
reconsider M2 = Mx2Tran M as Function of RLSp2RVSp(TOP-REAL k),
RLSp2RVSp(TOP-REAL k) by Th32;
A1: RLSp2RVSp(TOP-REAL k) = ModuleStr (# the carrier of TOP-REAL k,
the addF of TOP-REAL k, the ZeroF of TOP-REAL k,
MultF_Real*(TOP-REAL k) #) by DUALSP01:def 2;
for x,y be Element of RLSp2RVSp(TOP-REAL k) holds M2.(x + y) = M2.x + M2.y
proof
let x,y be Element of RLSp2RVSp(TOP-REAL k);
reconsider xr = x,yr = y as Element of TOP-REAL k by A1;
A2: x + y = xr + yr by A1;
M2.(x + y) = (Mx2Tran M).xr + (Mx2Tran M).yr by A2,MATRTOP1:22
.= M2.x + M2.y by A1;
hence thesis;
end;
then
A3: M2 is additive;
for a being Scalar of F_Real, x being Vector of RLSp2RVSp(TOP-REAL k)
holds M2.(a * x) = a * (M2 . x)
proof
let a be Scalar of F_Real,x be Vector of RLSp2RVSp(TOP-REAL k);
reconsider ra = a as Real;
reconsider rx = x as Element of TOP-REAL k by A1;
reconsider X = RLSp2RVSp(TOP-REAL 3) as ModuleStr over F_Real;
A4: a * x = a * rx
proof
MultF_Real*(TOP-REAL k) = the Mult of TOP-REAL k by DUALSP01:def 1;
hence thesis by A1,RLVECT_1:def 1;
end;
a * ((Mx2Tran M).x) = a * (M2.x)
proof
a * (M2.x) = (the Mult of TOP-REAL k).(a,(Mx2Tran M).x)
by A1,DUALSP01:def 1
.= a * ((Mx2Tran M).rx) by RLVECT_1:def 1;
hence thesis;
end;
hence thesis by A4,MATRTOP1:23;
end;
hence thesis by A3,MOD_2:def 2;
end;
theorem Th34:
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)
proof
assume that
A1: M = <*<*p`1,p`2,p`3*>,<*q`1,q`2,q`3*>,<*r`1,r`2,r`3*>*> and
A2: the_rank_of M < 3;
per cases by A2,Th31;
suppose
A3: lines M is linearly-dependent;
Line(M,1) = p & Line(M,2) = q & Line(M,3) = r by A1,Th22;
then lines M = {p, q, r} by Th21;
then {p , q, r} is linearly-dependent by A3,MATRTOP2:7;
hence thesis by RLVECT_4:7;
end;
suppose not M is without_repeated_line;
reconsider M2 = Mx2Tran M as linear-transformation of
RLSp2RVSp(TOP-REAL 3),RLSp2RVSp(TOP-REAL 3) by Th33;
A4: not M2 is one-to-one by A2,MATRTOP1:39;
ex x be Element of RLSp2RVSp(TOP-REAL 3) st x in ker M2 &
not x in (0).RLSp2RVSp(TOP-REAL 3)
proof
assume
A5: not ex x be Element of RLSp2RVSp(TOP-REAL 3) st x in ker M2 &
not x in (0).RLSp2RVSp(TOP-REAL 3);
A6: the carrier of ker M2 c= the carrier of RLSp2RVSp(TOP-REAL 3)
by VECTSP_4:def 2;
A7: the carrier of (0).RLSp2RVSp(TOP-REAL 3) c= the carrier of ker M2
proof
let x be object;
assume x in the carrier of (0).RLSp2RVSp(TOP-REAL 3);
then x in (0).RLSp2RVSp(TOP-REAL 3);
then x = 0.RLSp2RVSp(TOP-REAL 3) by VECTSP_4:35;
then x in ker M2 by RANKNULL:11;
hence thesis;
end;
the carrier of ker M2 c= the carrier of (0).RLSp2RVSp(TOP-REAL 3)
proof
let x be object;
assume
A8: x in the carrier of ker M2; then
A9: x in ker M2;
reconsider y = x as Element of the carrier of
RLSp2RVSp(TOP-REAL 3) by A8,A6;
y in (0).RLSp2RVSp(TOP-REAL 3) by A5,A9;
hence thesis;
end;
then the carrier of ker M2 = the carrier of (0).RLSp2RVSp(TOP-REAL 3)
by A7;
hence thesis by A4,MATRLIN2:43,VECTSP_4:29;
end;
then consider x2 be Element of RLSp2RVSp(TOP-REAL 3) such that
A10: x2 in ker M2 and
A11: not x2 in (0).RLSp2RVSp(TOP-REAL 3);
A12: x2 <> 0.RLSp2RVSp(TOP-REAL 3) by A11,VECTSP_4:35;
A13: RLSp2RVSp(TOP-REAL 3) =
ModuleStr (# the carrier of TOP-REAL 3, the addF of TOP-REAL 3,
the ZeroF of TOP-REAL 3,
MultF_Real*(TOP-REAL 3) #) by DUALSP01:def 2; then
A14: 0.RLSp2RVSp(TOP-REAL 3) = the ZeroF of TOP-REAL 3
by STRUCT_0:def 6
.= 0.TOP-REAL 3 by STRUCT_0:def 6; then
A15: (Mx2Tran M).x2 = |[0,0,0]| by A10,EUCLID_5:4,RANKNULL:10;
reconsider pt = (Mx2Tran M).x2 as Element of TOP-REAL 3
by A10,A14,RANKNULL:10;
A16: <*pt`1,pt`2,pt`3*> = |[0,0,0]| by A15,EUCLID_5:3;
A17: pt`1 = pt.1 by EUCLID_5:def 1;
RLSp2RVSp(TOP-REAL 3) = ModuleStr (# the carrier of TOP-REAL 3,
the addF of TOP-REAL 3, the ZeroF of TOP-REAL 3,
MultF_Real*(TOP-REAL 3) #) by DUALSP01:def 2;
then the ZeroF of RLSp2RVSp(TOP-REAL 3)
= 0.TOP-REAL 3 by STRUCT_0:def 6; then
A18: x2 <> 0.TOP-REAL 3 by A12,STRUCT_0:def 6;
A19: len M = 3 by MATRIX_0:def 2; then
A20: dom M = Seg 3 by FINSEQ_1:def 3; then
A21: len(Col(M,1)) = 3 & for j be Nat st j in Seg 3 holds
(Col(M,1)).j = M*(j,1) by A19, MATRIX_0:def 8;
A22: Col(M,1).1 = M*(1,1) & Col(M,1).2 = M*(2,1) & Col(M,1).3 = M*(3,1)
by A20,MATRIX_0:def 8,FINSEQ_1:1;
A23: len(Col(M,2)) = 3 & for j be Nat st j in Seg 3 holds
(Col(M,2)).j = M*(j,2) by A19, A20,MATRIX_0:def 8;
A24: Col(M,2).1 = M*(1,2) & Col(M,2).2 = M*(2,2) & Col(M,2).3 = M*(3,2)
by A20,MATRIX_0:def 8,FINSEQ_1:1;
A25: len(Col(M,3)) = 3 & for j be Nat st j in Seg 3 holds
(Col(M,3)).j = M*(j,3) by A19,A20, MATRIX_0:def 8;
A26: Col(M,3).1 = M*(1,3) & Col(M,3).2 = M*(2,3) & Col(M,3).3 = M*(3,3)
by A20,MATRIX_0:def 8,FINSEQ_1:1;
A27: pt`2 = pt.2 by EUCLID_5:def 2;
reconsider x3 = x2 as Element of TOP-REAL 3 by A13;
A28: pt`3 = pt.3 by EUCLID_5:def 3;
reconsider x4 = x3 as FinSequence of F_Real by RVSUM_1:145;
A29: @x3 = x3 by MATRTOP1:def 1; then
A30: @x3 = <*x3`1,x3`2,x3`3*> by EUCLID_5:3;
A31: 0 = pt.1 by A17,A16,FINSEQ_1:78
.= (@ x3) "*" (Col(M,1)) by MATRTOP1:18;
reconsider a1 = x3`1, a2 = x3`2, a3 = x3`3,
b1 = M*(1,1), b2 = M*(2,1), b3 = M*(3,1),
c1 = M*(1,2), c2 = M*(2,2), c3 = M*(3,2),
d1 = M*(1,3), d2 = M*(2,3), d3 = M*(3,3) as
Element of F_Real by XREAL_0:def 1;
A32: <*<*p`1,p`2,p`3*>,<*q`1,q`2,q`3*>,<*r`1,r`2,r`3*>*>
= <* <* M*(1,1), M*(1,2), M*(1,3) *>, <* M*(2,1), M*(2,2), M*(2,3) *>,
<* M*(3,1), M*(3,2), M*(3,3) *> *> by A1,MATRIXR2:37;
A33: p = <*p`1,p`2,p`3*> by EUCLID_5:3 .= <* M*(1,1), M*(1,2), M*(1,3) *>
by A32,FINSEQ_1:78;
A34: q = <*q`1,q`2,q`3*> by EUCLID_5:3 .= <* M*(2,1), M*(2,2), M*(2,3) *>
by A32,FINSEQ_1:78;
A35: r = <*r`1,r`2,r`3*> by EUCLID_5:3 .= <* M*(3,1), M*(3,2), M*(3,3) *>
by A32,FINSEQ_1:78;
reconsider q1 = <*x3`1,x3`2,x3`3*>, r1 = <* M*(1,1),M*(2,1),M*(3,1) *>,
r2 = <* M*(1,2),M*(2,2),M*(3,2) *>,
r3 = <* M*(1,3),M*(2,3),M*(3,3) *>
as FinSequence of the carrier of F_Real by A29,EUCLID_5:3;
A36: 0 = q1 "*" r1 by A31,A22,A30,A21,FINSEQ_1:45
.= a1 * b1 + a2 * b2 + a3 * b3 by Th6;
A37: 0 = pt.2 by A16,FINSEQ_1:78,A27
.= (@ x3) "*" (Col(M,2)) by MATRTOP1:18;
A38: 0 = q1 "*" r2 by A37,A23,FINSEQ_1:45,A24,A30
.= a1 * c1 + a2 * c2 + a3 * c3 by Th6;
A39: 0 = pt.3 by A16,FINSEQ_1:78,A28
.= (@ x3) "*" (Col(M,3)) by MATRTOP1:18;
A40: 0 = q1 "*" r3 by A39,A26,A25,FINSEQ_1:45,A30
.= a1 * d1 + a2 * d2 + a3 * d3 by Th6;
A41: a1 <> 0 or a2 <> 0 or a3 <> 0 by A18,EUCLID_5:3,EUCLID_5:4;
a1 * p + a2 * q + a3 * r = a1 * |[ b1, c1, d1]| + (a2 * |[ b2, c2, d2]| +
a3 * |[ b3, c3, d3]|) by A33,RVSUM_1:15,A34,A35
.= a1 * |[ b1, c1, d1]| + (a2 * |[ b2, c2, d2]| +
|[ a3*b3, a3*c3, a3*d3 ]|) by EUCLID_5:8
.= a1 * |[ b1, c1, d1]| +
(|[ a2*b2, a2*c2, a2*d2]| +
|[ a3*b3, a3*c3, a3*d3 ]|) by EUCLID_5:8
.= |[ a1*b1, a1*c1, a1*d1]| +
(|[ a2*b2, a2*c2, a2*d2]| +
|[ a3*b3, a3*c3, a3*d3 ]|) by EUCLID_5:8
.= |[ a1*b1, a1*c1, a1*d1]| +
|[ a2*b2+(a3*b3), a2*c2+(a3*c3),
a2*d2+(a3*d3) ]| by EUCLID_5:6
.= |[ a1*b1+(a2*b2+a3*b3),
a1*c1+(a2*c2+a3*c3),
a1*d1+(a2*d2+a3*d3)]| by EUCLID_5:6
.= 0.(TOP-REAL 3) by A36,A38,A40,EUCLID_5:4;
hence thesis by A41;
end;
end;
theorem Th35:
(a*p + b*q + c*r = 0.(TOP-REAL 3) & (a <> 0 or b <> 0 or c <> 0))
implies |{p,q,r}| = 0
proof
assume a*p + b*q + c*r = 0.(TOP-REAL 3) & (a<>0 or b<>0 or c <>0);
then consider a,b,c such that
A1: a*p + b*q + c*r = 0.(TOP-REAL 3) and
A2: a <> 0 or b <> 0 or c <> 0;
per cases by A2;
suppose a <> 0;
hence thesis by A1,Th12;
end;
suppose b <> 0;
then
A3: |{q,p,r}| = 0 by A1,Th12;
|{p,q,r}| = - |{q,p,r}| by Th25;
hence thesis by A3;
end;
suppose
A4: c <> 0;
c*r + a*p + b*q = 0.(TOP-REAL 3) by A1,RLVECT_1:def 3;
then |{r,p,q}| = 0 by A4,Th12;
hence thesis by EUCLID_5:33;
end;
end;
theorem Th36:
|{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)
proof
assume
A1: |{p,q,r}| = 0;
reconsider M = <*<*p`1,p`2,p`3*>,<*q`1,q`2,q`3*>,<*r`1,r`2,r`3*>*>
as Matrix of 3,F_Real by Th16;
Det M = 0 by A1,Th29
.= 0.F_Real by STRUCT_0:def 6;
then the_rank_of M < 3 by Th30;
hence thesis by Th34;
end;
theorem Th37:
p,q,r are_LinDep iff |{p,q,r}| = 0
proof
hereby assume p,q,r are_LinDep;
then ex a,b,c st a*p + b*q + c*r = 0.TOP-REAL 3 &
(a<>0 or b<>0 or c <>0) by ANPROJ_1:def 2;
hence |{p,q,r}| = 0 by Th35;
end;
assume |{p,q,r}| = 0;
then ex a,b,c st a*p + b*q + c*r = 0.TOP-REAL 3 &
(a<>0 or b<>0 or c <>0) by Th36;
hence p,q,r are_LinDep by ANPROJ_1:def 2;
end;
begin :: Some properties about the cross product
theorem Th38:
|(p,p <X> q)| = 0
proof
thus |(p,p <X> q)| = |{p,p,q}| by EUCLID_5:def 5
.= 0 by EUCLID_5:31;
end;
theorem Th39:
|(p,q <X> p)| = 0
proof
thus |(p,q <X> p)| = |{p,q,p}| by EUCLID_5:def 5
.= 0 by EUCLID_5:31;
end;
theorem Th40:
|{ o, p, (o <X> p) <X> (q <X> r) }| = 0 &
|{ q, r, (o <X> p) <X> (q <X> r) }| = 0
proof
set s = (o <X> p) <X> (q <X> r);
thus |{o,p,s}| = |( o <X> p , s)| by EUCLID_5:35
.= 0 by Th38;
thus |{q,r,s}| = |( q <X> r, (o <X> p) <X> (q <X> r) )| by EUCLID_5:35
.= 0 by Th39;
end;
theorem Th41:
o,p, (o <X> p) <X> (q <X> r) are_LinDep &
q,r, (o <X> p) <X> (q <X> r) are_LinDep
proof
|{o,p, (o <X> p) <X> (q <X> r)}| = 0 &
|{q,r, (o <X> p) <X> (q <X> r)}| = 0 by Th40;
hence thesis by Th37;
end;
theorem Th42:
0.TOP-REAL 3 <X> p = 0.TOP-REAL 3 & p <X> 0.TOP-REAL 3 = 0.TOP-REAL 3
proof
A1: 0.TOP-REAL 3 <X> p = |[0,0,0]| <X> |[p`1,p`2,p`3]| by EUCLID_5:3,EUCLID_5:4
.= 0.TOP-REAL 3 by EUCLID_5:19;
p <X> 0.TOP-REAL 3 = - 0.TOP-REAL 3 by A1,EUCLID_5:17
.= 0.TOP-REAL 3 by RLVECT_1:12;
hence thesis by A1;
end;
theorem
|{p,q,0.TOP-REAL 3}| = 0
proof
|{p,q,0.TOP-REAL 3}| = |(p, q <X> 0.TOP-REAL 3)| by EUCLID_5:def 5
.= |(p,0.TOP-REAL 3)| by Th42;
hence thesis by EUCLID_2:32;
end;
theorem
p <X> q = 0.TOP-REAL 3 & r = |[1,1,1]| implies p,q,r are_LinDep
proof
assume that
A1: p <X> q = 0.TOP-REAL 3 and
A2: r = |[1,1,1]|;
|[ (p`2 * q`3) - (p`3 * q`2) , (p`3 * q`1) - (p`1 * q`3) ,
(p`1 * q`2) - (p`2 * q`1) ]| = |[0,0,0]| by A1,EUCLID_5:def 4,EUCLID_5:4;
then (p`2 * q`3) - (p`3 * q`2) = |[0,0,0]|`1 &
(p`3 * q`1) - (p`1 * q`3) = |[0,0,0]|`2 &
(p`1 * q`2) - (p`2 * q`1) = |[0,0,0]|`3 by EUCLID_5:14; then
A3: (p`2 * q`3) - (p`3 * q`2) = 0 & (p`3 * q`1) - (p`1 * q`3) = 0 &
(p`1 * q`2) - (p`2 * q`1) = 0 by EUCLID_5:14;
reconsider r = |[1,1,1]| as Element of TOP-REAL 3;
|{p,q,r}| = 0
proof
r`1 = 1 & r`2 = 1 & r`3 = 1 by EUCLID_5:2;
then |{ p,q,r }| = p`1 * q`2 * 1 - p`3* q`2 * 1 -
p`1*q`3* 1 + p`2*q`3* 1 -
p`2*q`1* 1 + p`3*q`1* 1 by Th23
.= 0 by A3;
hence thesis;
end;
hence thesis by A2,Th37;
end;
theorem Th43:
p is not zero & q is not zero &
p <X> q = 0.TOP-REAL 3 implies are_Prop p,q
proof
assume that
A1: p is not zero and
A2: q is not zero and
A3: p <X> q = 0.TOP-REAL 3;
A4: |[ (p`2 * q`3) - (p`3 * q`2) , (p`3 * q`1) - (p`1 * q`3) ,
(p`1 * q`2) - (p`2 * q`1) ]| = |[0,0,0]|
by A3,EUCLID_5:def 4,EUCLID_5:4; then
A5: (p`2 * q`3) - (p`3 * q`2) = |[0,0,0]|`1 &
(p`3 * q`1) - (p`1 * q`3) = |[0,0,0]|`2 &
(p`1 * q`2) - (p`2 * q`1) = |[0,0,0]|`3 by EUCLID_5:14; then
A6: (p`2 * q`3) - (p`3 * q`2) = 0 & (p`3 * q`1) - (p`1 * q`3) = 0 &
(p`1 * q`2) - (p`2 * q`1) = 0 by EUCLID_5:14;
per cases;
suppose
A7: p`1 <> 0 & p`2 <> 0 & p`3 <> 0;
A8: q`1 <> 0 & q`2 <> 0 & q`3 <> 0
proof
assume q`1 = 0 or q`2 = 0 or q`3 = 0;
then per cases;
suppose
A9: q`1 = 0; then
A10: q`3 = 0 by A6,A7,XCMPLX_1:6;
q`2 = 0 by A9,A6,A7,XCMPLX_1:6;
hence thesis by A9,A10,EUCLID_5:3,EUCLID_5:4,A2;
end;
suppose
A11: q`2 = 0;
then p`2 * q`3 = 0 by A5,EUCLID_5:14; then
A12: q`3 = 0 by A7,XCMPLX_1:6;
then p`3 * q`1 = 0 by A5,EUCLID_5:14;
then q`1 = 0 by A7,XCMPLX_1:6;
hence thesis by A2,A11,A12,EUCLID_5:3,EUCLID_5:4;
end;
suppose
A13: q`3 = 0;
then p`3 * q`1 = 0 by A5,EUCLID_5:14; then
A14: q`1 = 0 by A7,XCMPLX_1:6;
then p`1 * q`2 = 0 by A5,EUCLID_5:14;
then q`2 = 0 by A7,XCMPLX_1:6;
hence thesis by A2,A13,A14,EUCLID_5:3,EUCLID_5:4;
end;
end;
reconsider l = p`2 / q`2 as Real;
p = l * q
proof
A15: p`1 = p`3 * q`1 / q`3 by A8,A6,XCMPLX_1:89
.= (p`3 / q`3)* q`1 by XCMPLX_1:74;
A16: p`2 = l * q`2 by A8,XCMPLX_1:87;
p`3 = p`1 * q`3 / q`1 by A8,A6,XCMPLX_1:89
.= (p`1 / q`1)* q`3 by XCMPLX_1:74; then
A17: p`3 = l * q`3 by A8,A6,XCMPLX_1:94;
p = |[p`1,p`2,p`3]| by EUCLID_5:3
.= |[l*q`1,l*q`2,l*q`3]| by A16,A17,A15,A8,A4,XCMPLX_1:94
.= l * q by EUCLID_5:7;
hence thesis;
end;
hence thesis by A7,A8,XCMPLX_1:50,ANPROJ_1:1;
end;
suppose
A18: p`1 = 0;
then per cases by EUCLID_5:3,A1,EUCLID_5:4;
suppose
A19: p`2 <> 0;
then
A20: q`1 = 0 by A18,A6,XCMPLX_1:6;
A21: q`2 <> 0
proof
assume
A22: q`2 = 0;
then p`2 * q`3 = 0 by A5,EUCLID_5:14;
then q`3 = 0 by A19,XCMPLX_1:6;
hence thesis by A20,A22,EUCLID_5:3,A2,EUCLID_5:4;
end;
set l = p`2 / q`2;
p = l * q
proof
p`3 = p`2 * q`3 / q`2 by A6,A21,XCMPLX_1:89;
then
A22: p`3 = l * q`3 by XCMPLX_1:74;
p = |[p`1,p`2,p`3]| by EUCLID_5:3
.= |[l*q`1,l*q`2,l*q`3]| by A20,A18,A21,XCMPLX_1:87,A22
.= l * q by EUCLID_5:7;
hence thesis;
end;
hence thesis by A21,A19,XCMPLX_1:50,ANPROJ_1:1;
end;
suppose
A23: p`3 <> 0;
A24: q`1 = 0
proof
p`3 * q`1 = 0 by A18,A5,EUCLID_5:14;
hence thesis by A23,XCMPLX_1:6;
end;
A25: q`3 <> 0
proof
assume
A26: q`3 = 0;
then q`2 = 0 by A6,A23,XCMPLX_1:6;
hence thesis by A24,A26,EUCLID_5:3,A2,EUCLID_5:4;
end;
set l = p`3 / q`3;
p = l * q
proof
A27: l * q`2 = p`2 * q`3 / q`3 by A6,XCMPLX_1:74
.= p`2 by A25,XCMPLX_1:89;
p = |[p`1,p`2,p`3]| by EUCLID_5:3
.= |[l * q`1,l * q`2,l * q`3]| by A24,A18,A27,A25,XCMPLX_1:87
.= l * q by EUCLID_5:7;
hence thesis;
end;
hence thesis by A23,A25,XCMPLX_1:50,ANPROJ_1:1;
end;
end;
suppose
A28: p`2 = 0;
then per cases by A1,EUCLID_5:3,EUCLID_5:4;
suppose
A29: p`1 <> 0;
A30: q`2 = 0
proof
p`1 * q`2 = 0 by A28,A5,EUCLID_5:14;
hence thesis by A29,XCMPLX_1:6;
end;
A31: q`1 <> 0
proof
assume
A32: q`1 = 0;
then q`3 = 0 by A6,A29,XCMPLX_1:6;
hence thesis by A30,A32,EUCLID_5:3,A2,EUCLID_5:4;
end;
set l = p`1 / q`1;
p = l * q
proof
p`3 = p`1 * q`3 / q`1 by A6,A31,XCMPLX_1:89; then
A33: p`3 = p`1 / q`1 * q`3 by XCMPLX_1:74;
p = |[p`1,p`2,p`3]| by EUCLID_5:3
.= |[l*q`1,l*q`2,l*q`3]| by A28,A30,A31,XCMPLX_1:87,A33
.= l * q by EUCLID_5:7;
hence thesis;
end;
hence thesis by A31,A29,XCMPLX_1:50,ANPROJ_1:1;
end;
suppose
A34: p`3 <> 0;
then
A35: q`2 = 0 by A28,A6,XCMPLX_1:6;
A36: q`3 <> 0
proof
assume
A37: q`3 = 0;
then p`3 * q`1 = 0 by A5,EUCLID_5:14;
then q`1 = 0 by A34,XCMPLX_1:6;
hence thesis by A35,A37,EUCLID_5:3,A2,EUCLID_5:4;
end;
set l = p`3 / q`3;
p = l * q
proof
A38: l * q`1 = q`3 * p`1 / q`3 by A6,XCMPLX_1:74
.= p`1 by A36,XCMPLX_1:89;
p = |[p`1,p`2,p`3]| by EUCLID_5:3
.= |[l * q`1,l * q`2,l * q`3]| by A28,A35,A38,A36,XCMPLX_1:87
.= l * q by EUCLID_5:7;
hence thesis;
end;
hence thesis by A34,A36,XCMPLX_1:50,ANPROJ_1:1;
end;
end;
suppose
A39: p`3 = 0;
then per cases by A1,EUCLID_5:3,EUCLID_5:4;
suppose
A40: p`2 <> 0;
A41: q`3 = 0
proof
p`2 * q`3 = 0 by A39,A5,EUCLID_5:14;
hence thesis by A40,XCMPLX_1:6;
end;
A42: q`2 <> 0
proof
assume
A43: q`2 = 0;
then q`1 = 0 by A6,A40,XCMPLX_1:6;
hence thesis by A41,A43,EUCLID_5:3,A2,EUCLID_5:4;
end;
set l = p`2 / q`2;
p = l * q
proof
p`1 = p`2 * q`1 / q`2 by A6,A42,XCMPLX_1:89; then
A44: p`1 = l * q`1 by XCMPLX_1:74;
p = |[p`1,p`2,p`3]| by EUCLID_5:3
.= |[l*q`1,l*q`2,l*q`3]| by A39,A41,A42,XCMPLX_1:87,A44
.= l * q by EUCLID_5:7;
hence thesis;
end;
hence thesis by A42,A40,XCMPLX_1:50,ANPROJ_1:1;
end;
suppose
A45: p`1 <> 0;
then
A46: q`3 = 0 by A39,A6,XCMPLX_1:6;
A47: q`1 <> 0
proof
assume
A48: q`1 = 0;
then p`1 * q`2 = 0 by A5,EUCLID_5:14;
then q`2 = 0 by A45,XCMPLX_1:6;
hence thesis by A2,A46,A48,EUCLID_5:3,EUCLID_5:4;
end;
set l = p`1 / q`1;
p = l * q
proof
A49: l * q`2 = q`1 * p`2 / q`1 by A6,XCMPLX_1:74
.= p`2 by A47,XCMPLX_1:89;
p = |[p`1,p`2,p`3]| by EUCLID_5:3
.= |[l * q`1,l * q`2,l * q`3]| by A39,A46,A49,A47,XCMPLX_1:87
.= l * q by EUCLID_5:7;
hence thesis;
end;
hence thesis by A45,A47,XCMPLX_1:50,ANPROJ_1:1;
end;
end;
end;
theorem Th44:
for p,q,r,s be non zero Point of TOP-REAL 3 st
(p <X> q) <X> (r <X> s) is zero holds
are_Prop p,q or are_Prop r,s or are_Prop p <X> q,r <X> s
proof
let p,q,r,s be non zero Point of TOP-REAL 3;
assume (p <X> q) <X> (r <X> s) is zero;
then p <X> q is zero or r <X> s is zero or
are_Prop p <X> q,r <X> s by Th43;
hence thesis by Th43;
end;
theorem Th45:
|{ p, q, p <X> q }| = |(q,q)| * |(p,p)| - |(q,p)| * |(p,q)|
proof
|{ p, q, p <X> q }| = |( p , q <X> (p <X> q) )| by EUCLID_5:def 5
.= |( p, |(q,q)| * p - |(q,p)| * q )| by EUCLID_5:32
.= |(p, |(q,q)| * p)| - |( p, |(q,p)| * q)|
by EUCLID_2:27
.= |(q,q)| * |(p,p)| - |( p, |(q,p)| * q)|
by EUCLID_2:20
.= |(q,q)| * |(p,p)| - |(q,p)| * |(p,q)| by EUCLID_2:20;
hence thesis;
end;
theorem Th46:
|(p <X> q, p <X> q)| = |(q,q)| * |(p,p)| - |(q,p)| * |(p,q)|
proof
set r1 = (p <X> q)`1, r2 = (p <X> q)`2, r3 = (p <X> q)`3;
p <X> q = |[ (p`2 * q`3) - (p`3 * q`2) , (p`3 * q`1) - (p`1 * q`3) ,
(p`1 * q`2) - (p`2 * q`1) ]| by EUCLID_5:def 4; then
A1: r1 = p`2 * q`3 - p`3 * q`2 & r2 = p`3 * q`1 - p`1 * q`3 &
r3 = p`1 * q`2 - p`2 * q`1 by EUCLID_5:2;
A2: |(p <X> q,p <X> q)| = r1 * r1 + r2 * r2 + r3 * r3 by EUCLID_5:29;
|(q,q)| * |(p,p)| - |(q,p)| * |(p,q)| =
(q`1 * q`1 + q`2 * q`2 + q`3 * q`3) * |(p,p)| - |(q,p)| * |(p,q)|
by EUCLID_5:29
.= (q`1 * q`1 + q`2 * q`2 + q`3 * q`3) *
(p`1 * p`1 + p`2 * p`2 + p`3 * p`3) - |(q,p)| * |(p,q)|
by EUCLID_5:29
.= (q`1 * q`1 + q`2 * q`2 + q`3 * q`3) *
(p`1 * p`1 + p`2 * p`2 + p`3 * p`3) - (q`1*p`1+q`2*p`2+q`3*p`3)
* |(p,q)| by EUCLID_5:29
.= (q`1 * q`1 + q`2 * q`2 + q`3 * q`3) *
(p`1 * p`1 + p`2 * p`2 + p`3 * p`3) - (q`1*p`1+q`2*p`2+q`3*p`3) *
(p`1*q`1+p`2*q`2+p`3*q`3) by EUCLID_5:29;
hence thesis by A1,A2;
end;
theorem Th47:
p is non zero & |(p,q)| = 0 & |(p,r)| = 0 & |(p,s)| = 0 implies |{q,r,s}| = 0
proof
assume that
A1: p is non zero and
A2: |(p,q)| = 0 and
A3: |(p,r)| = 0 and
A4: |(p,s)| = 0;
A5: p`1 * q`1 + p`2 * q`2 + p`3 * q`3 = 0 by A2,EUCLID_5:29;
A6: p`1 * r`1 + p`2 * r`2 + p`3 * r`3 = 0 by A3,EUCLID_5:29;
A7: p`1 * s`1 + p`2 * s`2 + p`3 * s`3 = 0 by A4,EUCLID_5:29;
per cases by A1,EUCLID_5:3,EUCLID_5:4;
suppose
A8: p`1 <> 0;
set l2 = p`2 / p`1, l3 = p`3 / p`1;
A9: q`1 = - l2 * q`2 - l3 * q`3 by Th11,A8,A5;
A10: r`1 = - l2 * r`2 - l3 * r`3 by Th11,A8,A6;
A11: s`1 = - l2 * s`2 - l3 * s`3 by Th11,A8,A7;
|{q,r,s}| = (- l2 * q`2 - l3 * q`3) * r`2 * s`3 -
q`3 * r`2 * (- l2 * s`2 - l3 * s`3) -
(- l2 * q`2 - l3 * q`3) * r`3 * s`2 +
q`2*r`3*(- l2 * s`2 - l3 * s`3) -
q`2*(- l2 * r`2 - l3 * r`3) * s`3 +
q`3*(- l2 * r`2 - l3 * r`3)*s`2 by A9,A10,A11,Th23
.= 0;
hence thesis;
end;
suppose
A12: p`2 <> 0;
set l1 = p`1 / p`2, l3 = p`3 / p`2;
A13: q`2 = - l1 * q`1 - l3 * q`3 by Th11,A12,A5;
A14: r`2 = - l1 * r`1 - l3 * r`3 by Th11,A12,A6;
A15: s`2 = - l1 * s`1 - l3 * s`3 by Th11,A12,A7;
|{q,r,s}| = q`1 * r`2 * s`3 - q`3*r`2*s`1 -
q`1*r`3*s`2 + q`2*r`3*s`1 -
q`2*r`1*s`3 + q`3*r`1*s`2 by Th23
.= 0 by A13,A14,A15;
hence thesis;
end;
suppose
A16: p`3 <> 0;
set l1 = p`1 / p`3, l2 = p`2 / p`3;
p`3 * q`3 + p`1 * q`1 + p`2 * q`2 = 0 by A5; then
A17: q`3 = - l1 * q`1 - l2 * q`2 by Th11,A16;
p`3 * r`3 + p`1 * r`1 + p`2 * r`2 = 0 by A6; then
A18: r`3 = - l1 * r`1 - l2 * r`2 by Th11,A16;
p`1 * s`1 + p`2 * s`2 + p`3 * s`3 = 0 by A4,EUCLID_5:29; then
p`3 * s`3 + p`1 * s`1 + p`2 * s`2 = 0; then
A19: s`3 = - l1 * s`1 - l2 * s`2 by Th11,A16;
|{q,r,s}| = q`1 * r`2 * s`3 - q`3*r`2*s`1 -
q`1*r`3*s`2 + q`2*r`3*s`1 -
q`2*r`1*s`3 + q`3*r`1*s`2 by Th23
.= 0 by A17,A18,A19;
hence thesis;
end;
end;
theorem
|{ p, q, p <X> q }| = |. p <X> q .|^2
proof
|{ p, q, p <X> q }| = |(q,q)| * |(p,p)| - |(q,p)| * |(p,q)| by Th45
.= |(p <X> q,p <X> q)| by Th46;
hence thesis by EUCLID_2:4;
end;
theorem
ProjectiveSpace TOP-REAL 3 is CollProjectivePlane
proof
set PTR3 = ProjectiveSpace TOP-REAL 3;
ex u,v,w1 being Element of TOP-REAL 3 st for a,b,c be Real st
a * u + b * v + c * w1 = 0.TOP-REAL 3 holds a = 0 & b = 0 & c = 0
proof
reconsider u = <e1>, v = <e2>, w = <e3> as Element of TOP-REAL 3
by EUCLID:22;
take u,v,w;
now
let a,b,c be Real;
assume a * <e1> + b * <e2> + c * <e3> = 0.TOP-REAL 3; then
A1: |[a,b,c]| = |[0,0,0]| by EUCLID_5:4,EUCLID_8:39;
|[a,b,c]|`1 = a & |[a,b,c]|`2 = b & |[a,b,c]|`3 = c by EUCLID_5:2;
hence a = 0 & b = 0 & c = 0 by A1,EUCLID_5:2;
end;
hence thesis;
end;
then TOP-REAL 3 is up-3-dimensional by ANPROJ_2:def 6;
then reconsider PTR3 as CollProjectiveSpace;
for p,p1,q,q1 be Element of PTR3 ex r being Element of PTR3 st
p,p1,r are_collinear & q,q1,r are_collinear
proof
let p,p1,q,q1 be Element of PTR3;
consider up be Element of TOP-REAL 3 such that
A2: up is not zero and
A3: p = Dir(up) by ANPROJ_1:26;
consider up1 be Element of TOP-REAL 3 such that
A4: up1 is not zero and
A5: p1 = Dir(up1) by ANPROJ_1:26;
consider uq be Element of TOP-REAL 3 such that
A6: uq is not zero and
A7: q = Dir(uq) by ANPROJ_1:26;
consider uq1 be Element of TOP-REAL 3 such that
A8: uq1 is not zero and
A9: q1 = Dir(uq1) by ANPROJ_1:26;
ex r being Element of PTR3 st p,p1,r are_collinear & q,q1,r are_collinear
proof
set w = (up <X> up1) <X> (uq <X> uq1);
per cases;
suppose w is zero;
then per cases by A4,A6,A8,A2,Th44;
suppose are_Prop up,up1;
then
A10: p = p1 by A3,A5,A2,A4,ANPROJ_1:22;
take q;
thus p,p1,q are_collinear by A10,COLLSP:2;
thus q,q1,q are_collinear by COLLSP:2;
end;
suppose are_Prop uq,uq1;
then
A11: q = q1 by A6,A7,A8,A9,ANPROJ_1:22;
take p;
thus p,p1,p are_collinear by COLLSP:2;
thus q,q1,p are_collinear by A11,COLLSP:2;
end;
suppose
A12: are_Prop up <X> up1,uq <X> uq1;
then consider a be Real such that
a <> 0 and
A13: uq <X> uq1 = a * (up <X> up1) by ANPROJ_1:1;
per cases;
suppose up <X> up1 is zero;
then are_Prop up,up1 by A2,A4,Th43; then
A14: p = p1 by A3,A5,A2,A4,ANPROJ_1:22;
take q;
thus p,p1,q are_collinear by A14,COLLSP:2;
thus q,q1,q are_collinear by COLLSP:2;
end;
suppose
A15: up <X> up1 is not zero;
A16: uq <X> uq1 is not zero
proof
assume
A17: uq <X> uq1 is zero;
consider a be Real such that
A18: a <> 0 and
A19: uq <X> uq1 = a * (up <X> up1) by A12,ANPROJ_1:1;
set r1 = (up <X> up1)`1,r2 = (up <X> up1)`2,r3=(up <X> up1)`3;
|[a * r1,a * r2,a * r3]| = a * |[r1,r2,r3]| by EUCLID_5:8
.= |[0,0,0]|
by A19,A17,EUCLID_5:3,EUCLID_5:4;
then a * r1 = 0 & a * r2 = 0 & a * r3 = 0 by FINSEQ_1:78;
then r1 = 0 & r2 = 0 & r3 = 0 by A18,XCMPLX_1:6;
hence thesis by A15,EUCLID_5:3,EUCLID_5:4;
end;
reconsider r = Dir up as Element of PTR3 by A2,ANPROJ_1:26;
take r;
|{up,up1,up}| = 0 by EUCLID_5:31;
hence p,p1,r are_collinear by A2,A3,A4,A5,Th37,ANPROJ_2:23;
now
thus uq <X> uq1 is non zero by A16;
thus |(uq <X> uq1,uq)| = |{uq,uq,uq1}| by EUCLID_5:def 5
.= 0 by EUCLID_5:31;
thus |(uq <X> uq1,uq1)| = |{uq1,uq,uq1}| by EUCLID_5:def 5
.= 0 by EUCLID_5:31;
reconsider rp1 = up <X> up1, rp = up as Element of REAL 3
by EUCLID:22;
A20: a * |(up <X> up1,up)| = |(a * rp1,rp)|
by EUCLID_8:68
.= |(a * (up <X> up1),up)|;
|(up <X> up1,up)| = |{up,up,up1}| by EUCLID_5:def 5
.= 0 by EUCLID_5:31;
hence |(uq <X> uq1,up)| = 0 by A20,A13;
end;
then |{uq,uq1,up}| = 0 by Th47;
hence q,q1,r are_collinear by A2,A6,A7,A8,A9,Th37,ANPROJ_2:23;
end;
end;
end;
suppose
A21: w is not zero;
then reconsider r = Dir w as Element of PTR3 by ANPROJ_1:26;
take r;
thus p,p1,r are_collinear by A2,A3,A4,A5,A21,Th41,ANPROJ_2:23;
thus q,q1,r are_collinear by A6,A7,A8,A9,A21,Th41,ANPROJ_2:23;
end;
end;
hence thesis;
end;
hence thesis by ANPROJ_2:def 14;
end;
begin :: Real projective plane and homography
theorem Th48:
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
proof
let u,v,w,x being Element of TOP-REAL 3;
assume that
A1: u is not zero and
A2: x is not zero and
A3: Dir u = Dir x;
A4: are_Prop u,x by A1,A2,A3,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A5: u = a * x by ANPROJ_1:1;
consider b be Real such that
b <> 0 and
A6: x = b * u by A4,ANPROJ_1:1;
hereby
assume
A7: |{u,v,w}| = 0;
thus |{x,v,w}| = b * |{u,v,w}| by A6,Th26
.= 0 by A7;
end;
assume
A8: |{x,v,w}| = 0;
thus |{u,v,w}| = a * |{x,v,w}| by A5,Th26
.= 0 by A8;
end;
theorem Th49:
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
proof
let u,v,w,x being Element of TOP-REAL 3;
assume that
A1: v is not zero and
A2: x is not zero and
A3: Dir v = Dir x;
A4: are_Prop v,x by A1,A2,A3,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A5: v = a * x by ANPROJ_1:1;
consider b be Real such that
b <> 0 and
A6: x = b * v by A4,ANPROJ_1:1;
hereby
assume
A7: |{u,v,w}| = 0;
thus |{u,x,w}| = b * |{u,v,w}| by A6,Th27
.= 0 by A7;
end;
assume
A8: |{u,x,w}| = 0;
thus |{u,v,w}| = a * |{u,x,w}| by A5,Th27
.= 0 by A8;
end;
theorem Th50:
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
proof
let u,v,w,x being Element of TOP-REAL 3;
assume that
A1: w is not zero and
A2: x is not zero and
A3: Dir w = Dir x;
A4: are_Prop w,x by A1,A2,A3,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A5: w = a * x by ANPROJ_1:1;
consider b be Real such that
b <> 0 and
A6: x = b * w by A4,ANPROJ_1:1;
hereby
assume
A7: |{u,v,w}| = 0;
thus |{u,v,x}| = b * |{u,v,w}| by A6,Th28
.= 0 by A7;
end;
assume
A8: |{u,v,x}| = 0;
thus |{u,v,w}| = a * |{u,v,x}| by A5,Th28
.= 0 by A8;
end;
theorem
(1_Rmatrix(3)).1 = <e1> & (1_Rmatrix(3)).2 = <e2> &
(1_Rmatrix(3)).3 = <e3> by MATRIXR2:77,MATRIXR2:78,EUCLID_8:def 1,
EUCLID_8:def 2,EUCLID_8:def 3;
theorem
Base_FinSeq(3,1) = <e1> & Base_FinSeq(3,2) = <e2> &
Base_FinSeq(3,3) = <e3> by MATRIXR2:77,EUCLID_8:def 1,EUCLID_8:def 2,
EUCLID_8:def 3;
theorem Th51:
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 *>
proof
let pr be FinSequence of D;
assume len pr = 3;
then
A2: Indices <*pr*> = [:Seg 1,Seg 3:] by MATRIX_0:23;
consider p be FinSequence of D such that
A3: p = <*pr*>.1 and
A4: (<*pr*>)*(1,1) = p.1 by A2,Th3,MATRIX_0:def 5;
A5: len Col(<*pr*>,1) = len <*pr*> by MATRIX_0:def 8;
A6: len <*pr*> = 1 by FINSEQ_1:39;
then
A7: dom <*pr*> = Seg 1 by FINSEQ_1:def 3;
then Col(<*pr*>,1).1 = <*pr*>*(1,1) by FINSEQ_1:1,MATRIX_0:def 8
.= pr.1 by A4,A3;
hence Col(<*pr*>,1) = <* pr.1 *> by A6,A5,FINSEQ_1:40;
consider p be FinSequence of D such that
A8: p = <*pr*>.1 and
A9: (<*pr*>)*(1,2) = p.2 by A2,Th3,MATRIX_0:def 5;
A10: len Col(<*pr*>,2) = len <*pr*> by MATRIX_0:def 8;
Col(<*pr*>,2).1 = <*pr*>*(1,2) by A7,FINSEQ_1:1,MATRIX_0:def 8
.= pr.2 by A9,A8;
hence Col(<*pr*>,2) = <* pr.2 *> by A6,A10,FINSEQ_1:40;
consider p be FinSequence of D such that
A11: p = <*pr*>.1 and
A12: (<*pr*>)*(1,3) = p.3 by A2,Th3,MATRIX_0:def 5;
A13: len Col(<*pr*>,3) = len <*pr*> by MATRIX_0:def 8;
Col(<*pr*>,3).1 = <*pr*>*(1,3) by A7,FINSEQ_1:1,MATRIX_0:def 8
.= pr.3 by A12,A11;
hence Col(<*pr*>,3) = <* pr.3 *> by A6,A13,FINSEQ_1:40;
end;
theorem Th52:
Col(<*<e1>*>,1) = <* 1 *> &
Col(<*<e1>*>,2) = <* 0 *> &
Col(<*<e1>*>,3) = <* 0 *>
proof
A1: len <e1> = 3 by CARD_1:def 7;
<e1>.1 = 1 & <e1>.2 = 0 & <e1>.3 = 0 by EUCLID_8:def 1;
hence thesis by A1,Th51;
end;
theorem Th53:
Col(<*<e2>*>,1) = <* 0 *> &
Col(<*<e2>*>,2) = <* 1 *> &
Col(<*<e2>*>,3) = <* 0 *>
proof
A1: len <e2> = 3 by CARD_1:def 7;
<e2>.1 = 0 & <e2>.2 = 1 & <e2>.3 = 0 by EUCLID_8:def 2;
hence thesis by A1,Th51;
end;
theorem Th54:
Col(<*<e3>*>,1) = <* 0 *> &
Col(<*<e3>*>,2) = <* 0 *> &
Col(<*<e3>*>,3) = <* 1 *>
proof
A1: len <e3> = 3 by CARD_1:def 7;
<e3>.1 = 0 & <e3>.2 = 0 & <e3>.3 = 1 by EUCLID_8:def 3;
hence thesis by A1,Th51;
end;
theorem Th55:
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 *>
proof
A1: 1.(F_Real,3) = MXF2MXR 1.(F_Real,3) by MATRIXR1:def 2
.= 1_Rmatrix(3) by MATRIXR2:def 2;
A2: [1,1] in Indices(1.(F_Real,3)) by Th1,MATRIX_0:24;
A3: 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1;
then 1 in dom 1_Rmatrix(3) by Th13; then
A4: Col(1_Rmatrix(3),1).1 = 1.(F_Real,3) *(1,1) by A1,MATRIX_0:def 8
.= 1.F_Real by A2,MATRIX_1:def 3
.= 1 by STRUCT_0:def 7;
A5: [2,1] in Indices(1.(F_Real,3)) by Th1,MATRIX_0:24;
2 in dom 1_Rmatrix(3) by A3,Th13; then
A6: Col(1_Rmatrix(3),1).2 = 1.(F_Real,3) *(2,1) by A1,MATRIX_0:def 8
.= 0.F_Real by A5,MATRIX_1:def 3
.= 0 by STRUCT_0:def 6;
A7: [3,1]in Indices(1.(F_Real,3)) by Th1,MATRIX_0:24;
3 in dom 1_Rmatrix(3) by A3,Th13; then
A8: Col(1_Rmatrix(3),1).3 = 1.(F_Real,3) *(3,1) by A1,MATRIX_0:def 8
.= 0.F_Real by A7,MATRIX_1:def 3
.= 0 by STRUCT_0:def 6;
len Col(1_Rmatrix(3),1) = len 1.(F_Real,3) by A1,MATRIX_0:def 8
.= 3 by MATRIX_0:24;
hence Col(1.(F_Real,3),1) = <* 1,0,0 *> by A1,A4,A6,A8,FINSEQ_1:45;
A9: [1,2] in Indices(1.(F_Real,3)) by Th1,MATRIX_0:24;
A10: 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1;
then 1 in dom 1_Rmatrix(3) by Th13; then
A11: Col(1_Rmatrix(3),2).1 = 1.(F_Real,3) *(1,2) by A1,MATRIX_0:def 8
.= 0.F_Real by A9,MATRIX_1:def 3
.= 0 by STRUCT_0:def 6;
A12: [2,2] in Indices(1.(F_Real,3)) by Th1,MATRIX_0:24;
2 in dom 1_Rmatrix(3) by A10,Th13; then
A13: Col(1_Rmatrix(3),2).2 = 1.(F_Real,3) *(2,2) by A1,MATRIX_0:def 8
.= 1.F_Real by A12,MATRIX_1:def 3
.= 1 by STRUCT_0:def 7;
A14: [3,2]in Indices(1.(F_Real,3)) by Th1,MATRIX_0:24;
3 in dom 1_Rmatrix(3) by A10,Th13; then
A15: Col(1_Rmatrix(3),2).3 = 1.(F_Real,3) *(3,2) by A1,MATRIX_0:def 8
.= 0.F_Real by A14,MATRIX_1:def 3
.= 0 by STRUCT_0:def 6;
len Col(1_Rmatrix(3),2) = len 1.(F_Real,3) by A1,MATRIX_0:def 8
.= 3 by MATRIX_0:24;
hence Col(1.(F_Real,3),2) = <* 0,1,0 *> by A1,A11,A13,A15,FINSEQ_1:45;
A16: [1,3] in Indices(1.(F_Real,3)) by Th1,MATRIX_0:24;
A17: 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1;
then 1 in dom 1_Rmatrix(3) by Th13; then
A18: Col(1_Rmatrix(3),3).1 = 1.(F_Real,3) *(1,3) by A1,MATRIX_0:def 8
.= 0.F_Real by A16,MATRIX_1:def 3
.= 0 by STRUCT_0:def 6;
A19: [2,3] in Indices(1.(F_Real,3)) by Th1,MATRIX_0:24;
2 in dom 1_Rmatrix(3) by A17,Th13; then
A20: Col(1_Rmatrix(3),3).2 = 1.(F_Real,3) *(2,3) by A1,MATRIX_0:def 8
.= 0.F_Real by A19,MATRIX_1:def 3
.= 0 by STRUCT_0:def 6;
A21: [3,3]in Indices(1.(F_Real,3)) by Th1,MATRIX_0:24;
3 in dom 1_Rmatrix(3) by A17,Th13; then
A22: Col(1_Rmatrix(3),3).3 = 1.(F_Real,3) *(3,3) by A1,MATRIX_0:def 8
.= 1.F_Real by A21,MATRIX_1:def 3
.= 1 by STRUCT_0:def 7;
len Col(1_Rmatrix(3),3) = len 1.(F_Real,3) by A1,MATRIX_0:def 8
.= 3 by MATRIX_0:24;
hence Col(1.(F_Real,3),3) = <* 0,0,1 *> by A1,A18,A20,A22,FINSEQ_1:45;
end;
theorem Th56:
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 *>
proof
now
thus len Line(1.(F_Real,3),1) = width 1.(F_Real,3) by MATRIX_0:def 7
.= 3 by MATRIX_0:23;
[1,1] in Indices(1.(F_Real,3)) by MATRIX_0:23,Th1;
then Line(1.(F_Real,3),1).1 = 1.F_Real by MATRIX_3:7
.= 1 by STRUCT_0:def 7;
hence Line(1.(F_Real,3),1).1 = 1;
[1,2] in Indices(1.(F_Real,3)) by MATRIX_0:23,Th1;
then Line(1.(F_Real,3),1).2 = 0.F_Real by MATRIX_3:8
.= 0 by STRUCT_0:def 6;
hence Line(1.(F_Real,3),1).2 = 0;
[1,3] in Indices(1.(F_Real,3)) by MATRIX_0:23,Th1;
then Line(1.(F_Real,3),1).3 = 0.F_Real by MATRIX_3:8
.= 0 by STRUCT_0:def 6;
hence Line(1.(F_Real,3),1).3 = 0;
end;
hence Line(1.(F_Real,3),1) = <* 1,0,0 *> by FINSEQ_1:45;
now
thus len Line(1.(F_Real,3),2) = width 1.(F_Real,3) by MATRIX_0:def 7
.= 3 by MATRIX_0:23;
[2,1] in Indices(1.(F_Real,3)) by MATRIX_0:23,Th1;
then Line(1.(F_Real,3),2).1 = 0.F_Real by MATRIX_3:8
.= 0 by STRUCT_0:def 6;
hence Line(1.(F_Real,3),2).1 = 0;
[2,2] in Indices(1.(F_Real,3)) by MATRIX_0:23,Th1;
then Line(1.(F_Real,3),2).2 = 1.F_Real by MATRIX_3:7
.= 1 by STRUCT_0:def 7;
hence Line(1.(F_Real,3),2).2 = 1;
[2,3] in Indices(1.(F_Real,3)) by MATRIX_0:23,Th1;
then Line(1.(F_Real,3),2).3 = 0.F_Real by MATRIX_3:8
.= 0 by STRUCT_0:def 6;
hence Line(1.(F_Real,3),2).3 = 0;
end;
hence Line(1.(F_Real,3),2) = <* 0,1,0 *> by FINSEQ_1:45;
now
thus len Line(1.(F_Real,3),3) = width 1.(F_Real,3) by MATRIX_0:def 7
.= 3 by MATRIX_0:23;
[3,1] in Indices(1.(F_Real,3)) by MATRIX_0:23,Th1;
then Line(1.(F_Real,3),3).1 = 0.F_Real by MATRIX_3:8
.= 0 by STRUCT_0:def 6;
hence Line(1.(F_Real,3),3).1 = 0;
[3,2] in Indices(1.(F_Real,3)) by MATRIX_0:23,Th1;
then Line(1.(F_Real,3),3).2 = 0.F_Real by MATRIX_3:8
.= 0 by STRUCT_0:def 6;
hence Line(1.(F_Real,3),3).2 = 0;
[3,3] in Indices(1.(F_Real,3)) by MATRIX_0:23,Th1;
then Line(1.(F_Real,3),3).3 = 1.F_Real by MATRIX_3:7
.= 1 by STRUCT_0:def 7;
hence Line(1.(F_Real,3),3).3 = 1;
end;
hence Line(1.(F_Real,3),3) = <* 0,0,1 *> by FINSEQ_1:45;
end;
theorem Th57:
<*<e1>*>@ = <* <* 1 *>, <* 0 *> , <* 0 *> *> &
<*<e2>*>@ = <* <* 0 *>, <* 1 *> , <* 0 *> *> &
<*<e3>*>@ = <* <* 0 *>, <* 0 *> , <* 1 *> *>
proof
<e1> in REAL 3; then
A1: <e1> in 3-tuples_on REAL by EUCLID:def 1;
A2: len <*<e1>*> = 1 by FINSEQ_1:39;
rng <*<e1>*> = {<e1>} by FINSEQ_1:39;
then <e1> in rng <*<e1>*> by TARSKI:def 1; then
A4: width <*<e1>*> = len <e1> by A2,MATRIX_0:def 3
.= 3 by A1,FINSEQ_2:133;
A5: width (<*<e1>*>@) = len <*<e1>*> by A4,MATRIX_0:29
.= 1 by FINSEQ_1:39;
now
thus len (<*<e1>*>@) = 3 by MATRIX_0:def 6,A4; then
A7: <*<e1>*>@ is Matrix of 3,1,F_Real by A5,MATRIX_0:20;
A8: 1 in Seg 3 by FINSEQ_1:1;
hence <*<e1>*>@.1 = Line (<*<e1>*>@,1) by A7,MATRIX_0:52
.= <* 1 *> by A8,A4,MATRIX_0:59,Th52;
A9: 2 in Seg 3 by FINSEQ_1:1;
hence <*<e1>*>@.2 = Line (<*<e1>*>@,2) by A7,MATRIX_0:52
.= <* 0 *> by A9,A4,MATRIX_0:59,Th52;
A10: 3 in Seg 3 by FINSEQ_1:1;
hence <*<e1>*>@.3 = Line (<*<e1>*>@,3) by A7,MATRIX_0:52
.= <* 0 *> by A10,A4,MATRIX_0:59,Th52;
end;
hence <*<e1>*>@ = <* <* 1 *>, <* 0 *> , <* 0 *> *> by FINSEQ_1:45;
<e2> in REAL 3; then
A11: <e2> in 3-tuples_on REAL by EUCLID:def 1;
A12: len <*<e2>*> = 1 by FINSEQ_1:39;
rng <*<e2>*> = {<e2>} by FINSEQ_1:39;
then <e2> in rng <*<e2>*> by TARSKI:def 1; then
A13bis: width <*<e2>*> = len <e2> by A12,MATRIX_0:def 3
.= 3 by A11,FINSEQ_2:133; then
A14: width (<*<e2>*>@) = len <*<e2>*> by MATRIX_0:29
.= 1 by FINSEQ_1:39;
now
thus len (<*<e2>*>@) = 3 by MATRIX_0:def 6,A13bis; then
A16: <*<e2>*>@ is Matrix of 3,1,F_Real by A14,MATRIX_0:20;
A17: 1 in Seg 3 by FINSEQ_1:1;
hence <*<e2>*>@.1 = Line (<*<e2>*>@,1) by A16,MATRIX_0:52
.= <* 0 *> by A17,A13bis,MATRIX_0:59,Th53;
A18: 2 in Seg 3 by FINSEQ_1:1;
hence <*<e2>*>@.2 = Line (<*<e2>*>@,2) by A16,MATRIX_0:52
.= <* 1 *> by A18,A13bis,MATRIX_0:59,Th53;
A19: 3 in Seg 3 by FINSEQ_1:1;
hence <*<e2>*>@.3 = Line (<*<e2>*>@,3) by A16,MATRIX_0:52
.= <* 0 *> by A19,A13bis,MATRIX_0:59,Th53;
end;
hence <*<e2>*>@ = <* <* 0 *>, <* 1 *> , <* 0 *> *> by FINSEQ_1:45;
<e3> in REAL 3; then
A20: <e3> in 3-tuples_on REAL by EUCLID:def 1;
A21: len <*<e3>*> = 1 by FINSEQ_1:39;
rng <*<e3>*> = {<e3>} by FINSEQ_1:39;
then <e3> in rng <*<e3>*> by TARSKI:def 1; then
A23: width <*<e3>*> = len <e3> by A21,MATRIX_0:def 3
.= 3 by A20,FINSEQ_2:133;
A24: width (<*<e3>*>@) = len <*<e3>*> by A23,MATRIX_0:29
.= 1 by FINSEQ_1:39;
now
thus
A25: len (<*<e3>*>@) = 3 by MATRIX_0:def 6,A23;
A26: <*<e3>*>@ is Matrix of 3,1,F_Real by A25,A24,MATRIX_0:20;
A27: 1 in Seg 3 by FINSEQ_1:1;
hence <*<e3>*>@.1 = Line (<*<e3>*>@,1) by A26,MATRIX_0:52
.= <* 0 *> by A27,A23,MATRIX_0:59,Th54;
A28: 2 in Seg 3 by FINSEQ_1:1;
hence <*<e3>*>@.2 = Line (<*<e3>*>@,2) by A26,MATRIX_0:52
.= <* 0 *> by A28,A23,MATRIX_0:59,Th54;
A29: 3 in Seg 3 by FINSEQ_1:1;
hence <*<e3>*>@.3 = Line (<*<e3>*>@,3) by A26,MATRIX_0:52
.= <* 1 *> by A29,A23,MATRIX_0:59,Th54;
end;
hence <*<e3>*>@ = <* <* 0 *>, <* 0 *> , <* 1 *> *> by FINSEQ_1:45;
end;
reserve pf for FinSequence of D;
theorem Th58:
for pf being FinSequence of D holds
k in dom pf implies <*pf*>*(1,k) = pf.k
proof
let pf be FinSequence of D;
assume
A1: k in dom pf;
A2: Indices <*pf*> = [:Seg 1,Seg len pf:] by MATRIX_0:23
.= [:{1}, dom pf:] by FINSEQ_1:2,FINSEQ_1:def 3;
1 in {1} by TARSKI:def 1;
then [1,k] in Indices <*pf*> by A1,A2,ZFMISC_1:87;
then ex q be FinSequence of D st q = <*pf*>.1 &
<*pf*>*(1,k) = q.k by MATRIX_0:def 5;
hence thesis;
end;
theorem Th59:
k in dom pf implies Col(<*pf*>,k) = <*pf.k*>
proof
assume
A1: k in dom pf;
A2: len Col(<*pf*>,k) = len <*pf*> & for j be Nat st j in dom <*pf*> holds
Col(<*pf*>,k).j = <*pf*>*(j,k) by MATRIX_0:def 8; then
A3: len Col(<*pf*>,k) = 1 by FINSEQ_1:39; then
A4: dom Col(<*pf*>,k) = {1} by FINSEQ_1:def 3,FINSEQ_1:2;
(Col(<*pf*>,k)).1 = <*pf*>*(1,k) by FINSEQ_5:6,A2;
then rng Col(<*pf*>,k) = {<*pf*>*(1,k)} by A4,FUNCT_1:4;
then rng Col(<*pf*>,k) = {pf.k} by A1,Th58;
hence thesis by A3,FINSEQ_1:39;
end;
theorem
for pr being Element of REAL 3 st
pf = pr holds MXR2MXF ColVec2Mx pr = <*pf*>@
proof
let pr being Element of REAL 3;
assume
A1: pf = pr;
set M1 = MXR2MXF ColVec2Mx pr, M2 = ColVec2Mx pr;
A2: M1 = ColVec2Mx pr by MATRIXR1:def 1;
pr in REAL 3; then
A3: pr in 3-tuples_on REAL by EUCLID:def 1; then
A4: len pr = 3 by FINSEQ_2:133;
A5: len M2 = len pr & width M2 = 1 & for j be Nat st j in dom pr holds
M2.j = <*pr.j*> by A4,MATRIXR1:def 9;
now
A6: width <*pf*> = len pr by A1,MATRIX_0:23;
hence len M2 = len (<*pf*>@) by A5,MATRIX_0:def 6;
thus for k be Nat st 1 <= k & k <= len M2 holds M2.k = (<*pf*>@).k
proof
let k be Nat;
assume that
A7: 1 <= k and
A8: k <= len M2;
A9: k in Seg len pr by A5,A7,A8,FINSEQ_1:1; then
A10: k in dom pr by FINSEQ_1:def 3;
A11: len <*pf*> = 1 by MATRIX_0:23;
A12: width <*pf*> = 3 by A6,A3,FINSEQ_2:133;
Seg len (<*pf*>@) = Seg len pr by A6,MATRIX_0:def 6;
then dom (<*pf*>@) = Seg len pr by FINSEQ_1:def 3
.= dom pr
by FINSEQ_1:def 3; then
A13: k in dom (<*pf*>@) by A9,FINSEQ_1:def 3; then
A14: (<*pf*>@).k = Line(<*pf*>@,k) by MATRIX_0:60
.= Col(<*pf*>@@,k) by A13,MATRIX_0:58
.= Col(<*pf*>,k) by A12,A11,MATRIX_0:57
.= <*pf.k*> by A10,A1,Th59;
k in dom pr by A9,FINSEQ_1:def 3;
hence thesis by A4,MATRIXR1:def 9,A1,A14;
end;
end;
hence thesis by A2,FINSEQ_1:def 18;
end;
reserve PQR for Matrix of 3,F_Real;
theorem Th60:
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
proof
assume
A1: PQR = <*<*p`1,p`2,p`3*>,<*q`1,q`2,q`3*>,<*r`1,r`2,r`3*>*>;
1 in Seg 3 by FINSEQ_1:1;
hence Line(PQR,1) = PQR.1 by MATRIX_0:52
.= <*p`1,p`2,p`3*> by A1
.= p by EUCLID_5:3;
2 in Seg 3 by FINSEQ_1:1;
hence Line(PQR,2) = PQR.2 by MATRIX_0:52
.= <*q`1,q`2,q`3*> by A1
.= q by EUCLID_5:3;
3 in Seg 3 by FINSEQ_1:1;
hence Line(PQR,3) = PQR.3 by MATRIX_0:52
.= <*r`1,r`2,r`3*> by A1
.= r by EUCLID_5:3;
end;
theorem
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*>
proof
assume
A1: PQR = <*<*p`1,p`2,p`3*>,<*q`1,q`2,q`3*>,<*r`1,r`2,r`3*>*>;
len PQR = 3 by MATRIX_0:24; then
A2: dom PQR = Seg 3 by FINSEQ_1:def 3;
A3: PQR = <* <* PQR*(1,1), PQR*(1,2), PQR*(1,3) *>,
<* PQR*(2,1), PQR*(2,2), PQR*(2,3) *>,
<* PQR*(3,1), PQR*(3,2), PQR*(3,3) *> *> by MATRIXR2:37;
then PQR.1 = <* PQR*(1,1), PQR*(1,2), PQR*(1,3) *>; then
A4: <* PQR*(1,1), PQR*(1,2), PQR*(1,3) *> = <*p`1,p`2,p`3*> by A1;
PQR.2 = <* PQR*(2,1), PQR*(2,2), PQR*(2,3) *> by A3; then
A5: <* PQR*(2,1), PQR*(2,2), PQR*(2,3) *> = <*q`1,q`2,q`3*>
by A1;
PQR.3 = <* PQR*(3,1), PQR*(3,2), PQR*(3,3) *> by A3; then
A6: <* PQR*(3,1), PQR*(3,2), PQR*(3,3) *> = <*r`1,r`2,r`3*>
by A1;
now
thus len Col(PQR,1) = len PQR by MATRIX_0:def 8
.= 3 by MATRIX_0:24;
thus len Col(PQR,2) = len PQR by MATRIX_0:def 8
.= 3 by MATRIX_0:24;
thus len Col(PQR,3) = len PQR by MATRIX_0:def 8
.= 3 by MATRIX_0:24;
thus Col(PQR,1).1 = PQR*(1,1) by A2,MATRIX_0:def 8,FINSEQ_1:1
.= p`1 by A4,FINSEQ_1:78;
thus Col(PQR,1).2 = PQR*(2,1) by A2,MATRIX_0:def 8,FINSEQ_1:1
.= q`1 by A5,FINSEQ_1:78;
thus Col(PQR,1).3 = PQR*(3,1) by A2,MATRIX_0:def 8,FINSEQ_1:1
.= r`1 by A6,FINSEQ_1:78;
thus Col(PQR,2).1 = PQR*(1,2) by A2,MATRIX_0:def 8,FINSEQ_1:1
.= p`2 by A4,FINSEQ_1:78;
thus Col(PQR,2).2 = PQR*(2,2) by A2,MATRIX_0:def 8,FINSEQ_1:1
.= q`2 by A5,FINSEQ_1:78;
thus Col(PQR,2).3 = PQR*(3,2) by A2,MATRIX_0:def 8,FINSEQ_1:1
.= r`2 by A6,FINSEQ_1:78;
thus Col(PQR,3).1 = PQR*(1,3) by A2,MATRIX_0:def 8,FINSEQ_1:1
.= p`3 by A4,FINSEQ_1:78;
thus Col(PQR,3).2 = PQR*(2,3) by A2,MATRIX_0:def 8,FINSEQ_1:1
.= q`3 by A5,FINSEQ_1:78;
thus Col(PQR,3).3 = PQR*(3,3) by A2,MATRIX_0:def 8,FINSEQ_1:1
.= r`3 by A6,FINSEQ_1:78;
end;
hence thesis by FINSEQ_1:45;
end;
theorem Th61:
width <*pf*> = len pf
proof
A1: len <*pf*> = 1 by FINSEQ_1:39;
rng <*pf*> = {pf} by FINSEQ_1:39;
then pf in rng <*pf*> by TARSKI:def 1;
hence thesis by A1,MATRIX_0:def 3;
end;
theorem Th62:
len pf = 3 implies Line(<*pf*>@,1) = <* pf.1 *> &
Line(<*pf*>@,2) = <* pf.2 *> & Line(<*pf*>@,3) = <* pf.3 *>
proof
assume
A1: len pf = 3;
A3: width <*pf*> = 3 by A1,Th61;
1 in Seg width <*pf*> by A3,FINSEQ_1:1;
hence Line(<*pf*>@,1) = Col(<*pf*>,1) by MATRIX_0:59
.= <* pf.1 *> by A1,Th51;
2 in Seg width <*pf*> by A3,FINSEQ_1:1;
hence Line(<*pf*>@,2) = Col(<*pf*>,2) by MATRIX_0:59
.= <* pf.2 *> by A1,Th51;
3 in Seg width <*pf*> by A3,FINSEQ_1:1;
hence Line(<*pf*>@,3) = Col(<*pf*>,3) by MATRIX_0:59
.= <* pf.3 *> by A1,Th51;
end;
theorem Th63:
len pf = 3 implies <*pf*>@ = <* <* pf.1 *>, <* pf.2 *>, <* pf.3 *> *>
proof
assume
A1: len pf = 3;
A2: len <*pf*> = 1 by FINSEQ_1:39;
rng <*pf*> = {pf} by FINSEQ_1:39;
then pf in rng <*pf*> by TARSKI:def 1; then
A3: width <*pf*> = 3 by A1,A2,MATRIX_0:def 3; then
A4: width (<*pf*>@) = len <*pf*> by MATRIX_0:29
.= 1 by FINSEQ_1:39;
now
thus len (<*pf*>@) = 3 by MATRIX_0:def 6,A3; then
A5: <*pf*>@ is Matrix of 3,1,D by A4,MATRIX_0:20;
1 in Seg 3 by FINSEQ_1:1;
hence <*pf*>@.1 = Line (<*pf*>@,1) by A5,MATRIX_0:52
.= <* pf.1 *> by A1,Th62;
2 in Seg 3 by FINSEQ_1:1;
hence <*pf*>@.2 = Line (<*pf*>@,2) by A5,MATRIX_0:52
.= <* pf.2 *> by A1,Th62;
3 in Seg 3 by FINSEQ_1:1;
hence <*pf*>@.3 = Line (<*pf*>@,3) by A5,MATRIX_0:52
.= <* pf.3 *> by A1,Th62;
end;
hence <*pf*>@ = <* <* pf.1 *>, <* pf.2 *>, <* pf.3 *> *> by FINSEQ_1:45;
end;
definition
let D;
let p be FinSequence of D;
assume
A1: len p = 3;
func F2M p -> FinSequence of 1-tuples_on D equals
:DEF1:
<* <*p.1*>, <*p.2*> , <*p.3*> *>;
coherence
proof
A0: rng p c= D by FINSEQ_1:def 4;
A2: <*p.1*> in 1-tuples_on D & <*p.2*> in 1-tuples_on D &
<*p.3*> in 1-tuples_on D
proof
A3: dom p = Seg 3 by A1,FINSEQ_1:def 3;
then p.1 in rng p by FUNCT_1:3,FINSEQ_1:1;
hence <*p.1*> in 1-tuples_on D by A0,FINSEQ_2:98;
p.2 in rng p by A3,FINSEQ_1:1,FUNCT_1:3;
hence <*p.2*> in 1-tuples_on D by A0,FINSEQ_2:98;
p.3 in rng p by A3,FINSEQ_1:1,FUNCT_1:3;
hence <*p.3*> in 1-tuples_on D by A0,FINSEQ_2:98;
end;
A4: rng ( <* <*p.1*>, <*p.2*>, <*p.3*> *> )
= { <* p.1 *>, <* p.2 *>, <* p.3 *> } by FINSEQ_2:128;
{ <*p.1*>,<*p.2*>,<*p.3*> } c= 1-tuples_on D by A2,ENUMSET1:def 1;
hence thesis by A4,FINSEQ_1:def 4;
end;
end;
theorem Th64:
for p being FinSequence of REAL st len p = 3 holds len F2M p = 3
proof
let p being FinSequence of REAL;
assume len p = 3;
then F2M p = <* <*p.1*>, <*p.2*>, <*p.3*> *> by DEF1;
hence thesis by FINSEQ_1:45;
end;
theorem
for p being FinSequence of REAL st len p = 3 holds
p is 3-element FinSequence of REAL
proof
let p being FinSequence of REAL;
assume len p = 3;
then p = <* p.1,p.2,p.3 *> by FINSEQ_1:45;
hence thesis;
end;
theorem Th65:
for p being FinSequence of REAL st p = |[0,0,0]| holds
F2M p = <* <* 0 *>, <* 0 *>, <* 0 *> *>
proof
let p being FinSequence of REAL;
assume p = |[0,0,0]|;
then len p = 3 & p.1 = 0 & p.2 = 0 & p.3 = 0 by FINSEQ_1:45;
hence thesis by DEF1;
end;
theorem
len pf = 3 implies
<* Col(<*pf*>,1), Col(<*pf*>,2), Col(<*pf*>,3) *> = F2M pf
proof
assume
A0: len pf = 3;
then Col(<*pf*>,1) = <* pf.1 *> & Col(<*pf*>,2) = <* pf.2 *> &
Col(<*pf*>,3) = <* pf.3 *> by Th51;
hence thesis by A0,DEF1;
end;
definition
let D;
let p be FinSequence of 1-tuples_on D;
assume
A1: len p = 3;
func M2F p -> FinSequence of D equals :DEF2:
<* (p.1).1, (p.2).1, (p.3).1 *>;
coherence
proof
rng <* (p.1).1, (p.2).1, (p.3).1 *> c= D
proof
let x be object;
assume x in rng <* (p.1).1, (p.2).1, (p.3).1 *>;
then x in { (p.1).1, (p.2).1, (p.3).1 } by FINSEQ_2:128; then
A2: x = (p.1).1 or x = (p.2).1 or x = (p.3).1 by ENUMSET1:def 1;
A3: dom p = Seg 3 by A1,FINSEQ_1:def 3; then
A4: p.1 in rng p by FINSEQ_1:1,FUNCT_1:3;
A5: rng p c= 1-tuples_on D by FINSEQ_1:def 4;
A0: 1-tuples_on D = the set of all <*d*> where d is Element of D
by FINSEQ_2:96;
then p.1 in the set of all <*d*> where d is Element of D by A4,A5;
then consider d be Element of D such that
A6: p.1 = <*d*>;
A7: (p.1).1 = d by A6;
p.2 in rng p by A3,FINSEQ_1:1,FUNCT_1:3;
then p.2 in the set of all <*d*> where d is Element of D by A0,A5;
then consider d be Element of D such that
A10: p.2 = <*d*>;
A11: (p.2).1 = d by A10;
A12: p.3 in rng p by A3,FINSEQ_1:1,FUNCT_1:3;
p.3 in 1-tuples_on D by A5,A12;
then consider d be Element of D such that
A14: p.3 = <*d*> by A0;
(p.3).1 = d by A14;
hence thesis by A2,A7,A11;
end;
hence thesis by FINSEQ_1:def 4;
end;
end;
theorem Th66:
for p being FinSequence of 1-tuples_on REAL st len p = 3 holds
M2F p is Point of TOP-REAL 3
proof
let p being FinSequence of 1-tuples_on REAL;
assume
A1: len p = 3;
A2: dom p = Seg 3 by A1,FINSEQ_1:def 3; then
A3: p.1 in rng p by FINSEQ_1:1,FUNCT_1:3;
A4: rng p c= 1-tuples_on REAL by FINSEQ_1:def 4;
1-tuples_on REAL = the set of all <*d*> where d is Element of REAL
by FINSEQ_2:96;
then p.1 in the set of all <*d*> where d is Element of REAL by A3,A4;
then consider d be Element of REAL such that
A5: p.1 = <*d*>;
A6: (p.1).1 = d by A5;
A7: p.2 in rng p by A2,FINSEQ_1:1,FUNCT_1:3;
1-tuples_on REAL = the set of all <*d*> where d is Element of REAL
by FINSEQ_2:96;
then p.2 in the set of all <*d*> where d is Element of REAL by A7,A4;
then consider d be Element of REAL such that
A9: p.2 = <*d*>;
A10: (p.2).1 = d by A9;
A11: p.3 in rng p by A2,FINSEQ_1:1,FUNCT_1:3;
rng p c= 1-tuples_on REAL by FINSEQ_1:def 4; then
A12: p.3 in 1-tuples_on REAL by A11;
1-tuples_on REAL = the set of all <*d*> where d is Element of REAL
by FINSEQ_2:96;
then consider d be Element of REAL such that
A13: p.3 = <*d*> by A12;
A14: (p.3).1 = d by A13;
M2F p = <* (p.1).1, (p.2).1, (p.3).1 *> by A1,DEF2;
then M2F p in 3-tuples_on REAL by A6,A10,A14,FINSEQ_2:104;
then M2F p in REAL 3 by EUCLID:def 1;
hence thesis by EUCLID:22;
end;
definition
let p be FinSequence of 1-tuples_on REAL;
let a be Real;
assume
A1: len p = 3;
func a * p -> FinSequence of 1-tuples_on REAL means
:DEF3:
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 *> *>;
existence
proof
dom p = Seg 3 by A1,FINSEQ_1:def 3; then
A2: p.1 in rng p & p.2 in rng p & p.3 in rng p by FINSEQ_1:1,FUNCT_1:3;
A3: rng p c= 1-tuples_on REAL by FINSEQ_1:def 4;
A4: 1-tuples_on REAL = the set of all <*d*> where d is Element of REAL
by FINSEQ_2:96;
then p.1 in the set of all <*d*> where d is Element of REAL by A2,A3;
then consider d1 be Element of REAL such that
A5: p.1 = <*d1*>;
reconsider p1 = d1 as Real;
p.2 in the set of all <*d*> where d is Element of REAL by A2,A3,A4;
then consider d2 be Element of REAL such that
A6: p.2 = <*d2*>;
reconsider p2 = d2 as Real;
p.3 in the set of all <*d*> where d is Element of REAL by A4,A2,A3;
then consider d3 be Element of REAL such that
A7: p.3 = <*d3*>;
reconsider p3 = d3 as Real;
now
take p1,p2,p3;
thus p1 = (p.1).1 & p2 = (p.2).1 & p3 = (p.3).1
by A5,A6,A7;
A8: <*a * p1*> in 1-tuples_on REAL & <*a * p2*> in 1-tuples_on REAL &
<*a * p3*> in 1-tuples_on REAL
proof
a * p1 in REAL by XREAL_0:def 1;
hence <* (a * p1) *> in 1-tuples_on REAL by FINSEQ_2:98;
a * p2 in REAL by XREAL_0:def 1;
hence <* (a * p2) *> in 1-tuples_on REAL by FINSEQ_2:98;
a * p3 in REAL by XREAL_0:def 1;
hence <* (a * p3) *> in 1-tuples_on REAL by FINSEQ_2:98;
end;
A9: rng ( <* <*a * p1*>, <* a * p2*> , <*a * p3*> *> )
= { <* a * p1 *>, <* a * p2 *>, <* a * p3 *> } by FINSEQ_2:128;
{ <*a * p1*>,<*a * p2*>,<*a * p3*> } c= 1-tuples_on REAL
by A8,ENUMSET1:def 1;
hence <* <* a * p1 *>, <* a * p2 *> , <* a * p3 *> *> is
FinSequence of 1-tuples_on REAL by A9,FINSEQ_1:def 4;
end;
hence thesis;
end;
uniqueness;
end;
theorem Th67:
for p being FinSequence of 1-tuples_on REAL st
len p = 3 holds M2F (a * p) = a * (M2F p)
proof
let p be FinSequence of 1-tuples_on REAL;
assume
A1: len p = 3;
then consider p1,p2,p3 be Real such that
A2: p1 = (p.1).1 & p2 = (p.2).1 & p3 = (p.3).1 and
A3: a * p = <* <* a * p1 *>, <* a * p2 *> , <* a * p3 *> *> by DEF3;
(a * p).1 = <* a * p1 *> & (a * p).2 = <* a * p2 *> &
(a * p).3 = <* a * p3 *> by A3; then
A4: ((a * p).1).1 = a * p1 & ((a * p).2).1 = a * p2 &
((a * p).3).1 = a * p3;
len (a * p) = 3 by A3,FINSEQ_1:45; then
A5: M2F (a * p) = |[ a * p1, a * p2, a * p3 ]| by A4,DEF2;
reconsider q = M2F p as FinSequence of F_Real;
M2F p = |[ p1,p2,p3 ]| by A1,A2,DEF2;
hence thesis by A5,EUCLID_8:59;
end;
theorem Th68:
for p being FinSequence of 1-tuples_on REAL st len p = 3 holds
<* <*(p.1).1*>, <*(p.2).1*> , <*(p.3).1*> *> = p
proof
let p be FinSequence of 1-tuples_on REAL;
assume
A1: len p = 3;
then dom p = Seg 3 by FINSEQ_1:def 3; then
A2: p.1 in rng p & p.2 in rng p & p.3 in rng p by FINSEQ_1:1,FUNCT_1:3;
A3: rng p c= 1-tuples_on REAL by FINSEQ_1:def 4;
A4: 1-tuples_on REAL = the set of all <*d*> where d is Element of REAL
by FINSEQ_2:96;
then p.1 in the set of all <*d*> where d is Element of REAL by A2,A3;
then consider d1 be Element of REAL such that
A5: p.1 = <*d1*>;
p.2 in the set of all <*d*> where d is Element of REAL by A2,A3,A4;
then consider d2 be Element of REAL such that
A7: p.2 = <*d2*>;
p.3 in the set of all <*d*> where d is Element of REAL by A2,A3,A4;
then consider d3 be Element of REAL such that
A9: p.3 = <*d3*>;
thus thesis by A5,A7,A9,A1,FINSEQ_1:45;
end;
theorem Th69:
for p being FinSequence of 1-tuples_on REAL st len p = 3 holds
F2M M2F p = p
proof
let p be FinSequence of 1-tuples_on REAL;
assume
A1: len p = 3;
set q = M2F p;
q = <* (p.1).1, (p.2).1, (p.3).1 *> by A1,DEF2;
then len q = 3 & q.1 = (p.1).1 & q.2 = (p.2).1 &
q.3 = (p.3).1 by FINSEQ_1:45;
then F2M q = <* <*(p.1).1*>, <*(p.2).1*> , <*(p.3).1*> *> by DEF1;
hence thesis by A1,Th68;
end;
theorem Th70:
for p being FinSequence of REAL st len p = 3 holds M2F F2M p = p
proof
let p be FinSequence of REAL;
assume
A1: len p = 3;
set q = F2M p;
q = <* <*p.1*>, <*p.2*> , <*p.3*> *> by A1,DEF1; then
A2: len q = 3 & q.1 = <*p.1*> & q.2 = <*p.2*> & q.3 = <*p.3*> by FINSEQ_1:45;
then (q.1).1 = p.1 & (q.2).1 = p.2 & (q.3).1 = p.3; then
M2F q = <*p.1,p.2,p.3*> by A2,DEF2
.= p by A1,FINSEQ_1:45;
hence thesis;
end;
theorem
<*<e1>*>@ = F2M <e1> & <*<e2>*>@ = F2M <e2> & <*<e3>*>@ = F2M <e3>
proof
len <e1> = 3 & <e1>.1 = 1 & <e1>.2 = 0 & <e1>.3 = 0
by EUCLID_8:def 1,FINSEQ_1:45;
hence <*<e1>*>@ = F2M <e1> by DEF1,Th57;
len <e2> = 3 & <e2>.1 = 0 & <e2>.2 = 1 & <e2>.3 = 0
by EUCLID_8:def 2,FINSEQ_1:45;
hence <*<e2>*>@ = F2M <e2> by DEF1,Th57;
len <e3> = 3 & <e3>.1 = 0 & <e3>.2 = 0 & <e3>.3 = 1
by EUCLID_8:def 3,FINSEQ_1:45;
hence <*<e3>*>@ = F2M <e3> by DEF1,Th57;
end;
theorem
for p being FinSequence of D st len p = 3 holds
<*p*>@ = F2M p
proof
let p be FinSequence of D;
assume
A1: len p = 3;
then <*p*>@ = <* <* p.1 *>, <* p.2 *> , <* p.3 *> *> by Th63;
hence thesis by A1,DEF1;
end;
theorem Th72:
Line(<*pf*>,1) = pf
proof
1 in Seg 1 by FINSEQ_1:1;
then Line(<*pf*>,1) = ( <*pf*> ).1 by MATRIX_0:52;
hence thesis;
end;
theorem Th73:
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) *>
proof
let M be Matrix of 3,1,D;
A1: len M = 3 & width M = 1 & Indices M = [:Seg 3,Seg 1:] by MATRIX_0:23;
now
A2: len Line(M,1) = width M by MATRIX_0:def 7
.= 1 by MATRIX_0:23;
dom <* M*(1,1) *> = Seg 1 by FINSEQ_1:def 8;
hence dom Line(M,1) = dom <* M*(1,1) *> by A2,FINSEQ_1:def 3;
thus for x be object st x in dom Line(M,1) holds
(Line(M,1)).x = ( <* M*(1,1) *>).x
proof
let x be object;
assume x in dom Line(M,1);
then x in {1} by A2,FINSEQ_1:def 3,FINSEQ_1:2; then
A3: x = 1 by TARSKI:def 1;
(Line(M,1)).1 = M*(1,1) by A1,FINSEQ_1:1,MATRIX_0:def 7
.= ( <* M*(1,1) *>).1;
hence thesis by A3;
end;
end;
hence Line(M,1) = <* M*(1,1) *> by FUNCT_1:def 11;
now
A4: len Line(M,2) = width M by MATRIX_0:def 7
.= 1 by MATRIX_0:23;
dom <* M*(2,1) *> = Seg 1 by FINSEQ_1:def 8;
hence dom Line(M,2) = dom <* M*(2,1) *> by A4,FINSEQ_1:def 3;
thus for x be object st x in dom Line(M,2) holds
(Line(M,2)).x = ( <* M*(2,1) *>).x
proof
let x be object;
assume x in dom Line(M,2);
then x in {1} by A4,FINSEQ_1:def 3,FINSEQ_1:2; then
A5: x = 1 by TARSKI:def 1;
(Line(M,2)).1 = M*(2,1) by A1,FINSEQ_1:1,MATRIX_0:def 7
.= ( <* M*(2,1) *>).1;
hence thesis by A5;
end;
end;
hence Line(M,2) = <* M*(2,1) *> by FUNCT_1:def 11;
now
A6: len Line(M,3) = width M by MATRIX_0:def 7
.= 1 by MATRIX_0:23;
dom <* M*(3,1) *> = Seg 1 by FINSEQ_1:def 8;
hence dom Line(M,3) = dom <* M*(3,1) *> by A6,FINSEQ_1:def 3;
thus for x be object st x in dom Line(M,3) holds
(Line(M,3)).x = ( <* M*(3,1) *>).x
proof
let x be object;
assume x in dom Line(M,3);
then x in {1} by A6,FINSEQ_1:def 3,FINSEQ_1:2; then
A7: x = 1 by TARSKI:def 1;
(Line(M,3)).1 = M*(3,1) by A1,FINSEQ_1:1,MATRIX_0:def 7
.= ( <* M*(3,1) *>).1;
hence thesis by A7;
end;
end;
hence Line(M,3) = <* M*(3,1) *> by FUNCT_1:def 11;
end;
reserve R for Ring;
theorem Th74:
for N being Matrix of 3,R
for p being FinSequence of R st len p = 3 holds
N * (<*p*>@) is (3,1)-size
proof
let N be Matrix of 3,R;
let p be FinSequence of R;
assume
A1: len p = 3;
then
A2: width <*p*> = 3 by MATRIX_0:23; then
A3: width N = width (<*p*>) by MATRIX_0:24
.= len (<*p*>@) by MATRIX_0:def 6;
now
len (N * (<*p*>@)) = len N by A3,MATRIX_3:def 4;
hence
A4: len (N * <*p*>@) = 3 by MATRIX_0:24;
thus for pf be FinSequence of R st pf in rng (N * <*p*>@) holds
len pf = 1
proof
let pf be FinSequence of R;
assume
A5: pf in rng (N * <*p*>@);
A6: len <*p*> = 1 by MATRIX_0:23;
A7: width <*p*> = 3 by A1,MATRIX_0:23;
A8: width N = width (<*p*>) by A2,MATRIX_0:24
.= len (<*p*>@) by MATRIX_0:def 6;
A9: width (<*p*>@) = len (<*p*>@@) by MATRIX_0:def 6
.= 1 by A6,A7,MATRIX_0:57;
consider s be FinSequence such that
A10: s in rng(N * (<*p*>@)) and
A11: len s = width(N * (<*p*>@)) by A4,MATRIX_0:def 3;
consider n0 be Nat such that
A12: for x be object st x in rng (N * (<*p*>@)) ex s be FinSequence st
s = x & len s = n0 by MATRIX_0:def 1;
A13: ex s0 be FinSequence st s0 = pf & len s0 = n0 by A12,A5;
ex s1 be FinSequence st s1 = s & len s1 = n0 by A10,A12;
hence thesis by A9,A8,MATRIX_3:def 4,A11,A13;
end;
end;
hence thesis by MATRIX_0:def 2;
end;
theorem Th75:
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) *>
proof
let pf be FinSequence of R;
let N be Matrix of 3,R;
assume len pf = 3;
then N * (<*pf*>@) is Matrix of 3,1,R by Th74;
hence thesis by Th73;
end;
theorem Th76:
Col(<*pf*>@,1) = pf
proof
len <*pf*> = 1 by FINSEQ_1:39;
then
dom <*pf*> = Seg 1 by FINSEQ_1:def 3;
then Col(<*pf*>@,1) = Line(<*pf*>,1) by FINSEQ_1:1,MATRIX_0:58;
hence thesis by Th72;
end;
theorem
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 <e1> & M * qf = F2M <e2> & M * rf = F2M <e3>
proof
let pf,qf,rf be FinSequence of F_Real;
assume that
A1: p = pf and
A2: q = qf and
A3: r = rf and
A4: |{p,q,r}| <> 0;
reconsider pr = p,qr = q,rr = r as Element of REAL 3 by EUCLID:22;
reconsider PQR = <*<*p`1,p`2,p`3*>,<*q`1,q`2,q`3*>,<*r`1,r`2,r`3*>*>
as Matrix of 3,F_Real by Th16;
len PQR = 3 by MATRIX_0:24;
then
A5: dom PQR = Seg 3 by FINSEQ_1:def 3;
then
A6: Col(PQR@,1) = Line(PQR,1) by FINSEQ_1:1,MATRIX_0:58
.= p by Th60;
A7: Col(PQR@,2) = Line(PQR,2) by A5,FINSEQ_1:1,MATRIX_0:58
.= q by Th60;
A8: Col(PQR@,3) = Line(PQR,3) by A5,FINSEQ_1:1,MATRIX_0:58
.= r by Th60;
|{ p,q,r }| = Det PQR by Th29
.= Det (PQR@) by MATRIXR2:43;
then Det PQR@ <> 0.F_Real by A4,STRUCT_0:def 6;
then Det(PQR@) is non zero by STRUCT_0:def 12;
then Det(PQR@) is unital;
then PQR@ is invertible by LAPLACE:34;
then consider N being Matrix of 3,F_Real such that
A9: N is_reverse_of PQR@ by LAPLACE:34,MATRIX_6:def 3;
take N;
thus N is invertible by A9,MATRIX_6:def 3;
pr in REAL 3 & qr in REAL 3 & rr in REAL 3; then
A10: pr in 3-tuples_on REAL & qr in 3-tuples_on REAL &
rr in 3-tuples_on REAL by EUCLID:def 1; then
A11: len pr = 3 & len qr = 3 & len rr = 3 by FINSEQ_2:133;
len (PQR@) = 3 by MATRIX_0:24; then
A12: width N = len (PQR@) by MATRIX_0:24;
A13: dom (N * PQR@) = Seg len (N * PQR@) by FINSEQ_1:def 3
.= Seg 3 by MATRIX_0:24;
A14: Indices(N * PQR@) = [: Seg 3,Seg 3:] by MATRIX_0:24;
A15: width <*pf*> = len pf by MATRIX_0:23
.= 3 by A10,A1,FINSEQ_2:133;
A16: width <*qf*> = len qf by MATRIX_0:23
.= 3 by A10,A2,FINSEQ_2:133;
A17: width <*rf*> = len rf by MATRIX_0:23
.= 3 by A10,A3,FINSEQ_2:133;
A18: width N = 3 by MATRIX_0:24
.= len (<*pf*>@) by MATRIX_0:def 6,A15;
A19: width N = 3 by MATRIX_0:24
.= len (<*qf*>@) by MATRIX_0:def 6,A16;
A20: width N = 3 by MATRIX_0:24
.= len (<*rf*>@) by MATRIX_0:def 6,A17;
A21: N * pf = N * (<*pf*>@) & N * qf = N * (<*qf*>@) &
N * rf = N * (<*rf*>@) by LAPLACE:def 9;
A22: len (N * pf) = len (N * (<*pf*>@)) by LAPLACE:def 9
.= len N by A18,MATRIX_3:def 4
.= 3 by MATRIX_0:24;
A23: len (N * qf) = len (N * (<*qf*>@)) by LAPLACE:def 9
.= len N by A19,MATRIX_3:def 4
.= 3 by MATRIX_0:24;
A24: len (N * rf) = len (N * (<*rf*>@)) by LAPLACE:def 9
.= len N by A20,MATRIX_3:def 4
.= 3 by MATRIX_0:24;
N * (<*pf*>@) is Matrix of 3,1,F_Real &
N * (<*qf*>@) is Matrix of 3,1,F_Real &
N * (<*rf*>@) is Matrix of 3,1,F_Real
by A1,A2,A3,A10,Th74,FINSEQ_2:133; then
A25: Indices(N * <*pf*>@) = [:Seg 3,Seg 1:] &
Indices(N * <*qf*>@) = [:Seg 3,Seg 1:] &
Indices(N * <*rf*>@) = [:Seg 3,Seg 1:] by MATRIX_0:23;
reconsider CN1 = Col(N * PQR@,1),
CN2 = Col(N * PQR@,2),
CN3 = Col(N * PQR@,3) as FinSequence of REAL;
N * (<*pf*>@) = F2M <e1>
proof
N * (<*pf*>@) = F2M CN1
proof
now
A26: dom (N * pf) = Seg 3 by A22,FINSEQ_1:def 3;
A27: len Col(N * PQR@,1) = len Col(1.(F_Real,3),1) by A9,MATRIX_6:def 2
.= len 1.(F_Real,3) by MATRIX_0:def 8
.= 3 by MATRIX_0:24; then
len F2M CN1 = 3 by Th64;
then dom F2M CN1 = Seg 3 by FINSEQ_1:def 3;
hence dom(N * (<*pf*>@)) = dom F2M CN1 by A21,A22,FINSEQ_1:def 3;
thus for x be object st x in dom(N * (<*pf*>@)) holds
(N * (<*pf*>@)).x = (F2M CN1).x
proof
let x be object;
assume
A28: x in dom(N * (<*pf*>@));
then reconsider y = x as Nat;
y in Seg 3 by A28,A26,LAPLACE:def 9;
then y = 1 or ... or y = 3 by FINSEQ_1:91;
then per cases;
suppose
A29: y = 1;
F2M CN1 = <* <*CN1.1*> ,<*CN1.2*>,<*CN1.3*> *> by A27,DEF1; then
A30: (F2M CN1).1 = <*CN1.1*>
.= <* (N * PQR@)*(1,1) *>
by FINSEQ_1:1,A13,MATRIX_0:def 8;
A31: <* (N * PQR@)*(1,1) *> = <* Line(N,1) "*" Col(PQR@,1) *>
by A12,A14,Th1,MATRIX_3:def 4;
A32: 1 in Seg 3 & N * (<*pf*>@) is Matrix of 3,1,F_Real
by FINSEQ_1:1,A10,A1,Th74,FINSEQ_2:133;
Line(N * (<*pf*>@),1) = <* Line(N,1) "*" Col(PQR@,1) *>
proof
1 in Seg 3 & 1 in Seg 1 by FINSEQ_1:1; then
A33: [1,1] in Indices (N * <*pf*>@) by A25,ZFMISC_1:87;
Line(N * (<*pf*>@),1) = <* (N * (<*pf*>@))*(1,1) *>
by A11,A1,Th75
.= <* Line(N,1) "*" Col(<*pf*>@,1) *>
by A18,A33,MATRIX_3:def 4;
hence thesis by A1,A6,Th76;
end;
hence thesis by A29,A32,MATRIX_0:52,A31,A30;
end;
suppose
A34: y = 2;
F2M CN1 = <* <*CN1.1*> ,<*CN1.2*>,<*CN1.3*> *> by A27,DEF1; then
A35: (F2M CN1).2 = <*CN1.2*>
.= <* (N * PQR@)*(2,1) *>
by A13,FINSEQ_1:1,MATRIX_0:def 8;
A36: <* (N * PQR@)*(2,1) *> = <* Line(N,2) "*" Col(PQR@,1) *>
by A12,MATRIX_3:def 4,A14,Th1;
A37: 1 in Seg 3 & N * (<*pf*>@) is Matrix of 3,1,F_Real
by FINSEQ_1:1,A10,A1,Th74,FINSEQ_2:133;
Line(N * (<*pf*>@),2) = <* Line(N,2) "*" Col(PQR@,1) *>
proof
2 in Seg 3 & 1 in Seg 1 by FINSEQ_1:1; then
A38: [2,1] in Indices (N * <*pf*>@) by A25,ZFMISC_1:87;
Line(N * (<*pf*>@),2) = <* (N * (<*pf*>@))*(2,1) *>
by A11,A1,Th75
.= <* Line(N,2) "*" Col(<*pf*>@,1) *>
by A18,A38,MATRIX_3:def 4;
hence thesis by A1,A6,Th76;
end;
hence thesis by A34,A37,FINSEQ_1:1,MATRIX_0:52,A36,A35;
end;
suppose
A39: y = 3;
F2M CN1 = <* <*CN1.1*> ,<*CN1.2*>,<*CN1.3*> *> by A27,DEF1; then
A40: (F2M CN1).3 = <*CN1.3*>
.= <* (N * PQR@)*(3,1) *>
by A13,FINSEQ_1:1,MATRIX_0:def 8;
A41: <* (N * PQR@)*(3,1) *> = <* Line(N,3) "*" Col(PQR@,1) *>
by A14,Th1,A12,MATRIX_3:def 4;
A42: 1 in Seg 3 & N * (<*pf*>@) is Matrix of 3,1,F_Real
by FINSEQ_1:1,A10,FINSEQ_2:133,A1,Th74;
Line(N * (<*pf*>@),3) = <* Line(N,3) "*" Col(PQR@,1) *>
proof
3 in Seg 3 & 1 in Seg 1 by FINSEQ_1:1; then
A43: [3,1] in Indices (N * <*pf*>@) by A25,ZFMISC_1:87;
Line(N * (<*pf*>@),3) = <* (N * (<*pf*>@))*(3,1) *>
by A1,A11,Th75
.= <* Line(N,3) "*" Col(<*pf*>@,1) *>
by A18,A43,MATRIX_3:def 4;
hence thesis by Th76,A1,A6;
end;
hence thesis by A41,A39,A42,FINSEQ_1:1,MATRIX_0:52,A40;
end;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
hence thesis by A9,MATRIX_6:def 2,Th55,EUCLID_8:def 1;
end;
hence N * pf = F2M <e1> by LAPLACE:def 9;
N * (<*qf*>@) = F2M <e2>
proof
N * (<*qf*>@) = F2M CN2
proof
now
A44: dom (N * qf) = Seg 3 by A23,FINSEQ_1:def 3;
A45: len Col(N * PQR@,2) = len Col(1.(F_Real,3),2) by A9,MATRIX_6:def 2
.= len 1.(F_Real,3) by MATRIX_0:def 8
.= 3 by MATRIX_0:24;
then len F2M CN2 = 3 by Th64;
then dom F2M CN2 = Seg 3 by FINSEQ_1:def 3;
hence dom(N * (<*qf*>@)) = dom F2M CN2 by A21,A23,FINSEQ_1:def 3;
thus for x be object st x in dom(N * (<*qf*>@)) holds
(N * (<*qf*>@)).x = (F2M CN2).x
proof
let x be object;
assume
A46: x in dom(N * (<*qf*>@));
then reconsider y = x as Nat;
y in Seg 3 by A46,A44,LAPLACE:def 9;
then y = 1 or ... or y = 3 by FINSEQ_1:91;
then per cases;
suppose
A47: y = 1;
F2M CN2 = <* <*CN2.1*> ,<*CN2.2*>,<*CN2.3*> *> by A45,DEF1; then
A48: (F2M CN2).1 = <*CN2.1*>
.= <* (N * PQR@)*(1,2) *>
by FINSEQ_1:1,A13,MATRIX_0:def 8;
A49: <* (N * PQR@)*(1,2) *> = <* Line(N,1) "*" Col(PQR@,2) *>
by A12,A14,Th1,MATRIX_3:def 4;
A50: 1 in Seg 3 & N * (<*qf*>@) is Matrix of 3,1,F_Real
by FINSEQ_1:1,A10,A2,Th74,FINSEQ_2:133;
Line(N * (<*qf*>@),1) = <* Line(N,1) "*" Col(PQR@,2) *>
proof
1 in Seg 3 & 1 in Seg 1 by FINSEQ_1:1; then
A51: [1,1] in Indices (N * <*qf*>@) by A25,ZFMISC_1:87;
Line(N * (<*qf*>@),1) = <* (N * (<*qf*>@))*(1,1) *>
by A11,A2,Th75
.= <* Line(N,1) "*" Col(<*qf*>@,1) *>
by A19,A51,MATRIX_3:def 4;
hence thesis by A2,A7,Th76;
end;
hence thesis by A47,A50,MATRIX_0:52,A49,A48;
end;
suppose
A52: y = 2;
F2M CN2 = <* <*CN2.1*> ,<*CN2.2*>,<*CN2.3*> *> by A45,DEF1; then
A53: (F2M CN2).2 = <*CN2.2*>
.= <* (N * PQR@)*(2,2) *>
by A13,FINSEQ_1:1,MATRIX_0:def 8;
A54: <* (N * PQR@)*(2,2) *> = <* Line(N,2) "*" Col(PQR@,2) *>
by A12,MATRIX_3:def 4,A14,Th1;
A55: 2 in Seg 3 & N * (<*qf*>@) is Matrix of 3,1,F_Real
by FINSEQ_1:1,A10,A2,Th74,FINSEQ_2:133;
Line(N * (<*qf*>@),2) = <* Line(N,2) "*" Col(PQR@,2) *>
proof
2 in Seg 3 & 1 in Seg 1 by FINSEQ_1:1; then
A56: [2,1] in Indices (N * <*qf*>@) by A25,ZFMISC_1:87;
Line(N * (<*qf*>@),2) = <* (N * (<*qf*>@))*(2,1) *>
by A11,A2,Th75
.= <* Line(N,2) "*" Col(<*qf*>@,1) *>
by A19,A56,MATRIX_3:def 4;
hence thesis by A2,A7,Th76;
end;
hence thesis by A52,A55,MATRIX_0:52,A54,A53;
end;
suppose
A57: y = 3;
F2M CN2 = <* <*CN2.1*> ,<*CN2.2*>,<*CN2.3*> *> by A45,DEF1; then
A58: (F2M CN2).3 = <*CN2.3*>
.= <* (N * PQR@)*(3,2) *>
by A13,FINSEQ_1:1,MATRIX_0:def 8;
A59: <* (N * PQR@)*(3,2) *> = <* Line(N,3) "*" Col(PQR@,2) *>
by A14,Th1,A12,MATRIX_3:def 4;
A60: 3 in Seg 3 & N * (<*qf*>@) is Matrix of 3,1,F_Real
by FINSEQ_1:1,A10,FINSEQ_2:133,A2,Th74;
Line(N * (<*qf*>@),3) = <* Line(N,3) "*" Col(PQR@,2) *>
proof
3 in Seg 3 & 1 in Seg 1 by FINSEQ_1:1; then
A61: [3,1] in Indices (N * <*qf*>@) by A25,ZFMISC_1:87;
Line(N * (<*qf*>@),3) = <* (N * (<*qf*>@))*(3,1) *>
by A2,A11,Th75
.= <* Line(N,3) "*" Col(<*qf*>@,1) *>
by A19,A61,MATRIX_3:def 4;
hence thesis by Th76,A2,A7;
end;
hence thesis by A59,A57,A60,MATRIX_0:52,A58;
end;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
hence thesis by A9,MATRIX_6:def 2,Th55,EUCLID_8:def 2;
end;
hence N * qf = F2M <e2> by LAPLACE:def 9;
N * (<*rf*>@) = F2M <e3>
proof
N * (<*rf*>@) = F2M CN3
proof
now
A62: dom (N * rf) = Seg 3 by A24,FINSEQ_1:def 3;
A63: len Col(N * PQR@,3) = len Col(1.(F_Real,3),3) by A9,MATRIX_6:def 2
.= len 1.(F_Real,3) by MATRIX_0:def 8
.= 3 by MATRIX_0:24;
len F2M CN3 = 3 by A63,Th64;
then dom F2M CN3 = Seg 3 by FINSEQ_1:def 3;
hence dom(N * (<*rf*>@)) = dom F2M CN3 by A21,A24,FINSEQ_1:def 3;
thus for x be object st x in dom(N * (<*rf*>@)) holds
(N * (<*rf*>@)).x = (F2M CN3).x
proof
let x be object;
assume
A64: x in dom(N * (<*rf*>@));
then reconsider y = x as Nat;
y in Seg 3 by A64,A62,LAPLACE:def 9;
then y = 1 or ... or y = 3 by FINSEQ_1:91;
then per cases;
suppose
A65: y = 1;
F2M CN3 = <* <*CN3.1*> ,<*CN3.2*>,<*CN3.3*> *> by A63,DEF1; then
A66: (F2M CN3).1 = <*CN3.1*>
.= <* (N * PQR@)*(1,3) *>
by FINSEQ_1:1,A13,MATRIX_0:def 8;
A67: <* (N * PQR@)*(1,3) *> = <* Line(N,1) "*" Col(PQR@,3) *>
by A12,A14,Th1,MATRIX_3:def 4;
A68: 1 in Seg 3 & N * (<*rf*>@) is Matrix of 3,1,F_Real
by FINSEQ_1:1,A10,A3,Th74,FINSEQ_2:133;
Line(N * (<*rf*>@),1) = <* Line(N,1) "*" Col(PQR@,3) *>
proof
1 in Seg 3 & 1 in Seg 1 by FINSEQ_1:1; then
A69: [1,1] in Indices (N * <*rf*>@) by A25,ZFMISC_1:87;
Line(N * (<*rf*>@),1) = <* (N * (<*rf*>@))*(1,1) *>
by A11,A3,Th75
.= <* Line(N,1) "*" Col(<*rf*>@,1) *>
by A20,A69,MATRIX_3:def 4;
hence thesis by A3,A8,Th76;
end;
hence thesis by A65,A68,MATRIX_0:52,A67,A66;
end;
suppose
A70: y = 2;
F2M CN3 = <* <*CN3.1*> ,<*CN3.2*>,<*CN3.3*> *> by A63,DEF1; then
A71: (F2M CN3).2 = <*CN3.2*>
.= <* (N * PQR@)*(2,3) *>
by A13,FINSEQ_1:1,MATRIX_0:def 8;
A72: <* (N * PQR@)*(2,3) *> = <* Line(N,2) "*" Col(PQR@,3) *>
by A12,MATRIX_3:def 4,A14,Th1;
A73: 1 in Seg 3 & N * (<*rf*>@) is Matrix of 3,1,F_Real
by FINSEQ_1:1,A10,A3,Th74,FINSEQ_2:133;
Line(N * (<*rf*>@),2) = <* Line(N,2) "*" Col(PQR@,3) *>
proof
2 in Seg 3 & 1 in Seg 1 by FINSEQ_1:1; then
A74: [2,1] in Indices (N * <*rf*>@) by A25,ZFMISC_1:87;
Line(N * (<*rf*>@),2) = <* (N * (<*rf*>@))*(2,1) *>
by A11,A3,Th75
.= <* Line(N,2) "*" Col(<*rf*>@,1) *>
by A20,A74,MATRIX_3:def 4;
hence thesis by A3,A8,Th76;
end;
hence thesis by A70,A73,FINSEQ_1:1,MATRIX_0:52,A72,A71;
end;
suppose
A75: y = 3;
F2M CN3 = <* <*CN3.1*> ,<*CN3.2*>,<*CN3.3*> *> by A63,DEF1; then
A76: (F2M CN3).3 = <*CN3.3*>
.= <* (N * PQR@)*(3,3) *>
by A13,FINSEQ_1:1,MATRIX_0:def 8;
A77: <* (N * PQR@)*(3,3) *> = <* Line(N,3) "*" Col(PQR@,3) *>
by A14,Th1,A12,MATRIX_3:def 4;
A78: 3 in Seg 3 & N * (<*rf*>@) is Matrix of 3,1,F_Real
by FINSEQ_1:1,A10,FINSEQ_2:133,A3,Th74;
Line(N * (<*rf*>@),3) = <* Line(N,3) "*" Col(PQR@,3) *>
proof
3 in Seg 3 & 1 in Seg 1 by FINSEQ_1:1; then
A79: [3,1] in Indices (N * <*rf*>@) by A25,ZFMISC_1:87;
Line(N * (<*rf*>@),3) = <* (N * (<*rf*>@))*(3,1) *>
by A3,A11,Th75
.= <* Line(N,3) "*" Col(<*rf*>@,1) *>
by A20,A79,MATRIX_3:def 4;
hence thesis by Th76,A3,A8;
end;
hence thesis by A77,A75,A78,MATRIX_0:52,A76;
end;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
hence thesis by A9,MATRIX_6:def 2,Th55,EUCLID_8:def 3;
end;
hence N * rf = F2M <e3> by LAPLACE:def 9;
end;
theorem Th77:
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 *>
proof
let pf,qf,rf be FinSequence of F_Real;
let pt,qt,rt be FinSequence of 1-tuples_on REAL;
assume that
A1: PQR = <*<*p`1,q`1,r`1*>,<*p`2,q`2,r`2*>,<*p`3,q`3,r`3*>*> and
A2: p = pf and
A3: q = qf and
A4: r = rf and
A5: pt = M * pf and
A6: qt = M * qf and
A7: rt = M * rf;
A8: PQR@ = <*<*p`1,p`2,p`3*>,<*q`1,q`2,q`3*>,<*r`1,r`2,r`3*>*> by A1,Th19;
A9: len PQR = 3 by MATRIX_0:24;
A10: width PQR = 3 by MATRIX_0:23;
A11: Indices(M * PQR) = [: Seg 3,Seg 3:] by MATRIX_0:24;
len (PQR@) = 3 by MATRIX_0:23; then
A12: dom (PQR@) = Seg 3 by FINSEQ_1:def 3; then
A13: Col((PQR@)@,1) = Line(PQR@,1) by FINSEQ_1:1,MATRIX_0:58
.= p by A8,Th60;
A14: Col((PQR@)@,2) = Line(PQR@,2) by A12,FINSEQ_1:1,MATRIX_0:58
.= q by A8,Th60;
A15: Col((PQR@)@,3) = Line(PQR@,3) by A12,FINSEQ_1:1,MATRIX_0:58
.= r by A8,Th60;
pf in TOP-REAL 3 & qf in TOP-REAL 3 & rf in TOP-REAL 3 by A2,A3,A4; then
A16: pf in REAL 3 & qf in REAL 3 & rf in REAL 3 by EUCLID:22; then
A17: len pf = 3 & len qf = 3 & len rf = 3 by EUCLID_8:50;
A18: width M = len (<*pf*>@) & width M = len (<*qf*>@) &
width M = len (<*rf*>@)
proof
width <*pf*> = 3 by A17,Th61;
then len (<*pf*>@) = width <*pf*> by MATRIX_0:29
.= len pf by MATRIX_0:23;
then len (<*pf*>@) = 3 by A16,EUCLID_8:50;
hence width M = len (<*pf*>@) by MATRIX_0:23;
width <*qf*> = 3 by A17,Th61;
then len (<*qf*>@) = width <*qf*> by MATRIX_0:29
.= len qf by MATRIX_0:23;
then len (<*qf*>@) = 3 by A16,EUCLID_8:50;
hence width M = len (<*qf*>@) by MATRIX_0:23;
width <*rf*> = 3 by A17,Th61;
then len (<*rf*>@) = width <*rf*> by MATRIX_0:29
.= len rf by MATRIX_0:23;
then len (<*rf*>@) = 3 by A16,EUCLID_8:50;
hence width M = len (<*rf*>@) by MATRIX_0:23;
end;
A19: len pt = 3 & len qt = 3 & len rt = 3
proof
width M = len (<*pf*>@) & len M = 3 by MATRIX_0:23,A18;
then len (M * <*pf*>@) = 3 by MATRIX_3:def 4;
hence len pt = 3 by A5,LAPLACE:def 9;
width M = len (<*qf*>@) & len M = 3 by A18,MATRIX_0:23;
then len (M * <*qf*>@) = 3 by MATRIX_3:def 4;
hence len qt = 3 by A6,LAPLACE:def 9;
width M = len (<*rf*>@) & len M = 3 by A18,MATRIX_0:23;
then len (M * <*rf*>@) = 3 by MATRIX_3:def 4;
hence len rt = 3 by A7,LAPLACE:def 9;
end;
set PQRM = <*<*pt.1,pt.2,pt.3*>,<*qt.1,qt.2,qt.3*>,<*rt.1,rt.2,rt.3*>*>;
A20: dom (M * PQR) = Seg len (M * PQR) by FINSEQ_1:def 3
.= Seg 3 by MATRIX_0:24;
A21: width (M * PQR) = 3 by MATRIX_0:23;
A22: len ((M * PQR)@) = 3 by MATRIX_0:23; then
A23: dom ((M * PQR)@) = Seg 3 by FINSEQ_1:def 3;
A24: 1 in Seg width(M * PQR) & 2 in Seg width (M * PQR) &
3 in Seg width (M * PQR) by A21,FINSEQ_1:1;
now
len <* M2F pt,M2F qt,M2F rt *> = 3 by FINSEQ_1:45;
hence dom ((M * PQR)@) = dom <* M2F pt,M2F qt,M2F rt *>
by A23,FINSEQ_1:def 3;
thus for x be object st x in dom ((M * PQR)@) holds
(M * PQR)@.x = <* M2F pt,M2F qt,M2F rt *>.x
proof
let x be object;
assume
A25: x in dom ((M * PQR)@);
then reconsider y = x as Nat;
y in Seg 3 by A25,A22,FINSEQ_1:def 3;
then y = 1 or ... or y = 3 by FINSEQ_1:91;
then per cases;
suppose
A26: y = 1;
A27: M * <*pf*>@ is Matrix of 3,1,F_Real by A16,EUCLID_8:50,Th74; then
A28: Indices (M * <*pf*>@) =[:Seg 3,Seg 1:] by MATRIX_0:23;
A29: now
thus len pt = 3 by A19;
<* (M * PQR)*(1,1) *> = pt.1
proof
1 in Seg 3 by FINSEQ_1:1; then
A30: width M = len PQR & [1,1] in Indices (M * PQR)
by A9,MATRIX_0:23,A11,ZFMISC_1:87;
A31: (M * <*pf*>@).1 = <* Line(M,1) "*" Col(PQR,1) *>
proof
A32: 1 in Seg 3 by FINSEQ_1:1;
Line(M * (<*pf*>@),1) = <* Line(M,1) "*" Col(PQR,1) *>
proof
1 in Seg 3 & 1 in Seg 1 by FINSEQ_1:1; then
A33: [1,1] in Indices (M * <*pf*>@) by A28,ZFMISC_1:87;
len pf = 3 by A16,EUCLID_8:50; then
Line(M * (<*pf*>@),1) = <* (M * (<*pf*>@))*(1,1) *> by Th75
.= <* Line(M,1) "*" Col(<*pf*>@,1) *>
by A18,A33,MATRIX_3:def 4
.= <* Line(M,1) "*" pf *> by Th76
.= <* Line(M,1) "*" Col(PQR,1) *>
by A13,A9,A10,MATRIX_0:57,A2;
hence thesis;
end;
hence thesis by A32,A27,MATRIX_0:52;
end;
pt.1 = (M * <*pf*>@).1 by A5,LAPLACE:def 9;
hence thesis by A30,MATRIX_3:def 4,A31;
end;
hence <* Line(M * PQR,1).1 *> = pt.1 by A24,MATRIX_0:def 7;
<* (M * PQR)*(2,1) *> = pt.2
proof
1 in Seg 3 & 2 in Seg 3 by FINSEQ_1:1; then
A34: width M = len PQR & [2,1] in Indices (M * PQR)
by A9,MATRIX_0:23,A11,ZFMISC_1:87;
A34BIS: (M * <*pf*>@).2 = <* Line(M,2) "*" Col(PQR,1) *>
proof
A35: 2 in Seg 3 by FINSEQ_1:1;
Line(M * (<*pf*>@),2) = <* Line(M,2) "*" Col(PQR,1) *>
proof
1 in Seg 1 & 2 in Seg 3 by FINSEQ_1:1; then
A36: [2,1] in Indices (M * <*pf*>@) by A28,ZFMISC_1:87;
len pf = 3 by A16,EUCLID_8:50; then
Line(M * (<*pf*>@),2) = <* (M * (<*pf*>@))*(2,1) *> by Th75
.= <* Line(M,2) "*" Col(<*pf*>@,1) *>
by A18,A36,MATRIX_3:def 4
.= <* Line(M,2) "*" pf *> by Th76
.= <* Line(M,2) "*" Col(PQR,1) *>
by A13,A9,A10,MATRIX_0:57,A2;
hence thesis;
end;
hence thesis by A35,A27,MATRIX_0:52;
end;
pt.2 = (M * <*pf*>@).2 by A5,LAPLACE:def 9;
hence thesis by A34,MATRIX_3:def 4,A34BIS;
end;
hence <* Line(M * PQR,2).1 *> = pt.2 by A24,MATRIX_0:def 7;
<* (M * PQR)*(3,1) *> = pt.3
proof
1 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1; then
A37: width M = len PQR & [3,1] in Indices (M * PQR)
by A9,MATRIX_0:23,A11,ZFMISC_1:87;
A38: (M * <*pf*>@).3 = <* Line(M,3) "*" Col(PQR,1) *>
proof
A39: 3 in Seg 3 by FINSEQ_1:1;
Line(M * (<*pf*>@),3) = <* Line(M,3) "*" Col(PQR,1) *>
proof
1 in Seg 1 & 3 in Seg 3 by FINSEQ_1:1; then
A39BIS: [3,1] in Indices (M * <*pf*>@) by A28,ZFMISC_1:87;
len pf = 3 by A16,EUCLID_8:50; then
Line(M * (<*pf*>@),3) = <* (M * (<*pf*>@))*(3,1) *> by Th75
.= <* Line(M,3) "*" Col(<*pf*>@,1) *>
by A18,A39BIS,MATRIX_3:def 4
.= <* Line(M,3) "*" pf *> by Th76
.= <* Line(M,3) "*" Col(PQR,1) *>
by A13,A9,A10,MATRIX_0:57,A2;
hence thesis;
end;
hence thesis by A39,A27,MATRIX_0:52;
end;
pt.3 = (M * <*pf*>@).3 by A5,LAPLACE:def 9;
hence thesis by A37,MATRIX_3:def 4,A38;
end;
hence <* Line(M * PQR,3).1 *> = pt.3 by A24,MATRIX_0:def 7;
end;
A40: Line(M * PQR,1).1 = (M * PQR)*(1,1) &
Line(M * PQR,2).1 = (M * PQR)*(2,1) &
Line(M * PQR,3).1 = (M * PQR)*(3,1) by A24,MATRIX_0:def 7;
1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1;
then [1,1] in Indices (M * PQR) &
[2,1] in Indices (M * PQR) &
[3,1] in Indices (M * PQR) by A11,ZFMISC_1:87; then
A41: (M * PQR)@ * (1,1) = (M * PQR)*(1,1) &
(M * PQR)@ * (1,2) = (M * PQR)*(2,1) &
(M * PQR)@ * (1,3) = (M * PQR)*(3,1) by MATRIX_0:def 6;
width ((M * PQR)@) = len (M * PQR) by A21,MATRIX_0:29; then
Seg width ((M * PQR)@) = dom (M * PQR) by FINSEQ_1:def 3; then
A43: Line((M * PQR)@,1).1 = (M * PQR)@*(1,1) &
Line((M * PQR)@,1).2 = (M * PQR)@*(1,2) &
Line((M * PQR)@,1).3 = (M * PQR)@*(1,3)
by A20,FINSEQ_1:1,MATRIX_0:def 7;
A44: 1 in Seg 3 by FINSEQ_1:1;
reconsider FMPQR = Line((M * PQR)@,1) as FinSequence of REAL;
width ((M * PQR)@) = 3 by MATRIX_0:23; then
A45: len FMPQR = 3 by MATRIX_0:def 7;
A46: <* <*Line((M * PQR)@,1).1*>, <*Line((M * PQR)@,1).2*>,
<*Line((M * PQR)@,1).3*> *> = F2M FMPQR by A45,DEF1;
FMPQR = M2F F2M FMPQR by A45,Th70
.= M2F pt by A46,A43,A41,A29,FINSEQ_1:45,A40;
then (M * PQR)@.1 = M2F pt by A44,MATRIX_0:52;
hence thesis by A26;
end;
suppose
A47: y = 2;
A48: M * <*qf*>@ is Matrix of 3,1,F_Real by A16,EUCLID_8:50,Th74; then
A49: Indices (M * <*qf*>@) =[:Seg 3,Seg 1:] by MATRIX_0:23;
A50: now
thus len qt = 3 by A19;
<* (M * PQR)*(1,2) *> = qt.1
proof
1 in Seg 3 & 2 in Seg 3 by FINSEQ_1:1; then
A51: width M = len PQR & [1,2] in Indices (M * PQR)
by A9,MATRIX_0:23,A11,ZFMISC_1:87;
A52: (M * <*qf*>@).1 = <* Line(M,1) "*" Col(PQR,2) *>
proof
A53: 1 in Seg 3 by FINSEQ_1:1;
Line(M * (<*qf*>@),1) = <* Line(M,1) "*" Col(PQR,2) *>
proof
1 in Seg 3 & 1 in Seg 1 by FINSEQ_1:1; then
A54: [1,1] in Indices (M * <*qf*>@) by A49,ZFMISC_1:87;
len qf = 3 by A16,EUCLID_8:50; then
Line(M * (<*qf*>@),1) = <* (M * (<*qf*>@))*(1,1) *> by Th75
.= <* Line(M,1) "*" Col(<*qf*>@,1) *>
by A18,A54,MATRIX_3:def 4
.= <* Line(M,1) "*" qf *> by Th76
.= <* Line(M,1) "*" Col(PQR,2) *>
by A14,A9,A10,MATRIX_0:57,A3;
hence thesis;
end;
hence thesis by A53,A48,MATRIX_0:52;
end;
qt.1 = (M * <*qf*>@).1 by A6,LAPLACE:def 9;
hence thesis by A51,MATRIX_3:def 4,A52;
end;
hence <* Line(M * PQR,1).2 *> = qt.1 by A24,MATRIX_0:def 7;
<* (M * PQR)*(2,2) *> = qt.2
proof
1 in Seg 3 & 2 in Seg 3 by FINSEQ_1:1; then
A55: width M = len PQR & [2,2] in Indices (M * PQR)
by A9,MATRIX_0:23,A11,ZFMISC_1:87;
A56: (M * <*qf*>@).2 = <* Line(M,2) "*" Col(PQR,2) *>
proof
A57: 2 in Seg 3 by FINSEQ_1:1;
Line(M * (<*qf*>@),2) = <* Line(M,2) "*" Col(PQR,2) *>
proof
1 in Seg 1 & 2 in Seg 3 by FINSEQ_1:1; then
A58: [2,1] in Indices (M * <*qf*>@) by A49,ZFMISC_1:87;
len qf = 3 by A16,EUCLID_8:50; then
Line(M * (<*qf*>@),2) = <* (M * (<*qf*>@))*(2,1) *> by Th75
.= <* Line(M,2) "*" Col(<*qf*>@,1) *>
by A18,A58,MATRIX_3:def 4
.= <* Line(M,2) "*" qf *> by Th76
.= <* Line(M,2) "*" Col(PQR,2) *>
by A14,A9,A10,MATRIX_0:57,A3;
hence thesis;
end;
hence thesis by A57,A48,MATRIX_0:52;
end;
qt.2 = (M * <*qf*>@).2 by A6,LAPLACE:def 9;
hence thesis by A55,MATRIX_3:def 4,A56;
end;
hence <* Line(M * PQR,2).2 *> = qt.2 by A24,MATRIX_0:def 7;
<* (M * PQR)*(3,2) *> = qt.3
proof
2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1; then
A57: width M = len PQR & [3,2] in Indices (M * PQR)
by A9,MATRIX_0:23,A11,ZFMISC_1:87;
A58: (M * <*qf*>@).3 = <* Line(M,3) "*" Col(PQR,2) *>
proof
A59: 3 in Seg 3 by FINSEQ_1:1;
Line(M * (<*qf*>@),3) = <* Line(M,3) "*" Col(PQR,2) *>
proof
1 in Seg 1 & 3 in Seg 3 by FINSEQ_1:1; then
A59BIS: [3,1] in Indices (M * <*qf*>@) by A49,ZFMISC_1:87;
len qf = 3 by A16,EUCLID_8:50; then
Line(M * (<*qf*>@),3) = <* (M * (<*qf*>@))*(3,1) *> by Th75
.= <* Line(M,3) "*" Col(<*qf*>@,1) *>
by A18,A59BIS,MATRIX_3:def 4
.= <* Line(M,3) "*" qf *> by Th76
.= <* Line(M,3) "*" Col(PQR,2) *>
by A14,A9,A10,MATRIX_0:57,A3;
hence thesis;
end;
hence thesis by A59,A48,MATRIX_0:52;
end;
qt.3 = (M * <*qf*>@).3 by A6,LAPLACE:def 9;
hence thesis by A57,MATRIX_3:def 4,A58;
end;
hence <* Line(M * PQR,3).2 *> = qt.3 by A24,MATRIX_0:def 7;
end;
A60: Line(M * PQR,1).2 = (M * PQR)*(1,2) &
Line(M * PQR,2).2 = (M * PQR)*(2,2) &
Line(M * PQR,3).2 = (M * PQR)*(3,2) by A24,MATRIX_0:def 7;
1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1;
then [1,2] in Indices (M * PQR) & [2,2] in Indices (M * PQR) &
[3,2] in Indices (M * PQR) by A11,ZFMISC_1:87; then
A61: (M * PQR)@ * (2,1) = (M * PQR)*(1,2) &
(M * PQR)@ * (2,2) = (M * PQR)*(2,2) &
(M * PQR)@ * (2,3) = (M * PQR)*(3,2) by MATRIX_0:def 6;
width ((M * PQR)@) = len (M * PQR) by A21,MATRIX_0:29; then
Seg width ((M * PQR)@) = dom (M * PQR) by FINSEQ_1:def 3; then
A62: Line((M * PQR)@,2).1 = (M * PQR)@*(2,1) &
Line((M * PQR)@,2).2 = (M * PQR)@*(2,2) &
Line((M * PQR)@,2).3 = (M * PQR)@*(2,3)
by A20,FINSEQ_1:1,MATRIX_0:def 7;
A63: 2 in Seg 3 by FINSEQ_1:1;
reconsider FMPQR = Line((M * PQR)@,2) as FinSequence of REAL;
width ((M * PQR)@) = 3 by MATRIX_0:23; then
A64: len FMPQR = 3 by MATRIX_0:def 7; then
A65: <* <*Line((M * PQR)@,2).1*>, <*Line((M * PQR)@,2).2*>,
<*Line((M * PQR)@,2).3*> *> = F2M FMPQR by DEF1;
FMPQR = M2F F2M FMPQR by A64,Th70
.= M2F qt by A65,A62,A61,A50,FINSEQ_1:45,A60;
then (M * PQR)@.2 = M2F qt by A63,MATRIX_0:52;
hence thesis by A47;
end;
suppose
A66: y = 3;
A67: M * <*rf*>@ is Matrix of 3,1,F_Real by A16,EUCLID_8:50,Th74; then
A68: Indices (M * <*rf*>@) =[:Seg 3,Seg 1:] by MATRIX_0:23;
A69: now
thus len rt = 3 by A19;
<* (M * PQR)*(1,3) *> = rt.1
proof
1 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1; then
A70: width M = len PQR & [1,3] in Indices (M * PQR)
by A9,MATRIX_0:23,A11,ZFMISC_1:87;
A71: (M * <*rf*>@).1 = <* Line(M,1) "*" Col(PQR,3) *>
proof
A72: 1 in Seg 3 by FINSEQ_1:1;
Line(M * (<*rf*>@),1) = <* Line(M,1) "*" Col(PQR,3) *>
proof
1 in Seg 3 & 1 in Seg 1 by FINSEQ_1:1; then
A73: [1,1] in Indices (M * <*rf*>@) by A68,ZFMISC_1:87;
len rf = 3 by A16,EUCLID_8:50; then
Line(M * (<*rf*>@),1) = <* (M * (<*rf*>@))*(1,1) *> by Th75
.= <* Line(M,1) "*" Col(<*rf*>@,1) *>
by A18,A73,MATRIX_3:def 4
.= <* Line(M,1) "*" rf *> by Th76
.= <* Line(M,1) "*" Col(PQR,3) *>
by A15,A9,A10,MATRIX_0:57,A4;
hence thesis;
end;
hence thesis by A72,A67,MATRIX_0:52;
end;
rt.1 = (M * <*rf*>@).1 by A7,LAPLACE:def 9;
hence thesis by A70,MATRIX_3:def 4,A71;
end;
hence <* Line(M * PQR,1).3 *> = rt.1 by A24,MATRIX_0:def 7;
<* (M * PQR)*(2,3) *> = rt.2
proof
2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1; then
A74: width M = len PQR & [2,3] in Indices (M * PQR)
by A9,MATRIX_0:23,A11,ZFMISC_1:87;
A75: (M * <*rf*>@).2 = <* Line(M,2) "*" Col(PQR,3) *>
proof
A76: 2 in Seg 3 by FINSEQ_1:1;
Line(M * (<*rf*>@),2) = <* Line(M,2) "*" Col(PQR,3) *>
proof
1 in Seg 1 & 2 in Seg 3 by FINSEQ_1:1; then
A77: [2,1] in Indices (M * <*rf*>@) by A68,ZFMISC_1:87;
len rf = 3 by A16,EUCLID_8:50; then
Line(M * (<*rf*>@),2) = <* (M * (<*rf*>@))*(2,1) *> by Th75
.= <* Line(M,2) "*" Col(<*rf*>@,1) *>
by A18,A77,MATRIX_3:def 4
.= <* Line(M,2) "*" rf *> by Th76
.= <* Line(M,2) "*" Col(PQR,3) *>
by A15,A9,A10,MATRIX_0:57,A4;
hence thesis;
end;
hence thesis by A76,A67,MATRIX_0:52;
end;
rt.2 = (M * <*rf*>@).2 by A7,LAPLACE:def 9;
hence thesis by A74,MATRIX_3:def 4,A75;
end;
hence <* Line(M * PQR,2).3 *> = rt.2 by A24,MATRIX_0:def 7;
<* (M * PQR)*(3,3) *> = rt.3
proof
3 in Seg 3 by FINSEQ_1:1; then
A78: width M = len PQR & [3,3] in Indices (M * PQR)
by A9,MATRIX_0:23,A11,ZFMISC_1:87;
A79: (M * <*rf*>@).3 = <* Line(M,3) "*" Col(PQR,3) *>
proof
A80: 3 in Seg 3 by FINSEQ_1:1;
Line(M * (<*rf*>@),3) = <* Line(M,3) "*" Col(PQR,3) *>
proof
1 in Seg 1 & 3 in Seg 3 by FINSEQ_1:1; then
A81: [3,1] in Indices (M * <*rf*>@) by A68,ZFMISC_1:87;
len rf = 3 by A16,EUCLID_8:50; then
Line(M * (<*rf*>@),3) = <* (M * (<*rf*>@))*(3,1) *> by Th75
.= <* Line(M,3) "*" Col(<*rf*>@,1) *>
by A18,A81,MATRIX_3:def 4
.= <* Line(M,3) "*" rf *> by Th76
.= <* Line(M,3) "*" Col(PQR,3) *>
by A15,A9,A10,MATRIX_0:57,A4;
hence thesis;
end;
hence thesis by A80,A67,MATRIX_0:52;
end;
rt.3 = (M * <*rf*>@).3 by A7,LAPLACE:def 9;
hence thesis by A78,MATRIX_3:def 4,A79;
end;
hence <* Line(M * PQR,3).3 *> = rt.3 by A24,MATRIX_0:def 7;
end;
A82: Line(M * PQR,1).3 = (M * PQR)*(1,3) &
Line(M * PQR,2).3 = (M * PQR)*(2,3) &
Line(M * PQR,3).3 = (M * PQR)*(3,3) by A24,MATRIX_0:def 7;
1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1;
then [1,3] in Indices (M * PQR) &
[2,3] in Indices (M * PQR) &
[3,3] in Indices (M * PQR) by A11,ZFMISC_1:87; then
A83: (M * PQR)@ * (3,1) = (M * PQR)*(1,3) &
(M * PQR)@ * (3,2) = (M * PQR)*(2,3) &
(M * PQR)@ * (3,3) = (M * PQR)*(3,3) by MATRIX_0:def 6;
width ((M * PQR)@) = len (M * PQR) by A21,MATRIX_0:29; then
Seg width ((M * PQR)@) = dom (M * PQR) by FINSEQ_1:def 3; then
A84: Line((M * PQR)@,3).1 = (M * PQR)@*(3,1) &
Line((M * PQR)@,3).2 = (M * PQR)@*(3,2) &
Line((M * PQR)@,3).3 = (M * PQR)@*(3,3)
by A20,FINSEQ_1:1,MATRIX_0:def 7;
3 in Seg 3 by FINSEQ_1:1; then
A85: (M * PQR)@.3 = Line((M*PQR)@,3) by MATRIX_0:52;
reconsider FMPQR = Line((M * PQR)@,3) as FinSequence of REAL;
width ((M * PQR)@) = 3 by MATRIX_0:23; then
A86: len FMPQR = 3 by MATRIX_0:def 7; then
A87: <* <*Line((M * PQR)@,3).1*>, <*Line((M * PQR)@,3).2*>,
<*Line((M * PQR)@,3).3*> *> = F2M FMPQR by DEF1;
FMPQR = M2F F2M FMPQR by A86,Th70
.= M2F rt by A87,A84,A83,A69,FINSEQ_1:45,A82;
hence thesis by A85,A66;
end;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
theorem
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
proof
let pt,qt,rt be FinSequence of 1-tuples_on REAL;
assume that
A1: M = <* M2F pt,M2F qt,M2F rt*> and
A2: Det M = 0 and
A3: M2F pt = p and
A4: M2F qt = q and
A5: M2F rt = r;
p = <*p`1,p`2,p`3*> & q = <*q`1,q`2,q`3*> &
r = <*r`1,r`2,r`3*> by EUCLID_5:3;
hence thesis by A2,A1,A3,A4,A5,Th29;
end;
theorem Th78:
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
proof
let pm,qm,rm be Point of TOP-REAL 3;
let pt,qt,rt be FinSequence of 1-tuples_on REAL;
let pf,qf,rf be FinSequence of F_Real;
assume that
A1: M is invertible and
A2: p = pf and
A3: q = qf and
A4: r = rf and
A5: pt = M * pf and
A6: qt = M * qf and
A7: rt = M * rf and
A8: M2F pt = pm and
A9: M2F qt = qm and
A10: M2F rt = rm;
reconsider PQR = <*<*p`1,p`2,p`3*>,<*q`1,q`2,q`3*>,<*r`1,r`2,r`3*>*>
as Matrix of 3,F_Real by Th16;
Det M is unital by A1, LAPLACE:34;
then Det M is non zero; then
A11: Det M <> 0.F_Real by STRUCT_0:def 12;
A12: pm = <*pm`1,pm`2,pm`3*> & qm = <*qm`1,qm`2,qm`3*> &
rm = <*rm`1,rm`2,rm`3*> by EUCLID_5:3;
p = <*p`1,p`2,p`3*> & q = <*q`1,q`2,q`3*> &
r = <*r`1,r`2,r`3*> by EUCLID_5:3;
then PQR@ = <*<*p`1,q`1,r`1*>,<*p`2,q`2,r`2*>,<*p`3,q`3,r`3*>*>
by Th20; then
A13: (M * (PQR@))@ = <* pm,qm,rm *> by A8,A9,A10,A2,A3,A4,A5,A6,A7,Th77;
A14: Det (M * (PQR@))@ = Det (M * (PQR)@) by MATRIXR2:43
.= Det M * Det (PQR)@ by MATRIXR2:45
.= Det M * Det PQR by MATRIXR2:43;
Det PQR = 0.F_Real iff Det ((M * (PQR@))@) = 0.F_Real
proof
thus Det PQR = 0.F_Real implies Det((M * (PQR@))@) = 0.F_Real by A14;
assume Det((M * (PQR@))@) = 0.F_Real;
then (Det M)" * (Det M * Det PQR) = Det M * 0.F_Real by A14;
then (Det M)" * Det M * Det PQR = 0.F_Real;
then 1.F_Real * Det PQR = 0.F_Real by A11,VECTSP_1:def 10;
hence Det PQR = 0.F_Real;
end;
then |{p,q,r}| = 0.F_Real iff |{pm,qm,rm}| = 0.F_Real by A13,A12,Th29;
hence thesis by STRUCT_0:def 6;
end;
theorem Th79:
0 < m implies
for M being Matrix of m,1,F_Real holds M is FinSequence of 1-tuples_on REAL
proof
assume
A0: 0 < m;
let M be Matrix of m,1,F_Real;
A1: len M = m by A0,MATRIX_0:23;
width M = 1 by A0,MATRIX_0:23;
then consider s be FinSequence such that
A2: s in rng M and
A3: len s = 1 by A0,A1,MATRIX_0:def 3;
consider n be Nat such that
A4: for x be object st x in rng M
ex s be FinSequence st s = x & len s = n by MATRIX_0:def 1;
consider s1 be FinSequence such that
A5: s1 = s and
A6: len s1 = n by A4,A2;
rng M c= 1-tuples_on REAL
proof
let x be object;
assume
A7: x in rng M;
then consider s being FinSequence such that
A8: s = x and
A9: len s = n by A4;
consider n0 be Nat such that
A10: for x be object st x in rng M ex p be FinSequence of F_Real st
x = p & len p = n0 by MATRIX_0:9;
consider p be FinSequence of F_Real such that
A11: x = p and
len p = n0 by A10,A7;
rng p c= REAL;
hence thesis by A11,A8,A9,A5,A6,A3,FINSEQ_2:132;
end;
hence thesis by FINSEQ_1:def 4;
end;
theorem Th80:
for uf being FinSequence of F_Real st len uf = 3 holds
<*uf*>@ = 1.(F_Real,3) * (<*uf*>@)
proof
let uf be FinSequence of F_Real;
assume
A1: len uf = 3;
then
A2: <*uf*>@ = <* <* uf.1 *>, <* uf.2 *> , <* uf.3 *> *> by Th63; then
A3: len (<*uf*>@) = 3 by FINSEQ_1:45;
set M = 1.(F_Real,3);
uf is 3-element by A1,CARD_1:def 7; then
A4: uf in REAL 3 by EUCLID_9:2;
now
A5: M * <*uf*>@ is Matrix of 3,1,F_Real by A4,EUCLID_8:50,Th74;
hence len (1.(F_Real,3) * (<*uf*>@)) = 3 by MATRIX_0:23;
thus (1.(F_Real,3) * (<*uf*>@)).1 = <* uf.1 *>
proof
1 in Seg 3 by FINSEQ_1:1; then
A6: (M * (<*uf*>@)).1 = Line(M * (<*uf*>@),1) by A5,MATRIX_0:52;
now
thus len Line(M * (<*uf*>@),1) = width (M * (<*uf*>@))
by MATRIX_0:def 7
.= 1 by A5,MATRIX_0:23;
thus Line(M * (<*uf*>@),1).1 = uf.1
proof
A7: [1,1] in Indices(M * (<*uf*>@)) by A5,MATRIX_0:23,Th2;
A8: width M = len (<*uf*>@) by A3,MATRIX_0:23;
reconsider a1 = 1,a2 = 0 as Element of F_Real;
A9: Line(M,1) = <* a1,a2,a2 *> & uf =<* uf.1,uf.2,uf.3 *>
by Th56,A1,FINSEQ_1:45;
dom uf = Seg 3 by A1,FINSEQ_1:def 3;
then reconsider uf1 = uf.1, uf2 = uf.2,
uf3 = uf.3 as Element of F_Real by FINSEQ_1:1,FINSEQ_2:11;
A10: Line(M,1) "*" uf = a1 * uf1 + a2 * uf2 + a2 * uf3 by A9,Th6
.= uf.1;
1 in Seg 1 by FINSEQ_1:1;
then 1 in Seg width (M * (<*uf*>@)) by A5,MATRIX_0:23;
then Line(M * (<*uf*>@),1).1 = (M * (<*uf*>@))*(1,1)
by MATRIX_0:def 7
.= Line(M,1) "*" Col( <*uf*>@,1)
by A7,A8,MATRIX_3:def 4
.= Line(M,1) "*" uf by Th76;
hence thesis by A10;
end;
end;
hence thesis by A6,FINSEQ_1:40;
end;
thus (1.(F_Real,3) * (<*uf*>@)).2 = <* uf.2 *>
proof
2 in Seg 3 by FINSEQ_1:1; then
A11: (M * (<*uf*>@)).2 = Line(M * (<*uf*>@),2) by A5,MATRIX_0:52;
now
thus len Line(M * (<*uf*>@ ),2) = width (M * (<*uf*>@))
by MATRIX_0:def 7
.= 1 by A5,MATRIX_0:23;
thus Line(M * (<*uf*>@),2).1 = uf.2
proof
A12: [2,1] in Indices(M * (<*uf*>@)) by A5,MATRIX_0:23,Th2;
A13: width M = len (<*uf*>@) by A3,MATRIX_0:23;
reconsider a1 = 1,a2 = 0 as Element of F_Real;
A14: Line(M,2) = <* a2,a1,a2 *> & uf =<* uf.1,uf.2,uf.3 *>
by Th56,A1,FINSEQ_1:45;
dom uf = Seg 3 by A1,FINSEQ_1:def 3;
then reconsider uf1 = uf.1,uf2 = uf.2,
uf3 = uf.3 as Element of F_Real by FINSEQ_1:1,FINSEQ_2:11;
A15: Line(M,2) "*" uf = a2 * uf1 + a1 * uf2 + a2 * uf3 by A14,Th6
.= uf.2;
1 in Seg 1 by FINSEQ_1:1;
then 1 in Seg width (M * (<*uf*>@)) by A5,MATRIX_0:23;
then Line(M * (<*uf*>@),2).1 = (M * (<*uf*>@))*(2,1)
by MATRIX_0:def 7
.= Line(M,2) "*" Col( <*uf*>@,1)
by A12,A13,MATRIX_3:def 4
.= Line(M,2) "*" uf by Th76;
hence thesis by A15;
end;
end;
hence thesis by A11,FINSEQ_1:40;
end;
thus (1.(F_Real,3) * (<*uf*>@)).3 = <* uf.3 *>
proof
3 in Seg 3 by FINSEQ_1:1; then
A16: (M * (<*uf*>@)).3 = Line(M * (<*uf*>@),3) by A5,MATRIX_0:52;
now
thus len Line(M * (<*uf*>@),3) = width (M * (<*uf*>@))
by MATRIX_0:def 7
.= 1 by A5,MATRIX_0:23;
thus Line(M * (<*uf*>@),3).1 = uf.3
proof
A17: [3,1] in Indices(M * (<*uf*>@)) by A5,MATRIX_0:23,Th2;
A18: width M = len (<*uf*>@) by A3,MATRIX_0:23;
reconsider a1 = 1,a2 = 0 as Element of F_Real;
A19: Line(M,3) = <* a2,a2,a1 *> & uf =<* uf.1,uf.2,uf.3 *>
by Th56,A1,FINSEQ_1:45;
dom uf = Seg 3 by A1,FINSEQ_1:def 3;
then reconsider uf1 = uf.1, uf2 = uf.2,
uf3 = uf.3 as Element of F_Real by FINSEQ_1:1,FINSEQ_2:11;
A20: Line(M,3) "*" uf = a2 * uf1 + a2 * uf2 + a1 * uf3 by A19,Th6
.= uf.3;
1 in Seg 1 by FINSEQ_1:1;
then 1 in Seg width (M * (<*uf*>@)) by A5,MATRIX_0:23;
then Line(M * (<*uf*>@),3).1 = (M * (<*uf*>@))*(3,1)
by MATRIX_0:def 7
.= Line(M,3) "*" Col( <*uf*>@,1)
by A17,A18,MATRIX_3:def 4
.= Line(M,3) "*" uf by Th76;
hence thesis by A20;
end;
end;
hence thesis by A16,FINSEQ_1:40;
end;
end;
hence thesis by A2,FINSEQ_1:45;
end;
theorem Th81:
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
proof
let u be Element of TOP-REAL 3;
let uf be FinSequence of F_Real;
assume that
A1: u = uf and
A2: <*uf*>@ = <* <* 0 *>, <* 0 *>, <* 0 *> *>;
u in TOP-REAL 3;
then u in REAL 3 by EUCLID:22; then
A3: u in 3-tuples_on REAL by EUCLID:def 1; then
A4: len uf = 3 by A1,FINSEQ_2:133;
<*uf*>@ = <* <* uf.1 *>, <* uf.2 *> , <* uf.3 *> *>
by A3,A1,FINSEQ_2:133,Th63;
then <* uf.1 *> = <* 0 *> & <* uf.2 *> = <* 0 *> &
<* uf.3 *> = <* 0 *> by A2,FINSEQ_1:78;
then uf.1 = 0 & uf.2 = 0 & uf.3 = 0 by FINSEQ_1:76;
hence thesis by A1,A4,FINSEQ_1:45,EUCLID_5:4;
end;
theorem Th82:
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
proof
let N be invertible Matrix of 3,F_Real;
let u,mu be Element of TOP-REAL 3;
let uf be FinSequence of F_Real;
let ut be FinSequence of 1-tuples_on REAL;
assume that
A1: u is non zero and
A2: u = uf and
A3: ut = N * uf and
A4: mu = M2F ut;
uf in TOP-REAL 3 by A2; then
A5: uf in REAL 3 by EUCLID:22;
A6: len uf = 3 by A5,EUCLID_8:50;
A7: width <*uf*> = 3 by A6,Th61; then
A8: len (<*uf*>@) = width <*uf*> by MATRIX_0:29
.= len uf by MATRIX_0:23; then
A9: len (<*uf*>@) = 3 by A5,EUCLID_8:50;
A10: len <*uf*> = 1 by MATRIX_0:23; then
A11: len (<*uf*>@) = 3 & width(<*uf*>@) = 1 by A7,MATRIX_0:29;
width N = 3 by MATRIX_0:24;
then len(N * (<*uf*>@)) = len N &
width (N * (<*uf*>@)) = width(<*uf*>@) by A11,MATRIX_3:def 4; then
A12: len(N * (<*uf*>@)) = 3 &
width (N * (<*uf*>@)) = 1 by A10,A7,MATRIX_0:29,MATRIX_0:24;
A13: width N = 3 by MATRIX_0:24
.= len (<*uf*>@) by A8,A5,EUCLID_8:50;
A14: len ut = len (N * (<*uf*>@)) by A3,LAPLACE:def 9
.= len N by A13,MATRIX_3:def 4
.= 3 by MATRIX_0:23;
assume
A15: mu is zero;
reconsider MU = M2F ut as FinSequence of REAL;
A16: ut = F2M (MU) by A14,Th69
.= <* <* 0 *>,<* 0 *>,<* 0 *> *> by A15,A4,EUCLID_5:4,Th65;
A17: (N~) is_reverse_of N by MATRIX_6:def 4;
A18: width (N~) = 3 by MATRIX_0:24;
A19: len N = 3 & width N = 3 by MATRIX_0:24;
A20: 1.(F_Real,3) * (<*uf*>@) = (N~) * N * (<*uf*>@) by A17,MATRIX_6:def 2
.= (N~) * (N * (<*uf*>@))
by A9,A18,A19,MATRIX_3:33;
A21: N * (<*uf*>@) is Matrix of 3,1,F_Real by A12,MATRIX_0:20;
N * (<*uf*>@) = <* <* 0 *>, <* 0 *>, <* 0 *> *> by LAPLACE:def 9,A3,A16;
then (N~) * (N * (<*uf*>@)) = <* <* 0 *>, <* 0 *>, <* 0 *> *>
by Th7,A21;
then <*uf*>@ = <* <* 0 *>, <* 0 *>, <* 0 *> *>
by A20,Th80,A5,EUCLID_8:50;
hence thesis by A1,A2,Th81;
end;
definition
let N be invertible Matrix of 3,F_Real;
func homography(N) -> Function of ProjectiveSpace TOP-REAL 3,
ProjectiveSpace TOP-REAL 3 means
:DEF4:
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;
existence
proof
defpred P[object,object] means
ex x be Point of ProjectiveSpace TOP-REAL 3 st x = $1 &
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 & $2 = Dir v;
A1: for x be object st x in the carrier of ProjectiveSpace TOP-REAL 3
ex y be object st y in the carrier of ProjectiveSpace TOP-REAL 3 & P[x,y]
proof
let x be object;
assume x in the carrier of ProjectiveSpace TOP-REAL 3;
then reconsider x1 = x as Element of ProjectiveSpace TOP-REAL 3;
consider u be Element of TOP-REAL 3 such that
A2: u is non zero and
A3: x1 = Dir u by ANPROJ_1:26;
reconsider uf = u as FinSequence of F_Real by EUCLID:24;
A4: N * (<*uf*>@) is (3,1)-size by FINSEQ_3:153,Th74;
A5: N * (<*uf*>@) is Matrix of 3,1,F_Real by FINSEQ_3:153,Th74;
N * (<*uf*>@) is FinSequence of 1-tuples_on REAL by A4,Th79;
then reconsider p = N * uf as FinSequence of 1-tuples_on REAL
by LAPLACE:def 9;
A6: the carrier of ProjectiveSpace TOP-REAL 3
= ProjectivePoints(TOP-REAL 3) by ANPROJ_1:23;
len p = len (N * <*uf*>@) by LAPLACE:def 9
.= 3 by A5,MATRIX_0:23;
then reconsider v = M2F p as Element of TOP-REAL 3 by Th66;
set y = Dir v;
A7: y is Element of ProjectivePoints(TOP-REAL 3) by A2,Th82,ANPROJ_1:21;
now
take x1;
thus x1 = x;
now
take u,v,uf,p;
thus x1 = Dir u by A3;
thus u is not zero by A2;
thus u = uf;
thus p = N * uf;
thus v = M2F p;
thus v is not zero by A2,Th82;
thus y = Dir v;
end;
hence ex u,v being Element of TOP-REAL 3,
uf being FinSequence of F_Real,
p being FinSequence of 1-tuples_on REAL st
x1 = Dir u & u is not zero & u = uf & p = N * uf &
v = M2F p & v is not zero & y = Dir v;
end;
hence thesis by A7,A6;
end;
ex f be Function of the carrier of ProjectiveSpace TOP-REAL 3,
the carrier of ProjectiveSpace TOP-REAL 3 st for x be object st
x in the carrier of ProjectiveSpace TOP-REAL 3 holds P[x,f.x]
from FUNCT_2:sch 1(A1);
then consider f be Function of the carrier of ProjectiveSpace TOP-REAL 3,
the carrier of ProjectiveSpace TOP-REAL 3 such that
A8: for x be object st x in the carrier of ProjectiveSpace TOP-REAL 3
holds P[x,f.x];
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 &
f.x = Dir v
proof
let x be Point of ProjectiveSpace TOP-REAL 3;
P[x,f.x] by A8;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of ProjectiveSpace TOP-REAL 3,
ProjectiveSpace TOP-REAL 3 such that
A9: 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 & f1.x = Dir v and
A10: 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 & f2.x = Dir v;
now
reconsider g1 = f1 as Function of the carrier of ProjectiveSpace
TOP-REAL 3,the carrier of ProjectiveSpace TOP-REAL 3;
dom g1 = the carrier of ProjectiveSpace TOP-REAL 3 by FUNCT_2:def 1;
hence dom f1 = dom f2 by FUNCT_2:def 1;
hereby
let x be object;
assume
A11: x in dom f1;
then consider u1,v1 being Element of TOP-REAL 3,
uf1 being FinSequence of F_Real,
p1 being FinSequence of 1-tuples_on REAL
such that
A12: x = Dir u1 and
A13: u1 is not zero and
A14: u1 = uf1 and
A15: p1 = N * uf1 and
A16: v1 = M2F p1 and
v1 is not zero and
A17: f1.x = Dir v1 by A9;
consider u2,v2 being Element of TOP-REAL 3,
uf2 being FinSequence of F_Real,
p2 being FinSequence of 1-tuples_on REAL
such that
A18: x = Dir u2 and
A19: u2 is not zero and
A20: u2 = uf2 and
A21: p2 = N * uf2 and
A22: v2 = M2F p2 and
v2 is not zero and
A23: f2.x = Dir v2 by A11,A10;
are_Prop u1,u2 by A12,A13,A18,A19,ANPROJ_1:22;
then consider a be Real such that
A24: a <> 0 and
A25: u1 = a * u2 by ANPROJ_1:1;
B01: width N = 3 by MATRIX_0:23;
A26: now
len uf1 = 3 by A14,FINSEQ_3:153;
then width <*uf1*> = 3 by Th61;
hence len (<*uf1*>@) = width <*uf1*> by MATRIX_0:29
.= len uf1 by MATRIX_0:23
.= 3 by A14,FINSEQ_3:153;
end;
A27: now
len uf2 = 3 by A20,FINSEQ_3:153;
then width <*uf2*> = 3 by Th61;
hence len (<*uf2*>@) = width <*uf2*> by MATRIX_0:29
.= len uf2 by MATRIX_0:23
.= 3 by A20,FINSEQ_3:153;
end;
A28: len p2 = len (N * (<*uf2*>@)) by A21,LAPLACE:def 9
.= len N by B01,A27,MATRIX_3:def 4;
now
M2F p1 = a * v2
proof
len p2 = 3 by A28,MATRIX_0:23; then
consider q1,q2,q3 be Real such that
A29: q1 = (p2.1).1 & q2 = (p2.2).1 & q3 = (p2.3).1 and
A30: a * p2 = <* <* a * q1 *>, <* a * q2 *> , <* a * q3 *> *> by DEF3;
A31: len (a * p2) = 3 by A30,FINSEQ_1:45;
A32: N * (<*uf1*>@) is Matrix of 3,1,F_Real by A14,FINSEQ_3:153,Th74;
then
A33: Indices (N * <*uf1*>@) = [:Seg 3,Seg 1:] by MATRIX_0:23;
A34: N * (<*uf2*>@) is (3,1)-size by A20,FINSEQ_3:153,Th74;
A35: len p1 = len (N * <*uf1*>@) by A15,LAPLACE:def 9
.= 3 by A32,MATRIX_0:23;
A36: p1 = a * p2
proof
p1 = <* <* a * q1 *>,<* a * q2 *>,<* a * q3 *> *>
proof
A37: p1 = N * (<*uf1*>@) by A15,LAPLACE:def 9; then
A38: len p1 = len N by B01,A26,MATRIX_3:def 4 .= 3 by MATRIX_0:23;
A39: p2 = N * (<*uf2*>@) by A21,LAPLACE:def 9;
A40: N * (<*uf1*>@) is Matrix of 3,1,F_Real
by A14,FINSEQ_3:153,Th74;
A41: 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1;
A42: Seg width (N * (<*uf1*>@)) = Seg 1 by A32,MATRIX_0:23;
A43: N * (<*uf2*>@) is Matrix of 3,1,F_Real
by A20,FINSEQ_3:153,Th74;
A44: 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 by FINSEQ_1:1;
A45: Seg width (N * (<*uf2*>@)) = Seg 1 by A43,MATRIX_0:23;
now
thus len p1 = 3 by A38;
thus p1.1 = <*a * q1*>
proof
A46: [1,1] in Indices (N * <*uf2*>@) by Th2,A34,MATRIX_0:23;
A47: p1.1 = Line(N * (<*uf1*>@),1)
by A37,A40,A41,MATRIX_0:52; then
A48: len (p1.1) = width (N * (<*uf1*>@)) by MATRIX_0:def 7
.= 1 by A40,MATRIX_0:23;
A49: (p1.1).1 = (N * (<*uf1*>@))*(1,1)
by A47,FINSEQ_1:1,A42,MATRIX_0:def 7
.= Line(N,1) "*" Col(<*uf1*>@,1)
by B01,A26,Th2,A33,MATRIX_3:def 4;
A50: p2.1 = Line(N * (<*uf2*>@),1) by A39,A43,A44,MATRIX_0:52;
A51: (p2.1).1 = (N * (<*uf2*>@))*(1,1)
by A50,FINSEQ_1:1,A45,MATRIX_0:def 7
.= Line(N,1) "*" Col(<*uf2*>@,1)
by B01,A46,A27,MATRIX_3:def 4;
Line(N,1) "*" Col(<*uf1*>@,1) =
a * (Line(N,1) "*" Col(<*uf2*>@,1))
proof
A52: u1`1 = u1.1 & u1`2 = u1.2 & u1`3 = u1.3
by EUCLID_5:def 1,EUCLID_5:def 2,EUCLID_5:def 3;
A53: u1 = |[ u1.1,u1.2,u1.3 ]| by A52,EUCLID_5:3;
u2`1 = u2.1 & u2`2 = u2.2 & u2`3 = u2.3
by EUCLID_5:def 1,EUCLID_5:def 2,EUCLID_5:def 3; then
A54: u2 = |[ u2.1,u2.2,u2.3 ]| by EUCLID_5:3;
A55: u1 = |[ a * u2.1,a * u2.2,a * u2.3 ]|
by A25,A54,EUCLID_5:8;
A56: Col(<*uf1*>@,1) = u1 & Col(<*uf2*>@,1) = u2
by Th76,A14,A20;
A57: len Line(N,1) = width N by MATRIX_0:def 7
.= 3 by MATRIX_0:23;
now
thus len Line(N,1) = 3 by A57;
Seg width N = Seg 3 by MATRIX_0:23;
hence Line(N,1).1 = N*(1,1) & Line(N,1).2 = N*(1,2) &
Line(N,1).3 = N*(1,3) by FINSEQ_1:1,MATRIX_0:def 7;
end;
then
A58: Line(N,1) = <* N*(1,1),N*(1,2),N*(1,3) *> by FINSEQ_1:45;
reconsider z1 = u1.1, z2 = u1.2, z3 = u1.3,
z4 = u2.1, z5 = u2.2, z6 = u2.3 as Element of F_Real
by XREAL_0:def 1;
A59: Line(N,1) "*" Col(<*uf1*>@,1) =
N*(1,1) * z1 + N*(1,2) * z2 + N*(1,3) * z3
by A58,A53,A56,Th6;
A60: Line(N,1) "*" Col(<*uf2*>@,1) =
N*(1,1) * z4 + N*(1,2) * z5 + N*(1,3) * z6
by A54,A58,A56,Th6;
u1.1 = a * u2.1 & u1.2 = a * u2.2 & u1.3 = a * u2.3
by A55;
hence thesis by A59,A60;
end;
hence thesis by A29,A51,A48,FINSEQ_1:40,A49;
end;
thus p1.2 = <*a * q2*>
proof
A61: [2,1] in Indices (N * <*uf2*>@) by Th2,A34,MATRIX_0:23;
A62: [2,1] in Indices (N * <*uf1*>@) by Th2,A32,MATRIX_0:23;
A63: p1.2 = Line(N * (<*uf1*>@),2) by A37,A40,A41,MATRIX_0:52;
then
A64: len (p1.2) = width (N * (<*uf1*>@)) by MATRIX_0:def 7
.= 1 by A40,MATRIX_0:23;
A65: (p1.2).1 = (N * (<*uf1*>@))*(2,1)
by A63,FINSEQ_1:1,A42,MATRIX_0:def 7
.= Line(N,2) "*" Col(<*uf1*>@,1)
by B01,A26,A62,MATRIX_3:def 4;
p2.2 = Line(N * (<*uf2*>@),2) by A39,A43,A44,MATRIX_0:52;
then
A66: (p2.2).1 = (N * (<*uf2*>@))*(2,1)
by FINSEQ_1:1,A45,MATRIX_0:def 7
.= Line(N,2) "*" Col(<*uf2*>@,1)
by B01,A27,A61,MATRIX_3:def 4;
Line(N,2) "*" Col(<*uf1*>@,1) =
a * (Line(N,2) "*" Col(<*uf2*>@,1))
proof
u1`1 = u1.1 & u1`2 = u1.2 & u1`3 = u1.3
by EUCLID_5:def 1,EUCLID_5:def 2,EUCLID_5:def 3;
then
A67: u1 = |[ u1.1,u1.2,u1.3 ]| by EUCLID_5:3;
u2`1 = u2.1 & u2`2 = u2.2 & u2`3 = u2.3
by EUCLID_5:def 1,EUCLID_5:def 2,EUCLID_5:def 3;
then
A68: u2 = |[ u2.1,u2.2,u2.3 ]| by EUCLID_5:3; then
A69: u1 = |[ a * u2.1,a * u2.2,a * u2.3 ]| by A25,EUCLID_5:8;
A70: Col(<*uf1*>@,1) = u1 & Col(<*uf2*>@,1) = u2
by Th76,A14,A20;
A71: len Line(N,2) = width N by MATRIX_0:def 7
.= 3 by MATRIX_0:23;
now
thus len Line(N,2) = 3 by A71;
Seg width N = Seg 3 by MATRIX_0:23;
hence Line(N,2).1 = N*(2,1) &
Line(N,2).2 = N*(2,2) &
Line(N,2).3 = N*(2,3) by FINSEQ_1:1,MATRIX_0:def 7;
end;
then
A72: Line(N,2) = <* N*(2,1),N*(2,2),N*(2,3) *> by FINSEQ_1:45;
reconsider z1 = u1.1, z2 = u1.2, z3 = u1.3,
z4 = u2.1, z5 = u2.2, z6 = u2.3 as Element of F_Real
by XREAL_0:def 1;
A73: Line(N,2) "*" Col(<*uf1*>@,1) =
N*(2,1) * z1 + N*(2,2) * z2 + N*(2,3) * z3
by A72,A67,A70,Th6;
A74: Line(N,2) "*" Col(<*uf2*>@,1) =
N*(2,1) * z4 + N*(2,2) * z5 + N*(2,3) * z6
by A68,A72,A70,Th6;
u1.1 = a * u2.1 & u1.2 = a * u2.2 & u1.3 = a * u2.3
by A69;
hence thesis by A73,A74;
end;
hence thesis by A64,FINSEQ_1:40,A65,A29,A66;
end;
thus p1.3 = <*a * q3*>
proof
A75: [3,1] in Indices (N * <*uf2*>@) by Th2,A34,MATRIX_0:23;
A76: [3,1] in Indices (N * <*uf1*>@) by Th2,A32,MATRIX_0:23;
A77: p1.3 = (N * (<*uf1*>@)).3 by A15,LAPLACE:def 9
.= Line(N * (<*uf1*>@),3) by A40,A41,MATRIX_0:52; then
A78: len (p1.3) = width (N * (<*uf1*>@)) by MATRIX_0:def 7
.= 1 by A40,MATRIX_0:23;
A79: (p1.3).1 = (N * (<*uf1*>@))*(3,1)
by A77,FINSEQ_1:1,A42,MATRIX_0:def 7
.= Line(N,3) "*" Col(<*uf1*>@,1)
by B01,A26,A76,MATRIX_3:def 4;
p2.3 = (N * (<*uf2*>@)).3 by A21,LAPLACE:def 9
.= Line(N * (<*uf2*>@),3) by A43,A44,MATRIX_0:52; then
A80: (p2.3).1 = (N * (<*uf2*>@))*(3,1)
by FINSEQ_1:1,A45,MATRIX_0:def 7
.= Line(N,3) "*" Col(<*uf2*>@,1)
by B01,A27,A75,MATRIX_3:def 4;
Line(N,3) "*" Col(<*uf1*>@,1) =
a * (Line(N,3) "*" Col(<*uf2*>@,1))
proof
u1`1 = u1.1 & u1`2 = u1.2 & u1`3 = u1.3
by EUCLID_5:def 1,EUCLID_5:def 2,EUCLID_5:def 3;
then
A81: u1 = |[ u1.1,u1.2,u1.3 ]| by EUCLID_5:3;
u2`1 = u2.1 & u2`2 = u2.2 & u2`3 = u2.3
by EUCLID_5:def 1,EUCLID_5:def 2,EUCLID_5:def 3;
then
A82: u2 = |[ u2.1,u2.2,u2.3 ]| by EUCLID_5:3;
A83: u1 = |[ a * u2.1,a * u2.2,a * u2.3 ]|
by A25,A82,EUCLID_5:8;
A84: Col(<*uf1*>@,1) = u1 & Col(<*uf2*>@,1) = u2
by Th76,A14,A20;
A85: len Line(N,3) = width N by MATRIX_0:def 7
.= 3 by MATRIX_0:23;
now
thus len Line(N,3) = 3 by A85;
Seg width N = Seg 3 by MATRIX_0:23;
hence Line(N,3).1 = N*(3,1) & Line(N,3).2 = N*(3,2) &
Line(N,3).3 = N*(3,3) by FINSEQ_1:1,MATRIX_0:def 7;
end;
then
A86: Line(N,3) = <* N*(3,1),N*(3,2),N*(3,3) *> by FINSEQ_1:45;
reconsider z1 = u1.1, z2 = u1.2, z3 = u1.3,
z4 = u2.1, z5 = u2.2,
z6 = u2.3 as Element of F_Real by XREAL_0:def 1;
A87: Line(N,3) "*" Col(<*uf1*>@,1) =
N*(3,1) * z1 + N*(3,2) * z2 + N*(3,3) * z3
by A86,A81,A84,Th6;
A88: Line(N,3) "*" Col(<*uf2*>@,1) =
N*(3,1) * z4 + N*(3,2) * z5 + N*(3,3) * z6
by A82,A86,A84,Th6;
u1.1 = a * u2.1 & u1.2 = a * u2.2 &
u1.3 = a * u2.3 by A83;
hence thesis by A87,A88;
end;
hence thesis by A78,A79,A29,A80,FINSEQ_1:40;
end;
end;
hence thesis by FINSEQ_1:45;
end;
hence thesis by A30;
end;
a * v2 = M2F (a * p2) by A28,MATRIX_0:23,A22,Th67
.= <* (p1.1).1, (p1.2).1, (p1.3).1 *> by A31,DEF2,A36;
hence thesis by A35,DEF2;
end;
hence v1 = a * v2 by A16;
thus v1 is non zero by A13,A14,A15,A16,Th82;
thus v2 is non zero by A19,A20,A21,A22,Th82;
end;
then are_Prop v1,v2 & v1 is not zero & v2 is not zero by A24,ANPROJ_1:1;
hence f1.x = f2.x by A17,A23,ANPROJ_1:22;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
end;
theorem
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
proof
let N be invertible Matrix of 3,F_Real;
let p,q,r be Point of ProjectiveSpace TOP-REAL 3;
thus p,q,r are_collinear implies
homography(N).p, homography(N).q, homography(N).r are_collinear
proof
assume
A1: p,q,r are_collinear;
consider up,vp being Element of TOP-REAL 3,
ufp being FinSequence of F_Real,
pp being FinSequence of 1-tuples_on REAL
such that
A2: p = Dir up and
A3: up is not zero and
A4: up = ufp and
A5: pp = N * ufp and
A6: vp = M2F pp and
vp is not zero and
A7: homography(N).p = Dir vp by DEF4;
consider uq,vq being Element of TOP-REAL 3,
ufq being FinSequence of F_Real,
pq being FinSequence of 1-tuples_on REAL such that
A8: q = Dir uq and
A9: uq is not zero and
A10: uq = ufq and
A11: pq = N * ufq and
A12: vq = M2F pq and
vq is not zero and
A13: homography(N).q = Dir vq by DEF4;
consider ur,vr being Element of TOP-REAL 3,
ufr being FinSequence of F_Real,
pr being FinSequence of 1-tuples_on REAL such that
A14: r = Dir ur and
A15: ur is not zero and
A16: ur = ufr and
A17: pr = N * ufr and
A18: vr = M2F pr and
vr is not zero and
A19: homography(N).r = Dir vr by DEF4;
consider u,v,w be Element of TOP-REAL 3 such that
A20: p = Dir u and
A21: q = Dir v and
A22: r = Dir w and
A23: u is not zero and
A24: v is not zero and
A25: w is not zero and
A26: u,v,w are_LinDep by A1,ANPROJ_2:23;
A27: |{u,v,w}| = 0 by A26,Th37;
are_Prop up,u by A20,A2,A23,A3,ANPROJ_1:22;
then consider ap be Real such that
ap <> 0 and
A28: up = ap * u by ANPROJ_1:1;
are_Prop uq,v by A8,A21,A24,A9,ANPROJ_1:22;
then consider aq be Real such that
aq <> 0 and
A29: uq = aq * v by ANPROJ_1:1;
are_Prop ur, w by A22,A14,A25,A15,ANPROJ_1:22;
then consider ar be Real such that
ar <> 0 and
A30: ur = ar * w by ANPROJ_1:1;
A31: |{ up,uq,ur }| = ap * |{u,aq * v,ar * w}| by Th26,A28,A29,A30
.= ap * (aq *|{u,v,ar * w}|) by Th27
.= ap * (aq * (ar * |{u,v,w}|)) by Th28
.= 0 by A27;
reconsider pf = up,qf = uq,rf = ur as FinSequence of F_Real by EUCLID:24;
A32: N * pf = N * (<*pf*>@) & N * qf = N * (<*qf*>@) &
N * rf = N * (<*rf*>@) by LAPLACE:def 9;
A33: len pf = 3 & len qf = 3 & len rf = 3 by FINSEQ_3:153;
N * (<*pf*>@) is Matrix of 3,1,F_Real &
N * (<*qf*>@) is Matrix of 3,1,F_Real &
N * (<*rf*>@) is Matrix of 3,1,F_Real by FINSEQ_3:153,Th74;
then reconsider pt = N * pf, qt = N * qf,
rt = N * rf as FinSequence of 1-tuples_on REAL by A32,Th79;
A34: pt = N * (<*pf*>@) & qt = N * (<*qf*>@) & rt = N * (<*rf*>@)
by LAPLACE:def 9;
A35: width N = 3 by MATRIX_0:23;
width <*pf*> = 3 by A33,Th61; then
A36: len (<*pf*>@) = width <*pf*> by MATRIX_0:29
.= len pf by MATRIX_0:23
.= 3 by FINSEQ_3:153;
width <*qf*> = 3 by A33,Th61; then
A37: len (<*qf*>@) = width <*qf*> by MATRIX_0:29
.= len qf by MATRIX_0:23
.= 3 by FINSEQ_3:153;
width <*rf*> = 3 by A33,Th61;
then len (<*rf*>@) = width <*rf*> by MATRIX_0:29
.= len rf by MATRIX_0:23
.= 3 by FINSEQ_3:153;
then len pt = len N & len qt = len N & len rt = len N
by A35,A37,A36,A34,MATRIX_3:def 4;
then reconsider pm = M2F pt,qm = M2F qt,
rm = M2F rt as Element of TOP-REAL 3 by MATRIX_0:23,Th66;
A38: |{ pm,qm,rm }| = 0 by A31,Th78;
pm is not zero & qm is not zero & rm is not zero
by A3,A9,A15,Th82;
hence thesis by A38,Th37,ANPROJ_2:23,A6,A12,A18,A7,A13,A19,
A4,A5,A10,A11,A16,A17;
end;
thus homography(N).p, homography(N).q, homography(N).r are_collinear
implies p,q,r are_collinear
proof
assume
A39: homography(N).p, homography(N).q, homography(N).r are_collinear;
consider up,vp being Element of TOP-REAL 3,
ufp being FinSequence of F_Real,
pp being FinSequence of 1-tuples_on REAL
such that
A40: p = Dir up and
A41: up is not zero and
A42: up = ufp and
A43: pp = N * ufp and
A44: vp = M2F pp and
A45: vp is not zero and
A46: homography(N).p = Dir vp by DEF4;
consider uq,vq being Element of TOP-REAL 3,
ufq being FinSequence of F_Real,
pq being FinSequence of 1-tuples_on REAL such that
A47: q = Dir uq and
A48: uq is not zero and
A49: uq = ufq and
A50: pq = N * ufq and
A51: vq = M2F pq and
A52: vq is not zero and
A53: homography(N).q = Dir vq by DEF4;
consider ur,vr being Element of TOP-REAL 3,
ufr being FinSequence of F_Real,
pr being FinSequence of 1-tuples_on REAL such that
A54: r = Dir ur and
A55: ur is not zero and
A56: ur = ufr and
A57: pr = N * ufr and
A58: vr = M2F pr and
A59: vr is not zero and
A60: homography(N).r = Dir vr by DEF4;
consider u,v,w being Point of TOP-REAL 3 such that
A61: homography(N).p = Dir(u) and
A62: homography(N).q = Dir(v) and
A63: homography(N).r = Dir(w) and
A64: u is not zero & v is not zero & w is not zero and
A65: (u = v or u = w or v = w or {u,v,w} is linearly-dependent) by A39,Th9;
u,v,w are_LinDep by A65,Th8;
then |{ u,v,w }| = 0 by Th37;
then |{ u,v,vr }| = 0 by A63,A60,A64,Th50,A59;
then |{ u,vq,vr }| = 0 by A62,A53,A64,Th49,A52;
then |{ vp,vq,vr }| = 0 by A61,A46,A64,Th48,A45;
then |{ up,uq,ur }| = 0 by A42,A43,A44,A49,A50,A51,A56,A57,A58,Th78;
then (up = uq or up = ur or uq = ur or {up,uq,ur} is linearly-dependent)
by Th37,Th8;
hence thesis by Th9,A40,A41,A47,A48,A54,A55;
end;
end;