:: The Inner Product and Conjugate of Matrix of Complex Numbers
:: by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received October 10, 2005
:: Copyright (c) 2005-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 NUMBERS, NAT_1, SUBSET_1, FINSEQ_2, MATRIX_1, ARYTM_3, FINSEQ_1,
TREES_1, RELAT_1, CARD_1, XXREAL_0, ZFMISC_1, XCMPLX_0, COMPLFLD,
MATRIX_5, ARYTM_1, COMPLEX1, QC_LANG1, FUNCT_1, RVSUM_1, BINOP_2, TARSKI,
XBOOLE_0, CARD_3, INCSP_1, FUNCOP_1, SETWISEO, ORDINAL4, PARTFUN1,
MATRIXC1, FUNCT_7;
notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, FUNCT_1,
RELSET_1, FUNCT_2, ZFMISC_1, NAT_D, PARTFUN1, BINOP_1, FUNCOP_1, NAT_1,
FINSEQ_1, FINSEQOP, SEQ_4, COMPLEX1, RVSUM_1, FINSEQ_2, BINOP_2,
MATRIX_5, MATRIX_0, MATRIX_1, MATRIX_3, RLVECT_1, COMPLSP2, SETWOP_2,
COMPLFLD, STRUCT_0, GROUP_1;
constructors SETWISEO, FINSOP_1, MATRIX_3, MATRIX_5, SEQ_4, BINOP_2, BINOP_1,
RVSUM_1, NAT_D, RELSET_1, COMPLSP2, PRE_POLY, REAL_1;
registrations XBOOLE_0, FUNCT_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1,
BINOP_2, FINSEQ_2, COMPLFLD, MATRIX_0, VALUED_0, RELSET_1, XREAL_0,
ORDINAL1, MEMBERED, MATRIX_1;
requirements NUMERALS, SUBSET, REAL, ARITHM;
equalities MATRIX_0, RVSUM_1, VALUED_1, MATRIX_1;
theorems FINSEQ_1, FUNCT_1, NAT_1, MATRIX_0, FINSEQ_2, COMPLEX1, BINOP_2,
FINSEQ_3, XCMPLX_0, ZFMISC_1, SEQ_4, FINSEQOP, COMPLSP2, FUNCOP_1,
FUNCT_2, FINSOP_1, SETWOP_2, FINSEQ_5, XREAL_1, MATRIX_3, COMPLFLD,
MATRIX_4, MATRIX_5, NUMBERS, XBOOLE_1, ORDINAL1, PARTFUN1, XXREAL_0,
XREAL_0, CARD_1, MATRIX_1;
schemes MATRIX_0, FINSEQ_2, FINSEQ_1, FUNCT_2, NAT_1;
begin
reserve i,j,n,k for Nat,
a for Element of COMPLEX,
R1,R2 for Element of i-tuples_on COMPLEX;
definition
let M be Matrix of COMPLEX;
func M*' -> Matrix of COMPLEX means
:Def1:
len it=len M & width it=width M &
for i,j being Nat st [i,j] in Indices M holds it*(i,j) = (M*(i,j))*';
existence
proof
deffunc F(Nat,Nat) = In((M*($1,$2))*',COMPLEX);
consider M1 being Matrix of len M,width M,COMPLEX such that
A1: for i,j st [i,j] in Indices M1 holds M1*(i,j) = F(i,j) from
MATRIX_0:sch 1;
take M1;
thus
A2: len M1=len M by MATRIX_0:def 2;
thus
A3: now
per cases;
suppose
A4: len M= 0;
then width M1=0 by A2,MATRIX_0:def 3;
hence width M1=width M by A4,MATRIX_0:def 3;
end;
suppose
len M>0;
hence width M1=width M by MATRIX_0:23;
end;
end;
A5: dom M = dom M1 by A2,FINSEQ_3:29;
let i,j be Nat;
assume [i,j] in Indices M;
then [i,j] in Indices M1 by A3,A5;
then M1*(i,j) = F(i,j) by A1;
hence thesis;
end;
uniqueness
proof
let M1,M2 be Matrix of COMPLEX;
assume that
A6: len M1=len M and
A7: width M1 =width M and
A8: for i,j st [i,j] in Indices M holds M1*(i,j)=(M*(i,j))*' and
A9: len M2=len M and
A10: width M2 =width M and
A11: for i,j st [i,j] in Indices M holds M2*(i,j)=(M*(i,j))*';
now
let i,j;
assume
A12: [i,j] in Indices M1;
A13: dom M1 = dom M by A6,FINSEQ_3:29;
hence M1*(i,j)=(M*(i,j))*' by A7,A8,A12
.=M2*(i,j) by A7,A11,A12,A13;
end;
hence thesis by A6,A7,A9,A10,MATRIX_0:21;
end;
involutiveness
proof let N,M be Matrix of COMPLEX;
assume that
A14: len N=len M and
A15: width N=width M and
A16: for i,j being Nat st [i,j] in Indices M holds N*(i,j) = (M*(i,j))*';
thus len M=len N by A14;
thus width M=width N by A15;
let i,j be Nat such that
A17: [i,j] in Indices N;
1 <= i & i <= len M & 1 <= j & j <= width M by A14,A15,A17,MATRIX_0:32;
then
A18: [i,j] in Indices M by MATRIX_0:30;
thus M*(i,j) = (M*(i,j))*'*'
.= (N*(i,j))*' by A18,A16;
end;
end;
theorem Th1:
for M be tabular FinSequence holds [i,j] in Indices M iff 1<= i &
i<=len M & 1<=j & j<=width M
proof
let M be tabular FinSequence;
thus [i,j] in Indices M implies 1<= i & i<=len M & 1<=j & j<=width M
proof
assume
A1: [i,j] in Indices M;
then [i,j] in [:Seg len M,Seg width M:] by FINSEQ_1:def 3;
then
A2: i in Seg len M by ZFMISC_1:87;
j in Seg width M by A1,ZFMISC_1:87;
hence thesis by A2,FINSEQ_1:1;
end;
assume that
A3: 1<= i and
A4: i<=len M and
A5: 1<=j and
A6: j<=width M;
A7: j in Seg width M by A5,A6,FINSEQ_1:1;
i in dom M by A3,A4,FINSEQ_3:25;
hence thesis by A7,ZFMISC_1:87;
end;
::$CT
theorem Th2:
for a being Complex,M being Matrix of COMPLEX holds len (a
*M)=len M & width (a*M)=width M
proof
let a be Complex,M be Matrix of COMPLEX;
a in COMPLEX by XCMPLX_0:def 2;
then reconsider ea=a as Element of F_Complex by COMPLFLD:def 1;
A1: width (a*M)=width COMPLEX2Field (a*M) by MATRIX_5:7
.= width COMPLEX2Field Field2COMPLEX (ea*(COMPLEX2Field M)) by
MATRIX_5:def 7
.= width (ea*(COMPLEX2Field M)) by MATRIX_5:6
.= width COMPLEX2Field M by MATRIX_3:def 5
.= width M by MATRIX_5:def 1;
len (a*M)=len COMPLEX2Field (a*M) by MATRIX_5:7
.= len COMPLEX2Field Field2COMPLEX (ea*(COMPLEX2Field M)) by MATRIX_5:def 7
.= len (ea*(COMPLEX2Field M)) by MATRIX_5:6
.= len COMPLEX2Field M by MATRIX_3:def 5
.= len M by MATRIX_5:def 1;
hence thesis by A1;
end;
theorem Th3:
for i,j being Nat,a being Complex,M being Matrix of
COMPLEX st [i,j] in Indices M holds (a*M)*(i,j) = a*(M*(i,j))
proof
let i,j be Nat,a be Complex,M be Matrix of COMPLEX;
reconsider m1=COMPLEX2Field M as Matrix of COMPLEX by COMPLFLD:def 1;
A1: M*(i,j) = m1*(i,j) by MATRIX_5:def 1
.= COMPLEX2Field(M)*(i,j) by COMPLFLD:def 1;
assume [i,j] in Indices M;
then
A2: [i,j] in Indices COMPLEX2Field M by MATRIX_5:def 1;
a in COMPLEX by XCMPLX_0:def 2;
then reconsider aa=a as Element of F_Complex by COMPLFLD:def 1;
reconsider m=COMPLEX2Field(a*M) as Matrix of COMPLEX by COMPLFLD:def 1;
A3: COMPLEX2Field(a*M) = COMPLEX2Field Field2COMPLEX (aa*(COMPLEX2Field M))
by MATRIX_5:def 7
.= aa*(COMPLEX2Field M) by MATRIX_5:6;
(a*M)*(i,j)= m*(i,j) by MATRIX_5:def 1
.= (aa*(COMPLEX2Field M))*(i,j) by A3,COMPLFLD:def 1
.= aa*((COMPLEX2Field M)*(i,j)) by A2,MATRIX_3:def 5
.= a*(COMPLEX2Field (M)*(i,j));
hence thesis by A1;
end;
theorem Th4:
for a being Complex,M being Matrix of COMPLEX holds (a*M)
*' = a*'*(M*')
proof
let a be Complex,M be Matrix of COMPLEX;
reconsider aa = a as Element of COMPLEX by XCMPLX_0:def 2;
A1: len (a*M) = len M by Th2;
A2: width (a*M) = width M by Th2;
A3: width M = width (M*') by Def1;
A4: len ((a*M)*') = len (a*M) by Def1;
A5: width ((a*M)*') = width (a*M) by Def1;
A6: len M = len (M*') by Def1;
A7: now
let i,j;
assume
A8: [i,j] in Indices (a*M)*';
then
A9: 1<= i by Th1;
A10: 1<=j by A8,Th1;
A11: j<=width (a*M) by A5,A8,Th1;
A12: i<=len (a*M) by A4,A8,Th1;
then
A13: [i,j] in Indices M by A1,A2,A9,A10,A11,Th1;
A14: [i,j] in Indices (M*') by A1,A6,A2,A3,A9,A12,A10,A11,Th1;
[i,j] in Indices (a*M) by A9,A12,A10,A11,Th1;
then ((a*M)*')*(i,j) = ((a*M)*(i,j))*' by Def1;
hence (a*M)*'*(i,j) = (aa*(M*(i,j)))*' by A13,Th3
.= aa*'*(M*(i,j))*' by COMPLEX1:35
.= a*'*((M*')*(i,j)) by A13,Def1
.= (a*'*(M*'))*(i,j) by A14,Th3;
end;
len (a*'*(M*')) = len (M*') by Th2;
then len (a*'*(M*')) = len M by Def1;
then
A15: len ((a*M)*')=len (a*'*(M*')) by A4,Th2;
width (a*'*(M*')) = width (M*') by Th2;
then width (a*'*(M*')) = width M by Def1;
hence thesis by A15,A5,A7,Th2,MATRIX_0:21;
end;
theorem Th5:
for M1,M2 being Matrix of COMPLEX holds len (M1+M2)=len M1 &
width (M1+M2)=width M1
proof
let M1,M2 be Matrix of COMPLEX;
A1: width (M1+M2)=width COMPLEX2Field (M1+M2) by MATRIX_5:7
.= width COMPLEX2Field Field2COMPLEX ((COMPLEX2Field M1)+(COMPLEX2Field
M2)) by MATRIX_5:def 3
.= width ((COMPLEX2Field M1)+(COMPLEX2Field M2)) by MATRIX_5:6
.= width COMPLEX2Field M1 by MATRIX_1:def 6
.= width M1 by MATRIX_5:def 1;
len (M1+M2)=len COMPLEX2Field (M1+M2) by MATRIX_5:7
.= len COMPLEX2Field Field2COMPLEX ((COMPLEX2Field M1)+(COMPLEX2Field M2
)) by MATRIX_5:def 3
.= len ((COMPLEX2Field M1)+(COMPLEX2Field M2)) by MATRIX_5:6
.= len COMPLEX2Field M1 by MATRIX_1:def 6
.= len M1 by MATRIX_5:def 1;
hence thesis by A1;
end;
theorem Th6:
for i,j being Nat,M1,M2 being Matrix of COMPLEX st [i,j] in
Indices M1 holds (M1+M2)*(i,j) = M1*(i,j) + M2*(i,j)
proof
let i,j be Nat,M1,M2 be Matrix of COMPLEX;
A1: COMPLEX2Field(M1+M2) = COMPLEX2Field Field2COMPLEX ((COMPLEX2Field M1)+(
COMPLEX2Field M2)) by MATRIX_5:def 3
.= (COMPLEX2Field M1)+(COMPLEX2Field M2) by MATRIX_5:6;
reconsider m1=COMPLEX2Field M1, m2=COMPLEX2Field M2 as Matrix of COMPLEX by
COMPLFLD:def 1;
set m=COMPLEX2Field(M1+M2);
reconsider m9=m as Matrix of COMPLEX by COMPLFLD:def 1;
A2: M1*(i,j) = m1*(i,j) by MATRIX_5:def 1
.=COMPLEX2Field(M1)*(i,j) by COMPLFLD:def 1;
assume [i,j] in Indices M1;
then
A3: [i,j] in Indices COMPLEX2Field M1 by MATRIX_5:def 1;
A4: M2*(i,j) = m2*(i,j) by MATRIX_5:def 1
.=COMPLEX2Field(M2)*(i,j) by COMPLFLD:def 1;
(M1+M2)*(i,j) = m9*(i,j) by MATRIX_5:def 1
.= m*(i,j) by COMPLFLD:def 1
.=(COMPLEX2Field M1)*(i,j)+(COMPLEX2Field M2)*(i,j) by A1,A3,MATRIX_1:def 6
;
hence thesis by A2,A4;
end;
theorem
for M1,M2 being Matrix of COMPLEX st len M1=len M2 & width M1=width M2
holds (M1 + M2)*' = M1*' + M2*'
proof
let M1,M2 be Matrix of COMPLEX;
assume that
A1: len M1=len M2 and
A2: width M1=width M2;
A3: len (M1 + M2) = len M1 by Th5;
A4: width ((M1 + M2)*') = width (M1 + M2) by Def1;
A5: width (M1 + M2) = width M1 by Th5;
A6: len ((M1 + M2)*') = len (M1 + M2) by Def1;
A7: now
let i,j;
assume
A8: [i,j] in Indices (M1+M2)*';
then
A9: 1<=j by Th1;
A10: 1<= i by A8,Th1;
A11: j<=width (M1+M2) by A4,A8,Th1;
then
A12: j<=width (M1*') by A5,Def1;
A13: i<=len (M1+M2) by A6,A8,Th1;
then i<=len (M1*') by A3,Def1;
then
A14: [i,j] in Indices (M1*') by A9,A10,A12,Th1;
A15: 1<= i by A8,Th1;
then
A16: [i,j] in Indices M1 by A3,A5,A13,A9,A11,Th1;
A17: [i,j] in Indices M2 by A1,A2,A3,A5,A15,A13,A9,A11,Th1;
[i,j] in Indices (M1+M2) by A15,A13,A9,A11,Th1;
then ((M1+M2)*')*(i,j) = ((M1+M2)*(i,j))*' by Def1;
hence (M1+M2)*'*(i,j) = (M1*(i,j)+M2*(i,j))*' by A16,Th6
.= (M1*(i,j))*'+(M2*(i,j))*' by COMPLEX1:32
.= M1*'*(i,j)+(M2*(i,j))*' by A16,Def1
.= (M1*')*(i,j)+(M2*')*(i,j) by A17,Def1
.= (M1*'+M2*')*(i,j) by A14,Th6;
end;
A18: width (M1*') = width M1 by Def1;
A19: width (M1*' + M2*') = width (M1*') by Th5;
A20: len (M1*' + M2*') = len (M1*') by Th5;
len (M1*') = len M1 by Def1;
hence thesis by A6,A3,A20,A4,A5,A19,A18,A7,MATRIX_0:21;
end;
theorem Th8:
for M being Matrix of COMPLEX holds len (-M)=len M & width (-M)= width M
proof
let M be Matrix of COMPLEX;
A1: width (-M)=width COMPLEX2Field (-M) by MATRIX_5:7
.= width COMPLEX2Field Field2COMPLEX (-COMPLEX2Field M) by MATRIX_5:def 4
.= width (-COMPLEX2Field M) by MATRIX_5:6
.= width COMPLEX2Field M by MATRIX_1:def 4
.= width M by MATRIX_5:def 1;
len (-M)=len COMPLEX2Field (-M) by MATRIX_5:7
.= len COMPLEX2Field Field2COMPLEX (-COMPLEX2Field M) by MATRIX_5:def 4
.= len (-COMPLEX2Field M) by MATRIX_5:6
.= len COMPLEX2Field M by MATRIX_1:def 4
.= len M by MATRIX_5:def 1;
hence thesis by A1;
end;
theorem Th9:
for i,j being Nat,M being Matrix of COMPLEX st [i,j] in Indices
M holds (-M)*(i,j)= -(M*(i,j))
proof
let i,j be Nat,M be Matrix of COMPLEX;
A1: COMPLEX2Field(-M) = COMPLEX2Field Field2COMPLEX (-COMPLEX2Field M) by
MATRIX_5:def 4
.= -(COMPLEX2Field M) by MATRIX_5:6;
reconsider m=COMPLEX2Field(-M) as Matrix of COMPLEX by COMPLFLD:def 1;
reconsider m1=COMPLEX2Field M as Matrix of COMPLEX by COMPLFLD:def 1;
A2: M*(i,j) =m1*(i,j) by MATRIX_5:def 1
.=COMPLEX2Field(M)*(i,j) by COMPLFLD:def 1;
assume [i,j] in Indices M;
then
A3: [i,j] in Indices COMPLEX2Field M by MATRIX_5:def 1;
(-M)*(i,j) = m*(i,j) by MATRIX_5:def 1
.= (-(COMPLEX2Field M))*(i,j) by A1,COMPLFLD:def 1
.= -((COMPLEX2Field M)*(i,j)) by A3,MATRIX_1:def 4;
hence thesis by A2;
end;
theorem Th10:
for M being Matrix of COMPLEX holds (-1)*M = -M
proof
let M be Matrix of COMPLEX;
A1: width (-M) = width M by Th8;
A2: width ((-1)*M) = width M by Th2;
A3: len ((-1)*M) = len M by Th2;
A4: now
let i,j;
assume
A5: [i,j] in Indices ((-1)*M);
then
A6: 1<= i by Th1;
A7: 1<=j by A5,Th1;
A8: j<=width M by A2,A5,Th1;
i<=len M by A3,A5,Th1;
then
A9: [i,j] in Indices M by A6,A7,A8,Th1;
hence ((-1)*M)*(i,j) = (-1)*(M*(i,j)) by Th3
.= -(M*(i,j))
.= (-M)*(i,j) by A9,Th9;
end;
len (-M) = len M by Th8;
hence thesis by A3,A1,A2,A4,MATRIX_0:21;
end;
theorem
for M being Matrix of COMPLEX holds (-M)*' = -(M*')
proof
let M be Matrix of COMPLEX;
(-M)*'= ((-1)*M)*' by Th10
.= ((-1r)*')*(M*') by Th4,COMPLEX1:def 4
.= (-1)*(M*') by COMPLEX1:30,33,def 4
.= -M*' by Th10;
hence thesis;
end;
theorem Th12:
for M1,M2 being Matrix of COMPLEX holds len (M1-M2)=len M1 &
width (M1-M2)=width M1
proof
let M1,M2 be Matrix of COMPLEX;
A1: width (M1-M2)=width COMPLEX2Field (M1-M2) by MATRIX_5:7
.= width COMPLEX2Field Field2COMPLEX ((COMPLEX2Field M1)-(COMPLEX2Field
M2)) by MATRIX_5:def 5
.= width ((COMPLEX2Field M1)-(COMPLEX2Field M2)) by MATRIX_5:6
.= width ((COMPLEX2Field M1)+-(COMPLEX2Field M2))
.= width COMPLEX2Field M1 by MATRIX_1:def 6
.= width M1 by MATRIX_5:def 1;
len (M1-M2)=len (COMPLEX2Field (M1-M2)) by MATRIX_5:7
.= len COMPLEX2Field Field2COMPLEX ((COMPLEX2Field M1)-(COMPLEX2Field M2
)) by MATRIX_5:def 5
.= len ((COMPLEX2Field M1)-(COMPLEX2Field M2)) by MATRIX_5:6
.= len ((COMPLEX2Field M1)+-(COMPLEX2Field M2))
.= len COMPLEX2Field M1 by MATRIX_1:def 6
.= len M1 by MATRIX_5:def 1;
hence thesis by A1;
end;
theorem Th13:
for i,j being Nat,M1,M2 be Matrix of COMPLEX st len M1=len M2 &
width M1=width M2 & [i,j] in Indices M1 holds (M1-M2)*(i,j)=(M1*(i,j)) - (M2*(i
,j))
proof
let i,j be Nat,M1,M2 be Matrix of COMPLEX;
assume that
A1: len M1 =len M2 and
A2: width M1=width M2 and
A3: [i,j] in Indices M1;
A4: j<=width M2 by A2,A3,Th1;
A5: 1<=j by A3,Th1;
A6: 1<= i by A3,Th1;
i<=len M2 by A1,A3,Th1;
then [i,j] in Indices M2 by A6,A5,A4,Th1;
then
A7: [i,j] in Indices COMPLEX2Field M2 by MATRIX_5:def 1;
reconsider m2=COMPLEX2Field M2 as Matrix of COMPLEX by COMPLFLD:def 1;
reconsider m1=COMPLEX2Field M1 as Matrix of COMPLEX by COMPLFLD:def 1;
set m=COMPLEX2Field(M1-M2);
A8: COMPLEX2Field(M1-M2) = COMPLEX2Field Field2COMPLEX ((COMPLEX2Field M1)-(
COMPLEX2Field M2)) by MATRIX_5:def 5
.= (COMPLEX2Field M1)-(COMPLEX2Field M2) by MATRIX_5:6;
reconsider m9=m as Matrix of COMPLEX by COMPLFLD:def 1;
A9: M1*(i,j) = m1*(i,j) by MATRIX_5:def 1
.= COMPLEX2Field(M1)*(i,j) by COMPLFLD:def 1;
A10: [i,j] in Indices COMPLEX2Field M1 by A3,MATRIX_5:def 1;
M2*(i,j) = m2*(i,j) by MATRIX_5:def 1
.= COMPLEX2Field(M2)*(i,j) by COMPLFLD:def 1;
then
A11: -(M2*(i,j))=-(COMPLEX2Field(M2)*(i,j));
(M1-M2)*(i,j) = m9*(i,j) by MATRIX_5:def 1
.= m*(i,j) by COMPLFLD:def 1
.= ((COMPLEX2Field M1)+(-(COMPLEX2Field M2)))*(i,j) by A8
.= (COMPLEX2Field M1)*(i,j)+(-COMPLEX2Field M2)*(i,j) by A10,MATRIX_1:def 6
.= (COMPLEX2Field M1)*(i,j)+-((COMPLEX2Field M2)*(i,j))
by A7,MATRIX_1:def 4;
hence thesis by A9,A11;
end;
theorem
for M1,M2 being Matrix of COMPLEX st len M1=len M2 & width M1=width M2
holds (M1 - M2)*' = M1*' - M2*'
proof
let M1,M2 be Matrix of COMPLEX;
assume that
A1: len M1=len M2 and
A2: width M1=width M2;
A3: len ((M1 - M2)*') = len (M1 - M2) by Def1;
A4: width ((M1 - M2)*') = width (M1 - M2) by Def1;
A5: width (M1 - M2) = width M1 by Th12;
A6: width (M1*') = width M1 by Def1;
A7: len (M1*') = len M1 by Def1;
A8: width (M2*') = width M2 by Def1;
A9: len (M1 - M2) = len M1 by Th12;
A10: len (M2*') = len M2 by Def1;
A11: now
let i,j;
assume
A12: [i,j] in Indices (M1-M2)*';
then
A13: 1<=j by Th1;
A14: 1<= i by A12,Th1;
A15: j<=width (M1-M2) by A4,A12,Th1;
then
A16: j<=width (M1*') by A5,Def1;
A17: i<=len (M1-M2) by A3,A12,Th1;
then i<=len (M1*') by A9,Def1;
then
A18: [i,j] in Indices (M1*') by A13,A14,A16,Th1;
A19: 1<= i by A12,Th1;
then
A20: [i,j] in Indices M1 by A9,A5,A17,A13,A15,Th1;
A21: [i,j] in Indices M2 by A1,A2,A9,A5,A19,A17,A13,A15,Th1;
[i,j] in Indices (M1-M2) by A19,A17,A13,A15,Th1;
then ((M1-M2)*')*(i,j) = ((M1-M2)*(i,j))*' by Def1;
hence (M1-M2)*'*(i,j) = (M1*(i,j)-M2*(i,j))*' by A1,A2,A20,Th13
.= (M1*(i,j))*'-(M2*(i,j))*' by COMPLEX1:34
.= M1*'*(i,j)-(M2*(i,j))*' by A20,Def1
.= (M1*')*(i,j)-(M2*')*(i,j) by A21,Def1
.= (M1*'-M2*')*(i,j) by A1,A2,A7,A10,A6,A8,A18,Th13;
end;
A22: width (M1*') = width M1 by Def1;
A23: width (M1*' - M2*') = width (M1*') by Th12;
len (M1*' - M2*') = len (M1*') by Th12;
hence thesis by A3,A7,A9,A4,A5,A23,A22,A11,MATRIX_0:21;
end;
definition
let M be Matrix of COMPLEX;
func M@" -> Matrix of COMPLEX equals
(M@)*';
coherence;
end;
definition
let x be FinSequence of COMPLEX;
assume
A1: len x > 0;
func FinSeq2Matrix x -> Matrix of COMPLEX means
len it = len x & width it = 1 & for j st j in Seg len x holds it.j =<*x.j*>;
existence
proof
reconsider n=len x as Element of NAT;
deffunc F(Nat) = <*x.$1*>;
consider M3 being FinSequence such that
A2: len M3=n & for j be Nat st j in dom M3 holds M3.j = F(j) from
FINSEQ_1:sch 2;
for y being object st y in rng M3 ex p being FinSequence of COMPLEX st y
= p & len p = 1
proof
let y be object;
assume y in rng M3;
then consider z be object such that
A3: z in dom M3 and
A4: y=M3.z by FUNCT_1:def 3;
reconsider z as Element of NAT by A3;
len <*x.z*>=1 by FINSEQ_1:39;
hence thesis by A2,A3,A4;
end;
then reconsider M2=M3 as Matrix of COMPLEX by MATRIX_0:9;
for p being FinSequence of COMPLEX st p in rng M2 holds len p = 1
proof
let p be FinSequence of COMPLEX;
assume p in rng M2;
then consider i be Nat such that
A5: i in dom M2 and
A6: M2.i =p by FINSEQ_2:10;
len <*x.i*>=1 by FINSEQ_1:39;
hence thesis by A2,A5,A6;
end;
then reconsider M1=M2 as Matrix of len M2,1,COMPLEX by MATRIX_0:def 2;
take M2;
A7: dom M3 = Seg n by A2,FINSEQ_1:def 3;
width M1 = 1 by A1,A2,MATRIX_0:23;
hence thesis by A2,A7;
end;
uniqueness
proof
let M1,M2 be Matrix of COMPLEX;
assume that
A8: len M1 = len x and
width M1 = 1 and
A9: for k st k in Seg len x holds M1.k =<*x.k*> and
A10: len M2 = len x and
width M2 = 1 and
A11: for k st k in Seg len x holds M2.k =<*x.k*>;
A12: dom M1 = Seg len x by A8,FINSEQ_1:def 3;
now
let k be Nat;
assume
A13: k in dom M1;
hence M1.k=<*x.k*> by A9,A12
.=M2.k by A11,A12,A13;
end;
hence thesis by A8,A10,FINSEQ_2:9;
end;
end;
definition
let M be Matrix of COMPLEX;
func Matrix2FinSeq M -> FinSequence of COMPLEX equals
Col(M,1);
coherence;
end;
definition
let F1,F2 be FinSequence of COMPLEX;
func mlt(F1,F2) -> FinSequence of COMPLEX equals
multcomplex.:(F1,F2);
coherence;
commutativity
proof
let F,F1,F2 be FinSequence of COMPLEX;
A1: dom multcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def 1;
then
A2: [:rng F2, rng F1:] c= dom multcomplex by ZFMISC_1:96;
[:rng F1, rng F2:] c= dom multcomplex by A1,ZFMISC_1:96;
then
A3: dom(multcomplex.:(F1,F2)) = dom F1 /\ dom F2 by FUNCOP_1:69
.= dom(multcomplex.:(F2,F1)) by A2,FUNCOP_1:69;
assume
A4: F = multcomplex.:(F1,F2);
for z being set st z in dom(multcomplex.:(F2,F1)) holds F.z =
multcomplex.(F2.z,F1.z)
proof
let z be set such that
A5: z in dom(multcomplex.:(F2,F1));
set F1z = F1.z, F2z =F2.z;
thus F.z = multcomplex.(F1.z,F2.z) by A4,A3,A5,FUNCOP_1:22
.= F1z * F2z by BINOP_2:def 5
.= multcomplex.(F2.z,F1.z) by BINOP_2:def 5;
end;
hence thesis by A4,A3,FUNCOP_1:21;
end;
end;
definition
let M be Matrix of COMPLEX;
let F be FinSequence of COMPLEX;
func M*F -> FinSequence of COMPLEX means
:Def6:
len it = len M & for i st i in Seg len M holds it.i=Sum mlt(Line(M,i),F);
existence
proof
deffunc V(Nat) = Sum mlt(Line(M,$1),F);
consider z being FinSequence of COMPLEX such that
A1: len z=len M & for i be Nat st i in dom z holds z.i=V(i) from
FINSEQ_2:sch 1;
take z;
dom z = Seg len M by A1,FINSEQ_1:def 3;
hence thesis by A1;
end;
uniqueness
proof
let p1,p2 be FinSequence of COMPLEX;
assume that
A2: len p1 = len M and
A3: for i st i in Seg len M holds p1.i=Sum mlt(Line(M,i),F) and
A4: len p2 = len M and
A5: for i st i in Seg len M holds p2.i=Sum mlt(Line(M,i),F);
A6: dom p1 = Seg len M by A2,FINSEQ_1:def 3;
now
let i be Nat;
assume
A7: i in dom p1;
then p1.i=Sum mlt(Line(M,i),F) by A3,A6;
hence p1.i = p2.i by A5,A6,A7;
end;
hence thesis by A2,A4,FINSEQ_2:9;
end;
end;
Lm1: for a being Element of COMPLEX,F being FinSequence of COMPLEX holds a*F =
(multcomplex[;](a,id COMPLEX))*F
proof
let a be Element of COMPLEX,F be FinSequence of COMPLEX;
a multcomplex = multcomplex[;](a,id COMPLEX) by SEQ_4:def 4;
hence thesis by SEQ_4:def 9;
end;
theorem Th15:
a*mlt(R1,R2) = mlt(a*R1,R2)
proof
thus a*mlt(R1,R2) = (multcomplex[;](a,id COMPLEX))*(mlt(R1,R2)) by Lm1
.= multcomplex.:((multcomplex[;](a,id COMPLEX))*R1,R2) by FINSEQOP:26
.= mlt(a*R1,R2) by Lm1;
end;
definition
let M be Matrix of COMPLEX;
let a be Complex;
func M*a -> Matrix of COMPLEX equals
a*M;
coherence;
end;
theorem
for a being Element of COMPLEX,M being Matrix of COMPLEX holds (M*a)*'
= a*'*(M*') by Th4;
theorem Th17:
for F1,F2 being FinSequence of COMPLEX,i being Nat holds i in
dom mlt(F1,F2) implies mlt(F1,F2).i = F1.i * F2.i
proof
let F1,F2 be FinSequence of COMPLEX,i be Nat;
set r1 = F1.i, r2 = F2.i;
assume i in dom mlt(F1,F2);
then mlt(F1,F2).i = multcomplex.(r1,r2) by FUNCOP_1:22;
hence thesis by BINOP_2:def 5;
end;
definition
let i be Element of NAT, R1,R2 be Element of i-tuples_on COMPLEX;
redefine func mlt(R1,R2) -> Element of i-tuples_on COMPLEX; :: redefines mlt (MATRIXC1, definition)
coherence by FINSEQ_2:120;
end;
theorem Th18:
mlt(R1,R2).j = R1.j * R2.j
proof
reconsider i,j1=j as Element of NAT by ORDINAL1:def 12;
reconsider R1,R2 as Element of i-tuples_on COMPLEX;
per cases;
suppose
A1: not j in Seg i;
then
A2: not j in dom R2 by FINSEQ_2:124;
not j in dom mlt(R1,R2) by A1,FINSEQ_2:124;
then mlt(R1,R2).j = R1.j1 *0 by FUNCT_1:def 2
.= R1.j * R2.j by A2,FUNCT_1:def 2;
hence thesis;
end;
suppose
j in Seg i;
then j in dom mlt(R1,R2) by FINSEQ_2:124;
hence thesis by Th17;
end;
end;
::$CT
theorem Th19:
for F being FinSequence of COMPLEX ex G being sequence of
COMPLEX st for n being Nat st 1<= n & n<=len F holds G.n=F.n
proof
let F be FinSequence of COMPLEX;
defpred P[object,object] means
($1 in Seg len F implies $2=F.$1) & (not $1 in Seg len F implies $2=0);
A1: for x being object st x in NAT
ex y being object st y in COMPLEX & P[x,y]
proof
let x be object;
assume x in NAT;
per cases;
suppose
A2: x in Seg len F;
take F.x;
F.x in COMPLEX by XCMPLX_0:def 2;
hence thesis by A2;
end;
suppose
A3: not x in Seg len F;
take 0;
0 in COMPLEX by XCMPLX_0:def 2;
hence thesis by A3;
end;
end;
ex G1 being sequence of COMPLEX st for x being object st x in NAT holds
P[x,G1.x] from FUNCT_2:sch 1(A1);
then consider G2 being sequence of COMPLEX such that
A4: for x being object st x in NAT holds (x in Seg len F implies G2.x=F.x)
& (not x in Seg len F implies G2.x=0);
for n being Nat st 1<= n & n<=len F holds G2.n=F.n
proof
let n be Nat;
assume that
A5: 1<= n and
A6: n<=len F;
n in Seg len F by A5,A6,FINSEQ_1:1;
hence thesis by A4;
end;
hence thesis;
end;
theorem Th20:
for F being FinSequence of COMPLEX st len (F*') >= 1 holds
addcomplex $$ (F*') = (addcomplex $$ F)*'
proof
let F be FinSequence of COMPLEX;
A1: len F = len (F*') by COMPLSP2:def 1;
assume
A2: len (F*') >= 1;
then consider f22 being sequence of COMPLEX such that
A3: f22.1 = (F*').1 and
A4: for n be Nat st 0 <> n & n < len (F*') holds f22.(n + 1)
= addcomplex.(f22.n,(F*').(n + 1)) and
A5: addcomplex $$ (F*') = f22.(len (F*')) by FINSOP_1:1;
A6: (len (F*')) in Seg len (F*') by A2,FINSEQ_1:1;
defpred P[set,set] means $2= f22.$1;
A7: for k be Nat st k in Seg len (F*') ex x being Element of COMPLEX st P[k,
x];
ex f2 being FinSequence of COMPLEX st dom f2 = Seg len (F*') & for k be
Nat st k in Seg len (F*') holds P[k,f2.k] from FINSEQ_1:sch 5(A7);
then consider f2 being FinSequence of COMPLEX such that
A8: dom f2 = Seg len (F*') and
A9: for k be Nat st k in Seg len (F*') holds P[k,f2.k];
consider f9 being sequence of COMPLEX such that
A10: for n being Nat st 1<= n & n<=len (f2*') holds f9.n=(f2*').n by Th19;
A11: len (f2*')=len f2 by COMPLSP2:def 1;
then 1<=len (f2*') by A2,A8,FINSEQ_1:def 3;
then
A12: f9.1=(f2*').1 by A10;
A13: len f2 = len (F*') by A8,FINSEQ_1:def 3;
A14: for n st 0 <> n & n < len (F*') holds f2.(n + 1) = addcomplex.(f2.n,(F
*').(n + 1))
proof
let n;
assume that
A15: 0 <> n and
A16: n < len (F*');
A17: n+1<=len (F*') by A16,NAT_1:13;
A18: 0+1<=n by A15,NAT_1:13;
then
A19: n in Seg len (F*') by A16,FINSEQ_1:1;
1<=n+1 by A18,NAT_1:13;
then (n+1) in Seg len (F*') by A17,FINSEQ_1:1;
then f2.(n + 1) = f22.(n + 1) by A9
.= addcomplex.(f22.n,(F*').(n + 1)) by A4,A15,A16
.= addcomplex.(f2.n,(F*').(n + 1)) by A9,A19;
hence thesis;
end;
A20: for n being Nat st 0 <> n & n < len F holds (f2*').(n + 1) =
addcomplex.((f2*').n,F.(n + 1))
proof
let n be Nat;
assume that
A21: 0 <> n and
A22: n < len F;
A23: n<=len f2 by A1,A8,A22,FINSEQ_1:def 3;
A24: 0+1<=n by A21,NAT_1:13;
then
A25: 1<=n+1 by NAT_1:13;
reconsider c = (F.(n + 1))*' as Element of COMPLEX by XCMPLX_0:def 2;
A26: n+1<=len F by A22,NAT_1:13;
then n+1<=len f2 by A1,A8,FINSEQ_1:def 3;
then (f2*').(n + 1) = (f2.(n+1))*' by A25,COMPLSP2:def 1
.= (addcomplex.(f2.n,(F*').(n + 1)))*' by A1,A14,A21,A22
.= (addcomplex.(f2.n,c))*' by A25,A26,COMPLSP2:def 1
.= (f2.n+c)*' by BINOP_2:def 3
.= (f2.n)*'+c*' by COMPLEX1:32
.= addcomplex.((f2.n)*',F.(n + 1)) by BINOP_2:def 3;
hence thesis by A24,A23,COMPLSP2:def 1;
end;
A27: for n be Nat st 0 <> n & n < len F holds f9.(n + 1) =
addcomplex.(f9.n,F.(n + 1))
proof
let n be Nat;
assume that
A28: 0 <> n and
A29: n < len F;
A30: 0+1<=n by A28,NAT_1:13;
n+1<=len (f2*') by A1,A13,A11,A29,NAT_1:13;
then
A31: f9.(n+1)=(f2*').(n+1) by A10,NAT_1:11;
n<=len (f2*') by A1,A13,A29,COMPLSP2:def 1;
then f9.n=(f2*').n by A10,A30;
hence thesis by A20,A28,A29,A31;
end;
A32: 1 in Seg len (F*') by A2,FINSEQ_1:1;
set d=(addcomplex $$ (F*'))*';
A33: len F >=1 by A2,COMPLSP2:def 1;
(f2*').(len F)=(f2*').(len (F*')) by COMPLSP2:def 1
.= (f2.(len (F*')))*' by A2,A13,COMPLSP2:def 1
.= d by A5,A9,A6;
then
A34: d=f9.(len F) by A2,A1,A13,A10,A11;
F.1=((F.1)*')*' .= ((F*').1)*' by A33,COMPLSP2:def 1
.= (f2.1)*' by A3,A9,A32
.= (f2*').1 by A2,A13,COMPLSP2:def 1;
then d = addcomplex $$ F by A33,A12,A27,A34,FINSOP_1:2;
hence thesis;
end;
theorem Th21:
for F being FinSequence of COMPLEX st len F >= 1 holds Sum(F*') = (Sum F)*'
proof
let F be FinSequence of COMPLEX;
assume len F >= 1;
then len (F*') >= 1 by COMPLSP2:def 1;
hence thesis by Th20;
end;
theorem Th22:
for x,y being FinSequence of COMPLEX st len x=len y holds (mlt(x
,(y*')))*' = mlt(y,(x*'))
proof
let x,y be FinSequence of COMPLEX;
assume
A1: len x=len y;
reconsider x19=x*' as Element of (len (x*'))-tuples_on COMPLEX by FINSEQ_2:92
;
reconsider y19=y as Element of (len y)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9=y*' as Element of (len (y*'))-tuples_on COMPLEX by FINSEQ_2:92;
reconsider x9=x as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
A2: len (x*') = len x by COMPLSP2:def 1;
A3: len (y*') = len y by COMPLSP2:def 1;
then
A4: len mlt(x,(y*')) = len x by A1,FINSEQ_2:72;
A5: len mlt(x,(y*')) = len (y*') by A1,A3,FINSEQ_2:72;
A6: now
let i be Nat;
assume that
A7: 1 <= i and
A8: i <= len ((mlt(x,(y*')))*');
A9: i <= len (mlt(x,(y*'))) by A8,COMPLSP2:def 1;
hence (mlt(x,(y*')))*'.i = ((mlt(x,(y*'))).i)*' by A7,COMPLSP2:def 1
.= (((x9.i)*((y9).i)))*' by A1,A3,Th18
.= (x.i)*'*((y*').i)*' by COMPLEX1:35
.= (x.i)*'*((y*')*'.i) by A5,A7,A9,COMPLSP2:def 1
.= (x.i)*'*(y.i)
.= ((x*').i)*(y.i) by A4,A7,A9,COMPLSP2:def 1
.= mlt(x19,y19).i by A1,A2,Th18
.= mlt(y,(x*')).i;
end;
len (mlt(x,(y*'))) = len ((mlt(x,(y*')))*') by COMPLSP2:def 1;
then len ((mlt(x,(y*')))*') = len mlt(y,(x*')) by A1,A2,A4,FINSEQ_2:72;
hence thesis by A6,FINSEQ_1:14;
end;
theorem Th23:
for x,y being FinSequence of COMPLEX,a being Element of COMPLEX
st len x=len y holds (mlt(x,a*y)) = a*mlt(x,y)
proof
let x,y be FinSequence of COMPLEX,a be Element of COMPLEX;
reconsider x9=x as Element of len x-tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9=y as Element of len y-tuples_on COMPLEX by FINSEQ_2:92;
assume len x=len y;
then mlt(x,a*y) = a*mlt(x9,y9) by Th15
.= a*mlt(x,y);
hence thesis;
end;
theorem Th24:
for x,y being FinSequence of COMPLEX,a being Element of COMPLEX
st len x=len y holds mlt(a*x,y) = a*mlt(x,y)
proof
let x,y be FinSequence of COMPLEX,a be Element of COMPLEX;
reconsider x9=x as Element of len x-tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9=y as Element of len y-tuples_on COMPLEX by FINSEQ_2:92;
assume len x=len y;
then mlt(a*x,y) = a*mlt(x9,y9) by Th15
.= a*mlt(x,y);
hence thesis;
end;
theorem Th25:
for x,y being FinSequence of COMPLEX st len x=len y holds (mlt(x
,y))*' = mlt(x*',y*')
proof
let x,y be FinSequence of COMPLEX;
A1: len ((mlt(x,y))*') = len (mlt(x,y)) by COMPLSP2:def 1;
A2: len (x*') = len x by COMPLSP2:def 1;
assume
A3: len x=len y;
A4: for i be Nat st 1 <=i & i <= len ((mlt(x,y))*') holds (mlt(x,(y)))*'.i=
mlt(x*',y*').i
proof
let i be Nat;
(mlt(x,y))*'.i = ((mlt(y,(x*')*')*').i)
.= (mlt(x*',y*').i) by A3,A2,Th22;
hence thesis;
end;
len (y*') = len y by COMPLSP2:def 1;
then len (mlt(x*',y*')) = len (x*') by A3,A2,FINSEQ_2:72;
then len ((mlt(x,y))*') = len (mlt(x*',y*')) by A3,A1,A2,FINSEQ_2:72;
hence thesis by A4,FINSEQ_1:14;
end;
Lm2: for a,b being Element of COMPLEX holds (multcomplex[;](a,id COMPLEX)).b =
a*b
proof
let a,b be Element of COMPLEX;
thus (multcomplex[;](a,id COMPLEX)).b = multcomplex.(a,(id COMPLEX).b) by
FUNCOP_1:53
.= multcomplex.(a,b)
.= a*b by BINOP_2:def 5;
end;
theorem Th26:
for F being FinSequence of COMPLEX,a being Element of COMPLEX
holds Sum(a*F) = a*(Sum F)
proof
let F be FinSequence of COMPLEX,a be Element of COMPLEX;
set rM = multcomplex[;](a,id COMPLEX);
thus Sum (a*F) = addcomplex $$(rM*F) by Lm1
.= rM.(addcomplex $$F) by SEQ_4:51,54,SETWOP_2:30
.= a*(Sum F) by Lm2;
end;
definition
let x be FinSequence of REAL;
func FR2FC(x) -> FinSequence of COMPLEX equals
x;
coherence
proof
rng x c= COMPLEX by NUMBERS:11,XBOOLE_1:1;
hence thesis by FINSEQ_1:def 4;
end;
end;
theorem
for R being FinSequence of REAL, F being FinSequence of COMPLEX st R =
F & len R >= 1 holds addreal $$ R = addcomplex $$ F
proof
let R be FinSequence of REAL,F be FinSequence of COMPLEX;
assume that
A1: R = F and
A2: len R >= 1;
consider f22 be sequence of REAL such that
A3: f22.1 = R.1 and
A4: for n be Nat st 0 <> n & n < len R holds f22.(n + 1) =
addreal.(f22.n,R.(n + 1)) and
A5: addreal $$ R = f22.len R by A2,FINSOP_1:1;
defpred P[set,set] means $2= f22.$1;
A6: for k be Nat st k in Seg len R ex x being Element of REAL st P[k,x]
proof let k be Nat;
f22.k in REAL by XREAL_0:def 1;
hence thesis;
end;
ex f2 being FinSequence of REAL st dom f2 = Seg len R & for k be Nat st
k in Seg len R holds P[k,f2.k] from FINSEQ_1:sch 5(A6);
then consider f2 being FinSequence of REAL such that
A7: dom f2 = Seg len R and
A8: for k be Nat st k in Seg len R holds P[k,f2.k];
consider f9 being sequence of COMPLEX such that
A9: for n being Nat st 1<= n & n<=len FR2FC f2 holds f9.n=(FR2FC f2).n by Th19;
A10: len f2 = len R by A7,FINSEQ_1:def 3;
then
A11: (FR2FC f2).(len F)=f9.(len F) by A1,A2,A9;
A12: for n st 0 <> n & n < len R holds f2.(n + 1) = addreal.(f2.n,R.(n + 1))
proof
let n;
assume that
A13: 0 <> n and
A14: n < len R;
A15: n+1<=len R by A14,NAT_1:13;
A16: 0+1<=n by A13,NAT_1:13;
then
A17: n in Seg len R by A14,FINSEQ_1:1;
1<=n+1 by A16,NAT_1:13;
then (n+1) in Seg len R by A15,FINSEQ_1:1;
then f2.(n + 1) = f22.(n + 1) by A8
.= addreal.(f22.n,R.(n + 1)) by A4,A13,A14
.= addreal.(f2.n,R.(n + 1)) by A8,A17;
hence thesis;
end;
A18: for n be Nat st 0 <> n & n < len F holds f9.(n + 1) =
addcomplex.(f9.n,F.(n + 1))
proof
let n be Nat;
assume that
A19: 0 <> n and
A20: n < len F;
A21: 0+1<=n by A19,NAT_1:13;
n<=len FR2FC f2 by A1,A7,A20,FINSEQ_1:def 3;
then f9.n=(FR2FC f2).n by A9,A21;
then
A22: addcomplex.(f9.n,F.(n + 1)) =addreal.(f2.n,R.(n + 1))
by A1,COMPLSP2:44;
n+1<=len (FR2FC f2) by A1,A10,A20,NAT_1:13;
then f9.(n+1)=(FR2FC f2).(n+1) by A9,NAT_1:11;
hence thesis by A1,A12,A19,A20,A22;
end;
set d = addreal $$ R;
A23: 1 in Seg len R by A2,FINSEQ_1:1;
A24: f9.1=(FR2FC f2).1 by A2,A10,A9;
len R in Seg len R by A2,FINSEQ_1:1;
then (FR2FC f2).len F = d by A1,A5,A8;
hence thesis by A1,A2,A3,A8,A23,A24,A18,A11,FINSOP_1:2;
end;
theorem
for x being FinSequence of REAL, y being FinSequence of COMPLEX st x=y
& len x >=1 holds Sum x = Sum y;
theorem Th29:
for F1,F2 being FinSequence of COMPLEX st len F1=len F2 holds
Sum(F1 - F2) = Sum F1 - Sum F2
proof
let F1,F2 be FinSequence of COMPLEX;
assume
A1: len F1=len F2;
reconsider y2=F2 as Element of (len F2)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider x2=F1 as Element of (len F1)-tuples_on COMPLEX by FINSEQ_2:92;
Sum(F1 - F2) = addcomplex $$(diffcomplex.:(F1,F2)) by SEQ_4:def 7
.= diffcomplex.(addcomplex$$x2,addcomplex$$y2) by A1,SEQ_4:51,52,def 3
,SETWOP_2:37
.= Sum F1 - Sum F2 by BINOP_2:def 4;
hence thesis;
end;
theorem
for x,y,z being FinSequence of COMPLEX st len x=len y & len y=len z
holds mlt((x-y),z) = mlt(x,z)-mlt(y,z)
proof
let x,y,z be FinSequence of COMPLEX;
assume that
A1: len x=len y and
A2: len y=len z;
reconsider x2=x, y2=y, z2=z as Element of (len x)-tuples_on COMPLEX by A1,A2,
FINSEQ_2:92;
A3: dom mlt(x-y,z)=Seg len mlt(x2-y2,z2) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,z2)-mlt(y2,z2)) by CARD_1:def 7
.= dom (mlt(x2,z2)-mlt(y2,z2)) by FINSEQ_1:def 3;
A4: dom mlt(x,z)=Seg len mlt(x2,z2) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,z2)-mlt(y2,z2)) by CARD_1:def 7
.= dom (mlt(x2,z2)-mlt(y2,z2)) by FINSEQ_1:def 3;
A5: dom (mlt(y,z))=Seg len(mlt(y2,z2)) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,z2)-mlt(y2,z2)) by CARD_1:def 7
.= dom (mlt(x2,z2)-mlt(y2,z2)) by FINSEQ_1:def 3;
for i being Nat st i in dom mlt(x-y,z) holds mlt(x-y,z).i=(mlt(x,z)-mlt(
y,z)).i
proof
let i be Nat;
assume
A6: i in dom mlt(x-y,z);
set a=x.i, b=y.i, d=(x-y).i, e=z.i;
len (x2-y2)=len x by CARD_1:def 7;
then dom (x2-y2)=Seg len x by FINSEQ_1:def 3
.=Seg len(mlt(x2,z2)) by CARD_1:def 7
.=dom (mlt(x,z)) by FINSEQ_1:def 3;
then
A7: d=a-b by A3,A4,A6,COMPLSP2:2;
thus mlt(x-y,z).i=d*e by A6,Th17
.=a*e-b*e by A7
.=mlt(x,z).i -b*e by A3,A4,A6,Th17
.=mlt(x,z).i -mlt(y,z).i by A3,A5,A6,Th17
.=(mlt(x,z)-mlt(y,z)).i by A3,A6,COMPLSP2:2;
end;
hence thesis by A3,FINSEQ_1:13;
end;
theorem Th31:
for x,y,z being FinSequence of COMPLEX st len x=len y & len y=
len z holds mlt(x,y-z) = mlt(x,y)-mlt(x,z)
proof
let x,y,z be FinSequence of COMPLEX;
assume that
A1: len x=len y and
A2: len y=len z;
reconsider x2=x, y2=y, z2=z as Element of (len x)-tuples_on COMPLEX by A1,A2,
FINSEQ_2:92;
A3: dom (mlt(x,y-z))=Seg len(mlt(x2,y2-z2)) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,y2)-mlt(x2,z2)) by CARD_1:def 7
.=dom (mlt(x2,y2)-mlt(x2,z2)) by FINSEQ_1:def 3;
A4: dom mlt(x,y)=Seg len(mlt(x2,y2)) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,y2)-mlt(x2,z2)) by CARD_1:def 7
.=dom (mlt(x2,y2)-mlt(x2,z2)) by FINSEQ_1:def 3;
A5: dom mlt(x,z)=Seg len mlt(x2,z2) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,y2)-mlt(x2,z2)) by CARD_1:def 7
.= dom (mlt(x2,y2)-mlt(x2,z2)) by FINSEQ_1:def 3;
for i being Nat st i in dom (mlt(x,y-z)) holds mlt(x,y-z).i=(mlt(x,y)-
mlt(x,z)).i
proof
let i be Nat;
assume
A6: i in dom mlt(x,y-z);
set a=y.i, b=z.i, d=(y-z).i, e=x.i;
len (y2-z2)=len x by CARD_1:def 7;
then dom (y2-z2)=Seg len x by FINSEQ_1:def 3
.=Seg len mlt(x2,y2) by CARD_1:def 7
.=dom mlt(x,y) by FINSEQ_1:def 3;
then
A7: d=a-b by A3,A4,A6,COMPLSP2:2;
thus mlt(x,y-z).i=e*d by A6,Th17
.=e*a-e*b by A7
.=mlt(x,y).i -e*b by A3,A4,A6,Th17
.=mlt(x,y).i -mlt(x,z).i by A3,A5,A6,Th17
.=(mlt(x,y)-mlt(x,z)).i by A3,A6,COMPLSP2:2;
end;
hence thesis by A3,FINSEQ_1:13;
end;
theorem
for x,y,z being FinSequence of COMPLEX st len x=len y & len y=len z
holds mlt(x,y+z) = mlt(x,y)+mlt(x,z)
proof
let x,y,z be FinSequence of COMPLEX;
assume that
A1: len x=len y and
A2: len y=len z;
reconsider x2=x, y2=y, z2=z as Element of (len x)-tuples_on COMPLEX by A1,A2,
FINSEQ_2:92;
A3: dom (mlt(x,y+z))=Seg len(mlt(x2,y2+z2)) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,y2)+mlt(x2,z2)) by CARD_1:def 7
.=dom (mlt(x2,y2)+mlt(x2,z2)) by FINSEQ_1:def 3;
A4: dom mlt(x,y)=Seg len mlt(x2,y2) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,y2)+mlt(x2,z2)) by CARD_1:def 7
.=dom (mlt(x2,y2)+mlt(x2,z2)) by FINSEQ_1:def 3;
A5: dom mlt(x,z)=Seg len mlt(x2,z2) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,y2)+mlt(x2,z2)) by CARD_1:def 7
.= dom (mlt(x2,y2)+mlt(x2,z2)) by FINSEQ_1:def 3;
for i being Nat st i in dom mlt(x,y+z) holds mlt(x,y+z).i=(mlt(x,y)+mlt(
x,z)).i
proof
let i be Nat;
assume
A6: i in dom mlt(x,y+z);
set a=y.i, b=z.i, d=(y+z).i, e=x.i;
len (y2+z2)=len x by CARD_1:def 7;
then dom (y2+z2)=Seg len x by FINSEQ_1:def 3
.=Seg len mlt(x2,y2) by CARD_1:def 7
.=dom mlt(x,y) by FINSEQ_1:def 3;
then
A7: d=a+b by A3,A4,A6,COMPLSP2:1;
thus mlt(x,y+z).i=e*d by A6,Th17
.=e*a+e*b by A7
.=mlt(x,y).i +e*b by A3,A4,A6,Th17
.=mlt(x,y).i +mlt(x,z).i by A3,A5,A6,Th17
.=(mlt(x,y)+mlt(x,z)).i by A3,A6,COMPLSP2:1;
end;
hence thesis by A3,FINSEQ_1:13;
end;
theorem Th33:
for x,y,z being FinSequence of COMPLEX st len x=len y & len y=
len z holds mlt((x+y),z) = mlt(x,z)+mlt(y,z)
proof
let x,y,z be FinSequence of COMPLEX;
assume that
A1: len x=len y and
A2: len y=len z;
reconsider x2=x, y2=y, z2=z as Element of (len x)-tuples_on COMPLEX by A1,A2,
FINSEQ_2:92;
A3: dom mlt(x+y,z)=Seg len mlt(x2+y2,z2) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,z2)+mlt(y2,z2)) by CARD_1:def 7
.= dom (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 3;
A4: dom mlt(x,z)=Seg len mlt(x2,z2) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,z2)+mlt(y2,z2)) by CARD_1:def 7
.= dom (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 3;
A5: dom mlt(y,z)=Seg len mlt(y2,z2) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,z2)+mlt(y2,z2)) by CARD_1:def 7
.= dom (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 3;
for i being Nat st i in dom mlt(x+y,z) holds mlt(x+y,z).i=(mlt(x,z)+mlt(
y,z)).i
proof
let i be Nat;
assume
A6: i in dom mlt(x+y,z);
set a=x.i, b=y.i, d=(x+y).i, e=z.i;
len (x2+y2)=len x by CARD_1:def 7;
then dom (x2+y2)=Seg len x by FINSEQ_1:def 3
.=Seg len mlt(x2,z2) by CARD_1:def 7
.=dom mlt(x,z) by FINSEQ_1:def 3;
then
A7: d=a+b by A3,A4,A6,COMPLSP2:1;
thus mlt(x+y,z).i=d*e by A6,Th17
.=a*e+b*e by A7
.=mlt(x,z).i +b*e by A3,A4,A6,Th17
.=mlt(x,z).i +mlt(y,z).i by A3,A5,A6,Th17
.=(mlt(x,z)+mlt(y,z)).i by A3,A6,COMPLSP2:1;
end;
hence thesis by A3,FINSEQ_1:13;
end;
theorem Th34:
for F1,F2 being FinSequence of COMPLEX st len F1=len F2 holds
Sum(F1 + F2) = Sum F1 + Sum F2
proof
let F1,F2 be FinSequence of COMPLEX;
assume
A1: len F1=len F2;
reconsider y2=F2 as Element of (len F2)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider x2=F1 as Element of (len F1)-tuples_on COMPLEX by FINSEQ_2:92;
Sum(F1 + F2) = addcomplex $$(addcomplex.:(F1,F2)) by SEQ_4:def 6
.= addcomplex.(addcomplex$$x2,addcomplex$$y2) by A1,SETWOP_2:35
.= Sum F1 + Sum F2 by BINOP_2:def 3;
hence thesis;
end;
theorem Th35:
for x1,y1 being FinSequence of COMPLEX for x2,y2 being
FinSequence of REAL st x1 = x2 & y1 = y2 & len x1=len y2 holds multcomplex.:(x1
,y1) = multreal.:(x2,y2)
proof
let x1,y1 be FinSequence of COMPLEX;
let x2,y2 be FinSequence of REAL;
assume that
A1: x1 = x2 and
A2: y1 = y2 and
A3: len x1=len y2;
for i being Element of NAT st i in dom x1 holds multcomplex.(x1.i,y1.i)=
multreal.(x2.i,y2.i)
proof
let i be Element of NAT;
x1.i * y1.i = multcomplex.(x1.i,y1.i) by BINOP_2:def 5;
hence thesis by A1,A2,BINOP_2:def 11;
end;
hence thesis by A1,A2,A3,COMPLSP2:45;
end;
theorem
for x,y being FinSequence of REAL st len x=len y holds FR2FC mlt(x,y)=
mlt(FR2FC x,FR2FC y) by Th35;
theorem Th37:
for x,y being FinSequence of COMPLEX st len x=len y holds |( x,y
)| = Sum mlt(x,(y*'))
proof
let x,y be FinSequence of COMPLEX;
A1: len Im y=len y by COMPLSP2:48;
A2: len (y*') = len (y*');
A3: y*' = -(-y*') .= ((-1)*(-1))*y*' by COMPLSP2:53
.= 1*y*';
A4: len (x*') = len x by COMPLSP2:def 1;
then
A5: len (x+x*') = len x by COMPLSP2:6;
A6: len (x*'+x) = len x by A4,COMPLSP2:6;
A7: len x = len x;
A8: x = -(-x) .= ((-1)*(-1))*x by COMPLSP2:53
.= 1*x;
set Imx=FR2FC Im x;
assume that
A9: len x=len y;
A10: len Imx = len y by A9,COMPLSP2:48
.= len (y*') by COMPLSP2:def 1;
set Imy=FR2FC Im y;
set Rey=FR2FC Re y;
set Rex=FR2FC Re x;
A11: len ((<i>)*(Imx))=len Imx by COMPLSP2:3
.= len x by COMPLSP2:48
.= len Rex by COMPLSP2:48;
A12: len Rex = len x by COMPLSP2:48;
A13: len Im x=len x by COMPLSP2:48;
then
A14: mlt(Im x,Im y)= mlt(FR2FC(Im x),FR2FC(Im y)) by A9,A1,Th35;
A15: len Re y=len y by COMPLSP2:48;
then
A16: mlt(Im x,Re y)= mlt(FR2FC(Im x),FR2FC(Re y)) by A9,A13,Th35;
A17: len Re x=len x by COMPLSP2:48;
then
A18: mlt(Re x,Re y)= mlt(FR2FC Re x,FR2FC Re y) by A9,A15,Th35;
A19: mlt(Re x,Im y)= mlt(FR2FC Re x,FR2FC Im y) by A9,A17,A1,Th35;
A20: len ((<i>)*(Imx))=len Imx by COMPLSP2:3
.= len y by A9,COMPLSP2:48
.= len (y*') by COMPLSP2:def 1;
Imx = (-1/2*<i>)*(x-x*') by COMPLSP2:def 3;
then
A21: <i>*Imx = <i>*(-1/2*<i>)*(x-x*') by COMPLSP2:53
.= (1/2)*(x-x*');
Imy = (-1/2*<i>)*(y-y*') by COMPLSP2:def 3;
then
A22: <i>*Imy = <i>*(-1/2*<i>)*(y-y*') by COMPLSP2:53
.= (1/2)*(y-y*');
A23: Rex = 1/2*(x+x*') by COMPLSP2:def 2;
A24: len (y*') = len y by COMPLSP2:def 1;
then
A25: len (y+y*') = len y by COMPLSP2:6;
len (x-x*') = len x by A4,COMPLSP2:7;
then
A26: Rex + <i>*Imx = 1/2*((x+x*') + (x-x*')) by A23,A21,A5,COMPLSP2:30
.= 1/2*(x+(x*' + x) -x*') by A4,A5,COMPLSP2:37
.= 1/2*(x+(x + x*' -x*')) by A4,A6,COMPLSP2:37
.= 1/2*(x+(x + (x*' -x*'))) by A4,COMPLSP2:37
.= 1/2*(x+(x + (0c (len (x*'))))) by COMPLSP2:34
.= 1/2*(x+(x + (0c (len x)))) by COMPLSP2:def 1
.= 1/2*(x+x) by COMPLSP2:33
.= 1/2*x+1/2*x by A7,COMPLSP2:30
.= (1/2+1/2)*x by COMPLSP2:63
.= x by A8;
A27: Rey = 1/2*(y+y*') by COMPLSP2:def 2;
len (y-y*') = len y by A24,COMPLSP2:7;
then
A28: Rey - <i>*Imy = 1/2*((y+y*') - (y-y*')) by A27,A22,A25,COMPLSP2:43
.= 1/2*((y*'+y) - y +y*') by A24,A25,COMPLSP2:40
.= 1/2*(y*'+(y - y) +y*') by A24,COMPLSP2:37
.= 1/2*(y*'+(0c (len y)) +y*') by COMPLSP2:34
.= 1/2*(y*'+y*') by A24,COMPLSP2:33
.= 1/2*y*'+1/2*y*' by A2,COMPLSP2:30
.= (1/2+1/2)*y*' by COMPLSP2:63
.= y*' by A3;
A29: len Rey = len y by COMPLSP2:48;
then
A30: len mlt(Rex,Rey) = len x by A9,A12,FINSEQ_2:72;
A31: len ((<i>)*(Imy))=len Imy by COMPLSP2:3
.= len y by COMPLSP2:48;
then len mlt(Rex,<i>*Imy)=len Rex by A9,A12,FINSEQ_2:72;
then
A32: len (mlt(Rex,Rey)-mlt(Rex,<i>*Imy))=len (mlt(Rex,Rey)) by A12,A30,
COMPLSP2:7;
A33: len Imx = len x by COMPLSP2:48;
then len (mlt(Imx,Rey)) = len x by A9,A29,FINSEQ_2:72;
then
A34: len mlt(Imx,Rey) =len mlt(Imx,<i>*Imy) by A9,A31,A33,FINSEQ_2:72;
A35: len Imy = len y by COMPLSP2:48;
then
A36: len (mlt(Imx,Imy)) = len x by A9,A33,FINSEQ_2:72;
A37: len (<i>*(mlt(Rex,Imy))) = len mlt(Rex,Imy) by COMPLSP2:3
.= len x by A9,A12,A35,FINSEQ_2:72;
A38: len (<i>*mlt(Imx,Rey)) = len (mlt(Imx,Rey)) by COMPLSP2:3
.= len x by A9,A29,A33,FINSEQ_2:72;
then
A39: len ((mlt(Rex,Rey) - ((<i>*(mlt(Rex,Imy)))))) = len (<i>*mlt(Imx,Rey))
by A30,A37,COMPLSP2:7;
len ((mlt(Rex,Rey)) - (<i>*(mlt(Rex,Imy)))) = len (<i>*mlt(Imx,Rey)) by A30
,A37,A38,COMPLSP2:7;
then
A40: len (((mlt(Rex,Rey) - (<i>*(mlt(Rex,Imy)))) + ((<i>*mlt(Imx,Rey)))) ) =
len ((mlt(Rex,Rey)) - (<i>*(mlt(Rex,Imy)))) by COMPLSP2:6
.= len mlt(Imx,Imy) by A36,A30,A37,COMPLSP2:7;
|( x,y )| = |(Re x,Re y)| - <i>*(|(Re x,Im y)|) + <i>*(|(Im x,Re y)|) +
|(Im x,Im y)| by COMPLSP2:def 4
.= Sum mlt(Re x,Re y) - <i>*(|(Re x,Im y)|) + <i>*(|(Im x,Re y)|) + |(Im
x,Im y)|
.= Sum mlt(Re x,Re y) - <i>*(Sum mlt(Re x,Im y)) + <i>*(|(Im x,Re y)|) +
|(Im x,Im y)|
.= Sum mlt(Re x,Re y) - <i>*(Sum mlt(Re x,Im y)) + <i>*(Sum mlt(Im x,Re
y)) + |(Im x,Im y)|
.= Sum (mlt(Rex,Rey)) - <i>*(Sum mlt(Rex,Imy)) + <i>*(Sum mlt(Imx,Rey))
+ Sum mlt(Im x,Im y) by A16,A18,A19
.= Sum (mlt(Rex,Rey)) - (Sum(<i>*(mlt(Rex,Imy)))) + <i>*(Sum mlt(Imx,Rey
)) + Sum mlt(Imx,Imy) by A14,Th26
.= Sum (mlt(Rex,Rey)) - (Sum(<i>*(mlt(Rex,Imy)))) + (Sum (<i>*mlt(Imx,
Rey))) + Sum mlt(Imx,Imy) by Th26
.= Sum ((mlt(Rex,Rey)) - ((<i>*(mlt(Rex,Imy))))) + (Sum (<i>*mlt(Imx,Rey
))) + Sum mlt(Imx,Imy) by A30,A37,Th29
.= Sum (((mlt(Rex,Rey)) - ((<i>*( mlt(Rex,Imy))))) + ((<i>*mlt(Imx,Rey))
)) + Sum mlt(Imx,Imy) by A39,Th34
.= Sum (mlt(Rex,Rey)- <i>*(mlt(Rex,Imy)) + <i>*mlt(Imx,Rey) + mlt(Imx,
Imy)) by A40,Th34
.= Sum (mlt(Rex,Rey)- (mlt(Rex,<i>*Imy)) + <i>*mlt(Imx,Rey) + mlt(Imx,
Imy)) by A9,A12,A35,Th23
.= Sum (mlt(Rex,Rey)-mlt(Rex,<i>*Imy) + (<i>*(mlt(Imx,Rey))+(--mlt(Imx,
Imy)))) by A36,A30,A38,A32,COMPLSP2:28
.= Sum (mlt(Rex,Rey)-mlt(Rex,<i>*Imy) + (<i>*(mlt(Imx,Rey))-<i>*<i>*(mlt
(Imx,Imy))))
.= Sum (mlt(Rex,Rey)-mlt(Rex,<i>*Imy) + (<i>*(mlt(Imx,Rey))-<i>*(<i>*(
mlt(Imx,Imy))))) by COMPLSP2:53
.= Sum (mlt(Rex,Rey)-mlt(Rex,<i>*Imy) + (<i>*(mlt(Imx,Rey))-<i>*(mlt(Imx
,<i>*Imy)))) by A9,A35,A33,Th23
.= Sum (mlt(Rex,Rey)-mlt(Rex,<i>*Imy) + <i>*(mlt(Imx,Rey)-mlt(Imx,<i>*
Imy))) by A34,COMPLSP2:43
.= Sum (mlt(Rex,Rey)-mlt(Rex,<i>*Imy) + <i>*mlt(Imx,y*')) by A9,A31,A29,A33
,A28,Th31
.= Sum (mlt(Rex,Rey-<i>*Imy) + <i>*mlt(Imx,y*')) by A9,A31,A29,A12,Th31
.= Sum ((mlt(Rex,y*'))+(mlt((<i>)*(Imx),y*'))) by A10,A28,Th24
.= Sum mlt(x,y*') by A11,A20,A26,Th33;
hence thesis;
end;
theorem
for i,j being Nat,M1,M2 being Matrix of COMPLEX st width M1=width M2 &
j in Seg len M1 holds Line(M1+M2,j)=Line(M1,j)+Line(M2,j)
proof
let i,j be Nat,M1,M2 be Matrix of COMPLEX;
assume that
A1: width M1=width M2 and
A2: j in Seg len M1;
len Line(M2,j)=width M1 by A1,MATRIX_0:def 7
.= len Line(M1,j) by MATRIX_0:def 7;
then
A3: len (Line(M1,j)+Line(M2,j))=len (Line(M1,j)) by COMPLSP2:6
.= width M1 by MATRIX_0:def 7;
A4: len (Line(M1+M2,j))=width (M1+M2) by MATRIX_0:def 7
.= width M1 by Th5;
A5: width (M1+M2)=width M1 by Th5;
now
let i be Nat;
assume that
A6: 1 <= i and
A7: i <= len Line(M1+M2,j);
A8: i in Seg width M1 by A4,A6,A7,FINSEQ_1:1;
i in Seg width M1 by A4,A6,A7,FINSEQ_1:1;
then [j,i] in [:Seg len M1,Seg width M1:] by A2,ZFMISC_1:87;
then
A9: [j,i] in Indices M1 by FINSEQ_1:def 3;
i in Seg len (Line(M1,j)+Line(M2,j)) by A3,A4,A6,A7,FINSEQ_1:1;
then
A10: i in dom (Line(M1,j)+Line(M2,j)) by FINSEQ_1:def 3;
A11: i in Seg width M2 by A1,A4,A6,A7,FINSEQ_1:1;
i in Seg width (M1+M2) by A5,A4,A6,A7,FINSEQ_1:1;
hence (Line(M1+M2,j)).i = (M1+M2)*(j,i) by MATRIX_0:def 7
.= M1*(j,i)+M2*(j,i) by A9,Th6
.= M1*(j,i)+(Line(M2,j)).i by A11,MATRIX_0:def 7
.= (Line(M1,j)).i+(Line(M2,j)).i by A8,MATRIX_0:def 7
.= (Line(M1,j)+Line(M2,j)).i by A10,COMPLSP2:1;
end;
hence thesis by A3,A4,FINSEQ_1:14;
end;
theorem Th39:
for M being Matrix of COMPLEX st i in Seg len M holds Line(M,i)=
(Line(M*',i))*'
proof
let M be Matrix of COMPLEX;
assume
A1: i in Seg len M;
A2: len Line(M,i)=width M by MATRIX_0:def 7;
A3: len ((Line(M*',i))*')=len (Line(M*',i)) by COMPLSP2:def 1
.= width (M*') by MATRIX_0:def 7
.= width M by Def1;
for j be Nat st 1 <= j & j <= len (Line(M,i)) holds (Line(M,i)).j=((Line
(M*',i))*').j
proof
A4: i <= len M by A1,FINSEQ_1:1;
A5: 1 <= i by A1,FINSEQ_1:1;
let j be Nat;
assume that
A6: 1 <= j and
A7: j <= len Line(M,i);
A8: j in Seg width M by A2,A6,A7,FINSEQ_1:1;
then
A9: j in Seg width (M*') by Def1;
j <= len ((Line(M*',i))*') by A3,A7,MATRIX_0:def 7;
then
A10: j <= len Line(M*',i) by COMPLSP2:def 1;
j <= width M by A7,MATRIX_0:def 7;
then
A11: [i,j] in Indices M by A6,A5,A4,Th1;
(Line(M,i)).j = ((M*(i,j))*')*' by A8,MATRIX_0:def 7
.= ((M*')*(i,j))*' by A11,Def1
.= ((Line(M*',i)).j)*' by A9,MATRIX_0:def 7
.= ((Line(M*',i))*').j by A6,A10,COMPLSP2:def 1;
hence thesis;
end;
hence thesis by A2,A3,FINSEQ_1:14;
end;
theorem Th40:
for F being FinSequence of COMPLEX,M being Matrix of COMPLEX st
len F=width M holds mlt(F,(Line((M*'),i))*') = mlt(Line((M*'),i),(F*'))*'
proof
let F be FinSequence of COMPLEX,M be Matrix of COMPLEX;
assume
A1: len F=width M;
len (Line((M*'),i))=width (M*') by MATRIX_0:def 7
.= width M by Def1;
hence thesis by A1,Th22;
end;
theorem Th41:
for F being FinSequence of COMPLEX,M being Matrix of COMPLEX st
len F = width M & len F >= 1 holds (M*F)*'=(M*')*(F*')
proof
let F be FinSequence of COMPLEX,M be Matrix of COMPLEX;
assume that
A1: len F = width M and
A2: len F >= 1;
A3: len (F*') = len F by COMPLSP2:def 1;
A4: width (M*')=width M by Def1;
A5: len ((M*F)*')=len (M*F) by COMPLSP2:def 1
.= len M by Def6;
A6: len (M*') = len M by Def1;
A7: now
let i be Nat;
assume that
A8: 1 <= i and
A9: i <= len ((M*F)*');
A10: i in Seg len M by A5,A8,A9,FINSEQ_1:1;
len (Line((M*'),i)) = len (F*') by A1,A3,A4,MATRIX_0:def 7;
then
A11: len (mlt(Line((M*'),i),(F*'))) >= 1 by A2,A3,FINSEQ_2:72;
A12: i in Seg len (M*') by A5,A6,A8,A9,FINSEQ_1:1;
i <= len ((M*F)) by A9,COMPLSP2:def 1;
hence ((M*F)*').i = ((M*F).i)*' by A8,COMPLSP2:def 1
.= Sum(mlt(F,Line(M,i)))*' by A10,Def6
.= Sum(mlt(F,(Line((M*'),i))*'))*' by A10,Th39
.= Sum((mlt(Line((M*'),i),(F*')))*')*' by A1,Th40
.= (Sum(mlt(Line((M*'),i),(F*'))))*'*' by A11,Th21
.= ((M*')*(F*')).i by A12,Def6;
end;
len (M*'*(F*'))=len (M*') by Def6
.= len M by Def1;
hence thesis by A5,A7,FINSEQ_1:14;
end;
theorem
for F1,F2,F3 being FinSequence of COMPLEX st len F1 = len F2 & len F2
= len F3 holds mlt(F1,mlt(F2,F3)) = mlt(mlt(F1,F2),F3)
proof
let F1,F2,F3 be FinSequence of COMPLEX;
assume that
A1: len F1=len F2 and
A2: len F2=len F3;
reconsider f3=F3 as Element of (len F3)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider f2=F2 as Element of (len F2)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider f1=F1 as Element of (len F1)-tuples_on COMPLEX by FINSEQ_2:92;
thus mlt(F1,mlt(F2,F3)) = multcomplex.:(multcomplex.:(f1,f2),f3) by A1,A2,
FINSEQOP:28
.= mlt(mlt(F1,F2),F3);
end;
theorem
for F being FinSequence of COMPLEX holds Sum -F = -(Sum F)
proof
let F be FinSequence of COMPLEX;
thus Sum -F = addcomplex $$(compcomplex*F) by SEQ_4:def 8
.= compcomplex.(addcomplex $$ F) by SEQ_4:51,52,SETWOP_2:31
.= -(Sum F) by BINOP_2:def 1;
end;
theorem Th44:
for F1,F2 being FinSequence of COMPLEX holds Sum(F1^F2) = Sum F1 + Sum F2
proof
let F1,F2 be FinSequence of COMPLEX;
thus Sum(F1^F2) = addcomplex.(addcomplex $$ F1,addcomplex $$ F2) by
FINSOP_1:5
.= Sum F1 + Sum F2 by BINOP_2:def 3;
end;
definition
let M be Matrix of COMPLEX;
func LineSum M -> FinSequence of COMPLEX means
:Def9:
len it=len M & for i being Nat st i in Seg len M holds it.i=Sum Line(M,i);
existence
proof
deffunc F(Nat) = Sum Line(M,$1);
consider z being FinSequence of COMPLEX such that
A1: len z = len M and
A2: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
take z;
thus len z = len M by A1;
let j be Nat;
dom z = Seg len M by A1,FINSEQ_1:def 3;
hence thesis by A2;
end;
uniqueness
proof
let p1,p2 be FinSequence of COMPLEX;
assume that
A3: len p1=len M and
A4: for j st j in Seg len M holds p1.j = Sum Line(M,j) and
A5: len p2=len M and
A6: for j st j in Seg len M holds p2.j = Sum Line(M,j);
A7: dom p1 = Seg len M by A3,FINSEQ_1:def 3;
for j be Nat st j in dom p1 holds p1.j=p2.j
proof
let j be Nat;
assume
A8: j in dom p1;
then p1.j = Sum Line(M,j) by A4,A7;
hence thesis by A6,A7,A8;
end;
hence thesis by A3,A5,FINSEQ_2:9;
end;
end;
definition
let M be Matrix of COMPLEX;
func ColSum M -> FinSequence of COMPLEX means
:Def10:
len it=width M & for j
being Nat st j in Seg width M holds it.j=Sum (Col(M,j));
existence
proof
deffunc F(Nat) = Sum Col(M,$1);
consider f being FinSequence of COMPLEX such that
A1: len f = width M and
A2: for j be Nat st j in dom f holds f.j = F(j) from FINSEQ_2:sch 1;
take f;
thus len f = width M by A1;
let j be Nat;
dom f = Seg width M by A1,FINSEQ_1:def 3;
hence thesis by A2;
end;
uniqueness
proof
let p1,p2 be FinSequence of COMPLEX;
assume that
A3: len p1=width M and
A4: for j st j in Seg width M holds p1.j = Sum (Col(M,j)) and
A5: len p2=width M and
A6: for j st j in Seg width M holds p2.j = Sum (Col(M,j));
A7: dom p1 = Seg width M by A3,FINSEQ_1:def 3;
for j be Nat st j in dom p1 holds p1.j=p2.j
proof
let j be Nat;
assume
A8: j in dom p1;
then p1.j = (Sum (Col(M,j))) by A4,A7;
hence thesis by A6,A7,A8;
end;
hence thesis by A3,A5,FINSEQ_2:9;
end;
end;
theorem Th45:
for F being FinSequence of COMPLEX holds len F = 1 implies Sum F = F.1
proof
let F be FinSequence of COMPLEX;
assume len F = 1;
then F = <* F.1 *> by FINSEQ_1:40;
hence thesis by FINSOP_1:11;
end;
theorem Th46:
for f,g being FinSequence of COMPLEX,n being Nat st len f = n +
1 & g = f|n holds Sum f = Sum g + f/.(len f)
proof
let f,g be FinSequence of COMPLEX,n be Nat;
assume that
A1: len f = n + 1 and
A2: g = f|n;
A3: dom f = Seg(n+1) by A1,FINSEQ_1:def 3;
set q = <*f/.len f*>;
set p = g^q;
A4: len q = 1 by FINSEQ_1:39;
set n9=Seg n;
A5: g=f|n9 by A2,FINSEQ_1:def 16;
A6: n <= len f by A1,NAT_1:11;
A7: now
let u be object;
assume
A8: u in dom f;
then u in { k where k is Nat : 1 <= k & k <= n+1 } by A3,FINSEQ_1:def 1;
then consider i being Nat such that
A9: u = i and
A10: 1 <= i and
A11: i <= n+1;
now
per cases;
case
A12: i = n+1;
then
A13: len g + 1 <= i by A1,A2,FINSEQ_1:59,NAT_1:11;
i <= len g + len q by A1,A2,A4,A12,FINSEQ_1:59,NAT_1:11;
hence p.i = q.(i-len g) by A13,FINSEQ_1:23
.= q.(n+1-n) by A1,A2,A12,FINSEQ_1:59,NAT_1:11
.= f/.(n+1) by A1,FINSEQ_1:40
.= f.i by A8,A9,A12,PARTFUN1:def 6;
end;
case
i <> n+1;
then i < n+1 by A11,XXREAL_0:1;
then i <= n by NAT_1:13;
then i in { k where k is Nat : 1 <= k & k <= n } by A10;
then i in Seg n by FINSEQ_1:def 1;
then
A14: i in dom g by A5,A6,FINSEQ_1:17;
then p.i = g.i by FINSEQ_1:def 7;
hence p.i = f.i by A5,A14,FUNCT_1:47;
end;
end;
hence f.u = p.u by A9;
end;
len(g^q) = len g + len q by FINSEQ_1:22
.= len g + 1 by FINSEQ_1:40
.= len f by A1,A2,FINSEQ_1:59,NAT_1:11;
then dom f = Seg len(g^q) by FINSEQ_1:def 3
.= dom(g^q) by FINSEQ_1:def 3;
then f = g^<*(f/.(len f))*> by A7,FUNCT_1:2;
hence Sum f = Sum g + Sum <*(f/.len f)*> by Th44
.= Sum g + (f/.len f) by FINSOP_1:11;
end;
theorem Th47:
for M being Matrix of COMPLEX st len M > 0 holds Sum LineSum M = Sum ColSum M
proof
defpred P[Nat] means for N being Matrix of COMPLEX st $1+1=len N holds Sum
LineSum N=Sum ColSum N;
let M be Matrix of COMPLEX;
assume len M > 0;
then 0+1 <= len M by NAT_1:8;
then 0+1-1<=len M-1 by XREAL_1:9;
then
A1: len M-'1=len M-1 by XREAL_0:def 2;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A3: P[k];
for N being Matrix of COMPLEX st k+1+1=len N holds Sum LineSum N=Sum
ColSum N
proof
reconsider k1=k+1 as Element of NAT;
let N be Matrix of COMPLEX;
consider n such that
A4: for x being object st x in rng N ex p being FinSequence of COMPLEX
st x = p & len p = n by MATRIX_0:9;
A5: rng (N|k1) c= rng N by FINSEQ_5:19;
then for x being object st x in rng (N|k1) ex p being FinSequence of
COMPLEX st x=p & len p=n by A4;
then reconsider N2=N|k1 as Matrix of COMPLEX by MATRIX_0:9;
set g1=LineSum N2;
consider n3 being Nat such that
A6: for x2 being object st x2 in rng N holds ex s being FinSequence st
s=x2 & len s=n3 by MATRIX_0:def 1;
set f3=LineSum N;
A7: len Line(N,(k+1+1))=width N by MATRIX_0:def 7;
assume
A8: k+1+1=len N;
then
A9: len N2=k+1 by FINSEQ_1:59,NAT_1:11;
A10: len g1 = len N2 by Def9
.= k1 by A8,FINSEQ_1:59,NAT_1:11;
1+k>=1 by NAT_1:11;
then
A11: len N2>=1 by A8,FINSEQ_1:59,NAT_1:11;
then
A12: len N2>0;
1 in Seg len N2 by A11,FINSEQ_1:1;
then 1 in dom N2 by FINSEQ_1:def 3;
then
A13: N2.1 in rng N2 by FUNCT_1:3;
then ex s3 being FinSequence st s3=N2.1 & len s3=n3 by A5,A6;
then
A14: width N2=n3 by A13,A12,MATRIX_0:def 3;
A15: len N>=1 by A8,NAT_1:11;
then
A16: len N>0;
1 in Seg len N by A15,FINSEQ_1:1;
then
A17: 1 in dom N by FINSEQ_1:def 3;
then
A18: N.1 in rng N by FUNCT_1:3;
A19: ex s2 being FinSequence st s2=N.1 & len s2=n3 by A6,A17,FUNCT_1:3;
then
A20: width N2= width N by A18,A14,A16,MATRIX_0:def 3;
len f3= k1+1 by A8,Def9;
then
A21: len (f3|k1) = len g1 by A10,FINSEQ_1:59,NAT_1:11;
A22: for n being Nat st 1 <= n & n <= len (f3|k1) holds (f3|k1).n=g1.n
proof
let n be Nat;
assume that
A23: 1 <= n and
A24: n <= len (f3|k1);
A25: n <= k1+1 by A10,A21,A24,NAT_1:13;
then
A26: n in Seg len N by A8,A23,FINSEQ_1:1;
A27: for n1 being Nat st 1 <= n1 & n1 <= len (Line(N,n)) holds Line(N
,n).n1=Line(N2,n).n1
proof
A28: N2.n=N.n by A10,A21,A24,FINSEQ_3:112;
A29: n<=len N2 by A21,A24,Def9;
let n1 be Nat;
assume that
A30: 1 <= n1 and
A31: n1 <= len (Line(N,n));
A32: n1 in Seg (len (Line(N,n))) by A30,A31,FINSEQ_1:1;
then
A33: n1 in Seg width N2 by A20,MATRIX_0:def 7;
A34: n1 in Seg width N by A32,MATRIX_0:def 7;
then n1 <= width N by FINSEQ_1:1;
then [n,n1] in Indices N by A8,A23,A25,A30,Th1;
then
A35: ex pn being FinSequence of COMPLEX st pn=N.n & N*(n,n1)= pn.
n1 by MATRIX_0:def 5;
n1<=width N by A34,FINSEQ_1:1;
then n1<=width N2 by A8,A18,A19,A14,MATRIX_0:def 3;
then
A36: [n,n1] in Indices (N2) by A23,A30,A29,Th1;
n1 in Seg width N by A32,MATRIX_0:def 7;
then Line(N,n).n1=N*(n,n1) by MATRIX_0:def 7
.=N2*(n,n1) by A36,A35,A28,MATRIX_0:def 5
.=Line(N2,n).n1 by A33,MATRIX_0:def 7;
hence thesis;
end;
len Line(N,n) = width N by MATRIX_0:def 7
.= width N2 by A8,A18,A19,A14,MATRIX_0:def 3
.= len (Line(N2,n)) by MATRIX_0:def 7;
then
A37: Line(N,n)=Line(N2,n) by A27,FINSEQ_1:14;
n in Seg len (f3|k1) by A23,A24,FINSEQ_1:1;
then n in dom(f3|k1) by FINSEQ_1:def 3;
then
A38: n in dom(f3|Seg k1) by FINSEQ_1:def 16;
n in Seg k1 by A10,A21,A23,A24,FINSEQ_1:1;
then
A39: n in Seg len N2 by A8,FINSEQ_1:59,NAT_1:11;
(f3|k1).n=(f3|Seg k1).n by FINSEQ_1:def 16
.=(LineSum(N)).n by A38,FUNCT_1:47
.= Sum (Line(N2,n)) by A26,A37,Def9
.= g1.n by A39,Def9;
hence thesis;
end;
len ColSum N2=width N2 by Def10;
then
A40: len (ColSum(N2)+Line(N,(k+1+1))) = width N by A20,A7,COMPLSP2:6
.= len ColSum N by Def10;
A41: len ColSum N2=width N2 by Def10
.= width N by A8,A18,A19,A14,MATRIX_0:def 3
.= len Line(N,(k+1+1)) by MATRIX_0:def 7;
A42: k+1+1 in Seg len N by A8,FINSEQ_1:3;
then k+1+1 in Seg len LineSum N by Def9;
then
A43: k+1+1 in dom LineSum N by FINSEQ_1:def 3;
A44: len N >= k+1 by A8,NAT_1:11;
A45: for j st 1<=j & j<=width N holds (ColSum N2).j+N*(k+1+1,j)=(ColSum N).j
proof
let j;
assume that
A46: 1<=j and
A47: j<=width N;
set g=Col(N2,j);
set f=Col(N,j);
A48: k1 <= len f by A44,MATRIX_0:def 8;
A49: for n be Nat st 1 <=n & n <= len (f|k1) holds (f|k1).n=g.n
proof
let n be Nat;
assume that
A50: 1 <= n and
A51: n <= len (f|k1);
A52: n <= k1 by A48,A51,FINSEQ_1:59;
then
A53: N2.n=N.n by FINSEQ_3:112;
n <= k1+1 by A52,NAT_1:13;
then n in Seg len N by A8,A50,FINSEQ_1:1;
then
A54: n in dom N by FINSEQ_1:def 3;
n<=len N by A8,A52,NAT_1:13;
then [n,j] in Indices N by A46,A47,A50,Th1;
then
A55: ex pn being FinSequence of COMPLEX st pn=N.n & N*(n,j)= pn.j
by MATRIX_0:def 5;
A56: j<=width N2 by A8,A18,A19,A14,A47,MATRIX_0:def 3;
n in Seg k1 by A50,A52,FINSEQ_1:1;
then
A57: n in dom N2 by A9,FINSEQ_1:def 3;
n in Seg len (f|k1) by A50,A51,FINSEQ_1:1;
then n in dom(f|k1) by FINSEQ_1:def 3;
then
A58: n in dom(f|Seg k1) by FINSEQ_1:def 16;
n<=len N2 by A9,A48,A51,FINSEQ_1:59;
then
A59: [n,j] in Indices N2 by A46,A50,A56,Th1;
(f|k1).n=(f|Seg k1).n by FINSEQ_1:def 16
.=(Col(N,j)).n by A58,FUNCT_1:47
.= N*(n,j) by A54,MATRIX_0:def 8
.= N2*(n,j) by A59,A55,A53,MATRIX_0:def 5
.= g.n by A57,MATRIX_0:def 8;
hence thesis;
end;
A60: k+1+1 in Seg len N by A8,FINSEQ_1:4;
then
A61: k+1+1 in dom N by FINSEQ_1:def 3;
len g = len N2 by MATRIX_0:def 8
.= k1 by A8,FINSEQ_1:59,NAT_1:11;
then
A62: g=f|k1 by A48,A49,FINSEQ_1:14,59;
A63: len (Col(N,j))=len N by MATRIX_0:def 8;
k+1+1 in Seg len Col(N,j) by A60,MATRIX_0:def 8;
then
A64: k+1+1 in dom Col(N,j) by FINSEQ_1:def 3;
A65: j in Seg width N by A46,A47,FINSEQ_1:1;
then
(ColSum N2).j+N*(k+1+1,j) = Sum (Col(N2,j))+N*((k+1+1),j) by A20,Def10
.= Sum (Col(N2,j))+Col(N,j).(k+1+1) by A61,MATRIX_0:def 8
.= Sum (Col(N2,j))+Col(N,j)/.(k+1+1) by A64,PARTFUN1:def 6
.= Sum (Col(N,j)) by A8,A63,A62,Th46
.=(ColSum N).j by A65,Def10;
hence thesis;
end;
A66: for j be Nat st 1<=j & j<= len ColSum N holds (ColSum(N2)+Line(N,k+
1+1)).j=(ColSum N).j
proof
let j be Nat;
assume that
A67: 1<=j and
A68: j<= len ColSum N;
j in Seg len ColSum N by A67,A68,FINSEQ_1:1;
then
A69: j in Seg width N2 by A20,Def10;
then
A70: j<=width N by A20,FINSEQ_1:1;
j in Seg len ((ColSum(N2)+Line(N,k+1+1))) by A40,A67,A68,FINSEQ_1:1;
then j in dom ((ColSum(N2)+Line(N,k+1+1))) by FINSEQ_1:def 3;
then (ColSum(N2)+Line(N,(k+1+1))).j = (ColSum N2).j+(Line(N,k+1+1)).j
by COMPLSP2:1
.= (ColSum N2).j+N*(k+1+1,j) by A20,A69,MATRIX_0:def 7
.= (ColSum N).j by A45,A67,A70;
hence thesis;
end;
len LineSum N = len N by Def9;
then Sum LineSum N =Sum (LineSum N2)+(LineSum N)/.(k+1+1) by A8,A21,A22
,Th46,FINSEQ_1:14
.=Sum (LineSum N2)+(LineSum N).(k+1+1) by A43,PARTFUN1:def 6
.=Sum (ColSum N2)+(LineSum N).(k+1+1) by A3,A9
.=Sum (ColSum N2)+Sum (Line(N,(k+1+1))) by A42,Def9
.=Sum (ColSum(N2)+Line(N,(k+1+1))) by A41,Th34
.=Sum ColSum N by A40,A66,FINSEQ_1:14;
hence thesis;
end;
hence thesis;
end;
for N being Matrix of COMPLEX st 0+1=len N holds Sum LineSum N=Sum ColSum N
proof
let N be Matrix of COMPLEX;
A71: len Line(N,1)=width N by MATRIX_0:def 7;
assume
A72: 0+1=len N;
then
A73: 1 in Seg len N by FINSEQ_1:3;
A74: 1 in Seg 1 by FINSEQ_1:3;
A75: for j be Nat st 1<=j & j<= width N holds (ColSum(N)).j=Line(N,1).j
proof
A76: 1 in dom N by A72,A74,FINSEQ_1:def 3;
let j be Nat;
assume that
A77: 1<=j and
A78: j<= width N;
A79: len (Col(N,j)) = 1 by A72,MATRIX_0:def 8;
A80: j in Seg width N by A77,A78,FINSEQ_1:1;
then (ColSum N).j=Sum Col(N,j) by Def10
.= (Col(N,j)).1 by A79,Th45
.= N*(1,j) by A76,MATRIX_0:def 8
.= Line(N,1).j by A80,MATRIX_0:def 7;
hence thesis;
end;
A81: len LineSum N=1 by A72,Def9;
len ColSum N=width N by Def10;
then Sum ColSum N = Sum Line(N,1) by A71,A75,FINSEQ_1:14
.=(LineSum N).1 by A73,Def9
.= Sum LineSum N by A81,Th45;
hence thesis;
end;
then
A82: P[0];
for i holds P[i] from NAT_1:sch 2(A82,A2);
then (len M)-'1+1=len M implies Sum LineSum M=Sum ColSum M;
hence thesis by A1;
end;
definition
let M be Matrix of COMPLEX;
func SumAll M -> Element of COMPLEX equals
Sum LineSum M;
coherence;
end;
theorem Th48:
for M being Matrix of COMPLEX holds ColSum M = LineSum(M@)
proof
let M be Matrix of COMPLEX;
A1: len ColSum M=width M by Def10;
A2: len (LineSum(M@))=len (M@) by Def9;
A3: now
let i be Nat;
assume that
A4: 1 <= i and
A5: i <= len ColSum M;
i <= len LineSum(M@) by A2,A1,A5,MATRIX_0:def 6;
then i in Seg len LineSum(M@) by A4,FINSEQ_1:1;
then
A6: i in Seg len (M@) by Def9;
A7: i in Seg width M by A1,A4,A5,FINSEQ_1:1;
hence (ColSum M).i = Sum Col(M,i) by Def10
.= Sum (Line(M@,i)) by A7,MATRIX_0:59
.= (LineSum(M@)).i by A6,Def9;
end;
len ColSum M=len LineSum(M@) by A2,A1,MATRIX_0:def 6;
hence thesis by A3,FINSEQ_1:14;
end;
theorem Th49:
for M being Matrix of COMPLEX st len M > 0 holds SumAll M = SumAll (M@)
proof
let M be Matrix of COMPLEX;
assume len M > 0;
then SumAll M = Sum ColSum M by Th47
.= SumAll(M@) by Th48;
hence thesis;
end;
definition
let x,y be FinSequence of COMPLEX,M be Matrix of COMPLEX;
assume that
A1: len x=len M and
A2: len y=width M;
func QuadraticForm(x,M,y) -> Matrix of COMPLEX means
:Def12:
len it = len x & width it=len y &
for i,j being Nat st [i,j] in Indices M holds it*(i,j)=(x.i)
*(M*(i,j))*((y.j)*');
existence
proof
deffunc F(Nat,Nat) = In((x.$1)*(M*($1,$2))*((y.$2)*'),COMPLEX);
consider M1 being Matrix of len M,width M,COMPLEX such that
A3: for i,j st [i,j] in Indices M1 holds M1*(i,j) = F(i,j) from
MATRIX_0:sch 1;
take M1;
thus
A4: len M1=len x by A1,MATRIX_0:def 2;
thus
A5: now
per cases;
suppose
A6: len M= 0;
then width M1=0 by A1,A4,MATRIX_0:def 3;
hence width M1=len y by A2,A6,MATRIX_0:def 3;
end;
suppose
len M>0;
hence width M1=len y by A2,MATRIX_0:23;
end;
end;
A7: dom M = dom M1 by A1,A4,FINSEQ_3:29;
let i,j be Nat;
assume [i,j] in Indices M;
then [i,j] in Indices M1 by A7,A5,A2;
then M1*(i,j) = F(i,j) by A3;
hence thesis;
end;
uniqueness
proof
let M1,M2 be Matrix of COMPLEX;
assume that
A8: len M1=len x and
A9: width M1=len y and
A10: for i,j st [i,j] in Indices M holds M1*(i,j)=(x.i)*(M*(i,j))*((y.
j) *') and
A11: len M2=len x and
A12: width M2=len y and
A13: for i,j st [i,j] in Indices M holds M2*(i,j)=(x.i)*(M*(i,j))*((y. j) *');
now
let i,j;
assume
A14: [i,j] in Indices M1;
A15: dom M1 = dom M by A1,A8,FINSEQ_3:29;
hence M1*(i,j)=(x.i)*(M*(i,j))*((y.j)*') by A2,A9,A10,A14
.=M2*(i,j) by A2,A9,A13,A14,A15;
end;
hence thesis by A8,A9,A11,A12,MATRIX_0:21;
end;
end;
theorem Th50:
for x,y being FinSequence of COMPLEX,M being Matrix of COMPLEX
st len x = len M & len y = width M & len y > 0 holds (QuadraticForm(x,M,y))@ =
(QuadraticForm(y,M@",x))*'
proof
let x,y be FinSequence of COMPLEX,M be Matrix of COMPLEX;
assume that
A1: len x=len M and
A2: len y =width M and
A3: len y > 0;
A4: width (M@") = width (M@) by Def1
.= len x by A1,A2,A3,MATRIX_0:54;
A5: width (QuadraticForm(x,M,y))=len y by A1,A2,Def12;
then
A6: width ((QuadraticForm(x,M,y))@) = len (QuadraticForm(x,M,y)) by A3,
MATRIX_0:54;
len (M@")=len (M@) by Def1;
then
A7: len (M@")=width M by MATRIX_0:def 6;
A8: len (x*') = len x by COMPLSP2:def 1;
A9: len ((QuadraticForm(x,M,y))@) = width (QuadraticForm(x,M,y)) by
MATRIX_0:def 6;
A10: len (M@") = len (M@) by Def1
.= len y by A2,MATRIX_0:def 6;
then
A11: width (QuadraticForm(y,M@",x))= len x by A4,Def12;
A12: len ((QuadraticForm(y,M@",x))*')=len (QuadraticForm(y,M@",x)) by Def1
.= len y by A10,A4,Def12;
A13: len ((QuadraticForm(x,M,y))@) = width (QuadraticForm(x,M,y)) by
MATRIX_0:def 6
.= len y by A1,A2,Def12;
A14: len QuadraticForm(y,M@",x) = len y by A10,A4,Def12;
A15: for i,j st [i,j] in Indices ((QuadraticForm(x,M,y))@) holds ((
QuadraticForm(y,M@",x))*')*(i,j) = ((QuadraticForm(x,M,y))@)*(i,j)
proof
let i,j;
reconsider i9=i, j9=j as Element of NAT by ORDINAL1:def 12;
assume
A16: [i,j] in Indices ((QuadraticForm(x,M,y))@);
then
A17: 1<=j by Th1;
A18: j<=len QuadraticForm(x,M,y) by A6,A16,Th1;
then
A19: j<=len M by A1,A2,Def12;
A20: 1<=i by A16,Th1;
A21: i<=width QuadraticForm(x,M,y) by A9,A16,Th1;
then i<=width M by A1,A2,Def12;
then
A22: [j,i] in Indices M by A17,A20,A19,Th1;
A23: j<=width (M@") by A1,A2,A4,A18,Def12;
A24: 1<=i by A16,Th1;
1<=i by A16,Th1;
then
A25: [j,i] in Indices (QuadraticForm(x,M,y)) by A21,A17,A18,Th1;
i<=len (M@") by A1,A2,A7,A21,Def12;
then
A26: [i,j] in Indices (M@") by A17,A24,A23,Th1;
A27: j<=len x by A1,A2,A18,Def12;
A28: j<=len x by A1,A2,A18,Def12;
A29: j<=width QuadraticForm(y,M@",x) by A1,A2,A11,A18,Def12;
A30: 1<=i by A16,Th1;
i<=len QuadraticForm(y,M@",x) by A1,A2,A14,A21,Def12;
then [i,j] in Indices QuadraticForm(y,M@",x) by A17,A30,A29,Th1;
then ((QuadraticForm(y,M@",x))*')*(i,j) = ((QuadraticForm(y,M@",x))*(i,j)
*') by Def1
.= ((y.i)*((M@")*(i,j))*((x.j)*'))*' by A10,A4,A26,Def12
.= ((y.i)*((M@")*(i9,j9))*((x*'.j)))*' by A17,A27,COMPLSP2:def 1
.= (((y.i)*((M@")*(i,j)))*')*((x*'.j)*') by COMPLEX1:35
.= (((y.i)*((M@")*(i9,j9)))*')*((x*')*'.j) by A8,A17,A28,COMPLSP2:def 1
.= ((y.i)*')*(((M@")*(i,j)*'))*((x*')*'.j) by COMPLEX1:35
.= ((y.i)*')*(((M@")*')*(i,j))*((x*')*'.j) by A26,Def1
.= ((y.i)*')*(((M@")*')*(i,j))*(x.j)
.= ((y.i)*')*((M@)*(i,j))*(x.j)
.= ((y.i)*')*(M*(j,i))*(x.j) by A22,MATRIX_0:def 6
.= (x.j)*(M*(j,i))*((y.i)*')
.= (QuadraticForm(x,M,y))*(j,i) by A1,A2,A22,Def12
.= ((QuadraticForm(x,M,y))@)*(i,j) by A25,MATRIX_0:def 6;
hence thesis;
end;
A31: width ((QuadraticForm(y,M@",x))*') = width (QuadraticForm(y,M@",x)) by
Def1
.= len x by A10,A4,Def12;
width ((QuadraticForm(x,M,y))@) = len (QuadraticForm(x,M,y)) by A3,A5,
MATRIX_0:54
.= len x by A1,A2,Def12;
hence thesis by A13,A12,A31,A15,MATRIX_0:21;
end;
theorem Th51:
for x,y being FinSequence of COMPLEX,M being Matrix of COMPLEX
st len x=len M & len y =width M holds (QuadraticForm(x,M,y))*'=QuadraticForm(x
*',M*',y*')
proof
let x,y be FinSequence of COMPLEX,M be Matrix of COMPLEX;
assume that
A1: len x=len M and
A2: len y =width M;
A3: len (y*') = len y by COMPLSP2:def 1;
then
A4: len (y*') = width (M*') by A2,Def1;
len (M*') = len M by Def1;
then
A5: len (x*') = len (M*') by A1,COMPLSP2:def 1;
then
A6: len (QuadraticForm(x*',M*',y*')) = len (x*') by A4,Def12
.= len M by A1,COMPLSP2:def 1;
A7: width ((QuadraticForm(x,M,y))*')=width QuadraticForm(x,M,y) by Def1;
A8: len ((QuadraticForm(x,M,y))*') = len QuadraticForm(x,M,y) by Def1;
A9: for i,j st [i,j] in Indices ((QuadraticForm(x,M,y))*') holds ((
QuadraticForm(x,M,y))*')*(i,j) = (QuadraticForm(x*',M*',y*'))*(i,j)
proof
let i,j;
reconsider i9=i, j9=j as Element of NAT by ORDINAL1:def 12;
assume
A10: [i,j] in Indices ((QuadraticForm(x,M,y))*');
then
A11: 1<=i by Th1;
A12: i<=len (QuadraticForm(x,M,y)) by A8,A10,Th1;
then
A13: i<=len x by A1,A2,Def12;
i<=len M by A1,A2,A12,Def12;
then
A14: i<=len (M*') by Def1;
A15: j<=width (QuadraticForm(x,M,y)) by A7,A10,Th1;
then
A16: j<=len y by A1,A2,Def12;
j<=width M by A1,A2,A15,Def12;
then
A17: j<=width (M*') by Def1;
1<=j by A10,Th1;
then
A18: [i,j] in Indices (M*') by A11,A14,A17,Th1;
A19: j<=width M by A1,A2,A15,Def12;
A20: 1<=i by A10,Th1;
A21: 1<=j by A10,Th1;
i<=len M by A1,A2,A12,Def12;
then
A22: [i,j] in Indices M by A21,A20,A19,Th1;
[i,j] in Indices QuadraticForm(x,M,y) by A11,A12,A21,A15,Th1;
then
((QuadraticForm(x,M,y))*')*(i,j) =((QuadraticForm(x,M,y))*(i,j))*' by Def1
.=((x.i)*(M*(i,j))*((y.j)*'))*' by A1,A2,A22,Def12
.=((x.i)*(M*(i9,j9))*((y*'.j)))*' by A21,A16,COMPLSP2:def 1
.= (((x.i)*(M*(i,j)))*')*((y*'.j)*') by COMPLEX1:35
.= (((x.i)*(M*(i9,j9)))*')*((y*')*'.j) by A3,A21,A16,COMPLSP2:def 1
.= ((x.i)*')*((M*(i,j)*'))*(((y*')*'.j)) by COMPLEX1:35
.= ((x.i)*')*((M*')*(i,j))*(((y*')*'.j)) by A22,Def1
.= ((x.i)*')*((M*')*(i9,j9))*(((y*').j)*') by A3,A21,A16,COMPLSP2:def 1
.= ((x*').i)*((M*')*(i9,j9))*(((y*').j)*') by A11,A13,COMPLSP2:def 1
.= (QuadraticForm(x*',M*',y*'))*(i,j) by A5,A4,A18,Def12;
hence thesis;
end;
A23: width ((QuadraticForm(x,M,y))*')=width (QuadraticForm(x,M,y)) by Def1
.= len y by A1,A2,Def12;
A24: width QuadraticForm(x*',M*',y*')=len (y*') by A5,A4,Def12
.= len y by COMPLSP2:def 1;
len ((QuadraticForm(x,M,y))*') = len QuadraticForm(x,M,y) by Def1
.= len M by A1,A2,Def12;
hence thesis by A6,A23,A24,A9,MATRIX_0:21;
end;
theorem Th52:
for x,y being FinSequence of COMPLEX st len x=len y & 0 < len y
holds |(x,y)|=(|(y,x)|)*'
proof
let x,y be FinSequence of COMPLEX;
assume that
A1: len x=len y and
A2: 0 < len y;
A3: 0+1 <= len x by A1,A2,NAT_1:8;
len (x*') = len (x) by COMPLSP2:def 1;
then
A4: len (mlt(y,(x*'))) = len y by A1,FINSEQ_2:72;
(|(y,x)|)*' = (Sum (mlt(y,(x*'))))*' by A1,Th37
.= Sum (mlt(y,(x*'))*') by A1,A3,A4,Th21
.= Sum (mlt(x,(y*'))) by A1,Th22
.= |(x, y)| by A1,Th37;
hence thesis;
end;
theorem Th53:
for x,y being FinSequence of COMPLEX st len x=len y & 0 < len y
holds (|(x,y)|)*'=|(x*',y*')|
proof
let x,y be FinSequence of COMPLEX;
assume that
A1: len x=len y and
A2: 0 < len y;
A3: 0+1 <= len x by A1,A2,NAT_1:8;
A4: len (y*') = len y by COMPLSP2:def 1;
then
A5: len (mlt(x,y*')) = len x by A1,FINSEQ_2:72;
len (x*') = len x by COMPLSP2:def 1;
then |(x*',y*')| = Sum (mlt(x*',(y*')*')) by A1,A4,Th37
.= Sum ((mlt(x,y*'))*') by A1,A4,Th25
.= (Sum (mlt(x,y*')))*' by A3,A5,Th21
.= (|(x, y)|)*' by A1,Th37;
hence thesis;
end;
theorem
for M being Matrix of COMPLEX st width M > 0 holds (M@)*' =(M*')@
proof
let M be Matrix of COMPLEX;
assume
A1: width M > 0;
width (M*') = width M by Def1;
then
A2: width ((M*')@) = len (M*') by A1,MATRIX_0:54
.= len M by Def1;
A3: width ((M@)*') = width (M@) by Def1;
A4: len ((M@)*') = len (M@) by Def1
.= width M by MATRIX_0:def 6;
A5: width ((M@)*') = width (M@) by Def1
.= len M by A1,MATRIX_0:54;
A6: len ((M@)*') = len (M@) by Def1;
A7: for i,j st [i,j] in Indices ((M@)*') holds ((M@)*')*(i,j) = ((M*')@)*(i, j)
proof
let i,j;
assume
A8: [i,j] in Indices ((M@)*');
then
A9: 1<= i by Th1;
A10: 1<=j by A8,Th1;
A11: j<=width (M@) by A3,A8,Th1;
i<=len (M@) by A6,A8,Th1;
then
A12: [i,j] in Indices (M@) by A9,A10,A11,Th1;
then
A13: [j,i] in Indices (M) by MATRIX_0:def 6;
j<=width ((M@)*') by A8,Th1;
then
A14: j<=len (M*') by A5,Def1;
i<=len ((M@)*') by A8,Th1;
then
A15: i<=width (M*') by A4,Def1;
A16: 1<=i by A8,Th1;
1<= j by A8,Th1;
then
A17: [j,i] in Indices (M*') by A14,A16,A15,Th1;
((M@)*')*(i,j) = ((M@)*(i,j))*' by A12,Def1
.= (M*(j,i))*' by A13,MATRIX_0:def 6
.= ((M*'))*(j,i) by A13,Def1
.= ((M*')@)*(i,j) by A17,MATRIX_0:def 6;
hence thesis;
end;
len ((M*')@) = width (M*') by MATRIX_0:def 6
.= width M by Def1;
hence thesis by A4,A5,A2,A7,MATRIX_0:21;
end;
theorem Th55:
for x,y being FinSequence of COMPLEX,M being Matrix of COMPLEX
st len x=width M & len y = len M & len x>0 & len y>0 holds |(x,(M@")*y)| =
SumAll QuadraticForm(x,M@,y)
proof
let x,y be FinSequence of COMPLEX,M be Matrix of COMPLEX;
assume that
A1: len x=width M and
A2: len y = len M and
A3: len x>0 and
A4: len y>0;
A5: width (M@) = len y by A1,A2,A3,MATRIX_0:54;
then
A6: width ((M@)*')=len y by Def1;
A7: dom LineSum QuadraticForm(x,M@,y) = Seg len LineSum QuadraticForm(x,M@,
y) by FINSEQ_1:def 3
.= Seg len QuadraticForm(x,M@,y) by Def9;
A8: len (M@)=len x by A1,MATRIX_0:def 6;
A9: len LineSum(QuadraticForm(x,M@,y)) = len QuadraticForm(x,M@,y) by Def9
.= len x by A8,A5,Def12;
A10: len (M@")=len (M@) by Def1
.=len x by A1,MATRIX_0:def 6;
then
A11: len ((M@")*y)= len x by Def6;
then len (((M@")*y)*')= len x by COMPLSP2:def 1;
then
A12: len LineSum(QuadraticForm(x,M@,y)) = len mlt(x,((M@")*y)*') by A9,
FINSEQ_2:72;
A13: 0+1<=len y by A4,NAT_1:13;
for i be Nat st 1<=i & i<=len (LineSum(QuadraticForm(x,M@,y))) holds (
LineSum(QuadraticForm(x,M@,y))).i = (mlt(x,((M@")*y)*')).i
proof
let i be Nat;
assume that
A14: 1<=i and
A15: i<=len LineSum(QuadraticForm(x,M@,y));
A16: len y = width QuadraticForm(x,M@,y) by A8,A5,Def12
.=len Line(QuadraticForm(x,M@,y),i) by MATRIX_0:def 7;
A17: len (Line(M@",i))=len y by A6,MATRIX_0:def 7;
then
A18: len mlt(Line(M@",i),y)>=1 by A13,FINSEQ_2:72;
len (M@)=len QuadraticForm(x,M@,y) by A8,A5,Def12;
then
A19: len (M@)=len LineSum(QuadraticForm(x,M@,y)) by Def9;
then
A20: i in Seg len (M@") by A8,A10,A14,A15,FINSEQ_1:1;
A21: for j being Nat st 1<=j & j<= len (Line(QuadraticForm(x,M@,y),i))
holds ((x.i)*(mlt(Line((M@"),i),y))*').j =(Line(QuadraticForm(x,M@,y),i)).j
proof
A22: len (Line(M@,i))=width (M@) by MATRIX_0:def 7
.=len y by A1,A2,A3,MATRIX_0:54
.=len (y*') by COMPLSP2:def 1;
let j be Nat;
assume that
A23: 1<=j and
A24: j<= len (Line(QuadraticForm(x,M@,y),i));
A25: j in Seg width (M@) by A5,A16,A23,A24,FINSEQ_1:1;
j in Seg len y by A16,A23,A24,FINSEQ_1:1;
then j in Seg len (y*') by COMPLSP2:def 1;
then j in Seg len mlt(Line(M@,i),y*') by A22,FINSEQ_2:72;
then
A26: j in dom mlt(Line(M@,i),y*') by FINSEQ_1:def 3;
j in Seg len (Line(QuadraticForm(x,M@,y),i)) by A23,A24,FINSEQ_1:1;
then
A27: j in Seg width QuadraticForm(x,M@,y) by MATRIX_0:def 7;
j <= width (M@) by A1,A2,A3,A16,A24,MATRIX_0:54;
then
A28: [i,j] in Indices (M@) by A14,A15,A19,A23,Th1;
((x.i)*(mlt(Line((M@"),i),y))*').j =(x.i)*(((mlt(Line((M@"),i),y))
*').j) by COMPLSP2:16
.=(x.i)*((mlt((Line((M@"),i))*',y*')).j) by A17,Th25
.=(x.i)*((mlt(Line(M@,i),y*')).j) by A8,A10,A20,Th39
.=(x.i)*(((Line(M@,i)).j)*((y*').j)) by A26,Th17
.=(x.i)*(((Line(M@,i)).j)*((y.j)*')) by A16,A23,A24,COMPLSP2:def 1
.=(x.i)*((Line(M@,i)).j)*((y.j)*')
.=(x.i)*((M@)*(i,j))*((y.j)*') by A25,MATRIX_0:def 7
.=(QuadraticForm(x,M@,y))*(i,j) by A8,A5,A28,Def12;
hence thesis by A27,MATRIX_0:def 7;
end;
i in Seg len LineSum(QuadraticForm(x,M@,y)) by A14,A15,FINSEQ_1:1;
then
A29: i in dom LineSum(QuadraticForm(x,M@,y)) by FINSEQ_1:def 3;
A30: len Line((M@"),i)=len y by A6,MATRIX_0:def 7;
A31: len ((x.i)*(mlt(Line((M@"),i),y))*') =len ((mlt(Line((M@"),i),y))*')
by COMPLSP2:3
.=len (mlt(Line((M@"),i),y)) by COMPLSP2:def 1
.=len (Line(QuadraticForm(x,M@,y),i)) by A16,A30,FINSEQ_2:72;
i in Seg len mlt(x,((M@")*y)*') by A12,A14,A15,FINSEQ_1:1;
then i in dom mlt(x,((M@")*y)*') by FINSEQ_1:def 3;
then (mlt(x,((M@")*y)*')).i =(x.i)*((((M@")*y)*').i) by Th17
.=(x.i)*((((M@")*y).i)*') by A11,A9,A14,A15,COMPLSP2:def 1;
then
(mlt(x,((M@")*y)*')).i = (x.i)*((Sum(mlt(Line((M@"),i),y)))*') by A20,Def6
.=(x.i)*(Sum((mlt(Line((M@"),i),y))*')) by A18,Th21
.=Sum((x.i)*(mlt(Line((M@"),i),y))*') by Th26;
then (mlt(x,((M@")*y)*')).i=Sum (Line(QuadraticForm(x,M@,y),i)) by A31,A21,
FINSEQ_1:14;
hence thesis by A7,A29,Def9;
end;
then Sum LineSum(QuadraticForm(x,M@,y))=Sum mlt(x,((M@")*y)*') by A12,
FINSEQ_1:14;
hence thesis by A11,Th37;
end;
theorem Th56:
for x,y being FinSequence of COMPLEX,M being Matrix of COMPLEX
st len y=len M & len x =width M & len x>0 & len y>0 holds |(M*x,y)| = SumAll
QuadraticForm(x,M@,y)
proof
let x,y be FinSequence of COMPLEX, M be Matrix of COMPLEX;
assume that
A1: len y=len M and
A2: len x =width M and
A3: len x>0 and
A4: len y>0;
A5: (M@)@"=M*' by A1,A2,A3,A4,MATRIX_0:57;
A6: width (M@)=len M by A2,A3,MATRIX_0:54;
A7: len (x*')= width M by A2,COMPLSP2:def 1;
len (y*')= len M by A1,COMPLSP2:def 1;
then
A8: len QuadraticForm(y*',M,x*') = len M by A7,Def12;
A9: len (x*')=len x by COMPLSP2:def 1;
A10: 0+1<=len x by A3,NAT_1:13;
A11: len (y*')=len y by COMPLSP2:def 1;
A12: len (M@)=width M by MATRIX_0:def 6;
A13: len (M*x)=len M by Def6;
hence |(M*x,y)| = (|(y,M*x)|)*' by A1,A4,Th52
.= (|(y*',(M*x)*')|) by A1,A4,A13,Th53
.= |(y*',((M*')*(x*')) )| by A2,A10,Th41
.= SumAll QuadraticForm(y*',(M@)@,x*') by A1,A2,A3,A4,A9,A11,A12,A6,A5,Th55
.= SumAll QuadraticForm(y*',M,x*') by A1,A2,A3,A4,MATRIX_0:57
.= SumAll((QuadraticForm(y*',M,x*'))@) by A1,A4,A8,Th49
.= SumAll((QuadraticForm(x*',(M@"),y*'))*') by A1,A2,A3,A9,A11,Th50
.= SumAll(((QuadraticForm(x,(M@),y))*')*') by A1,A2,A12,A6,Th51
.= SumAll QuadraticForm(x,M@,y);
end;
theorem Th57:
for x,y being FinSequence of COMPLEX, M being Matrix of COMPLEX
st len x=width M & len y =len M & width M>0 & len M>0 holds |(M*x,y)| = |(x,(M
@")*y)|
proof
let x,y be FinSequence of COMPLEX, M be Matrix of COMPLEX;
assume that
A1: len x=width M and
A2: len y =len M and
A3: width M>0 and
A4: len M >0;
|(x,(M@")*y)| = SumAll(QuadraticForm(x,M@,y)) by A1,A2,A3,A4,Th55;
hence thesis by A1,A2,A3,A4,Th56;
end;
theorem
for x,y being FinSequence of COMPLEX,M being Matrix of COMPLEX st len
x=len M & len y =width M & width M>0 & len M>0 holds |(x,M*y)| = |((M@")*x,y)|
proof
let x,y be FinSequence of COMPLEX, M be Matrix of COMPLEX;
assume that
A1: len x=len M and
A2: len y =width M and
A3: width M>0 and
A4: len M>0;
A5: len ((M@")*x)=len (M@") by Def6
.=len (M@) by Def1
.=width M by MATRIX_0:def 6;
len (M*y) =len x by A1,Def6;
hence |(x,M*y)| = (|(M*y,x)|)*' by A1,A4,Th52
.= (|(y,(M@")*x)|)*' by A1,A2,A3,A4,Th57
.= |((M@")*x,y)| by A2,A3,A5,Th52;
end;