Copyright (c) 1993 Association of Mizar Users
environ
vocabulary VECTSP_1, RLVECT_1, MATRIX_1, FINSEQ_2, ARYTM_1, FINSEQ_1, TREES_1,
FUNCT_1, RELAT_1, BOOLE, INCSP_1, CAT_3, RVSUM_1, GROUP_1, BINOP_1,
SETWISEO, SQUARE_1, MATRIX_2, QC_LANG1, FINSUB_1, FINSET_1, FUNCOP_1,
PARTFUN1, FINSEQOP, FUNCT_5, SUBSET_1, FVSUM_1, MATRIX_3;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, STRUCT_0,
FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, BINOP_1,
FUNCT_3, FUNCOP_1, RLVECT_1, VECTSP_1, SETWISEO, SETWOP_2, FINSEQ_2,
FINSEQOP, MATRIX_1, FINSUB_1, MATRIX_2, NAT_1, SQUARE_1, FVSUM_1,
TREES_1, FUNCT_5, CAT_2;
constructors ALGSTR_1, BINOP_1, SETWISEO, SETWOP_2, FINSEQOP, MATRIX_2, NAT_1,
SQUARE_1, FVSUM_1, CAT_2, FINSOP_1, MEMBERED, PARTFUN1, RELAT_2,
XBOOLE_0;
clusters SUBSET_1, FUNCT_1, FINSUB_1, FINSET_1, RELSET_1, STRUCT_0, FVSUM_1,
MATRIX_2, FUNCOP_1, XREAL_0, ARYTM_3, VECTSP_1, MEMBERED, ZFMISC_1,
FUNCT_2, PARTFUN1, XBOOLE_0, NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
theorems FINSEQ_1, FINSEQ_2, TARSKI, FUNCT_2, NAT_1, BINOP_1, TREES_1,
FUNCT_1, SETWISEO, VECTSP_1, ZFMISC_1, FVSUM_1, SETWOP_2, MATRIX_1,
MATRIX_2, FUNCT_3, REAL_1, FINSEQOP, FUNCOP_1, FINSUB_1, FUNCT_5,
FINSEQ_3, RLVECT_1, RELAT_1, FINSOP_1, RELSET_1, XBOOLE_0, XBOOLE_1,
XCMPLX_1;
schemes FUNCT_2, FINSEQ_2, MATRIX_1, MATRIX_2, FUNCT_3, SETWISEO, FUNCT_1;
begin
reserve x,y,z,x1,x2,y1,y2,z1,z2 for set,
i,j,k,l,n,m for Nat,
D for non empty set,
K for Field;
:: Auxiliary theorems
theorem Th1:
n = n + k implies k=0
proof
assume n=n+k;
then n+0=n+k;
hence 0=k by XCMPLX_1:2;
end;
definition let K,n,m;
func 0.(K,n,m) -> Matrix of n,m,K equals:
Def1: n |-> (m |-> 0.K);
coherence by MATRIX_1:10;
end;
definition let K;let A be Matrix of K;
func -A -> Matrix of K means:
Def2:len it= len A & width it =width A &
for i,j holds [i,j] in Indices A implies it*(i,j)= -(A*(i,j));
existence
proof
deffunc F(Nat,Nat) = -(A*($1,$2));
consider M being Matrix of len A,width A,K such that
A1:for i,j st [i,j] in Indices M holds M*(i,j) = F(i,j)
from MatrixLambda;
set n=len A;
reconsider A1=A as Matrix of n,width A,K by MATRIX_2:7;
A2:Indices A1=[:Seg n,Seg width A:] by MATRIX_1:26;
A3:now per cases by NAT_1:19;
case n > 0;
hence len M=len A & width M=width A & Indices A = Indices M by A2,
MATRIX_1:24;
case n =0;
then len A=0 & len M=0 by MATRIX_1:def 3;
then width A=0 & width M=0 by MATRIX_1:def 4;
hence len M=len A & width M=width A & Indices A = Indices M by A2,
MATRIX_1:26;
end;
reconsider M as Matrix of K;
take M;
thus thesis by A1,A3;
end;
uniqueness
proof
set n=len A;
let M1,M2 be Matrix of K;
assume that A4:len M1= len A & width M1 =width A &
for i,j st [i,j] in Indices A holds
M1*(i,j) =-(A*(i,j))
and A5:len M2= len A & width M2 =width A &
for i,j st [i,j] in Indices A holds
M2*(i,j) =-(A*(i,j));
reconsider A1=A as Matrix of n,width A,K by MATRIX_2:7;
reconsider M1 as Matrix of n,width A,K by A4,MATRIX_2:7;
reconsider M2 as Matrix of n,width A,K by A5,MATRIX_2:7;
A6:Indices A1=[:Seg n,Seg width A:] by MATRIX_1:26;
A7:Indices M1=[:Seg n,Seg width M1:] & Indices M2=[:Seg n,Seg width M2:]
by MATRIX_1:26;
A8: now per cases by NAT_1:19;
case n > 0;
then Indices M1=[:Seg n,Seg width A:] &
Indices M2=[:Seg n,Seg width A:] by MATRIX_1:24;
hence Indices A = Indices M1 & Indices M1= Indices M2 by A6;
case n =0;
then len A=0 & len M1=0 & len M2=0 by MATRIX_1:def 3;
then width A=0 & width M1=0 & width M2=0 by MATRIX_1:def 4;
hence Indices A = Indices M1 & Indices M1= Indices M2 by A6,A7;
end;
now let i,j;
assume [i,j] in Indices A;
then M1*(i,j) = -(A*(i,j)) & M2*(i,j) = -(A*(i,j)) by A4,A5;
hence M1*(i,j)=M2*(i,j);
end;
hence thesis by A8,MATRIX_1:28;
end;
end;
definition let K;let A,B be Matrix of K;
func A+B -> Matrix of K means:
Def3: len it =len A & width it=width A &
for i,j holds [i,j] in Indices A implies
it*(i,j) = A*(i,j) + B*(i,j);
existence
proof
deffunc F(Nat,Nat) = A*($1,$2) + B*($1,$2);
consider M being Matrix of len A,width A,K such that
A1: for i,j st [i,j] in Indices M holds M*(i,j) = F(i,j)
from MatrixLambda;
reconsider A1=A as Matrix of len A,width A,K by MATRIX_2:7;
A2:Indices A1=[:Seg len A,Seg width A:] by MATRIX_1:26;
set n=len A;
A3:now per cases by NAT_1:19;
case n > 0;
hence len M=len A & width M=width A & Indices A = Indices M by A2,
MATRIX_1:24;
case n =0;
then len A=0 & len M=0 by MATRIX_1:def 3;
then width A=0 & width M=0 by MATRIX_1:def 4;
hence len M=len A & width M=width A & Indices A = Indices M by A2,
MATRIX_1:26;
end;
reconsider M as Matrix of K;
take M;
thus thesis by A1,A3;
end;
uniqueness
proof let M1,M2 be Matrix of K;
assume that
A4:len M1 =len A & width M1=width A &
for i,j st [i,j] in Indices A holds
M1*(i,j)=A*(i,j) + B*(i,j)
and A5:len M2 =len A &width M2=width A &
for i,j st [i,j] in Indices A holds
M2*(i,j) = A*(i,j) + B*(i,j);
set n=len A;
reconsider A1=A as Matrix of n,width A,K by MATRIX_2:7;
reconsider M1 as Matrix of n,width A,K by A4,MATRIX_2:7;
reconsider M2 as Matrix of n,width A,K by A5,MATRIX_2:7;
A6:Indices A1=[:Seg n,Seg width A:] by MATRIX_1:26;
A7:Indices M1=[:Seg n,Seg width M1:] &
Indices M2=[:Seg n ,Seg width M2:] by MATRIX_1:26;
A8: now per cases by NAT_1:19;
case n > 0;
then Indices M1=[:Seg n,Seg width A:] &
Indices M2=[:Seg n,Seg width A:] by MATRIX_1:24;
hence Indices A = Indices M1 & Indices M1= Indices M2 by A6;
case n =0;
then len A=0 & len M1=0 & len M2=0 by MATRIX_1:def 3;
then width A=0 & width M1=0 & width M2=0 by MATRIX_1:def 4;
hence Indices A = Indices M1 & Indices M1= Indices M2 by A6,A7;
end;
now let i,j;
assume [i,j] in Indices A;
then M1*(i,j)=(A*(i,j) + B*(i,j)) &
M2*(i,j)=(A*(i,j) + B*(i,j)) by A4,A5;
hence M1*(i,j)=M2*(i,j);
end;
hence thesis by A8,MATRIX_1:28;
end;
end;
canceled;
theorem
Th3: for i,j st [i,j] in Indices (0.(K,n,m)) holds
(0.(K,n,m))*(i,j)= 0.K
proof
let i,j;
assume A1:[i,j] in Indices (0.(K,n,m));
A2:Indices (0.(K,n,m))= [:Seg n,Seg width (0.(K,n,m)):] by MATRIX_1:26;
now per cases by NAT_1:19;
case n > 0;
then [i,j] in [:Seg n,Seg m:] by A1,MATRIX_1:24;
then A3:i in Seg n & j in Seg m by ZFMISC_1:106;
(0.(K,n,m))=n |->(m |-> 0.K) by Def1;
then A4:(0.(K,n,m)).i= m |-> 0.K by A3,FINSEQ_2:70;
(m |-> 0.K).j= 0.K by A3,FINSEQ_2:70;
hence (0.(K,n,m))*(i,j)=0.K by A1,A4,MATRIX_1:def 6;
case n=0;
hence (0.(K,n,m))*(i,j)=0.K by A1,A2,FINSEQ_1:4,ZFMISC_1:113;
end;
hence thesis;
end;
theorem
for A,B being Matrix of K st len A= len B & width A=width B
holds A + B = B + A
proof let A,B be Matrix of K;
assume A1:len A= len B & width A=width B;
then dom A = dom B by FINSEQ_3:31;
then A2:Indices A= [:dom A,Seg width A:] &
Indices B=[:dom A,Seg width A:] by A1,MATRIX_1:def 5;
A3:len A=len (A+B) & width A=width (A+B) by Def3;
then dom A = dom(A+B) by FINSEQ_3:31;
then A4:Indices A = Indices (A + B) by A2,A3,MATRIX_1:def 5;
A5:len (A+B)=len (B+A) & width (A+B)=width (B+A) by A1,A3,Def3;
now let i,j;
assume A6:[i,j] in Indices (A + B);
hence (A + B)*(i,j)=B*(i,j) + A*(i,j) by A4,Def3
.=( B + A)*(i,j) by A2,A4,A6,Def3;
end;
hence thesis by A5,MATRIX_1:21;
end;
theorem
for A,B,C being Matrix of K st len A=len B & len A=len C &
width A=width B & width A=width C holds
(A + B) + C= A + (B + C)
proof let A,B,C be Matrix of K;
assume A1:len A=len B & len A=len C &
width A=width B & width A=width C;
then dom A = dom B & dom A = dom C by FINSEQ_3:31;
then A2:Indices A= [:dom A,Seg width A:] &
Indices B=[:dom A,Seg width A:] &
Indices C= [:dom A,Seg width A:] by A1,MATRIX_1:def 5;
A3:len (A+B)=len A & width (A+B)=width A by Def3;
then dom A = dom(A+B) by FINSEQ_3:31;
then A4:Indices (A+B)=[:dom A,Seg width A:] by A3,MATRIX_1:def 5;
A5:len ((A+B)+C)=len (A+B) & width ((A+B)+C)=width (A+B) by Def3;
then dom A = dom((A+B)+C) by A3,FINSEQ_3:31;
then A6:Indices ((A+B)+C)=[:dom A,Seg width A:] by A3,A5,MATRIX_1:def 5;
A7:len (A+(B+C))=len A & width (A+(B+C))=width A by Def3;
now let i,j;
assume A8:[i,j] in Indices ((A + B) + C);
hence ((A + B)+C)*(i,j)=(A+B)*(i,j) + C*(i,j) by A4,A6,Def3
.=(A*(i,j) + B*(i,j)) + C*(i,j) by A2,A6,A8,Def3
.=A*(i,j) + (B*(i,j) + C*(i,j))
by RLVECT_1:def 6
.=A*(i,j) + ( B + C)*(i,j) by A2,A6,A8,Def3
.=(A + ( B + C))*(i,j) by A2,A6,A8,Def3;
end;
hence thesis by A3,A5,A7,MATRIX_1:21;
end;
theorem
for A being Matrix of n,m,K holds A + 0.(K,n,m)= A
proof
let A be Matrix of n,m,K;
now per cases by NAT_1:19;
case n > 0;
then A1:len A=n & len (0.(K,n,m))=n & width A=m & width (0.(K,n,m))=m &
Indices A=[:Seg n,Seg m:] & Indices (0.(K,n,m))=[:Seg n,Seg m:] by
MATRIX_1:24;
A2:len A= len (A+0.(K,n,m)) & width A= width (A+0.(K,n,m)) by Def3;
then Seg n = dom A & dom A = dom(A+0.(K,n,m))
by A1,FINSEQ_1:def 3,FINSEQ_3:31;
then A3:Indices A= Indices (A+0.(K,n,m)) by A1,A2,MATRIX_1:def 5;
now let i,j;
assume A4:[i,j] in Indices (A+ 0.(K,n,m));
hence (A+ 0.(K,n,m)) *(i,j)=A*(i,j) + 0.(K,n,m)*(i,j) by A3,Def3
.=A*(i,j) +0.K by A1,A3,A4,Th3
.=A*(i,j) by RLVECT_1:10;
end;
hence thesis by A2,MATRIX_1:21;
case A5: n=0;
A6:len A= len (A+0.(K,n,m)) & width A= width (A+0.(K,n,m)) by Def3;
then dom A= dom(A+0.(K,n,m)) by FINSEQ_3:31;
then Indices A= [:dom A,Seg width A:] &
Indices (A+0.(K,n,m))=[:dom A,Seg width A:] by A6,MATRIX_1:def 5;
then for i,j st [i,j] in Indices (A+ 0.(K,n,m)) holds
(A+ 0.(K,n,m))*(i,j)= A*(i,j) by A5,MATRIX_1:23;
hence thesis by A6,MATRIX_1:21;
end;
hence thesis;
end;
theorem
for A being Matrix of n,m,K holds A + (-A) = 0.(K,n,m)
proof let A be Matrix of n,m,K;
A1:len -A=len A & width -A=width A by Def2;
A2:len (A+ -A)=len A & width (A+ -A)=width A by Def3;
A3:Indices A= Indices 0.(K,n,m) by MATRIX_1:27;
A4: now per cases by NAT_1:19;
case A5:n > 0;
then A6:len A=n & width A=m & Indices A=[:Seg n,Seg m:] by MATRIX_1:24;
len -A=n & width -A=m & len (A+ -A)=n & width (A + -A) =m &
len (0.(K,n,m))=n & width (0.(K,n,m))=m by A1,A2,A5,MATRIX_1:24;
hence len (0.(K,n,m))=len (A+ -A) & width (0.(K,n,m))=width (A+ -A);
Seg n = dom A & dom A = dom -A & dom A = dom(A + (-A))
by A1,A2,A6,FINSEQ_1:def 3,FINSEQ_3:31;
hence Indices A= Indices (-A) & Indices A= Indices (A + (-A)) by A1,A2,
A6,MATRIX_1:def 5;
case n=0;
then A7:len A=0 & width A=0 & Indices A= {} & len (0.(K,n,m))=0 &
width (0.(K,n,m))=0 by MATRIX_1:23;
hence len (0.(K,n,m))=len (A+ -A) & width (0.(K,n,m))=width (A+ -A)
by Def3;
dom(-A) = Seg 0 & dom(A+ -A) = Seg 0 by A1,A2,A7,FINSEQ_1:def 3;
then Indices (-A)=[:Seg 0,Seg 0:]& Indices (A+ -A)=[:Seg 0,Seg 0:]
by A1,A2,A7,MATRIX_1:def 5;
hence Indices A= Indices (-A)& Indices A= Indices (A + (-A)) by A7,
FINSEQ_1:4,ZFMISC_1:113;
end;
now let i,j;
assume A8:[i,j] in Indices A;
hence (A + (-A))*(i,j)=A*(i,j)+ (-A)*(i,j) by Def3
.=A*(i,j)+ (-A*(i,j)) by A8,Def2
.=0.K by RLVECT_1:16
.=(0.(K,n,m))*(i,j) by A3,A8,Th3;
end;
hence thesis by A4,MATRIX_1:21;
end;
definition let K;let A,B be Matrix of K;
assume A1:width A=len B;
func A*B ->Matrix of K means
:Def4: len it=len A & width it=width B &
for i,j st [i,j] in Indices it holds
it*(i,j)=Line(A,i) "*" Col(B,j);
existence
proof
deffunc F(Nat,Nat) = Line(A,$1) "*" Col(B,$2);
consider M being Matrix of len A,width B,K such that
A2: for i,j st [i,j] in Indices M holds M*(i,j) = F(i,j)
from MatrixLambda;
A3: now per cases by NAT_1:19;
case len A > 0;
hence len M=len A & width M= width B by MATRIX_1:24;
case A4:len A=0;
then len B=0 by A1,MATRIX_1:def 4;
then A5:width B=0 by MATRIX_1:def 4;
len M=0 by A4,MATRIX_1:26;
hence len M=len A & width M= width B by A4,A5,MATRIX_1:def 4;
end;
take M;
thus thesis by A2,A3;
end;
uniqueness
proof let M1,M2 be Matrix of K;
assume that A6:len M1=len A & width M1=width B &
for i,j st [i,j] in Indices M1 holds
M1*(i,j)= Line(A,i) "*" Col(B,j) and
A7:len M2=len A & width M2=width B &
for i,j st [i,j] in Indices M2 holds
M2*(i,j)= Line(A,i) "*" Col(B,j);
dom M2 = dom M1 by A6,A7,FINSEQ_3:31;
then A8: Indices M1=[:dom M1,Seg width M1:] &
Indices M2=[:dom M1,Seg width M1:] by A6,A7,MATRIX_1:def 5;
now let i,j;
assume A9:[i,j] in Indices M1;
then M1*(i,j)= Line(A,i) "*" Col(B,j) by A6;
hence M1*(i,j)=M2*(i,j) by A7,A8,A9;
end;
hence thesis by A6,A7,MATRIX_1:21;
end;
end;
definition let n,k,m;let K;let A be Matrix of n,k,K;
let B be Matrix of width A,m,K;
redefine func A*B -> Matrix of len A,width B,K;
coherence
proof
width A= len B by MATRIX_1:26;
then len (A*B)=len A & width (A*B)=width B by Def4;
hence thesis by MATRIX_2:7;
end;
end;
definition let K;let M be Matrix of K;
let a be Element of K;
func a*M -> Matrix of K means
len it=len M & width it =width M &
for i,j st [i,j] in Indices M holds it*(i,j)=a*(M*(i,j));
existence
proof
deffunc F(Nat,Nat) = a*(M*($1,$2));
consider N being Matrix of len M,width M,K such that
A1:for i,j st [i,j] in Indices N holds N*(i,j) = F(i,j)
from MatrixLambda;
take N;
A2:len N=len M by MATRIX_1:def 3;
A3:now per cases by NAT_1:18;
case A4:len M= 0;
then width N=0 by A2,MATRIX_1:def 4;
hence width N=width M by A4,MATRIX_1:def 4;
case len M>0;
hence (width N)=width M by MATRIX_1:24;
end;
dom M = dom N by A2,FINSEQ_3:31;
then Indices N=[:dom M,Seg width M:] &
Indices M=[:dom M,Seg width M:] by A3,MATRIX_1:def 5;
hence thesis by A1,A3,MATRIX_1:def 3;
end;
uniqueness
proof
let A,B be Matrix of K;
assume that A5:len A=len M & width A =width M &
for i,j st [i,j] in Indices M holds A*(i,j)=a*(M*(i,j)) and
A6:len B=len M & width B =width M &
for i,j st [i,j] in Indices M holds B*(i,j)=a*(M*(i,j));
now let i,j;
assume A7:[i,j] in Indices A;
dom A = dom M by A5,FINSEQ_3:31;
then A8: Indices A=[:dom M,Seg width M:] &
Indices M= [:dom M,Seg width M:]by A5,MATRIX_1:def 5;
hence A*(i,j)=a*(M*(i,j)) by A5,A7
.=B*(i,j) by A6,A7,A8;
end;
hence A=B by A5,A6,MATRIX_1:21;
end;
end;
definition let K;let M be Matrix of K;
let a be Element of K;
func M*a -> Matrix of K equals
a*M;
coherence;
end;
theorem
for p,q being FinSequence of the carrier of K st len p=len q holds
len (mlt(p,q))=len p & len (mlt(p,q))=len q
proof
let p,q be FinSequence of the carrier of K;
assume A1:len p=len q;
reconsider r=mlt(p,q) as FinSequence of the carrier of K;
r=(the mult of K).:(p,q) by FVSUM_1:def 7;
hence thesis by A1,FINSEQ_2:86;
end;
theorem
for i,l st [i,l] in Indices (1.(K,n)) & l=i holds (Line(1.(K,n),i)).l=1_ K
proof
let i,l;
assume A1:[i,l] in Indices (1.(K,n)) & l=i;
Indices (1.(K,n))=[:dom (1.(K,n)),Seg width (1.(K,n)):]
by MATRIX_1:def 5;
then i in dom (1.(K,n)) & l in Seg width (1.(K,n))by A1,ZFMISC_1:106;
hence (Line(1.(K,n),i)).l=(1.(K,n))*(i,l) by MATRIX_1:def 8
.= 1_ K by A1,MATRIX_1:def 12;
end;
theorem
for i,l st [i,l] in Indices (1.(K,n)) &
l<>i holds (Line(1.(K,n),i)).l=0.K
proof
let i,l;
assume A1:[i,l] in Indices (1.(K,n)) & l<>i;
Indices (1.(K,n))=[:dom (1.(K,n)),Seg width (1.(K,n)):]
by MATRIX_1:def 5;
then i in dom (1.(K,n)) & l in Seg width (1.(K,n))by A1,ZFMISC_1:106;
hence (Line(1.(K,n),i)).l=(1.(K,n))*(i,l) by MATRIX_1:def 8
.= 0.K by A1,MATRIX_1:def 12;
end;
theorem
for l,j st [l,j] in Indices (1.(K,n))
& l=j holds (Col(1.(K,n),j)).l=1_ K
proof
let l,j;
assume A1:[l,j] in Indices (1.(K,n)) & l=j;
Indices (1.(K,n))=[:dom (1.(K,n)),Seg width (1.(K,n)):]
by MATRIX_1:def 5;
then l in dom (1.(K,n)) & j in Seg width (1.(K,n))by A1,ZFMISC_1:106;
hence (Col(1.(K,n),j)).l=(1.(K,n))*(l,j) by MATRIX_1:def 9
.= 1_ K by A1,MATRIX_1:def 12;
end;
theorem
for l,j st [l,j] in Indices (1.(K,n))
& l<>j holds (Col(1.(K,n),j)).l=0.K
proof
let l,j;
assume A1:[l,j] in Indices (1.(K,n)) & l<>j;
Indices (1.(K,n))=[:dom (1.(K,n)),Seg width (1.(K,n)):]
by MATRIX_1:def 5;
then l in dom (1.(K,n)) & j in Seg width (1.(K,n))by A1,ZFMISC_1:106;
hence (Col(1.(K,n),j)).l=(1.(K,n))*(l,j) by MATRIX_1:def 9
.= 0.K by A1,MATRIX_1:def 12;
end;
Lm1:
for L be add-associative right_zeroed right_complementable
(non empty LoopStr)
for p be FinSequence of the carrier of L st
for i be Nat st i in dom p holds p.i = 0.L holds
Sum p = 0.L
proof
let L be add-associative right_zeroed right_complementable
(non empty LoopStr);
let p be FinSequence of the carrier of L;
assume A1: for k be Nat st k in dom p holds p.k = 0.L;
defpred P[FinSequence of the carrier of L] means
(for k be Nat st k in dom $1 holds $1.k = 0.L) implies Sum($1) = 0.L;
A2:P[<*>the carrier of L] by RLVECT_1:60;
A3: for p being FinSequence of the carrier of L,
x being Element of L st P[p] holds P[p^<*x*>]
proof
let p be FinSequence of the carrier of L;
let x be Element of L;
assume A4: ( for k be Nat st k in dom p holds p.k = 0.L ) implies
Sum(p) = 0.L;
assume A5: for k be Nat st k in dom(p^<*x*>) holds (p^<*x*>).k = 0.L;
A6: for k be Nat st k in dom p holds p.k = 0.L
proof
let k be Nat such that
A7: k in dom p;
A8: dom p c= dom(p^<*x*>) by FINSEQ_1:39;
thus p.k = (p^<*x*>).k by A7,FINSEQ_1:def 7
.= 0.L by A5,A7,A8;
end;
A9: len(p^<*x*>) = len p + len<*x*> by FINSEQ_1:35
.= len p + 1 by FINSEQ_1:56;
len p + 1 in Seg (len p + 1) by FINSEQ_1:6;
then A10: len p + 1 in dom(p^<*x*>) by A9,FINSEQ_1:def 3;
A11: x = (p^<*x*>).(len p + 1) by FINSEQ_1:59;
thus Sum(p^<*x*>) = Sum(p) + Sum(<*x*>) by RLVECT_1:58
.= Sum(p) + x by RLVECT_1:61
.= 0.L + 0.L by A4,A5,A6,A10,A11
.= 0.L by RLVECT_1:def 7;
end;
for p be FinSequence of the carrier of L holds P[p] from IndSeqD(A2,A3);
hence thesis by A1;
end;
theorem Th13:
for K being add-associative right_zeroed right_complementable
(non empty LoopStr) holds
Sum (n |-> 0.K) = 0.K
proof
let K be add-associative right_zeroed right_complementable
(non empty LoopStr);
set p = n |-> 0.K;
for i be Nat st i in dom p holds p.i = 0.K
proof
let i be Nat; assume i in dom p;
then i in Seg n by FINSEQ_2:68;
hence thesis by FINSEQ_2:70;
end;
hence thesis by Lm1;
end;
theorem Th14:
for K being add-associative right_zeroed right_complementable
(non empty LoopStr)
for p being FinSequence of the carrier of K
for i st i in dom p & for k st k in dom p & k<>i holds p.k=0.K
holds Sum p=p.i
proof
let K being add-associative right_zeroed right_complementable
(non empty LoopStr);
let p be FinSequence of the carrier of K;
let i;
assume A1: i in dom p &
for k st k in dom p & k<>i holds p.k=0.K;
then reconsider a=p.i as Element of K by FINSEQ_2:13;
A2:1<=i & i <= len p by A1,FINSEQ_3:27;
A3:i<>0 by A1,FINSEQ_3:27;
reconsider p1=p|Seg i as FinSequence of the carrier of K by FINSEQ_1:23;
p1 is_a_prefix_of p by TREES_1:def 1;
then consider p2 being FinSequence
such that A4:p=p1^p2 by TREES_1:8;
i in Seg i by A3,FINSEQ_1:5;
then i in (dom p) /\ (Seg i) by A1,XBOOLE_0:def 3;
then A5:i in dom p1 by RELAT_1:90;
then p1 <> {} by FINSEQ_1:26;
then len p1<>0 by FINSEQ_1:25;
then consider p3 being FinSequence of the carrier of K,
x being Element of K such that A6:p1=p3^<*x*>
by FINSEQ_2:22;
reconsider p2 as FinSequence of the carrier of K by A4,FINSEQ_1:50;
A7:i =len p1 by A2,FINSEQ_1:21
.=len p3+ len <*x*> by A6,FINSEQ_1:35
.= len p3 + 1 by FINSEQ_1:56;
then A8:x =p1.i by A6,FINSEQ_1:59 .=a by A4,A5,FINSEQ_1:def 7;
A9:for k st k in Seg len p2 holds p2.k=0.K
proof
let k;
assume k in Seg len p2;
then A10:k in dom p2 by FINSEQ_1:def 3;
A11:1<=i & i <=len p1 by A5,FINSEQ_3:27;
0<>k by A10,FINSEQ_3:27;
then A12:len p1<>len p1 + k by Th1;
len p1 <= len p1 + k by NAT_1:37;
then A13:i<>len p1 + k by A11,A12,REAL_1:def 5;
A14: (len p1+ k) in dom p by A4,A10,FINSEQ_1:41;
thus p2.k=p.(len p1+k) by A4,A10,FINSEQ_1:def 7
.=0.K by A1,A13,A14;
end;
A15:p2=len p2 |->0.K
proof
A16:len (len p2 |->0.K)=len p2 by FINSEQ_2:69;
now let j;
assume A17:j in Seg len p2;
hence p2.j =0.K by A9
.= (len p2 |->0.K).j by A17,FINSEQ_1:4,FINSEQ_2:71;
end;
hence thesis by A16,FINSEQ_2:10;
end;
A18:for k st k in Seg len p3 holds p3.k=0.K
proof
let k;
assume A19:k in Seg len p3;
then 1<=k & k <= len p3 by FINSEQ_1:3;
then A20:i<> k by A7,NAT_1:38;
A21:k in dom p3 by A19,FINSEQ_1:def 3;
then A22: k in dom p1 by A6,FINSEQ_2:18;
then A23:k in dom p & k in dom p1 by A4,FINSEQ_2:18;
thus p3.k=p1.k by A6,A21,FINSEQ_1:def 7
.=p.k by A4,A22,FINSEQ_1:def 7
.=0.K by A1,A20,A23;
end;
A24:p3=len p3 |->0.K
proof
A25:len (len p3 |->0.K)=len p3 by FINSEQ_2:69;
now let j;
assume A26:j in Seg len p3;
hence p3.j =0.K by A18
.= (len p3 |->0.K).j by A26,FINSEQ_1:4,FINSEQ_2:71;
end;
hence thesis by A25,FINSEQ_2:10;
end;
Sum p=Sum(p3^<*x*>) + Sum(len p2 |->0.K) by A4,A6,A15,RLVECT_1:58
.=Sum(p3^<*x*>) + 0.K by Th13
.=Sum(p3^<*x*>) by RLVECT_1:10
.=Sum(len p3 |->0.K) + x by A24,FVSUM_1:87
.=0.K + a by A8,Th13
.=p.i by RLVECT_1:10;
hence thesis;
end;
theorem
Th15:for p,q being FinSequence of the carrier of K
holds len (mlt(p,q))=min(len p,len q)
proof
let p,q be FinSequence of the carrier of K;
reconsider r=mlt(p,q) as FinSequence of the carrier of K;
r=(the mult of K).:(p,q) by FVSUM_1:def 7;
hence thesis by FINSEQ_2:85;
end;
theorem Th16:
for p,q being FinSequence of the carrier of K
for i st i in dom p & p.i=1_ K &
for k st k in dom p & k<>i holds p.k=0.K
for j st j in dom (mlt(p,q)) holds
(i=j implies mlt(p,q).j=(q.i)) & (i<>j implies mlt(p,q).j=0.K)
proof
let p,q be FinSequence of the carrier of K;
let i;
assume that A1:i in dom p & p.i=1_ K and
A2:for k st k in dom p & k<>i holds p.k=0.K;
let j;
assume A3:j in dom (mlt(p,q));
A4: dom p = Seg len p & dom q = Seg len q &
dom(mlt(p,q)) = Seg len (mlt(p,q)) by FINSEQ_1:def 3;
len (mlt(p,q))=min(len p,len q) by Th15;
then j in (dom p) /\ (dom q) by A3,A4,FINSEQ_2:2;
then A5:j in dom p & j in dom q by XBOOLE_0:def 3;
thus (i=j implies mlt(p,q).j=(q.i))
proof
assume A6:i=j;
reconsider b=q.j as Element of K by A5,FINSEQ_2:13;
thus mlt(p,q).j=b*(1_ K) by A1,A3,A6,FVSUM_1:73
.=q.i by A6,VECTSP_1:def 19;
end;
thus (i<>j implies mlt(p,q).j=0.K)
proof
assume i<>j;
then A7:p.j=0.K by A2,A5;
reconsider b=q.j as Element of K by A5,FINSEQ_2:13;
thus mlt(p,q).j=(0.K)*b by A3,A7,FVSUM_1:73
.=0.K by VECTSP_1:44;
end;
end;
theorem Th17:
for i,j st [i,j] in Indices (1.(K,n)) holds
(i=j implies (Line((1.(K,n)),i)).j=1_ K) &
(i<>j implies (Line((1.(K,n)),i)).j=0.K)
proof
let i,j;
set B=1.(K,n);
assume A1:[i,j] in Indices (1.(K,n));
Indices B=[:dom B,Seg width B:] by MATRIX_1:def 5;
then i in dom B & j in Seg width B by A1,ZFMISC_1:106;
then A2:(Line(B,i)).j = B*(i,j) by MATRIX_1:def 8;
hence i=j implies (Line((1.(K,n)),i)).j=1_ K by A1,MATRIX_1:def 12;
thus thesis by A1,A2,MATRIX_1:def 12;
end;
theorem Th18:
for i,j st [i,j] in Indices (1.(K,n)) holds
(i=j implies (Col((1.(K,n)),j)).i=1_ K) &
(i<>j implies (Col((1.(K,n)),j)).i=0.K)
proof
let i,j;
set B=1.(K,n);
assume A1:[i,j] in Indices (1.(K,n));
Indices B=[:dom B,Seg width B:] by MATRIX_1:def 5;
then i in dom B & j in Seg width B by A1,ZFMISC_1:106;
then A2:(Col(B,j)).i = B*(i,j) by MATRIX_1:def 9;
hence i=j implies (Col((1.(K,n)),j)).i=1_ K by A1,MATRIX_1:def 12;
thus thesis by A1,A2,MATRIX_1:def 12;
end;
theorem Th19:
for p,q being FinSequence of the carrier of K
for i st i in dom p & i in dom q & p.i=1_ K &
for k st k in dom p & k<>i holds p.k=0.K
holds Sum(mlt(p,q))=q.i
proof
let p,q be FinSequence of the carrier of K;
let i;
assume that A1:i in dom p & i in dom q & p.i=1_ K and
A2:for k st k in dom p & k<>i holds p.k=0.K;
reconsider r=mlt(p,q) as FinSequence of the carrier of K;
A3:i in dom r & r.i=q.i
proof
A4: dom p = Seg len p & dom q = Seg len q &
dom (mlt(p,q)) = Seg len (mlt(p,q)) by FINSEQ_1:def 3;
len (mlt(p,q))=min(len p,len q) by Th15;
then A5: dom p /\ dom q = dom (mlt(p,q)) by A4,FINSEQ_2:2;
then A6:i in dom (mlt(p,q)) by A1,XBOOLE_0:def 3;
thus i in dom r by A1,A5,XBOOLE_0:def 3;
thus r.i=q.i by A1,A2,A6,Th16;
end;
for k st k in dom r & k<>i holds r.k=0.K by A1,A2,Th16;
hence Sum(mlt(p,q))=q.i by A3,Th14;
thus thesis;
end;
theorem
for A being Matrix of n,K holds 1.(K,n)*A=A
proof
let A be Matrix of n,K;
set B=1.(K,n);
A1:len B=n & width B=n & len A=n & width A=n by MATRIX_1:25;
then A2:len (B*A)=len (B) & width (B*A)=width A by Def4;
now let i,j;
assume A3:[i,j] in Indices (B*A);
A4: dom A = Seg len A & dom B = Seg len B &
dom (B*A) = Seg len (B*A) by FINSEQ_1:def 3;
Indices (B*A)=[:dom (B*A),Seg width(B*A):] by MATRIX_1:def 5;
then A5:i in dom B & i in Seg width B by A1,A2,A3,A4,ZFMISC_1:106;
then [i,i] in [:dom B,Seg width B:] by ZFMISC_1:106;
then A6:[i,i] in Indices B by MATRIX_1:def 5;
i in Seg len(Line(B,i)) by A5,MATRIX_1:def 8;
then A7:i in dom (Line(B,i)) by FINSEQ_1:def 3;
i in Seg len (Col(A,j)) by A1,A5,MATRIX_1:def 9;
then A8:i in dom (Col(A,j)) by FINSEQ_1:def 3;
A9: (Line(B,i)).i=1_ K &
for k st k in dom (Line (B,i)) & k<>i holds (Line(B,i)).k=0.K
proof
thus (Line(B,i)).i=1_ K by A6,Th17;
now let k;
assume A10:k in dom (Line (B,i)) & k<>i;
then k in Seg len (Line (B,i)) by FINSEQ_1:def 3;
then k in Seg width B by MATRIX_1:def 8;
then [i,k] in [:dom B,Seg width B:] by A5,ZFMISC_1:106;
then [i,k] in Indices B by MATRIX_1:def 5;
hence (Line(B,i)).k=0.K by A10,Th17;
end;
hence thesis;
end;
thus (B*A)*(i,j)= Line(B,i) "*" Col(A,j) by A1,A3,Def4
.=Sum(mlt(Line(B,i),Col(A,j))) by FVSUM_1:def 10
.=Col(A,j).i by A7,A8,A9,Th19
.=A*(i,j) by A1,A4,A5,MATRIX_1:def 9;
end;
hence thesis by A1,A2,MATRIX_1:21;
end;
theorem
for A being Matrix of n,K holds A*(1.(K,n))=A
proof
let A be Matrix of n,K;
set B=1.(K,n);
A1:len B=n & width B=n & len A=n & width A=n by MATRIX_1:25;
then A2:len (A*B)=len A & width (A*B)=width B by Def4;
now let i,j;
assume A3:[i,j] in Indices (A*B);
Indices (A*B)=[:dom (A*B),Seg width(A*B):] by MATRIX_1:def 5;
then A4:j in Seg width B & j in Seg width A by A1,A2,A3,ZFMISC_1:106;
then j in dom B & j in Seg width A by A1,FINSEQ_1:def 3;
then [j,j] in [:dom B,Seg width B:] by A1,ZFMISC_1:106;
then A5:[j,j] in Indices B by MATRIX_1:def 5;
j in Seg len (Col(B,j)) & j in Seg len (Line(A,i))
by A1,A4,MATRIX_1:def 8,def 9;
then A6:j in dom (Col(B,j)) & j in dom (Line(A,i)) by FINSEQ_1:def 3;
A7: (Col(B,j)).j=1_ K &
for k st k in dom (Col(B,j)) & k<>j holds (Col(B,j)).k=0.K
proof
thus (Col(B,j)).j=1_ K by A5,Th18;
now let k;
assume A8:k in dom (Col(B,j)) & k<>j;
then k in Seg len (Col(B,j)) by FINSEQ_1:def 3;
then k in Seg len B by MATRIX_1:def 9;
then k in dom B by FINSEQ_1:def 3;
then [k,j] in [:dom B,Seg width B:] by A4,ZFMISC_1:106;
then [k,j] in Indices B by MATRIX_1:def 5;
hence (Col(B,j)).k=0.K by A8,Th18;
end;
hence thesis;
end;
thus (A*B)*(i,j)= Line(A,i) "*" Col(B,j) by A1,A3,Def4
.=Col(B,j) "*" Line(A,i) by FVSUM_1:115
.=Sum(mlt(Col(B,j),Line(A,i))) by FVSUM_1:def 10
.=Line(A,i).j by A6,A7,Th19
.=A*(i,j) by A4,MATRIX_1:def 8;
end;
hence thesis by A1,A2,MATRIX_1:21;
end;
theorem
for a,b being Element of K holds
<*<*a*>*> * <*<*b*>*> =<*<*a*b*>*>
proof let a,b be Element of K;
reconsider A=<*<*a*>*> as Matrix of 1,K;
reconsider B=<*<*b*>*> as Matrix of 1,K;
reconsider D=<*<*a*b*>*> as Matrix of 1,K;
A1:len A =1 & width A=1 & len B=1 & width B=1 & Indices A=[:Seg 1,Seg 1:]
& Indices B=[:Seg 1 ,Seg 1:] & len D=1 & width D=1 &
Indices D=[:Seg 1,Seg 1:] by MATRIX_1:25;
reconsider C=A*B as Matrix of K;
A2:Line(<*<*a*>*>,1)=<*a*>
proof
A3:len Line(A,1)=width A by MATRIX_1:def 8
.=1 by MATRIX_1:25;
1 in Seg width A by A1,FINSEQ_1:4,TARSKI:def 1;
then Line(A,1).1=<*<*a*>*>*(1,1) by MATRIX_1:def 8
.=a by MATRIX_2:5;
hence thesis by A3,FINSEQ_1:57;
end;
A4:Col(<*<*b*>*>,1)=<*b*>
proof
A5:len Col(B,1)=len B by MATRIX_1:def 9
.=1 by MATRIX_1:25;
1 in Seg len B by A1,FINSEQ_1:4,TARSKI:def 1;
then 1 in dom B by FINSEQ_1:def 3;
then Col(B,1).1=<*<*b*>*>*(1,1) by MATRIX_1:def 9
.=b by MATRIX_2:5;
hence thesis by A5,FINSEQ_1:57;
end;
A6:len C=1 & width C=1 by A1,Def4;
then reconsider C as Matrix of 1,K by MATRIX_2:7;
Seg len C = dom C by FINSEQ_1:def 3;
then A7:Indices C=[:Seg 1,Seg 1:] by A6,MATRIX_1:def 5;
now let i,j;
assume A8:[i,j] in Indices C;
then i in Seg 1 & j in Seg 1 by A7,ZFMISC_1:106;
then A9:i=1 & j=1 by FINSEQ_1:4,TARSKI:def 1;
hence C*(i,j)=<*a*> "*" <*b*> by A1,A2,A4,A8,Def4
.=a * b by FVSUM_1:113
.=<*<*a*b*>*>*(i,j) by A9,MATRIX_2:5;
end;
hence thesis by MATRIX_1:28;
end;
theorem
for a1,a2,b1,b2,c1,c2,d1,d2 being Element of K holds
(a1,b1)][(c1,d1)*(a2,b2)][(c2,d2) =
(a1*a2+b1*c2,a1*b2+b1*d2)][(c1*a2+d1*c2,c1*b2+ d1*d2)
proof let a1,a2,b1,b2,c1,c2,d1,d2 be Element of K;
reconsider A=(a1,b1)][(c1,d1) as Matrix of 2,K;
reconsider B=(a2,b2)][(c2,d2) as Matrix of 2,K;
reconsider D=(a1*a2+b1*c2,a1*b2+b1*d2)][(c1*a2+d1*c2,c1*b2+ d1*d2)
as Matrix of 2,K;
A1:len A =2 & width A=2 & len B=2 & width B=2 & Indices A=[:Seg 2,Seg 2:]
& Indices B=[:Seg 2 ,Seg 2:] & len D=2 & width D=2 &
Indices D=[:Seg 2,Seg 2:] by MATRIX_1:25;
reconsider C=A*B as Matrix of K;
A2:Line(A,1)=<*a1,b1*>
proof
A3:len Line(A,1)=width A by MATRIX_1:def 8
.=2 by MATRIX_1:25;
A4:1 in {1,2} & 2 in{1,2} by TARSKI:def 2;
then A5:Line(A,1).1=A*(1,1) by A1,FINSEQ_1:4,MATRIX_1:def 8
.=a1 by MATRIX_2:6;
Line(A,1).2=A*(1,2) by A1,A4,FINSEQ_1:4,MATRIX_1:def 8
.=b1 by MATRIX_2:6;
hence thesis by A3,A5,FINSEQ_1:61;
end;
A6:Line(A,2)=<*c1,d1*>
proof
A7:len Line(A,2)=width A by MATRIX_1:def 8
.=2 by MATRIX_1:25;
A8:1 in {1,2} & 2 in{1,2} by TARSKI:def 2;
then A9:Line(A,2).1=A*(2,1) by A1,FINSEQ_1:4,MATRIX_1:def 8
.=c1 by MATRIX_2:6;
Line(A,2).2=A*(2,2) by A1,A8,FINSEQ_1:4,MATRIX_1:def 8
.=d1 by MATRIX_2:6;
hence thesis by A7,A9,FINSEQ_1:61;
end;
A10: Seg len A = dom A & Seg len B = dom B by FINSEQ_1:def 3;
A11:Col(B,1)=<*a2,c2*>
proof
A12:len Col(B,1)=len B by MATRIX_1:def 9
.=2 by MATRIX_1:25;
A13:1 in {1,2} & 2 in {1,2} by TARSKI:def 2;
then A14:Col(B,1).1=B*(1,1) by A1,A10,FINSEQ_1:4,MATRIX_1:def 9
.=a2 by MATRIX_2:6;
Col(B,1).2=B*(2,1) by A1,A10,A13,FINSEQ_1:4,MATRIX_1:def 9
.=c2 by MATRIX_2:6;
hence thesis by A12,A14,FINSEQ_1:61;
end;
A15:Col(B,2)=<*b2,d2*>
proof
A16:len Col(B,2)=len B by MATRIX_1:def 9
.=2 by MATRIX_1:25;
A17:1 in {1,2} & 2 in {1,2} by TARSKI:def 2;
then A18:Col(B,2).1=B*(1,2) by A1,A10,FINSEQ_1:4,MATRIX_1:def 9
.=b2 by MATRIX_2:6;
Col(B,2).2=B*(2,2) by A1,A10,A17,FINSEQ_1:4,MATRIX_1:def 9
.=d2 by MATRIX_2:6;
hence thesis by A16,A18,FINSEQ_1:61;
end;
A19:len C=2 & width C=2 by A1,Def4;
then reconsider C as Matrix of 2,K by MATRIX_2:7;
dom C = Seg len C by FINSEQ_1:def 3;
then A20:Indices C=[:Seg 2,Seg 2:] by A19,MATRIX_1:def 5;
now let i,j;
assume A21:[i,j] in Indices C;
then A22: i in Seg 2 & j in Seg 2 by A20,ZFMISC_1:106;
now per cases by A22,FINSEQ_1:4,TARSKI:def 2;
case i=1 & j=1;
hence C*(1,1)=<*a1,b1*> "*" <*a2,c2*> by A1,A2,A11,A21,Def4
.=a1 * a2+ b1*c2 by FVSUM_1:114
.=D*(1,1) by MATRIX_2:6;
case i=1 & j=2;
hence C*(1,2)=<*a1,b1*> "*" <*b2,d2*> by A1,A2,A15,A21,Def4
.=a1 * b2+ b1*d2 by FVSUM_1:114
.=D*(1,2) by MATRIX_2:6;
case i=2 & j=1;
hence C*(2,1)=<*c1,d1*> "*" <*a2,c2*> by A1,A6,A11,A21,Def4
.=c1 * a2+ d1*c2 by FVSUM_1:114
.=D*(2,1) by MATRIX_2:6;
case i=2 & j=2;
hence C*(2,2)=<*c1,d1*> "*" <*b2,d2*> by A1,A6,A15,A21,Def4
.=c1 * b2+ d1*d2 by FVSUM_1:114
.=D*(2,2) by MATRIX_2:6;
end;
hence C*(i,j)=D*(i,j);
end;
hence thesis by MATRIX_1:28;
end;
theorem
for A,B being Matrix of K st width A=len B & width B<>0 holds
(A*B) @=(B @)*(A @)
proof
let A,B be Matrix of K;
assume A1:width A=len B & width B<>0;
then A2:width B>0 by NAT_1:19;
A3:len (B@)=width B & len (A@)=width A by MATRIX_1:def 7;
then A4:width (B@)=len (A@) by A1,A2,MATRIX_2:12;
then A5:len ((B@)*(A@))=len (B@) & width ((B@)*(A@))=width (A@) by Def4;
A6:len ((A*B)@)=width (A*B) by MATRIX_1:def 7
.=width B by A1,Def4;
width (A*B)>0 by A1,A2,Def4;
then A7:width ((A*B)@)=len (A*B) by MATRIX_2:12
.=len A by A1,Def4;
A8:len (B@*A@)=len (B@) by A4,Def4
.=width B by MATRIX_1:def 7;
A9:width (B@*A@)=width (A@) by A4,Def4;
A10:now let i,j;
assume A11:[i,j] in Indices ((B@)*(A@));
dom((B@)*(A@))=dom(B@) by A5,FINSEQ_3:31;
then A12:[i,j] in [:dom (B@),Seg width (A@):] by A5,A11,MATRIX_1:def 5;
now per cases by NAT_1:18;
case width A=0;
hence ((B@)*(A@))*(i,j)=((A*B)@)*(i,j) by A1,MATRIX_1:def 4;
case width A>0;
then width (A@)= len A by MATRIX_2:12;
then Seg width B = dom (B@) & Seg width (A@) = dom A
by A3,FINSEQ_1:def 3;
then A13:i in Seg width B & j in dom A by A12,ZFMISC_1:106;
then A14:Line(B@,i)=Col(B,i) & Col(A@,j)=Line(A,j) by MATRIX_2:16,17;
j in Seg len A by A13,FINSEQ_1:def 3;
then j in Seg len (A*B) by A1,Def4;
then A15: j in dom (A*B) by FINSEQ_1:def 3;
i in Seg width (A*B) by A1,A13,Def4;
then [j,i] in [:dom(A*B),Seg width (A*B):] by A15,ZFMISC_1:106;
then A16:[j,i]in Indices (A*B) by MATRIX_1:def 5;
thus ((B@)*(A@))*(i,j)= Col(B,i) "*" Line(A,j) by A4,A11,A14,Def4
.= Line(A,j) "*" Col(B,i) by FVSUM_1:115
.=(A*B)*(j,i) by A1,A16,Def4
.=((A*B)@)*(i,j) by A16,MATRIX_1:def 7;
end;
hence ((B@)*(A@))*(i,j)=((A*B)@)*(i,j);
end;
width (A@)=len A
proof
now per cases by NAT_1:18;
case width A=0;
hence width (A@)=len A by A1,MATRIX_1:def 4;
case width A>0;
hence width (A@)= len A by MATRIX_2:12;
end;
hence thesis;
end;
hence thesis by A6,A7,A8,A9,A10,MATRIX_1:21;
end;
begin :: The product of Matrices
definition let I,J be non empty set;
let X be Element of Fin I;
let Y be Element of Fin J;
redefine func [:X,Y:]-> Element of Fin [:I,J:];
coherence
proof
X c= I & X is finite & Y c= J & Y is finite by FINSUB_1:def 5;
then [:X,Y:] c=[:I,J:] by ZFMISC_1:119;
hence thesis by FINSUB_1:def 5;
end;
end;
definition let I,J,D be non empty set;
let G be BinOp of D;
let f be Function of I,D;
let g be Function of J,D;
redefine func G*(f,g)-> Function of [:I,J:],D;
coherence by FINSEQOP:84;
end;
theorem Th25:
for I, J,D be non empty set for F,G be BinOp of D
for f be Function of I,D for g being Function of J,D
for X being Element of Fin I for Y being Element of Fin J st
F is commutative & F is associative & ( [:Y,X:]<>{} or F has_a_unity )&
G is commutative holds
F $$ ([:X,Y:],G*(f,g))=F$$([:Y,X:],G*(g,f))
proof
let I, J,D be non empty set;
let F,G be BinOp of D;
let f be Function of I,D;
let g be Function of J,D;
let X be Element of Fin I ,Y be Element of Fin J;
assume A1: F is commutative & F is associative &
([:Y,X:]<>{} or F has_a_unity);
assume A2:G is commutative;
A3:X c= I & Y c=J by FINSUB_1:def 5;
deffunc F(set,set) = [$2,$1];
consider h being Function such that A4:dom h=[:J,I:] &
for x,y st x in J & y in I holds h.[x,y]= F(x,y) from Lambda_3;
A5:h is one-to-one
proof
now let z1,z2;
assume A6:z1 in dom h & z2 in dom h & h.z1=h.z2;
then consider x1,y1 such that A7:z1=[x1,y1] by A4,ZFMISC_1:102;
consider x2,y2 such that A8:z2=[x2,y2] by A4,A6,ZFMISC_1:102;
A9:x1 in J & y1 in I & x2 in J & y2 in I by A4,A6,A7,A8,ZFMISC_1:106;
then A10:h.z1=[y1,x1] by A4,A7;
h.z2=[y2,x2] by A4,A8,A9;
then y1=y2 & x1=x2 by A6,A10,ZFMISC_1:33;
hence z1=z2 by A7,A8;
end;
hence thesis by FUNCT_1:def 8;
end;
A11:h.:([:Y,X:])=[:X,Y:]
proof
for y holds y in [:X,Y:] iff y in h.:([:Y,X:])
proof
let y;
thus y in [:X,Y:] implies y in h.:([:Y,X:])
proof
assume A12:y in [:X,Y:];
then consider y1,x1 such that A13:y=[y1,x1] by ZFMISC_1:102;
A14:y1 in X & x1 in Y by A12,A13,ZFMISC_1:106;
then A15:[x1,y1] in [:Y,X:] by ZFMISC_1:106;
A16:[x1,y1] in dom h by A3,A4,A14,ZFMISC_1:106;
h.[x1,y1]=y by A3,A4,A13,A14;
hence thesis by A15,A16,FUNCT_1:def 12;
end;
assume y in h.:([:Y,X:]);
then consider x such that A17:x in dom h & x in [:Y,X:] & y = h.x by
FUNCT_1:def 12;
consider x1,y1 such that A18:x=[x1,y1] by A17,ZFMISC_1:102;
A19: x1 in Y & y1 in X by A17,A18,ZFMISC_1:106;
then y=[y1,x1] by A3,A4,A17,A18;
hence thesis by A19,ZFMISC_1:106;
end;
hence thesis by TARSKI:2;
end;
A20:for x st x in [:J,I:] holds h.x in [:I,J:]
proof
let x;
assume A21:x in[:J,I:];
then consider y,z such that A22:x=[y,z] by ZFMISC_1:102;
A23:y in J & z in I by A21,A22,ZFMISC_1:106;
then h.x=[z,y] by A4,A22;
hence thesis by A23,ZFMISC_1:106;
end;
A24:G*(g,f)=(G*(f,g))*h
proof
reconsider G as Function of [:D,D:],D;
A25:dom (G*(f,g))=[:I,J:] by FUNCT_2:def 1;
A26:dom (G*(g,f))=[:J,I:] by FUNCT_2:def 1;
(for x holds x in dom (G*(g,f)) iff x in dom h & h.x in dom (G*(f,g))) &
(for x st x in dom (G*(g,f)) holds (G*(g,f)).x = (G*(f,g)).(h.x))
proof
thus for x holds
x in dom (G*(g,f)) iff x in dom h & h.x in dom (G*(f,g))
proof
let x;
thus x in dom (G*(g,f)) implies x in dom h & h.x in dom (G*(f,g))
proof
assume A27: x in dom (G*(g,f));
then consider y,z such that A28:x=[y,z] by A26,ZFMISC_1:102;
A29:y in J & z in I by A26,A27,A28,ZFMISC_1:106;
then h.x=[z,y] by A4,A28;
hence thesis by A4,A25,A27,A29,FUNCT_2:def 1,ZFMISC_1:106;
end;
assume x in dom h & h.x in dom (G*(f,g));
hence thesis by A4,FUNCT_2:def 1;
end;
thus (for x st x in dom (G*(g,f)) holds (G*(g,f)).x = (G*(f,g)).(h.x))
proof
let x;
assume A30: x in dom (G*(g,f));
then consider y,z such that A31:x=[y,z] by A26,ZFMISC_1:102;
reconsider y as Element of J by A26,A30,A31,ZFMISC_1:106;
reconsider z as Element of I by A26,A30,A31,ZFMISC_1:106;
A32:[z,y] in dom (G*(f,g)) & [y,z] in dom (G*(g,f)) by A25,A26,
ZFMISC_1:106;
thus (G*(f,g)).(h.x)= (G*(f,g)).[z,y] by A4,A31
.=G.[f.z,g.y] by A32,FINSEQOP:82
.=G.(f.z,g.y) by BINOP_1:def 1
.=G.(g.y,f.z) by A2,BINOP_1:def 2
.=G.[g.y,f.z] by BINOP_1:def 1
.=(G*(g,f)).x by A31,A32,FINSEQOP:82;
end;
thus thesis;
end;
hence thesis by FUNCT_1:20;
end;
reconsider h as Function of [:J,I:],[:I,J:] by A4,A20,FUNCT_2:5;
F $$ ([:X,Y:],G*(f,g))=F $$ ([:Y,X:],(G*(f,g))*h) by A1,A5,A11,SETWOP_2:8
.=F $$ ([:Y,X:],G*(g,f)) by A24;
hence thesis;
end;
theorem Th26:
for I, J be non empty set for F,G be BinOp of D
for f be Function of I,D for g being Function of J,D st
F is commutative & F is associative & F has_a_unity holds
for x being Element of I for y being Element of J holds
F $$([:{x},{y}:],G*(f,g))=F$$({x},G[:](f,F$$({y},g)))
proof
let I, J be non empty set;
let F,G be BinOp of D;
let f be Function of I,D;
let g be Function of J,D;
assume A1: F is commutative & F is associative & F has_a_unity;
reconsider G as Function of [:D,D:],D;
A2:dom (G*(f,g))=[:I,J:] by FUNCT_2:def 1;
now let x be Element of I;let y be Element of J;
A3:[x,y] in [:I,J:] by ZFMISC_1:106;
reconsider u=[x,y] as Element of [:I,J:] by ZFMISC_1:106;
A4: F $$([:{x},{y}:],G*(f,g))= F $$({u},G*(f,g)) by ZFMISC_1:35
.= G*(f,g).[x,y] by A1,SETWISEO:26
.=G.[f.x,g.y] by A2,A3,FINSEQOP:82
.=G.(f.x,g.y) by BINOP_1:def 1;
reconsider z=g.y as Element of D;
A5: dom f=I by FUNCT_2:def 1;
dom <:f, dom f --> z:> = dom f /\ dom (dom f --> z) by FUNCT_3:def 8
.= dom f /\ dom f by FUNCOP_1:19
.=dom f;
then A6: x in dom <:f, dom f --> z:> by A5;
A7:rng f c= D by RELSET_1:12;
A8: {z} c= D by ZFMISC_1:37;
rng (dom f --> z) c= {z} by FUNCOP_1:19;
then A9:rng (dom f --> z) c=D by A8,XBOOLE_1:1;
A10:dom G =[:D,D:] by FUNCT_2:def 1;
A11:rng<:f, dom f --> z:> c= [:rng f,rng (dom f --> z):] by FUNCT_3:71;
[:rng f,rng (dom f --> z):] c= [:D,D:] by A7,A9,ZFMISC_1:119;
then rng<:f, dom f --> z:> c= dom G by A10,A11,XBOOLE_1:1;
then x in dom (G * <:f, dom f --> z:>) by A6,RELAT_1:46;
then A12:x in dom (G[:](f,z))by FUNCOP_1:def 4;
F$$({x},G[:](f,F$$({y},g)))=(G[:](f,F$$({y},g))).x by A1,SETWISEO:26
.=(G[:](f,g.y)).x by A1,SETWISEO:26
.= G.(f.x,g.y) by A12,FUNCOP_1:35;
hence F $$([:{x},{y}:],G*(f,g))=F$$({x},G[:](f,F$$({y},g))) by A4;
end;
hence thesis;
end;
theorem Th27:
for I, J be non empty set for F,G be BinOp of D
for f be Function of I,D for g being Function of J,D
for X being Element of Fin I for Y being Element of Fin J st
F is commutative & F is associative & F has_a_unity &
F has_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I holds
F $$([:{x},Y:],G*(f,g))=F$$({x},G[:](f,F$$(Y,g)))
proof
let I, J be non empty set;
let F,G be BinOp of D;
let f be Function of I,D;
let g be Function of J,D;
let X be Element of Fin I;
let Y be Element of Fin J;
assume A1: F is commutative & F is associative & F has_a_unity
& F has_an_inverseOp & G is_distributive_wrt F;
now let x be Element of I;
defpred P[Element of Fin J] means
F$$([:{x},$1:],G*(f,g))=F$$({x},G[:](f,F$$($1,g)));
A2: P[{}.J]
proof
reconsider T={}.[:I,J:] as Element of Fin [:I,J:];
A3: T=[:{x},{}.J:] by ZFMISC_1:113;
A4: dom f=I by FUNCT_2:def 1; set z=the_unity_wrt F;
dom <:f, dom f --> z:> = dom f /\ dom (dom f --> z) by FUNCT_3:def 8
.= dom f /\ dom f by FUNCOP_1:19
.=dom f;
then A5: x in dom <:f, dom f --> z:> by A4;
A6:rng f c= D by RELSET_1:12;
A7: {z} c= D by ZFMISC_1:37;
rng (dom f --> z) c= {z} by FUNCOP_1:19;
then A8:rng (dom f --> z) c=D by A7,XBOOLE_1:1;
A9:dom G =[:D,D:] by FUNCT_2:def 1;
A10:rng<:f, dom f --> z:> c= [:rng f,rng (dom f --> z):] by FUNCT_3:71;
[:rng f,rng (dom f --> z):] c= [:D,D:] by A6,A8,ZFMISC_1:119;
then rng<:f, dom f --> z:> c= dom G by A9,A10,XBOOLE_1:1;
then x in dom (G*<:f, dom f --> z:>) by A5,RELAT_1:46;
then A11:x in dom (G[:](f,z))by FUNCOP_1:def 4;
F$$({x},G[:](f,F$$({}.J,g)))=F$$({x},G[:](f,the_unity_wrt F))
by A1,SETWISEO:40
.=(G[:](f,the_unity_wrt F)).x by A1,SETWISEO:26
.= G.(f.x,the_unity_wrt F) by A11,FUNCOP_1:35
.=the_unity_wrt F by A1,FINSEQOP:70;
hence thesis by A1,A3,SETWISEO:40;
end;
A12:for Y1 being Element of Fin J,y being Element of J
st P[Y1] holds P[Y1 \/ {y}]
proof
let Y1 be Element of Fin J,y be Element of J;
assume A13: F$$([:{x},Y1:],G*(f,g))=F$$({x},G[:](f,F$$(Y1,g)));
reconsider s={y} as Element of Fin J;
now per cases;
case y in Y1;
then Y1 \/ {y} = Y1 by ZFMISC_1:46;
hence F$$([:{x},Y1 \/ {y}:],G*(f,g))=F$$({x},G[:](f,F$$(Y1 \/
{y},g))) by A13;
case not y in Y1;
then A14:Y1 misses {y} by ZFMISC_1:56;
then A15:[:{x},Y1:] misses [:{x},s:] by ZFMISC_1:127;
thus F$$([:{x},Y1 \/ {y}:],G*(f,g))
=F$$([:{x},Y1:] \/ [:{x},s:],G*(f,g)) by ZFMISC_1:120
.=F.(F$$([:{x},Y1:],G*(f,g)),F$$([:{x},s:],G*(f,g)))
by A1,A15,SETWOP_2:6
.=F.(F$$({x},G[:](f,F$$(Y1,g))),F$$({x},G[:](f,F$$(s,g))))
by A1,A13,Th26
.=F$$({x},F.:(G[:](f,F$$(Y1,g)),G[:](f,F$$(s,g)))) by A1,SETWOP_2:12
.=F$$({x},G[:](f,F.(F$$(Y1,g),F$$(s,g)))) by A1,FINSEQOP:37
.=F$$({x},G[:](f,F$$(Y1 \/ {y},g))) by A1,A14,SETWOP_2:6;
end;
hence thesis;
end;
thus for Y being Element of Fin J holds P[Y] from FinSubInd3(A2,A12);
end;
hence thesis;
end;
theorem Th28:
for I, J being non empty set
for F,G being BinOp of D
for f being Function of I,D for g being Function of J,D
for X being Element of Fin I for Y being Element of Fin J st
F has_a_unity & F is commutative & F is associative &
F has_an_inverseOp & G is_distributive_wrt F holds
F$$([:X,Y:],G*(f,g))=F$$(X,G[:](f,F$$(Y,g)))
proof
let I, J be non empty set;
let F,G be BinOp of D;
let f be Function of I,D;
let g be Function of J,D;
let X be Element of Fin I;
let Y be Element of Fin J;
assume that
A1: F has_a_unity & F is commutative & F is associative and
A2: F has_an_inverseOp & G is_distributive_wrt F;
defpred P[Element of Fin I] means
F$$([:$1,Y:],G*(f,g))=F$$($1,G[:](f,F$$(Y,g)));
A3: P[{}.I]
proof
reconsider T={}.[:I,J:] as Element of Fin [:I,J:];
T=[:{}.I,Y:] by ZFMISC_1:113;
then F $$([:{}.I,Y:],G*(f,g))= the_unity_wrt F by A1,SETWISEO:40;
hence thesis by A1,SETWISEO:40;
end;
A4:for X1 being Element of Fin I,x being Element of I
st P[X1] holds P[X1 \/ {x}]
proof
let X1 be Element of Fin I,x be Element of I;
assume A5: F$$([:X1,Y:],G*(f,g))=F$$(X1,G[:](f,F$$(Y,g)));
reconsider s={x} as Element of Fin I;
now per cases;
case x in X1;
then X1 \/ {x} = X1 by ZFMISC_1:46;
hence F$$([:X1 \/ {x},Y:],G*(f,g))=F$$(X1 \/ {x},G[:](f,F$$(Y,g))) by A5
;
case not x in X1;
then A6:X1 misses {x} by ZFMISC_1:56;
then A7:[:X1,Y:] misses [:s,Y:] by ZFMISC_1:127;
thus F$$([:X1 \/ {x},Y:],G*(f,g))
=F$$([:X1,Y:] \/ [:s,Y:],G*(f,g))by ZFMISC_1:120
.=F.(F $$([:X1,Y:],G*(f,g)),F $$([:s,Y:],G*(f,g))) by A1,A7,SETWOP_2:6
.=F.(F$$(X1,G[:](f,F$$(Y,g))),F$$(s,G[:](f,F$$(Y,g))))
by A1,A2,A5,Th27
.=F$$(X1 \/ {x},G[:](f,F$$(Y,g))) by A1,A6,SETWOP_2:6;
end;
hence thesis;
end;
for X1 being Element of Fin I holds P[X1] from FinSubInd3(A3,A4);
hence thesis;
end;
theorem
for I, J be non empty set for F,G be BinOp of D
for f be Function of I,D for g being Function of J,D st
F is commutative associative & F has_a_unity & G is commutative holds
for x being Element of I for y being Element of J holds
F $$([:{x},{y}:],G*(f,g))=F$$({y},G[;](F$$({x},f),g))
proof
let I, J be non empty set;
let F,G be BinOp of D;
let f be Function of I,D;
let g be Function of J,D;
assume A1: F is commutative associative & F has_a_unity
& G is commutative;
now let x be Element of I;let y be Element of J;
thus F $$ ([:{x},{y}:],G*(f,g))=F$$([:{y},{x}:],G*(g,f)) by A1,Th25
.=F$$({y},G[:](g,F$$({x},f))) by A1,Th26
.=F$$({y},G[;]
(F$$({x},f),g)) by A1,FUNCOP_1:79;
end;
hence thesis;
end;
theorem
for I, J being non empty set
for F,G being BinOp of D
for f being Function of I,D for g being Function of J,D
for X being Element of Fin I for Y being Element of Fin J st
F has_a_unity & F is commutative associative &
F has_an_inverseOp & G is_distributive_wrt F & G is commutative holds
F$$([:X,Y:],G*(f,g))=F$$(Y,G[;](F$$(X,f),g))
proof
let I, J be non empty set;
let F,G be BinOp of D;
let f be Function of I,D;
let g be Function of J,D;
let X be Element of Fin I;
let Y be Element of Fin J;
assume that
A1: F has_a_unity & F is commutative & F is associative and
A2: F has_an_inverseOp & G is_distributive_wrt F & G is commutative;
thus F $$ ([:X,Y:],G*(f,g))=F$$([:Y,X:],G*(g,f)) by A1,A2,Th25
.=F$$(Y,G[:](g,F$$(X,f))) by A1,A2,Th28
.=F$$(Y,G[;](F$$(X,f),g)) by A2,FUNCOP_1:79;
end;
theorem
Th31: for I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for Y being Element of Fin J st
F has_a_unity & F is commutative associative &
F has_an_inverseOp holds
for x being Element of I holds
(for i being Element of I holds g.i=F$$(Y,(curry f).i)) implies
F$$([:{x},Y:],f)=F$$({x},g)
proof
let I, J be non empty set;
let F be BinOp of D;
let f be Function of [:I,J:],D;
let g be Function of I,D;
let Y be Element of Fin J;
assume A1:F has_a_unity & F is commutative & F is associative &
F has_an_inverseOp;
now let x be Element of I;
assume A2:(for i being Element of I holds g.i=F$$(Y,(curry f).i));
deffunc F(set) = [x,$1];
consider h being Function such that A3:dom h = J & for y st y in J holds
h.y = F(y) from Lambda;
A4:h is one-to-one
proof
now let x1,x2;
assume A5:x1 in dom h & x2 in dom h & h.x1=h.x2;
then [x,x1]=h.x2 by A3
.=[x,x2] by A3,A5;
hence x1=x2 by ZFMISC_1:33;
end;
hence thesis by FUNCT_1:def 8;
end;
A6:h.:Y=[:{x},Y:]
proof
for y holds y in [:{x},Y:] iff y in h.:(Y)
proof
let y;
thus y in [:{x},Y:] implies y in h.:(Y)
proof
assume A7:y in [:{x},Y:];
then consider y1,x1 such that A8:y=[y1,x1] by ZFMISC_1:102;
A9:Y c= J by FINSUB_1:def 5;
A10: y1 in {x} & x1 in Y by A7,A8,ZFMISC_1:106;
then h.x1=[x,x1] by A3,A9
.=y by A8,A10,TARSKI:def 1;
hence thesis by A3,A9,A10,FUNCT_1:def 12;
end;
assume y in h.:(Y);
then consider z such that A11:z in dom h & z in
Y & y = h.z by FUNCT_1:def 12;
y=[x,z] by A3,A11;
hence thesis by A11,ZFMISC_1:128;
end;
hence thesis by TARSKI:2;
end;
A12:dom ((curry f).x) = J & dom (f *h)=J & rng h c= [:I,J:]
proof
A13:dom f=[:I,J:] by FUNCT_2:def 1;
then consider g being Function such that A14:g=(curry f).x & dom g= J
& rng g c= rng f & for y st y in J holds g.y = f.[x,y]
by FUNCT_5:36;
thus dom ((curry f).x)=J by A14;
now let y;
assume y in rng h;
then consider z such that A15:z in dom h & y = h.z by FUNCT_1:def 5;
y=[x,z] by A3,A15;
hence y in dom f by A3,A13,A15,ZFMISC_1:106;
end;
then rng h c= dom f by TARSKI:def 3;
hence dom (f*h)=J & rng h c= [:I,J:] by A3,FUNCT_2:def 1,RELAT_1:46;
end;
A16: for y st y in J holds ((curry f).x).y=(f*h).y
proof
let y;
assume A17:y in J;
dom f=[:I,J:] by FUNCT_2:def 1;
then consider g being Function such that A18:g=(curry f).x & dom g= J
& rng g c= rng f & for y st y in J holds g.y = f.[x,y]
by FUNCT_5:36;
thus (f*h).y=f.(h.y) by A12,A17,FUNCT_1:22
.= f.[x,y] by A3,A17
.=((curry f).x).y by A17,A18;
end;
reconsider h as Function of J,[:I,J:] by A3,A12,FUNCT_2:4;
thus F$$([:{x},Y:],f)=F$$(Y,f*h) by A1,A4,A6,SETWOP_2:8
.=F $$ (Y,(curry f).x) by A12,A16,FUNCT_1:9
.=g.x by A2
.=F$$({x},g) by A1,SETWISEO:26;
end;
hence thesis;
end;
theorem
Th32:
for I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for X being Element of Fin I for Y being Element of Fin J st
(for i being Element of I holds g.i=F$$(Y,(curry f).i))&
F has_a_unity & F is commutative & F is associative &
F has_an_inverseOp holds
F$$([:X,Y:],f)=F$$(X,g)
proof
let I, J be non empty set;
let F be BinOp of D;
let f be Function of [:I,J:],D;
let g be Function of I,D;
let X be Element of Fin I; let Y be Element of Fin J;
assume A1:(for i being Element of I holds g.i=F$$(Y,(curry f).i))&
F has_a_unity & F is commutative & F is associative &
F has_an_inverseOp;
defpred P[Element of Fin I] means F$$([:$1,Y:],f)=F$$($1,g);
A2: P[{}.I]
proof
reconsider T={}.[:I,J:] as Element of Fin [:I,J:];
T=[:{}.I,Y:] by ZFMISC_1:113;
then F $$([:{}.I,Y:],f)= the_unity_wrt F by A1,SETWISEO:40;
hence thesis by A1,SETWISEO:40;
end;
A3:for X1 being Element of Fin I,x being Element of I holds
P[X1] implies P[X1 \/ {x}]
proof
let X1 be Element of Fin I,x be Element of I;
assume A4: F$$([:X1,Y:],f)=F$$(X1,g);
reconsider s={x} as Element of Fin I;
now per cases;
case x in X1;
then X1 \/ {x} = X1 by ZFMISC_1:46;
hence F$$([:X1 \/ {x},Y:],f)=F$$(X1 \/ {x},g) by A4;
case not x in X1;
then A5:X1 misses {x} by ZFMISC_1:56;
then A6:[:X1,Y:] misses [:s,Y:] by ZFMISC_1:127;
thus F$$([:X1 \/ {x},Y:],f)
=F$$([:X1,Y:] \/ [:s,Y:],f)by ZFMISC_1:120
.=F.(F $$([:X1,Y:],f),F $$([:s,Y:],f)) by A1,A6,SETWOP_2:6
.=F.(F$$(X1,g),F$$(s,g)) by A1,A4,Th31
.=F$$(X1 \/ {x},g) by A1,A5,SETWOP_2:6;
end;
hence thesis;
end;
for X1 being Element of Fin I holds P[X1] from FinSubInd3(A2,A3);
hence thesis;
end;
theorem
Th33: for I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I st
F has_a_unity & F is commutative & F is associative &
F has_an_inverseOp holds
for y being Element of J holds
(for j being Element of J holds g.j=F$$(X,(curry' f).j)) implies
F$$([:X,{y}:],f)=F$$({y},g)
proof
let I, J be non empty set;
let F be BinOp of D;
let f be Function of [:I,J:],D;
let g be Function of J,D;
let X be Element of Fin I;
assume A1:F has_a_unity & F is commutative & F is associative &
F has_an_inverseOp;
now let y be Element of J;
assume A2:(for j being Element of J holds g.j=F$$(X,(curry' f).j));
deffunc F(set) = [$1,y];
consider h being Function such that A3:dom h = I & for x st x in I holds
h.x = F(x) from Lambda;
A4:h is one-to-one
proof
now let x1,x2;
assume A5:x1 in dom h & x2 in dom h & h.x1=h.x2;
then [x1,y]=h.x2 by A3
.=[x2,y] by A3,A5;
hence x1=x2 by ZFMISC_1:33;
end;
hence thesis by FUNCT_1:def 8;
end;
A6:h.:X=[:X,{y}:]
proof
for x holds x in [:X,{y}:] iff x in h.:(X)
proof
let x;
thus x in [:X,{y}:] implies x in h.:(X)
proof
assume A7:x in [:X,{y}:];
then consider x1,y1 such that A8:x=[x1,y1] by ZFMISC_1:102;
A9:X c= I by FINSUB_1:def 5;
A10: x1 in X & y1 in {y} by A7,A8,ZFMISC_1:106;
then h.x1=[x1,y] by A3,A9
.=x by A8,A10,TARSKI:def 1;
hence thesis by A3,A9,A10,FUNCT_1:def 12;
end;
assume x in h.:(X);
then consider z such that A11:z in dom h & z in
X & x = h.z by FUNCT_1:def 12;
x=[z,y] by A3,A11;
hence thesis by A11,ZFMISC_1:129;
end;
hence thesis by TARSKI:2;
end;
A12:dom ((curry' f).y) =I & dom (f *h)=I & rng h c= [:I,J:]
proof
A13:dom f=[:I,J:] by FUNCT_2:def 1;
then consider g being Function such that A14:g=(curry' f).y & dom g= I
& rng g c= rng f & for x st x in I holds g.x = f.[x,y]
by FUNCT_5:39;
thus dom ((curry' f).y)=I by A14;
now let x;
assume x in rng h;
then consider z such that A15:z in dom h & x = h.z by FUNCT_1:def 5;
x=[z,y] by A3,A15;
hence x in dom f by A3,A13,A15,ZFMISC_1:106;
end;
then rng h c= dom f by TARSKI:def 3;
hence dom (f*h)=I & rng h c= [:I,J:] by A3,FUNCT_2:def 1,RELAT_1:46;
end;
A16: for x st x in I holds ((curry' f).y).x=(f*h).x
proof
let x;
assume A17:x in I;
dom f=[:I,J:] by FUNCT_2:def 1;
then consider g being Function such that A18:g=(curry' f).y & dom g= I
& rng g c= rng f & for x st x in I holds g.x = f.[x,y]
by FUNCT_5:39;
thus (f*h).x=f.(h.x) by A12,A17,FUNCT_1:22
.= f.[x,y] by A3,A17
.=((curry' f).y).x by A17,A18;
end;
reconsider h as Function of I,[:I,J:] by A3,A12,FUNCT_2:4;
thus F$$([:X,{y}:],f)=F$$(X,f*h) by A1,A4,A6,SETWOP_2:8
.=F $$ (X,(curry' f).y) by A12,A16,FUNCT_1:9
.=g.y by A2
.=F$$({y},g) by A1,SETWISEO:26;
end;
hence thesis;
end;
theorem
Th34:
for I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I for Y being Element of Fin J st
(for j being Element of J holds g.j=F$$ (X , (curry' f).j) )&
F has_a_unity & F is commutative & F is associative &
F has_an_inverseOp holds
F$$([:X,Y:],f)=F$$(Y,g)
proof
let I, J be non empty set;
let F be BinOp of D;
let f be Function of [:I,J:],D;
let g be Function of J,D;
let X be Element of Fin I;
let Y be Element of Fin J;
assume A1:(for j being Element of J holds g.j=F$$(X,(curry' f).j)) &
F has_a_unity & F is commutative & F is associative &
F has_an_inverseOp;
defpred P[Element of Fin J] means F$$([:X,$1:],f)=F$$($1,g) ;
A2: P[{}.J]
proof
reconsider T={}.[:I,J:] as Element of Fin [:I,J:];
T=[:X,{}.J:] by ZFMISC_1:113;
then F $$([:X,{}.J:],f)= the_unity_wrt F by A1,SETWISEO:40;
hence thesis by A1,SETWISEO:40;
end;
A3:for Y1 being Element of Fin J,y being Element of J holds
P[Y1] implies P[Y1 \/ {y}]
proof
let Y1 be Element of Fin J,y be Element of J;
assume A4: F$$([:X,Y1:],f)=F$$(Y1,g);
reconsider s={y} as Element of Fin J;
now per cases;
case y in Y1;
then Y1 \/ {y} = Y1 by ZFMISC_1:46;
hence F$$([:X,Y1 \/ {y}:],f)=F$$(Y1 \/ {y},g) by A4;
case not y in Y1;
then A5:Y1 misses {y} by ZFMISC_1:56;
then A6:[:X,Y1:] misses [:X,s:] by ZFMISC_1:127;
thus F$$([:X,Y1 \/ {y}:],f)
=F$$([:X,Y1:] \/ [:X,s:],f)by ZFMISC_1:120
.=F.(F $$([:X,Y1:],f),F $$([:X,s:],f)) by A1,A6,SETWOP_2:6
.=F.(F$$(Y1,g),F$$(s,g)) by A1,A4,Th33
.=F$$(Y1 \/ {y},g) by A1,A5,SETWOP_2:6;
end;
hence thesis;
end;
for Y1 being Element of Fin J holds P[Y1] from FinSubInd3(A2,A3);
hence thesis;
end;
theorem
for A,B,C being Matrix of K st
width A=len B & width B=len C
holds (A*B)*C=A*(B*C)
proof
let A,B,C be Matrix of K;
assume A1:width A=len B & width B=len C;
A2: Seg len A = dom A & Seg len B = dom B & Seg len C = dom C
by FINSEQ_1:def 3;
0.K is_a_unity_wrt (the add of K) by FVSUM_1:8;
then A3:the add of K is commutative & the add of K is associative &
the add of K has_a_unity & the add of K has_an_inverseOp
by FVSUM_1:2,3,17,SETWISEO:def 2;
A4:len (A*B)=len A & width (A*B)=len C by A1,Def4;
A5:len (B*C)=width A & width (B*C)=width C by A1,Def4;
then A6:len (A*(B*C))=len A & width (A*(B*C))=width C by Def4;
A7:len ((A*B)*C)=len A & width ((A*B)*C)=width C by A4,Def4;
then A8: dom((A*B)*C)=dom A by FINSEQ_3:31;
then A9:Indices((A*B)*C)=[:dom A,Seg width C:] by A7,MATRIX_1:def 5;
dom(A*B)=dom A by A4,FINSEQ_3:31;
then A10:Indices (A*B)=[:dom A,Seg width B:] by A1,A4,MATRIX_1:def 5;
dom(B*C)=dom B by A1,A5,FINSEQ_3:31;
then A11:Indices (B*C)=[:dom B,Seg width C:] by A5,MATRIX_1:def 5;
dom(A*(B*C))=dom A by A6,FINSEQ_3:31;
then A12:Indices (A*(B*C))=[:dom A,Seg width C:] by A6,MATRIX_1:def 5;
A13:Indices ((A*B)*C)=[:dom A,Seg width C:] by A7,A8,MATRIX_1:def 5;
now let i,j;
assume A14: [i,j] in Indices ((A*B)*C);
then A15:i in dom A & j in Seg width C by A9,ZFMISC_1:106;
len (Line((A*B),i))=width (A*B) by MATRIX_1:def 8
.=len C by A1,Def4
.=len (Col(C,j)) by MATRIX_1:def 9;
then A16:len ((the mult of K).:(Line((A*B),i),Col(C,j)))=len (Col(C,j))
by FINSEQ_2:86
.=len C by MATRIX_1:def 9;
A17:len ((the mult of K).:(Line((A*B),i),Col(C,j)))=
len (mlt(Line((A*B),i),Col(C,j))) by FVSUM_1:def 7;
reconsider X=dom C as Element of Fin NAT;
reconsider Y=dom B as Element of Fin NAT;
deffunc F(Element of NAT ,Element of NAT) =
(A* (i,$2))*(B* ($2,$1))*(C* ($1,j));
consider f being Function of [:NAT,NAT:],(the carrier of K)
such that
A18:for k1 being Element of NAT for k2 being Element of NAT
holds f.[k1,k2] = F(k1,k2) from Lambda2D;
deffunc F( Element of NAT) = (the add of K)$$(Y,(curry f).$1);
consider g being Function of NAT,(the carrier of K)
such that
A19: for k being Element of NAT holds g.k = F(k) from LambdaD;
deffunc F'( Element of NAT) = (the add of K)$$(X,(curry' f).$1);
consider h being Function of NAT,(the carrier of K) such that
A20: for k being Element of NAT holds h.k = F'(k) from LambdaD;
A21:0.K = the_unity_wrt (the add of K) by FVSUM_1:9;
dom mlt(Line(A*B,i),Col(C,j)) = dom C by A16,A17,FINSEQ_3:31;
then A22:[#](mlt(Line(A*B,i),Col(C,j)),0.K)| dom C=mlt(Line(A*B,i),Col(C,j))
by SETWOP_2:23;
A23:dom B c=NAT
proof
now let x;
assume x in dom B;
then x is Nat by SETWISEO:14;
hence x in NAT;
end;
hence thesis by TARSKI:def 3;
end;
A24:for k
st k in NAT holds
((curry f).k)|dom B =(C*(k,j)) * mlt(Line(A,i),Col(B,k))
proof
let k;
assume k in NAT;
A25:{k} c=NAT & NAT c= NAT by ZFMISC_1:37;
A26:[:NAT,NAT:] <>{} &
dom f=[:NAT,NAT:] by FUNCT_2:def 1;
A27:dom curry f = NAT by FUNCT_2:def 1;
then A28:dom((curry f).k)=proj2 ( [:NAT,NAT:]/\
[:{k},proj2 [:NAT,NAT:]:])by A26,FUNCT_5:38
.= proj2([:{k},NAT:]/\[:NAT,NAT:] ) by FUNCT_5:11
.= proj2 [:{k},NAT:] by A25,ZFMISC_1:124
.= NAT by FUNCT_5:11;
A29:len (Line(A,i))= len B by A1,MATRIX_1:def 8
.= len (Col(B,k)) by MATRIX_1:def 9;
A30: len mlt(Line(A,i),Col(B,k))=
len ((the mult of K).:
(Line(A,i),Col(B,k))) by FVSUM_1:def 7;
A31: len ((the mult of K).:(Line(A,i),Col(B,k)))
=len (Line(A,i)) by A29,FINSEQ_2:86
.= len B by A1,MATRIX_1:def 8;
A32:dom ((the mult of K).:(Line(A,i),Col(B,k)))=
Seg len ((the mult of K).:(Line(A,i),Col(B,k))) by FINSEQ_1:def 3;
reconsider a=C*(k,j) as Element of K;
A33: dom(((curry f).k)|dom B)=NAT /\ dom B by A28,RELAT_1:90
.=dom B by A23,XBOOLE_1:28;
reconsider p=mlt(Line(A,i),Col(B,k)) as FinSequence of the carrier of K;
A34:(a*p)=(a multfield)* p by FVSUM_1:def 6;
rng p c=dom (a multfield)
proof
dom (a multfield)=the carrier of K by FUNCT_2:def 1;
hence thesis by FINSEQ_1:def 4;
end;
then A35: dom (a*p) = dom p by A34,RELAT_1:46;
then A36: dom (C*(k,j)*mlt(Line(A,i),Col(B,k)))=dom B by A30,A31,
FINSEQ_3:31;
now let l be set;
assume A37:l in dom B;
then reconsider l'=l as Nat by SETWISEO:14;
l' in dom p by A30,A31,A37,FINSEQ_3:31;
then reconsider b=p.l' as Element of K
by FINSEQ_2:13;
A38: l' in dom( (the mult of K) .: (Line(A,i),Col(B,k)) )
by A31,A32,A37,FINSEQ_1:def 3;
A39: l in dom(a*p) by A30,A31,A35,A37,FINSEQ_3:31;
thus (((curry f).k)|dom B).l=((curry f).k).l' by A37,FUNCT_1:72
.= f.[k,l'] by A27,A28,FUNCT_5:38
.=(A* (i,l'))*(B* (l',k))*(C* (k,j)) by A18
.=(the mult of K).( (A* (i,l'))*(B* (l',k)),(C* (k,j)))
by VECTSP_1:def 10
.=(the mult of K).
((the mult of K).((A*(i,l')),(B*(l',k))),(C*(k,j)))
by VECTSP_1:def 10
.=(the mult of K).
((the mult of K).((Line(A,i).l'),(B*(l',k))),(C*(k,j)))
by A1,A2,A37,MATRIX_1:def 8
.=(the mult of K).
((the mult of K).((Line(A,i).l'),(Col(B,k).l')),(C*(k,j)))
by A37,MATRIX_1:def 9
.=(the mult of K).
(( (the mult of K) .: (Line(A,i),Col(B,k)) ).l',(C*(k,j)))
by A38,FUNCOP_1:28
.=(the mult of K). ( (mlt(Line(A,i),Col(B,k))).l',(C*(k,j)))
by FVSUM_1:def 7
.=a*b by VECTSP_1:def 10
.=(C*(k,j) * mlt(Line(A,i),Col(B,k))).l
by A39,FVSUM_1:62;
end;
hence thesis by A33,A36,FUNCT_1:9;
end;
A40:dom C c=NAT
proof
now let x;
assume x in dom C;
then x is Nat by SETWISEO:14;
hence x in NAT;
end;
hence thesis by TARSKI:def 3;
end;
A41:g|dom C=mlt(Line(A*B,i),Col(C,j))
proof
A42:dom (g|dom C)=dom g /\ dom C by RELAT_1:90
.= NAT /\ dom C by FUNCT_2:def 1
.=dom C by A40,XBOOLE_1:28;
A43:dom mlt(Line(A*B,i),Col(C,j))=dom C by A16,A17,FINSEQ_3:31;
now let k' be set;
assume A44:k' in dom C;
then reconsider k=k' as Nat by SETWISEO:14;
A45:k in dom ((the mult of K).:(Line(A*B,i),Col(C,j))) by A16,A44,FINSEQ_3
:31;
len (Line(A,i))= len B by A1,MATRIX_1:def 8
.= len (Col(B,k)) by MATRIX_1:def 9;
then A46: len ((the mult of K).:(Line(A,i),Col(B,k)))
=len (Line(A,i)) by FINSEQ_2:86
.= len B by A1,MATRIX_1:def 8;
reconsider a=C*(k,j) as Element of K;
reconsider p=mlt(Line(A,i),Col(B,k)) as FinSequence of the carrier of K;
A47: len B = len p by A46,FVSUM_1:def 7;
A48:(a*p)=(a multfield)* p by FVSUM_1:def 6;
rng p c=dom (a multfield)
proof
dom (a multfield)=the carrier of K by FUNCT_2:def 1;
hence thesis by FINSEQ_1:def 4;
end;
then dom (a*p)=dom p by A48,RELAT_1:46;
then A49: dom (C*(k,j)*mlt(Line(A,i),Col(B,k)))=dom B by A47,FINSEQ_3:
31;
then [#](C*(k,j)*mlt(Line(A,i),Col(B,k)),0.K)| dom B
=C*(k,j)*mlt(Line(A,i),Col(B,k)) by SETWOP_2:23;
then A50:[#](C*(k,j)*mlt(Line(A,i),Col(B,k)),0.K)| dom B=
((curry f).k)| dom B by A24;
A51:(the add of K) is commutative & (the add of K ) is associative
& (the add of K) has_a_unity by FVSUM_1:2,3,10;
k in Seg width B by A1,A44,FINSEQ_1:def 3;
then A52:[i,k] in Indices (A*B) by A10,A15,ZFMISC_1:106;
A53: k in Seg width (A*B) by A4,A44,FINSEQ_1:def 3;
thus (g|dom C).k'=g.k by A42,A44,FUNCT_1:70
.=(the add of K)$$(Y,(curry f).k) by A19
.=(the add of K)$$(Y,[#](C*(k,j)*mlt(Line(A,i),Col(B,k)),0.K))
by A50,A51,SETWOP_2:9
.=(the add of K)$$ (a*p) by A3,A21,A49,SETWOP_2:def 2
.=Sum(a*p) by FVSUM_1:def 8
.= C*(k,j)*(Sum(mlt(Line(A,i),Col(B,k)))) by FVSUM_1:92
.= C*(k,j) *( Line(A,i) "*" Col(B,k)) by FVSUM_1:def 10
.=((A*B)*(i,k))*(C*(k,j)) by A1,A52,Def4
.=(the mult of K).((A*B)*(i,k),C*(k,j)) by VECTSP_1:def 10
.= (the mult of K).(Line(A*B,i).k,C*(k,j)) by A53,MATRIX_1:def 8
.= (the mult of K).(Line(A*B,i).k,Col(C,j).k) by A44,MATRIX_1:def 9
.= ((the mult of K).:(Line(A*B,i),Col(C,j))).k by A45,FUNCOP_1:28
.=(mlt(Line(A*B,i),Col(C,j))).k' by FVSUM_1:def 7;
end;
hence thesis by A42,A43,FUNCT_1:9;
end;
len (Col((B*C),j))=len (B*C) by MATRIX_1:def 9
.=width A by A1,Def4
.=len (Line(A,i)) by MATRIX_1:def 8;
then A54:len ((the mult of K).:(Line(A,i),Col(B*C,j)))=len (Line(A,i))
by FINSEQ_2:86
.=width A by MATRIX_1:def 8;
A55:len ((the mult of K).:(Line(A,i),Col(B*C,j)))=
len (mlt(Line(A,i),Col(B*C,j))) by FVSUM_1:def 7;
then dom mlt(Line(A,i),Col(B*C,j)) = dom B by A1,A54,FINSEQ_3:31;
then A56:[#](mlt(Line(A,i),Col(B*C,j)),0.K)| dom B=mlt(Line(A,i),Col(B*C,j))
by SETWOP_2:23;
A57:h|dom B=mlt(Line(A,i),Col(B*C,j))
proof
A58:dom B c=NAT
proof
now let x;
assume x in dom B;
then x is Nat by SETWISEO:14;
hence x in NAT;
end;
hence thesis by TARSKI:def 3;
end;
A59:dom (h|dom B)=dom h /\ dom B by RELAT_1:90
.= NAT /\ dom B by FUNCT_2:def 1
.=dom B by A58,XBOOLE_1:28;
A60:dom mlt(Line(A,i),Col(B*C,j))=dom B by A1,A54,A55,FINSEQ_3:31;
now let k' be set;
assume A61:k' in dom B;
then reconsider k=k' as Nat by SETWISEO:14;
A62:k in dom ((the mult of K).:
(Line(A,i),Col(B*C,j)))by A1,A54,A61,FINSEQ_3:31;
A63:len (Line(B,k))= len C by A1,MATRIX_1:def 8
.= len (Col(C,j)) by MATRIX_1:def 9;
A64:len mlt(Line(B,k),Col(C,j))=
len ((the mult of K).:(Line(B,k),Col(C,j))) by FVSUM_1:def 7;
A65: len ((the mult of K).:(Line(B,k),Col(C,j)))
=len (Line(B,k)) by A63,FINSEQ_2:86
.= len C by A1,MATRIX_1:def 8;
[:NAT,NAT:] <>{} &
dom f=[:NAT,NAT:] by FUNCT_2:def 1;
then consider G being Function such that A66:G= (curry' f).k &
dom G = NAT& rng G c= rng f &
for x st x in NAT holds G.x = f.[x,k] by FUNCT_5:39;
A67: dom(((curry' f).k)|dom C)=NAT /\ dom C by A66,RELAT_1:90
.=dom C by A40,XBOOLE_1:28;
reconsider a=A*(i,k) as Element of K;
reconsider p=mlt(Line(B,k),Col(C,j)) as FinSequence of the carrier of K;
A68:(a*p)=(a multfield)* p by FVSUM_1:def 6;
rng p c=dom (a multfield)
proof
dom (a multfield)=the carrier of K by FUNCT_2:def 1;
hence thesis by FINSEQ_1:def 4;
end;
then A69:dom (a*p)=dom p by A68,RELAT_1:46;
then A70: dom (A*(i,k)*mlt(Line(B,k),Col(C,j)))=dom C by A64,A65,FINSEQ_3:
31;
then A71:[#](A*(i,k)*mlt(Line(B,k),Col(C,j)),0.K)| dom C
=A*(i,k)*mlt(Line(B,k),Col(C,j)) by SETWOP_2:23;
A72:[#](A*(i,k)*mlt(Line(B,k),Col(C,j)),0.K)| dom C=
((curry' f).k)| dom C
proof
now let l be set;
assume A73:l in dom C;
then reconsider l'=l as Nat by SETWISEO:14;
l' in dom p by A64,A65,A73,FINSEQ_3:31;
then reconsider b=p.l' as Element of K
by FINSEQ_2:13;
A74: l' in Seg width B by A1,A73,FINSEQ_1:def 3;
A75: l' in dom ((the mult of K) .: (Line(B,k),Col(C,j)))
by A65,A73,FINSEQ_3:31;
A76: l in dom(a*p) by A64,A65,A69,A73,FINSEQ_3:31;
thus (((curry' f).k)|dom C).l=((curry' f).k).l'
by A73,FUNCT_1:72
.= f.[l',k] by A66
.=(A* (i,k))*(B* (k,l'))*(C* (l',j)) by A18
.=(A* (i,k))*((B* (k,l'))*(C* (l',j))) by VECTSP_1:def 16
.=(the mult of K).( (A* (i,k)),(B* (k,l'))*(C* (l',j)))
by VECTSP_1:def 10
.=(the mult of K).(A*(i,k),
(the mult of K).((B*(k,l')),(C*
(l',j)))) by VECTSP_1:def 10
.=(the mult of K).
(A*(i,k), (the mult of K).(( Line(B,k) ).l', ( C*(l',j))))
by A74,MATRIX_1:def 8
.=(the mult of K).
(A*(i,k),(the mult of K).((Line(B,k).l'),(Col(C,j)).l'))
by A73,MATRIX_1:def 9
.=(the mult of K).
(A*(i,k),( (the mult of K) .: (Line(B,k),Col(C,j))).l')
by A75,FUNCOP_1:28
.=(the mult of K).(A*(i,k), (mlt(Line(B,k),Col(C,j))).l')
by FVSUM_1:def 7
.=a*b by VECTSP_1:def 10
.=(A*(i,k)*mlt(Line(B,k),Col(C,j))).l
by A76,FVSUM_1:62;
end;
hence thesis by A67,A70,A71,FUNCT_1:9;
end;
A77:(the add of K) is commutative & (the add of K ) is associative
& (the add of K) has_a_unity by FVSUM_1:2,3,10;
A78:[k,j] in Indices (B*C) by A11,A15,A61,ZFMISC_1:106;
A79: k in Seg width A by A1,A61,FINSEQ_1:def 3;
A80: k in dom(B*C) by A1,A5,A61,FINSEQ_3:31;
thus (h|dom B).k'=h.k by A59,A61,FUNCT_1:70
.=(the add of K)$$(X,(curry' f).k) by A20
.=(the add of K)$$(X,[#](A*(i,k)*mlt(Line(B,k),Col(C,j)),0.K))
by A72,A77,SETWOP_2:9
.=(the add of K)$$ (a*p) by A3,A21,A70,SETWOP_2:def 2
.=Sum(a*p) by FVSUM_1:def 8
.= A*(i,k)*(Sum(mlt(Line(B,k),Col(C,j)))) by FVSUM_1:92
.= A*(i,k) *( Line(B,k) "*" Col(C,j)) by FVSUM_1:def 10
.= A*(i,k)*((B*C)*(k,j)) by A1,A78,Def4
.=(the mult of K).(A*(i,k),(B*C)*(k,j)) by VECTSP_1:def 10
.= (the mult of K).(Line(A,i).k,(B*C)*(k,j)) by A79,MATRIX_1:def 8
.= (the mult of K).(Line(A,i).k,Col(B*C,j).k)
by A80,MATRIX_1:def 9
.= ((the mult of K).:(Line(A,i),Col(B*C,j))).k by A62,FUNCOP_1:28
.=(mlt(Line(A,i),Col(B*C,j))).k' by FVSUM_1:def 7;
end;
hence thesis by A59,A60,FUNCT_1:9;
end;
A81: dom C = dom mlt(Line(A*B,i),Col(C,j)) by A16,A17,FINSEQ_3:31;
A82: dom (mlt(Line(A,i),Col(B*C,j))) = Y by A1,A54,A55,FINSEQ_3:31;
thus ((A*B)*C)*(i,j)=Line(A*B,i) "*" Col(C,j) by A4,A14,Def4
.=Sum(mlt(Line(A*B,i),Col(C,j))) by FVSUM_1:def 10
.=(the add of K) $$(mlt(Line(A*B,i),Col(C,j)))by FVSUM_1:def 8
.=(the add of K) $$(dom C,
[#](mlt(Line(A*B,i),Col(C,j)),0.K))
by A3,A21,A81,SETWOP_2:def 2
.=(the add of K)$$(X,g) by A3,A22,A41,SETWOP_2:9
.=(the add of K)$$([:X,Y:],f) by A3,A19,Th32
.=(the add of K)$$(Y,h) by A3,A20,Th34
.=(the add of K)$$(dom (mlt(Line(A,i),Col(B*C,j))),
[#](mlt(Line(A,i),Col(B*C,j)),the_unity_wrt(the add of K)))
by A3,A21,A56,A57,A82,SETWOP_2:9
.=(the add of K)$$(mlt(Line(A,i),Col(B*C,j)))
by A3,SETWOP_2:def 2
.=Sum(mlt(Line(A,i),Col(B*C,j))) by FVSUM_1:def 8
.=Line(A,i) "*" Col(B*C,j) by FVSUM_1:def 10
.=(A*(B*C))*(i,j) by A5,A12,A13,A14,Def4;
end;
hence thesis by A6,A7,MATRIX_1:21;
end;
begin :: Determinant
definition let n,K;let M be Matrix of n,K;
let p be Element of Permutations(n);
func Path_matrix(p,M) -> FinSequence of the carrier of K means
:Def7: len it=n & for i,j st i in dom it & j=p.i holds it.i=M*(i,j);
existence
proof
defpred P[Nat,set] means
for j st j=p.$1 holds $2 = M*($1,j);
A1:for k st k in Seg n ex x being Element of K st
P[k,x]
proof
let k;
assume A2:k in Seg n;
reconsider p as Function of Seg n,Seg n by MATRIX_2:def 11;
p.k in Seg n by A2,FUNCT_2:7;
then reconsider j=p.k as Nat by SETWISEO:14;
reconsider x=M*(k,j)as Element of K;
take x;
thus thesis;
end;
consider t being FinSequence of the carrier of K such that
A3: dom t = Seg n and
A4:for k st k in Seg n holds P[k,t.k] from SeqDEx(A1);
take t;
thus len t= n by A3,FINSEQ_1:def 3;
thus thesis by A3,A4;
end;
uniqueness
proof
for p1,p2 being FinSequence of the carrier of K st
(len p1=n & for i,j st i in dom p1 & j=p.i holds p1.i=M*(i,j)) &
(len p2=n & for i,j st i in dom p2 & j=p.i holds p2.i= M*(i,j))
holds p1=p2
proof
let p1,p2 be FinSequence of the carrier of K;
assume that A5:len p1=n and
A6:for i,j st i in dom p1 & j=p.i holds p1.i=M*(i,j)
and A7:len p2=n and
A8:for i,j st i in dom p2 & j=p.i holds p2.i= M*(i,j);
A9:dom p1 = Seg n & dom p2= Seg n by A5,A7,FINSEQ_1:def 3;
for i st i in Seg n holds p1.i = p2.i
proof
let i;
assume A10:i in Seg n;
reconsider p as Function of Seg n,Seg n by MATRIX_2:def 11;
p.i in Seg n by A10,FUNCT_2:7;
then reconsider j=p.i as Nat by SETWISEO:14;
p1.i=M*(i,j) by A6,A9,A10;
hence p1.i=p2.i by A8,A9,A10;
end;
hence thesis by A9,FINSEQ_1:17;
end;
hence thesis;
end;
end;
definition let n,K;let M be Matrix of n,K;
func Path_product(M) -> Function of Permutations(n),
the carrier of K means
:Def8: for p being Element of Permutations(n) holds
it.p = -((the mult of K) $$ Path_matrix(p,M),p);
existence
proof
deffunc V(Element of Permutations(n)) =
-((the mult of K) $$ Path_matrix($1,M),$1);
consider f being Function of Permutations(n),
the carrier of K such that
A1: for p being Element of Permutations(n) holds
f.p = V(p) from LambdaD;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f1,f2 be Function of Permutations(n), the carrier of K;
assume that
A2: for p being Element of Permutations(n) holds
f1.p = -((the mult of K) $$ Path_matrix(p,M),p) and
A3: for p being Element of Permutations(n) holds
f2.p = -((the mult of K) $$ Path_matrix(p,M),p);
now let p be Element of Permutations(n);
f1.p = -((the mult of K) $$ Path_matrix(p,M),p) by A2;
hence f1.p=f2.p by A3;
end;
hence thesis by FUNCT_2:113;
end;
end;
definition let n;let K;let M be Matrix of n,K;
func Det M -> Element of (the carrier of K) equals
:Def9:(the add of K) $$ (FinOmega(Permutations(n)),Path_product(M));
coherence;
end;
reserve a for Element of K;
theorem
Det <*<*a*>*> =a
proof
set M=<*<*a*>*>;
A1:idseq 1=id Seg 1 by FINSEQ_2:def 1;
A2:(Path_product(M)).(idseq 1)=a
proof
reconsider p = idseq 1 as Element of Permutations(1)
by A1,MATRIX_2:def 11;
A3:len Path_matrix(p,M) = 1 by Def7;
then A4:dom Path_matrix(p,M) = Seg 1 by FINSEQ_1:def 3;
then A5:1 in dom Path_matrix(p,M) by FINSEQ_1:4,TARSKI:def 1;
then 1=p.1 by A4,FINSEQ_2:56;
then Path_matrix(p,M).1=M*(1,1) by A5,Def7;
then Path_matrix(p,M).1=a by MATRIX_2:5;
then A6:Path_matrix(p,M)=<*a*> by A3,FINSEQ_1:57;
A7:(Path_product(M)).p = -((the mult of K) $$ Path_matrix(p,M),p)
by Def8;
A8:<*a*>=1|->a by FINSEQ_2:73;
-(a,p)=a
proof
reconsider q=(id Seg 1) as Element of Permutations(1)
by MATRIX_2:def 11;
len Permutations(1)=1 by MATRIX_2:20;
then q is even by MATRIX_2:29;
hence thesis by A1,MATRIX_2:def 16;
end;
hence thesis by A6,A7,A8,FINSOP_1:17;
end;
A9:FinOmega(Permutations(1))= {idseq 1} by MATRIX_2:21,def 17;
A10:idseq 1 in (Permutations(1)) by MATRIX_2:21,TARSKI:def 1;
A11:(the add of K) is commutative & (the add of K) is associative
by FVSUM_1:2,3;
Det M =(the add of K) $$ (FinOmega(Permutations(1)),Path_product(M))
by Def9
.=a by A2,A9,A10,A11,SETWISEO:26;
hence thesis;
end;
definition let n;let K; let M be Matrix of n,K;
func diagonal_of_Matrix(M) -> FinSequence of the carrier of K means
len it = n & for i st i in Seg n holds it.i=M*(i,i);
existence
proof
deffunc V(Nat) = M*($1,$1);
consider z being FinSequence of the carrier of K such that
A1:len z=n & for i st i in Seg n holds z.i=V(i) from SeqLambdaD;
take z;
thus thesis by A1;
end;
uniqueness
proof
let p1,p2 be FinSequence of the carrier of K;
assume that
A2: len p1 = n & for i st i in Seg n holds p1.i=M*(i,i) and
A3: len p2 = n & for i st i in Seg n holds p2.i=M*(i,i);
A4:dom p1 = Seg n & dom p2= Seg n by A2,A3,FINSEQ_1:def 3;
now let i;
assume A5: i in Seg n;
then p1.i=M*(i,i) by A2;
hence p1.i = p2.i by A3,A5;
end;
hence thesis by A4,FINSEQ_1:17;
end;
end;