:: A Theory of Matrices of Complex Elements
:: by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received December 10, 2004
:: Copyright (c) 2004-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 GROUP_1, COMPLFLD, SUPINF_2, CARD_1, MATRIX_1, NUMBERS, ARYTM_3,
ARYTM_1, RELAT_1, XCMPLX_0, SUBSET_1, FINSEQ_1, TREES_1, VECTSP_1, NAT_1,
ALGSTR_0, FUNCT_1, BINOP_2, COMPLEX1, XXREAL_0, VALUED_0, TARSKI,
ORDINAL4, MATRIX_5;
notations TARSKI, SUBSET_1, ORDINAL1, NAT_D, RELAT_1, FUNCT_1, VALUED_0,
MATRIX_0, STRUCT_0, ALGSTR_0, FINSEQ_1, BINOP_1, MATRIX_3, MATRIX_1,
NUMBERS, COMPLEX1, COMPLFLD, XCMPLX_0, GROUP_1, BINOP_2, XXREAL_0,
VECTSP_1, RLVECT_1;
constructors BINOP_1, COMPLFLD, FVSUM_1, MATRIX_3, BINOP_2, NAT_D, RVSUM_1,
RELSET_1, MATRIX_1;
registrations RELSET_1, XCMPLX_0, XREAL_0, STRUCT_0, VECTSP_1, COMPLFLD,
RVSUM_1, FINSEQ_1, NAT_1, MEMBERED;
requirements NUMERALS, SUBSET, ARITHM;
equalities ORDINAL1, MATRIX_1;
theorems FINSEQ_1, FUNCT_1, NAT_1, RLVECT_1, MATRIX_3, VECTSP_1, MATRIX_4,
COMPLFLD, COMPLEX1, GROUP_1, BINOP_2, FINSEQ_3, XCMPLX_0, XREAL_1,
VALUED_0, XXREAL_0, XREAL_0, MATRIX_0, RVSUM_1, MATRIX_1;
schemes NAT_1;
begin
theorem
1 = 1_F_Complex by COMPLEX1:def 4,COMPLFLD:8;
theorem
0.F_Complex = 0 by COMPLFLD:7;
definition
let A be Matrix of COMPLEX;
func COMPLEX2Field A -> Matrix of F_Complex equals
A;
coherence by COMPLFLD:def 1;
end;
definition
let A be Matrix of F_Complex;
func Field2COMPLEX A -> Matrix of COMPLEX equals
A;
coherence by COMPLFLD:def 1;
end;
theorem
for A,B being Matrix of COMPLEX st COMPLEX2Field A = COMPLEX2Field B
holds A=B;
theorem
for A,B being Matrix of F_Complex st Field2COMPLEX A = Field2COMPLEX B
holds A=B;
theorem
for A being Matrix of COMPLEX holds A = Field2COMPLEX COMPLEX2Field A;
theorem
for A being Matrix of F_Complex holds A = COMPLEX2Field Field2COMPLEX A;
definition
let A,B be Matrix of COMPLEX;
func A+B -> Matrix of COMPLEX equals
Field2COMPLEX ((COMPLEX2Field A)+(
COMPLEX2Field B));
coherence;
end;
definition
let A be Matrix of COMPLEX;
func -A -> Matrix of COMPLEX equals
Field2COMPLEX (-COMPLEX2Field A);
coherence;
end;
definition
let A,B be Matrix of COMPLEX;
func A - B -> Matrix of COMPLEX equals
Field2COMPLEX ((COMPLEX2Field A)-(
COMPLEX2Field B));
coherence;
func A*B -> Matrix of COMPLEX equals
Field2COMPLEX ((COMPLEX2Field A)*(
COMPLEX2Field B));
coherence;
end;
definition
let x be Complex, A be Matrix of COMPLEX;
func x * A -> Matrix of COMPLEX means
:Def7:
for ea being Element of
F_Complex st ea=x holds it=Field2COMPLEX (ea*(COMPLEX2Field A));
existence
proof
x in COMPLEX by XCMPLX_0:def 2;
then reconsider aa=x as Element of F_Complex by COMPLFLD:def 1;
set C=Field2COMPLEX (aa*(COMPLEX2Field A));
for ea being Element of F_Complex st ea=x holds C=Field2COMPLEX (ea*(
COMPLEX2Field A));
hence thesis;
end;
uniqueness
proof
x in COMPLEX by XCMPLX_0:def 2;
then reconsider aa=x as Element of F_Complex by COMPLFLD:def 1;
let C1,C2 be Matrix of COMPLEX;
assume that
A1: for ea being Element of F_Complex st ea=x holds C1=Field2COMPLEX (
ea*( COMPLEX2Field A)) and
A2: for ea being Element of F_Complex st ea=x holds C2=Field2COMPLEX (
ea*(COMPLEX2Field A));
C2=Field2COMPLEX (aa*(COMPLEX2Field A)) by A2;
hence thesis by A1;
end;
end;
theorem
for A being Matrix of COMPLEX holds len A = len COMPLEX2Field A &
width A=width COMPLEX2Field A;
theorem
for A being Matrix of F_Complex holds len A =len Field2COMPLEX A &
width A=width Field2COMPLEX A;
theorem Th9:
for K being Field, M being Matrix of K holds (1_K)*M=M
proof
let K be Field, M be Matrix of K;
A1: for i,j being Nat st [i,j] in Indices M holds ((1_K)*M)*(i,j)=M*(i,j)
proof
let i,j be Nat;
A2: (1_K)*(M*(i,j))=M*(i,j);
assume [i,j] in Indices M;
hence thesis by A2,MATRIX_3:def 5;
end;
len ((1_K)*M)=len M & width ((1_K)*M)=width M by MATRIX_3:def 5;
hence thesis by A1,MATRIX_0:21;
end;
theorem
for M being Matrix of COMPLEX holds 1*M=M
proof
set e=1_F_Complex;
let M be Matrix of COMPLEX;
1*M=Field2COMPLEX (e*(COMPLEX2Field M)) by Def7,COMPLEX1:def 4,COMPLFLD:8;
hence thesis by Th9;
end;
theorem
for K being Field, a,b being Element of K, M being Matrix of K holds a
*(b*M)=(a*b)*M
proof
let K be Field, a,b be Element of K, M being Matrix of K;
A1: len ((a*b)*M)=len M & width ((a*b)*M)=width M by MATRIX_3:def 5;
A2: len (a*(b*M))=len (b*M) by MATRIX_3:def 5;
A3: width (a*(b*M))=width (b*M) by MATRIX_3:def 5;
then
A4: width (a*(b*M)) =width M by MATRIX_3:def 5;
A5: len (b*M)=len M & width (b*M)=width M by MATRIX_3:def 5;
A6: for i,j being Nat st [i,j] in Indices (a*(b*M)) holds (a*(b*M))*(i,j)=((
a*b)*M)*(i,j)
proof
let i,j be Nat;
assume
A7: [i,j] in Indices (a*(b*M));
A8: Indices ((b*M))=Indices (M) by A5,MATRIX_4:55;
A9: Indices (a*(b*M))=Indices ((b*M)) by A2,A3,MATRIX_4:55;
then (a*(b*M))*(i,j) = (a*((b*M)*(i,j))) by A7,MATRIX_3:def 5
.= (a*(b*(M*(i,j)))) by A7,A9,A8,MATRIX_3:def 5
.= (a*b)*(M*(i,j)) by GROUP_1:def 3;
hence thesis by A7,A9,A8,MATRIX_3:def 5;
end;
len (a*(b*M)) =len M by A2,MATRIX_3:def 5;
hence thesis by A1,A4,A6,MATRIX_0:21;
end;
theorem Th12:
for K being Field, a,b being Element of K, M being Matrix of K
holds (a+b)*M=a*M + b*M
proof
let K be Field, a,b be Element of K, M be Matrix of K;
A1: len (a*M)=len (M) & width (a*M)=width (M) by MATRIX_3:def 5;
A2: len ((a+b)*M)=len (M) & width ((a+b)*M)=width (M) by MATRIX_3:def 5;
A3: for i,j be Nat st [i,j] in Indices ((a+b)*M) holds ((a+b)*M)*(i,j)=(a*M
+ b*M)*(i,j)
proof
let i,j be Nat;
assume
A4: [i,j] in Indices ((a+b)*M);
A5: Indices ((a+b)*M)=Indices M by A2,MATRIX_4:55;
Indices (a*M)=Indices M by A1,MATRIX_4:55;
then (a*M + b*M)*(i,j) =(a*M)*(i,j)+(b*M)*(i,j) by A4,A5,MATRIX_1:def 6
.=a*(M*(i,j))+(b*M)*(i,j) by A4,A5,MATRIX_3:def 5
.=a*(M*(i,j))+b*(M*(i,j)) by A4,A5,MATRIX_3:def 5
.=(a+b)*(M*(i,j)) by VECTSP_1:def 7;
hence thesis by A4,A5,MATRIX_3:def 5;
end;
len (a*M + b*M)=len (a*M) & width (a*M + b*M)=width (a*M) by MATRIX_1:def 6;
hence thesis by A2,A1,A3,MATRIX_0:21;
end;
theorem
for M being Matrix of COMPLEX holds M+M = 2*M
proof
reconsider e2=(1_F_Complex) + (1_F_Complex) as Element of F_Complex;
let M be Matrix of COMPLEX;
A1: (1_F_Complex)*(COMPLEX2Field M)= COMPLEX2Field M by Th9;
2 * M = Field2COMPLEX (e2*(COMPLEX2Field M)) by Def7,COMPLEX1:def 4
,COMPLFLD:8
.=Field2COMPLEX ((COMPLEX2Field M)+(COMPLEX2Field M)) by A1,Th12;
hence thesis;
end;
theorem
for M being Matrix of COMPLEX holds M+M+M = 3*M
proof
reconsider rr=1+1 as Element of COMPLEX by XCMPLX_0:def 2;
reconsider e3=(1_F_Complex) + (1_F_Complex)+ (1_F_Complex) as Element of
F_Complex;
let M be Matrix of COMPLEX;
A1: len M =len COMPLEX2Field M & width M=width COMPLEX2Field M;
A2: (1_F_Complex) + (1_F_Complex) =(the addF of F_Complex).(1_F_Complex,
1_F_Complex) by RLVECT_1:2
.=addcomplex.(1r,1r) by COMPLFLD:8,def 1
.=1+1 by BINOP_2:def 3,COMPLEX1:def 4;
(1_F_Complex) + (1_F_Complex) + (1_F_Complex) = (the addF of F_Complex).
(((1_F_Complex) + (1_F_Complex)),1_F_Complex) by RLVECT_1:2
.= addcomplex.(1+1,1) by A2,COMPLFLD:def 1
.= rr + 1 by BINOP_2:def 3
.= 3;
then 3*M= Field2COMPLEX (e3*(COMPLEX2Field M)) by Def7
.=Field2COMPLEX ((1_F_Complex)*(COMPLEX2Field M) + ((1_F_Complex)+ (
1_F_Complex))*(COMPLEX2Field M)) by Th12
.=Field2COMPLEX (COMPLEX2Field M + ((1_F_Complex)+ (1_F_Complex))*(
COMPLEX2Field M)) by Th9
.=Field2COMPLEX (COMPLEX2Field M + ((1_F_Complex)*(COMPLEX2Field M)+ (
1_F_Complex)*(COMPLEX2Field M))) by Th12
.=Field2COMPLEX (COMPLEX2Field M + (COMPLEX2Field M + (1_F_Complex)*(
COMPLEX2Field M))) by Th9
.=Field2COMPLEX (COMPLEX2Field M+(COMPLEX2Field M+COMPLEX2Field M)) by Th9
.=Field2COMPLEX (COMPLEX2Field M+COMPLEX2Field M+COMPLEX2Field M) by A1,
MATRIX_3:3;
hence thesis;
end;
definition
let n,m be Nat;
func 0_Cx(n,m) -> Matrix of COMPLEX equals
Field2COMPLEX (0.(F_Complex,n,m));
coherence;
end;
theorem
for n,m being Nat holds COMPLEX2Field 0_Cx(n,m)=0.(
F_Complex,n,m);
theorem :: MATRIX_4:6
for M1,M2 being Matrix of COMPLEX st len M1=len M2 & width M1=width M2
& M1 = M1 + M2 holds M2 = 0_Cx(len M1,width M1)
proof
let M1,M2 be Matrix of COMPLEX;
assume that
A1: len M1=len M2 & width M1=width M2 and
A2: M1 = M1 + M2;
0_Cx(len M1,width M1)=M1+M2+(-M1) by A2,MATRIX_4:2
.=Field2COMPLEX ((COMPLEX2Field M2)+(COMPLEX2Field M1) -(COMPLEX2Field
M1)) by A1,MATRIX_3:2
.=M2 by A1,MATRIX_4:21;
hence thesis;
end;
theorem :: MATRIX_4:8
for M1,M2 being Matrix of COMPLEX st len M1=len M2 & width M1=width M2
& M1+M2= 0_Cx(len M1,width M1) holds M2=-M1
proof
let M1,M2 be Matrix of COMPLEX;
assume that
A1: len M1=len M2 & width M1=width M2 and
A2: M1 + M2 = 0_Cx(len M1,width M1);
A3: len -M2=len M2 & width -M2=width M2 by MATRIX_1:def 4;
COMPLEX2Field(0_Cx(len M1,width M1)) = (COMPLEX2Field M1)-(-(
COMPLEX2Field M2)) by A2,MATRIX_4:1;
then COMPLEX2Field M1 = -COMPLEX2Field M2 by A1,A3,MATRIX_4:7;
hence thesis by MATRIX_4:1;
end;
theorem :: MATRIX_4:10
for M1,M2 being Matrix of COMPLEX st len M1=len M2 & width M1=width M2
& M2 - M1 = M2 holds M1=0_Cx(len M1,width M1)
proof
let M1,M2 be Matrix of COMPLEX;
assume that
A1: len M1=len M2 & width M1=width M2 and
A2: M2 - M1 = M2;
COMPLEX2Field M2 +(COMPLEX2Field M1) = (COMPLEX2Field M2) by A1,A2,
MATRIX_4:22;
hence thesis by A1,MATRIX_4:6;
end;
theorem
for M being Matrix of COMPLEX holds M + 0_Cx(len M,width M) = M
proof
let M be Matrix of COMPLEX;
A1: len M=len COMPLEX2Field M & width M=width COMPLEX2Field M;
M + 0_Cx(len M,width M) = M +(- 0_Cx(len M,width M)) by MATRIX_4:9
.= Field2COMPLEX ((COMPLEX2Field M)-(COMPLEX2Field M-COMPLEX2Field M))
by MATRIX_4:3
.= M by A1,MATRIX_4:11;
hence thesis;
end;
theorem Th20:
for K being Field, b being Element of K,M1,M2 being Matrix of K
st len M1 = len M2 & width M1 = width M2 holds b*(M1+M2)=b*M1 + b*M2
proof
let K be Field, b be Element of K, M1,M2 be Matrix of K;
A1: len (b*(M1+M2))=len (M1+M2) & width (b*(M1+M2)) = width (M1+M2) by
MATRIX_3:def 5;
A2: len (M1+M2)=len M1 & width (M1+M2)=width M1 by MATRIX_1:def 6;
A3: len (b*M1)=len M1 & width (b*M1)=width M1 by MATRIX_3:def 5;
assume
A4: len M1= len M2 & width M1=width M2;
A5: for i,j being Nat st [i,j] in Indices (b*(M1+M2)) holds (b*(M1+M2))*(i,j
)=(b*M1 + b*M2)*(i,j)
proof
let i,j be Nat;
assume
A6: [i,j] in Indices (b*(M1+M2));
A7: Indices M2=Indices M1 by A4,MATRIX_4:55;
A8: Indices (b*(M1+M2))=Indices (M1+M2) by A1,MATRIX_4:55;
A9: Indices (M1+M2)=Indices M1 by A2,MATRIX_4:55;
Indices (b*M1)=Indices M1 by A3,MATRIX_4:55;
then (b*M1 + b*M2)*(i,j) =(b*M1)*(i,j)+(b*M2)*(i,j) by A6,A8,A9,
MATRIX_1:def 6
.=b*(M1*(i,j))+(b*M2)*(i,j) by A6,A8,A9,MATRIX_3:def 5
.=b*(M1*(i,j))+b*(M2*(i,j)) by A6,A8,A9,A7,MATRIX_3:def 5
.=(b*(M1*(i,j)+M2*(i,j))) by VECTSP_1:def 7;
then (b*M1 + b*M2)*(i,j) = (b*((M1 + M2)*(i,j))) by A6,A8,A9,MATRIX_1:def 6
.= (b*(M1 + M2)*(i,j)) by A6,A8,MATRIX_3:def 5;
hence thesis;
end;
len (b*M1 + b*M2)=len (b*M1) & width (b*M1 + b*M2)=width (b*M1) by
MATRIX_1:def 6;
hence thesis by A1,A2,A3,A5,MATRIX_0:21;
end;
theorem
for M1,M2 being Matrix of COMPLEX for a being Complex st len M1
=len M2 & width M1=width M2 holds a*(M1 + M2) = a*M1 + a*M2
proof
let M1,M2 be Matrix of COMPLEX;
let a be Complex;
assume
A1: len M1=len M2 & width M1=width M2;
a in COMPLEX by XCMPLX_0:def 2;
then reconsider ea=a as Element of F_Complex by COMPLFLD:def 1;
A2: a*M1 + a*M2 = Field2COMPLEX ((COMPLEX2Field (Field2COMPLEX (ea*(
COMPLEX2Field M1)))+(COMPLEX2Field (a*M2)))) by Def7
.= Field2COMPLEX (((ea*(COMPLEX2Field M1))+(COMPLEX2Field (Field2COMPLEX
(ea*(COMPLEX2Field M2)))))) by Def7
.= Field2COMPLEX ((ea*(COMPLEX2Field M1)+(ea*(COMPLEX2Field M2))));
a*(M1 + M2) = Field2COMPLEX (ea*(COMPLEX2Field (M1+M2))) by Def7
.= Field2COMPLEX (ea*(COMPLEX2Field M1)+ea*(COMPLEX2Field M2)) by A1,Th20;
hence thesis by A2;
end;
theorem Th22:
for K being Field,M1,M2 being Matrix of K st width M1=len M2 &
len M1>0 holds 0.(K,len M1,width M1)*M2=0.(K,len M1,width M2)
proof
let K be Field,M1,M2 be Matrix of K;
assume that
A1: width M1=len M2 and
A2: len M1>0;
A4: len (0.(K,len M1,width M1))=len M1 by MATRIX_0:def 2;
then
A5: width (0.(K,len M1,width M1))=width M1 by A2,MATRIX_0:20;
then
A6: len ((0.(K,len M1,width M1))*M2)=len (0.(K,len M1,width M1)) by A1,
MATRIX_3:def 4;
A7: width ((0.(K,len M1,width M1))*M2)=width M2 by A1,A5,MATRIX_3:def 4;
set B=(0.(K,len M1,width M1))*M2;
A8: width -((0.(K,len M1,width M1))*M2)=width ((0.(K,len M1,width M1))*M2)
by MATRIX_1:def 4;
(0.(K,len M1,width M1))*M2 =((0.(K,len M1,width M1)+(0.(K,len M1,width
M1))))*M2 by MATRIX_3:4
.=((0.(K,len M1,width M1)))*M2+((0.(K,len M1,width M1)))*M2 by A1,A4,A5,
MATRIX_4:63;
then
len -((0.(K,len M1,width M1))*M2)=len ((0.(K,len M1,width M1))*M2) & 0.
(K, len M1,width M2)=B+B+(-B) by A4,A6,A7,MATRIX_1:def 4,MATRIX_4:2;
then 0.(K,len M1,width M2) =B+(B-B) by A8,MATRIX_3:3
.=(0.(K,len M1,width M1))*M2 by A6,A8,MATRIX_4:20;
hence thesis;
end;
theorem
for M1,M2 being Matrix of COMPLEX st width M1=len M2 &len M1>0&len M2>
0 holds 0_Cx(len M1,width M1)*M2=0_Cx(len M1,width M2)
proof
let M1,M2 be Matrix of COMPLEX;
A1: len M1=len COMPLEX2Field M1;
assume width M1=len M2 & len M1>0 & len M2>0;
hence thesis by A1,Th22;
end;
theorem Th24:
for K being Field,M1 being Matrix of K st len M1>0 holds 0.K*M1=
0.(K,len M1,width M1)
proof
let K be Field,M1 be Matrix of K;
A1: len (0.(K,len M1,width M1))=len M1 by MATRIX_0:def 2;
assume len M1>0;
then
A2: width (0.(K,len M1,width M1))=width M1 by A1,MATRIX_0:20;
A3: for i,j be Nat st [i,j] in Indices (0.(K,len M1,width M1)) holds ((0.K)*
M1)*(i,j)=(0.(K,len M1,width M1))*(i,j)
proof
let i,j be Nat;
assume
A4: [i,j] in Indices (0.(K,len M1,width M1));
Indices (0.(K,len M1,width M1))= Indices M1 by A1,A2,MATRIX_4:55;
then
A5: ((0.K)*M1)*(i,j)=(0.K)*(M1*(i,j)) by A4,MATRIX_3:def 5;
(0.(K,len M1,width M1))*(i,j)=0.K by A4,MATRIX_3:1;
hence thesis by A5;
end;
len (0.K*M1)=len M1 & width (0.K*M1)=width M1 by MATRIX_3:def 5;
hence thesis by A1,A2,A3,MATRIX_0:21;
end;
theorem
for M1 being Matrix of COMPLEX st len M1>0 holds 0*M1 = 0_Cx(len M1,
width M1)
proof
reconsider ea=0 as Element of F_Complex by COMPLFLD:def 1;
let M1 be Matrix of COMPLEX;
assume
A1: len M1>0;
0*M1 = Field2COMPLEX (ea*(COMPLEX2Field M1)) by Def7
.=0_Cx(len M1,width M1) by A1,Th24,COMPLFLD:7;
hence thesis;
end;
definition
let s be complex-valued Function, k be set;
redefine func s.k -> Element of COMPLEX; :: redefines . (FUNCT_1, definition)
coherence
proof
per cases;
suppose
A1: k in dom s;
A2: rng s c= COMPLEX by VALUED_0:def 1;
s.k in rng s by A1,FUNCT_1:def 3;
hence thesis by A2;
end;
suppose
not k in dom s;
then s.k = 0c by FUNCT_1:def 2;
hence thesis;
end;
end;
end;
theorem
for i,j being Nat,M1,M2 being Matrix of COMPLEX st len M2>0
holds ex s being FinSequence of COMPLEX st len s = len M2 & s.1=(M1*(i,1))*(M2*
(1,j)) & for k be Nat st 1<=k & k < len M2 holds s.(k+1)=s.k + (M1*(
i,k+1))*(M2*(k+1,j))
proof
let i,j be Nat,M1,M2 be Matrix of COMPLEX;
defpred P[Nat] means ex q being FinSequence of COMPLEX st 1<=$1+1
& $1+1<=len M2 implies ( len q=$1 +1 & q.1=(M1*(i,1))*(M2*(1,j)) &
(for k be Nat st 1<=k & k<$1+1
holds q.(k+1)=q.k+(M1*(i,k+1))*(M2*(k+1,j))));
reconsider q0=<*(M1*(i,1))*(M2*(1,j))*> as FinSequence of COMPLEX
by RVSUM_1:146;
A1: for k be Nat st 1<=k & k<1 holds q0.(k+1)=q0.k+(M1*(i,k+1))*(
M2*(k+1,j));
A2: for i2 being Nat st P[i2] holds P[i2+1]
proof
let i2 be Nat;
set k0=i2;
assume P[i2];
then consider q2 being FinSequence of COMPLEX such that
A3: 1<=i2+1 & i2+1<=len M2 implies len q2=i2+1 & q2.1=(M1*(i,1))*(M2*
(1,j)) & for k2 being Nat st 1<=k2 & k2<i2+1 holds q2.(k2+1)=q2.k2+(
M1*(i,k2+1))*(M2*(k2+1,j));
reconsider q3=q2^<* q2.(k0+1)+(M1*(i,k0+1+1))*(M2*(k0+1+1,j)) *>
as FinSequence of COMPLEX by RVSUM_1:146;
1<=i2+1+1 & i2+1+1<=len M2 implies len q3 = i2+1+1 & q3.1=(M1*(i,1))*
(M2*(1,j)) & for k be Nat st 1<=k & k< i2+1+1 holds q3.(k+1)=q3.k+(
M1*(i,k+1))*(M2*(k+1,j))
proof
assume that
1<=i2+1+1 and
A4: i2+1+1<=len M2;
A5: 1 <= i2+1 by NAT_1:12;
thus
A6: len q3 = len q2+len (<* q2.(k0+1)+(M1*(i,k0+1+1))*(M2*(k0+1+1,j))
*>) by FINSEQ_1:22
.=i2+1+1 by A3,A4,A5,FINSEQ_1:39,NAT_1:13;
A7: for k2 being Nat st 1<=k2 & k2<i2+1+1 holds q3.(k2+1)=
q3.k2+(M1*(i,k2+1))*(M2*(k2+1,j))
proof
let k2 be Nat;
assume that
A8: 1<=k2 and
A9: k2<i2+1+1;
A10: k2<=i2+1 by A9,NAT_1:13;
per cases by A10,XXREAL_0:1;
suppose
A11: k2<i2+1;
then k2 < len q3 by A6,NAT_1:13;
then
k2 < len q2 + len <* q2.(k0+1)+(M1*(i,k0+1+1))*(M2*(k0+1+1,j)
)*> by FINSEQ_1:22;
then k2 < len q2 + 1 by FINSEQ_1:39;
then k2 <= len q2 by NAT_1:13;
then k2 in dom q2 by A8,FINSEQ_3:25;
then
A12: q3.k2=q2.k2 by FINSEQ_1:def 7;
k2+1 < i2 + 1+1 by A11,XREAL_1:6;
then
k2+1 < len q2 + len <* q2.(k0+1)+(M1*(i,k0+1+1))*(M2*(k0+1+1,
j))*> by A6,FINSEQ_1:22;
then k2+1 < len q2 + 1 by FINSEQ_1:39;
then
A13: k2+1 <= len q2 by NAT_1:13;
1 <= k2+1 by A8,NAT_1:13;
then k2+1 in dom q2 by A13,FINSEQ_3:25;
then q3.(k2+1)=q2.(k2+1) by FINSEQ_1:def 7;
hence thesis by A3,A4,A5,A8,A11,A12,NAT_1:13;
end;
suppose
A14: k2=i2+1;
then k2 < i2 + 1+1 by NAT_1:13;
then
k2 < len q2 + len <* q2.(k0+1)+(M1*(i,k0+1+1))*(M2*(k0+1+1,j)
)*> by A6,FINSEQ_1:22;
then k2 < len q2 + 1 by FINSEQ_1:39;
then k2 <= len q2 by NAT_1:13;
then k2 in dom q2 by A8,FINSEQ_3:25;
then
A15: q3.k2=q2.k2 by FINSEQ_1:def 7;
1 in Seg 1 by FINSEQ_1:3;
then
(<* q2.(k0+1)+(M1*(i,k0+1+1))*(M2*(k0+1+1,j)) *>).1 = q2.(k0+
1)+(M1*(i,k0+1+1 ))*(M2*(k0+1+1,j)) & 1 in dom (<* q2.(k0+1)+(M1*(i,k0+1+1))*(
M2*(k0+1+1,j)) *> ) by FINSEQ_1:def 8;
hence thesis by A3,A4,A5,A14,A15,FINSEQ_1:def 7,NAT_1:13;
end;
end;
1 < len (q2^<* q2.(k0+1)+(M1*(i,k0+1+1))*(M2*(k0+1+1,j)) *>) by A5,A6,
NAT_1:13;
then 1 < len q2 + len <* q2.(k0+1)+(M1*(i,k0+1+1))*(M2*(k0+1+1,j))*>
by FINSEQ_1:22;
then 1 < len q2 + 1 by FINSEQ_1:39;
then 1 <= len q2 by NAT_1:13;
then 1 in dom q2 by FINSEQ_3:25;
hence thesis by A3,A4,A5,A7,FINSEQ_1:def 7,NAT_1:13;
end;
hence thesis;
end;
len q0 = 1 & q0.1=(M1*(i,1))*(M2*(1,j)) by FINSEQ_1:39;
then
A16: P[0] by A1;
A17: for j being Nat holds P[j] from NAT_1:sch 2(A16,A2);
assume
A18: len M2>0;
then 0+1<=len M2 by NAT_1:8;
then 0+1-1<=len M2-1 by XREAL_1:9;
then
A19: len M2-'1=len M2-1 by XREAL_0:def 2;
then 0+1<=(len M2)-'1+1 by A18,NAT_1:8;
hence thesis by A19,A17;
end;