:: The Product of Matrices of Elements of a Field and Determinants
:: by Katarzyna Zawadzka
::
:: Received May 17, 1993
:: Copyright (c) 1993-2021 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, XBOOLE_0, VECTSP_1, SUPINF_2, MATRIX_1, FINSEQ_2,
ARYTM_1, FINSEQ_1, TREES_1, RELAT_1, ZFMISC_1, XXREAL_0, CARD_1, ARYTM_3,
SUBSET_1, FUNCT_1, INCSP_1, FVSUM_1, RVSUM_1, ALGSTR_0, MESFUNC1,
RLVECT_1, CARD_3, ORDINAL4, TARSKI, STRUCT_0, QC_LANG1, FINSUB_1,
BINOP_1, SETWISEO, FUNCOP_1, PARTFUN1, FINSEQOP, FUNCT_5, FINSOP_1,
ABIAN, MATRIX_3, FUNCSDOM, FUNCT_7, FINSET_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1,
FINSET_1, BINOP_1, FINSEQ_4, STRUCT_0, ALGSTR_0, FUNCT_3, FUNCOP_1,
MATRIX_0, RLVECT_1, GROUP_1, VECTSP_1, SETWISEO, FINSOP_1, SETWOP_2,
FINSEQ_2, FINSEQOP, MATRIX_1, FINSUB_1, NAT_1, FVSUM_1, TREES_1, FUNCT_5;
constructors RELAT_2, PARTFUN1, SETWISEO, SQUARE_1, NAT_1, FINSEQOP, FINSOP_1,
SETWOP_2, FUNCT_5, ALGSTR_1, FVSUM_1, RELSET_1, FINSEQ_4, FUNCT_3,
BINOP_1, XTUPLE_0, MATRIX_0, MATRIX_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1,
FUNCT_2, FINSET_1, FINSUB_1, XXREAL_0, XREAL_0, NAT_1, STRUCT_0,
VECTSP_1, MATRIX_1, FVSUM_1, RELAT_1, CARD_1, FINSEQ_1, FINSEQ_2;
requirements NUMERALS, REAL, BOOLE, SUBSET;
equalities BINOP_1, FINSEQ_2, ALGSTR_0, MATRIX_0;
expansions BINOP_1;
theorems FINSEQ_1, FINSEQ_2, TARSKI, FUNCT_2, NAT_1, TREES_1, FUNCT_1,
SETWISEO, VECTSP_1, ZFMISC_1, FVSUM_1, SETWOP_2, MATRIX_1, FUNCT_3,
FINSEQOP, FUNCOP_1, FINSUB_1, FUNCT_5, FINSEQ_3, RLVECT_1, RELAT_1,
FINSOP_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, GROUP_1, ORDINAL1, XXREAL_0,
CARD_1, XTUPLE_0, SUBSET_1, MATRIX_0;
schemes FUNCT_2, FINSEQ_2, MATRIX_0, FINSEQ_1, FUNCT_3, SETWISEO, FUNCT_1,
BINOP_1;
begin
reserve x,y,z,x1,x2,y1,y2,z1,z2 for object,
i,j,k,l,n,m for Nat,
D for non empty set,
K for Ring;
definition
let K be Ring;
let n,m be Nat;
func 0.(K,n,m) -> Matrix of n,m,K equals
n |-> (m |-> 0.K);
coherence by MATRIX_0:10;
end;
definition
let K be Ring;
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
set n=len A;
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 MATRIX_0
:sch 1;
reconsider A1=A as Matrix of n,width A,K by MATRIX_0:51;
A2: Indices A1=[:Seg n,Seg width A:] by MATRIX_0:25;
A3: now
per cases;
case
n > 0;
hence len M=len A & width M=width A & Indices A = Indices M by A2,
MATRIX_0:23;
end;
case
A4: n =0;
then len M=0 by MATRIX_0:def 2;
then
A5: width M=0 by MATRIX_0:def 3;
width A=0 by A4,MATRIX_0:def 3;
hence len M=len A & width M=width A & Indices A = Indices M by A2,A5,
MATRIX_0:25;
end;
end;
reconsider M as Matrix of K;
take M;
thus thesis by A1,A3;
end;
uniqueness
proof
let M1,M2 be Matrix of K;
set n=len A;
assume that
A6: len M1= len A & width M1 =width A and
A7: for i,j st [i,j] in Indices A holds M1*(i,j) =-(A*(i,j)) and
A8: len M2= len A & width M2 =width A and
A9: for i,j st [i,j] in Indices A holds M2*(i,j) =-(A*(i,j));
reconsider M2 as Matrix of n,width A,K by A8,MATRIX_0:51;
reconsider M1 as Matrix of n,width A,K by A6,MATRIX_0:51;
reconsider A1=A as Matrix of n,width A,K by MATRIX_0:51;
A10: Indices A1=[:Seg n,Seg width A:] by MATRIX_0:25;
A11: Indices M1=[:Seg n,Seg width M1:] & Indices M2=[:Seg n,Seg width M2:]
by MATRIX_0:25;
A12: now
per cases;
case
A13: n > 0;
then Indices M1=[:Seg n,Seg width A:] by MATRIX_0:23;
hence Indices A = Indices M1 & Indices M1= Indices M2 by A10,A13,
MATRIX_0:23;
end;
case
A14: n =0;
then len M1=0 by MATRIX_0:def 2;
then
A15: width M1=0 by MATRIX_0:def 3;
len M2=0 by A14,MATRIX_0:def 2;
hence Indices A = Indices M1 & Indices M1= Indices M2 by A10,A11,A14
,A15,MATRIX_0:def 3;
end;
end;
now
let i,j;
assume
A16: [i,j] in Indices A;
then M1*(i,j) = -(A*(i,j)) by A7;
hence M1*(i,j)=M2*(i,j) by A9,A16;
end;
hence thesis by A12,MATRIX_0:27;
end;
end;
definition
let K be Ring;
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
set n=len A;
reconsider A1=A as Matrix of len A,width A,K by MATRIX_0:51;
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 MATRIX_0
:sch 1;
A2: Indices A1=[:Seg len A,Seg width A:] by MATRIX_0:25;
A3: now
per cases;
case
n > 0;
hence len M=len A & width M=width A & Indices A = Indices M by A2,
MATRIX_0:23;
end;
case
A4: n =0;
then len M=0 by MATRIX_0:def 2;
then
A5: width M=0 by MATRIX_0:def 3;
width A=0 by A4,MATRIX_0:def 3;
hence len M=len A & width M=width A & Indices A = Indices M by A2,A5,
MATRIX_0:25;
end;
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
A6: len M1 =len A & width M1=width A and
A7: for i,j st [i,j] in Indices A holds M1*(i,j)=A*(i,j) + B*(i,j) and
A8: len M2 =len A & width M2=width A and
A9: for i,j st [i,j] in Indices A holds M2*(i,j) = A*(i,j) + B*(i,j);
reconsider M2 as Matrix of n,width A,K by A8,MATRIX_0:51;
reconsider M1 as Matrix of n,width A,K by A6,MATRIX_0:51;
reconsider A1=A as Matrix of n,width A,K by MATRIX_0:51;
A10: Indices A1=[:Seg n,Seg width A:] by MATRIX_0:25;
A11: Indices M1=[:Seg n,Seg width M1:] & Indices M2=[:Seg n,Seg width M2:]
by MATRIX_0:25;
A12: now
per cases;
case
A13: n > 0;
then Indices M1=[:Seg n,Seg width A:] by MATRIX_0:23;
hence Indices A = Indices M1 & Indices M1= Indices M2 by A10,A13,
MATRIX_0:23;
end;
case
A14: n =0;
then len M1=0 by MATRIX_0:def 2;
then
A15: width M1=0 by MATRIX_0:def 3;
len M2=0 by A14,MATRIX_0:def 2;
hence Indices A = Indices M1 & Indices M1= Indices M2 by A10,A11,A14
,A15,MATRIX_0:def 3;
end;
end;
now
let i,j;
assume
A16: [i,j] in Indices A;
then M1*(i,j)=(A*(i,j) + B*(i,j)) by A7;
hence M1*(i,j)=M2*(i,j) by A9,A16;
end;
hence thesis by A12,MATRIX_0:27;
end;
end;
theorem Th1:
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_0:25;
per cases;
suppose
A3: n > 0;
reconsider m1=m as Element of NAT by ORDINAL1:def 12;
A4: [i,j] in [:Seg n,Seg m:] by A1,A3,MATRIX_0:23;
then j in Seg m by ZFMISC_1:87;
then
A5: (m1 |-> 0.K).j= 0.K by FUNCOP_1:7;
i in Seg n by A4,ZFMISC_1:87;
then (0.(K,n,m)).i= m |-> 0.K by FUNCOP_1:7;
hence thesis by A1,A5,MATRIX_0:def 5;
end;
suppose
n=0;
then Seg n = {};
hence thesis by A1,A2,ZFMISC_1:90;
end;
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 that
A1: len A= len B and
A2: width A=width B;
A3: width A=width (A+B) by Def3;
then
A4: width (A+B)=width (B+A) by A2,Def3;
A5: len A=len (A+B) by Def3;
then dom A = dom(A+B) by FINSEQ_3:29;
then
A6: Indices A = Indices (A + B) by A3;
dom A = dom B by A1,FINSEQ_3:29;
then
A7: Indices B=[:dom A,Seg width A:] by A2;
A8: now
let i,j;
assume
A9: [i,j] in Indices (A + B);
hence (A + B)*(i,j)=B*(i,j) + A*(i,j) by A6,Def3
.=( B + A)*(i,j) by A7,A6,A9,Def3;
end;
len (A+B)=len (B+A) by A1,A5,Def3;
hence thesis by A4,A8,MATRIX_0:21;
end;
theorem
for A,B,C being Matrix of K st len A=len B & width A=width B holds (A
+ B) + C= A + (B + C)
proof
let A,B,C be Matrix of K;
assume that
A1: len A=len B and
A2: width A=width B;
dom A = dom B by A1,FINSEQ_3:29;
then
A3: Indices B=[:dom A,Seg width A:] by A2;
A4: Indices A= [:dom A,Seg width A:];
A5: width ((A+B)+C)=width (A+B) by Def3;
A6: width (A+B)=width A by Def3;
A7: len (A+(B+C))=len A & width (A+(B+C))=width A by Def3;
A8: len (A+B)=len A by Def3;
A9: len ((A+B)+C)=len (A+B) by Def3;
then dom A = dom((A+B)+C) by A8,FINSEQ_3:29;
then
A10: Indices ((A+B)+C)=[:dom A,Seg width A:] by A6,A5;
dom A = dom(A+B) by A8,FINSEQ_3:29;
then
A11: Indices (A+B)=[:dom A,Seg width A:] by A6;
now
let i,j;
assume
A12: [i,j] in Indices ((A + B) + C);
hence ((A + B)+C)*(i,j)=(A+B)*(i,j) + C*(i,j) by A11,A10,Def3
.=(A*(i,j) + B*(i,j)) + C*(i,j) by A4,A10,A12,Def3
.=A*(i,j) + (B*(i,j) + C*(i,j)) by RLVECT_1:def 3
.=A*(i,j) + ( B + C)*(i,j) by A3,A10,A12,Def3
.=(A + (B + C))*(i,j) by A4,A10,A12,Def3;
end;
hence thesis by A8,A6,A9,A5,A7,MATRIX_0: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;
per cases;
suppose
A1: n > 0;
A2: width A= width (A+0.(K,n,m)) by Def3;
A3: Indices A=[:Seg n,Seg m:] by A1,MATRIX_0:23;
A4: len A= len (A+0.(K,n,m)) by Def3;
then dom A = dom(A+0.(K,n,m)) by FINSEQ_3:29;
then
A5: Indices A= Indices (A+0.(K,n,m)) by A2;
A6: Indices (0.(K,n,m))=[:Seg n,Seg m:] by A1,MATRIX_0:23;
now
let i,j;
assume
A7: [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 A5,Def3
.=A*(i,j) +0.K by A3,A6,A5,A7,Th1
.=A*(i,j) by RLVECT_1:4;
end;
hence thesis by A4,A2,MATRIX_0:21;
end;
suppose
A8: n=0;
A9: width A= width (A+0.(K,n,m)) by Def3;
A10: len A= len (A+0.(K,n,m)) by Def3;
then dom A= dom(A+0.(K,n,m)) by FINSEQ_3:29;
then Indices A= [:dom A,Seg width A:] & Indices (A+0.(K,n,m))=[:dom A,Seg
width A :] by A9;
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 A8,MATRIX_0:22;
hence thesis by A10,A9,MATRIX_0:21;
end;
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: width -A=width A by Def2;
A2: len (A+ -A)=len A by Def3;
A3: width (A+ -A)=width A by Def3;
A4: len -A=len A by Def2;
A5: now
per cases;
case
A6: n > 0;
then len (A+ -A)=n & width (A + -A) =m by A2,A3,MATRIX_0:23;
hence
len (0.(K,n,m))=len (A+ -A) & width (0.(K,n,m))=width (A+ -A) by A6,
MATRIX_0:23;
dom A = dom -A & dom A = dom(A + (-A)) by A4,A2,FINSEQ_3:29;
hence
Indices A= Indices (-A) & Indices A= Indices (A + (-A)) by A1,A3;
end;
case
A7: n=0;
then
A8: width A=0 by MATRIX_0:22;
then
A9: Seg width(-A) = Seg 0 by A1;
A10: len A=0 by A7,MATRIX_0:22;
then
A11: dom(-A) = Seg 0 by A4,FINSEQ_1:def 3;
A12: Indices (-A) = [:dom(-A),Seg width -A:] .= [:Seg 0,Seg width(-A):] by A11
.= [:Seg 0,Seg 0 qua set:] by A9;
dom(A+ -A) = Seg 0 by A2,A10,FINSEQ_1:def 3;
then
A13: Indices (A+ -A)=[:Seg 0,Seg 0 qua set:] by A3,A8;
len (0.(K,n,m))=0 & width (0.(K,n,m))=0 by A7,MATRIX_0:22;
hence len (0.(K,n,m))=len (A+ -A) & width (0.(K,n,m))=width (A+ -A) by
A10,A8,Def3;
Indices A= {} by A7,MATRIX_0:22;
hence Indices A= Indices (-A)& Indices A= Indices (A + (-A)) by A12,A13,
ZFMISC_1:90;
end;
end;
A14: Indices A= Indices 0.(K,n,m) by MATRIX_0:26;
now
let i,j;
assume
A15: [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 A15,Def2
.=0.K by RLVECT_1:5
.=(0.(K,n,m))*(i,j) by A14,A15,Th1;
end;
hence thesis by A5,MATRIX_0:21;
end;
definition
let K be Ring;
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 MATRIX_0
:sch 1;
take M;
now
per cases;
case
len A > 0;
hence len M=len A & width M= width B by MATRIX_0:23;
end;
case
A3: len A=0;
then len B=0 by A1,MATRIX_0:def 3;
then
A4: width B=0 by MATRIX_0:def 3;
len M=0 by A3,MATRIX_0:25;
hence len M=len A & width M= width B by A3,A4,MATRIX_0:def 3;
end;
end;
hence thesis by A2;
end;
uniqueness
proof
let M1,M2 be Matrix of K;
assume that
A5: len M1=len A and
A6: width M1=width B and
A7: for i,j st [i,j] in Indices M1 holds M1*(i,j)= Line(A,i) "*" Col( B, j) and
A8: len M2=len A and
A9: width M2=width B and
A10: for i,j st [i,j] in Indices M2 holds M2*(i,j)= Line(A,i) "*" Col( B, j);
dom M2 = dom M1 by A5,A8,FINSEQ_3:29;
then
A11: Indices M1=[:dom M1,Seg width M1:] & Indices M2=[:dom M1,Seg width M1
:] by A6,A9;
now
let i,j;
assume
A12: [i,j] in Indices M1;
then M1*(i,j)= Line(A,i) "*" Col(B,j) by A7;
hence M1*(i,j)=M2*(i,j) by A10,A11,A12;
end;
hence thesis by A5,A6,A8,A9,MATRIX_0:21;
end;
end;
definition
let n,k,m;
let K be Ring;
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_0:25;
then len (A*B)=len A & width (A*B)=width B by Def4;
hence thesis by MATRIX_0:51;
end;
end;
definition
let K be Ring;
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 MATRIX_0
:sch 1;
take N;
A2: len N=len M by MATRIX_0:def 2;
A3: now
per cases;
case
A4: len M= 0;
then width N=0 by A2,MATRIX_0:def 3;
hence width N=width M by A4,MATRIX_0:def 3;
end;
case
len M>0;
hence (width N)=width M by MATRIX_0:23;
end;
end;
dom M = dom N by A2,FINSEQ_3:29;
then Indices N=[:dom M,Seg width M:] by A3;
hence thesis by A1,A3,MATRIX_0:def 2;
end;
uniqueness
proof
let A,B be Matrix of K;
assume that
A5: len A=len M and
A6: width A =width M and
A7: for i,j st [i,j] in Indices M holds A*(i,j)=a*(M*(i,j)) and
A8: len B=len M & width B =width M and
A9: for i,j st [i,j] in Indices M holds B*(i,j)=a*(M*(i,j));
now
let i,j;
dom A = dom M by A5,FINSEQ_3:29;
then
A10: Indices A=[:dom M,Seg width M:] by A6;
assume
A11: [i,j] in Indices A;
hence A*(i,j)=a*(M*(i,j)) by A7,A10
.=B*(i,j) by A9,A11,A10;
end;
hence thesis by A5,A6,A8,MATRIX_0:21;
end;
end;
definition
let K be Ring;
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 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 K;
reconsider r=mlt(p,q) as FinSequence of K;
A1: r=(the multF of K).:(p,q) by FVSUM_1:def 7;
assume len p=len q;
hence thesis by A1,FINSEQ_2:72;
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 that
A1: [i,l] in Indices (1.(K,n)) and
A2: l=i;
l in Seg width (1.(K,n)) by A1,ZFMISC_1:87;
hence (Line(1.(K,n),i)).l=(1.(K,n))*(i,l) by MATRIX_0:def 7
.= 1.K by A1,A2,MATRIX_1:def 3;
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 that
A1: [i,l] in Indices (1.(K,n)) and
A2: l<>i;
l in Seg width (1.(K,n)) by A1,ZFMISC_1:87;
hence (Line(1.(K,n),i)).l=(1.(K,n))*(i,l) by MATRIX_0:def 7
.= 0.K by A1,A2,MATRIX_1:def 3;
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 that
A1: [l,j] in Indices (1.(K,n)) and
A2: l=j;
l in dom (1.(K,n)) by A1,ZFMISC_1:87;
hence (Col(1.(K,n),j)).l=(1.(K,n))*(l,j) by MATRIX_0:def 8
.= 1.K by A1,A2,MATRIX_1:def 3;
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 that
A1: [l,j] in Indices (1.(K,n)) and
A2: l<>j;
l in dom (1.(K,n)) by A1,ZFMISC_1:87;
hence (Col(1.(K,n),j)).l=(1.(K,n))*(l,j) by MATRIX_0:def 8
.= 0.K by A1,A2,MATRIX_1:def 3;
end;
Lm1: for L be add-associative right_zeroed right_complementable non empty
addLoopStr for p be FinSequence of L st for i be Element of 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
addLoopStr;
let p be FinSequence of L;
assume
A1: for k be Element of NAT st k in dom p holds p.k = 0.L;
defpred P[FinSequence of L] means (for k be Element of NAT st k in dom $1
holds $1.k = 0.L) implies Sum($1) = 0.L;
A2: for p being FinSequence of L, x being Element of L st P[p] holds P[p^<*x
*>]
proof
let p be FinSequence of L;
let x be Element of L;
assume
A3: ( for k be Element of NAT st k in dom p holds p.k = 0.L ) implies
Sum(p) = 0.L;
A4: len p + 1 in Seg (len p + 1) by FINSEQ_1:4;
assume
A5: for k be Element of NAT st k in dom(p^<*x*>) holds (p^<*x*>).k = 0.L;
A6: for k be Element of NAT st k in dom p holds p.k = 0.L
proof
A7: dom p c= dom(p^<*x*>) by FINSEQ_1:26;
let k be Element of NAT such that
A8: k in dom p;
thus p.k = (p^<*x*>).k by A8,FINSEQ_1:def 7
.= 0.L by A5,A8,A7;
end;
len(p^<*x*>) = len p + len<*x*> by FINSEQ_1:22
.= len p + 1 by FINSEQ_1:39;
then
A9: len p + 1 in dom(p^<*x*>) by A4,FINSEQ_1:def 3;
A10: x = (p^<*x*>).(len p + 1) by FINSEQ_1:42;
thus Sum(p^<*x*>) = Sum(p) + Sum(<*x*>) by RLVECT_1:41
.= Sum(p) + x by RLVECT_1:44
.= 0.L + 0.L by A3,A5,A6,A9,A10
.= 0.L by RLVECT_1:def 4;
end;
A11: P[<*>the carrier of L] by RLVECT_1:43;
for p be FinSequence of L holds P[p] from FINSEQ_2:sch 2(A11,A2);
hence thesis by A1;
end;
theorem Th11:
for n being Element of NAT
for K being add-associative right_zeroed right_complementable
non empty addLoopStr holds
Sum (n |-> 0.K) = 0.K
proof
let n be Element of NAT;
let K be add-associative right_zeroed right_complementable non empty
addLoopStr;
set p = n |-> 0.K;
for i be Element of NAT st i in dom p holds p.i = 0.K
proof
let i be Element of NAT;
assume i in dom p;
then i in Seg n by FUNCOP_1:13;
hence thesis by FUNCOP_1:7;
end;
hence thesis by Lm1;
end;
theorem Th12:
for K being add-associative right_zeroed right_complementable
non empty addLoopStr for p being FinSequence 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 be add-associative right_zeroed right_complementable non empty
addLoopStr;
let p be FinSequence of K;
let i;
assume that
A1: i in dom p and
A2: for k st k in dom p & k<>i holds p.k=0.K;
reconsider a=p.i as Element of K by A1,FINSEQ_2:11;
reconsider p1=p|Seg i as FinSequence of K by FINSEQ_1:18;
i<>0 by A1,FINSEQ_3:25;
then i in Seg i by FINSEQ_1:3;
then i in (dom p) /\ (Seg i) by A1,XBOOLE_0:def 4;
then
A3: i in dom p1 by RELAT_1:61;
then p1 <> {};
then len p1<>0;
then consider p3 being FinSequence of K, x being Element of K such that
A4: p1=p3^<*x*> by FINSEQ_2:19;
p1 is_a_prefix_of p by TREES_1:def 1;
then consider p2 being FinSequence such that
A5: p=p1^p2 by TREES_1:1;
reconsider p2 as FinSequence of K by A5,FINSEQ_1:36;
A6: dom p2 = Seg len p2 by FINSEQ_1:def 3;
A7: for k st k in Seg len p2 holds p2.k=0.K
proof
let k;
A8: i <=len p1 & len p1 <= len p1 + k by A3,FINSEQ_3:25,NAT_1:12;
assume k in Seg len p2;
then
A9: k in dom p2 by FINSEQ_1:def 3;
then 0<>k by FINSEQ_3:25;
then
A10: i<>len p1 + k by A8,XCMPLX_1:3,XXREAL_0:1;
thus p2.k=p.(len p1+k) by A5,A9,FINSEQ_1:def 7
.=0.K by A2,A5,A9,A10,FINSEQ_1:28;
end;
A11: now
let j be Nat;
assume
A12: j in dom p2;
hence p2.j =0.K by A7,A6
.= (len p2 |->0.K).j by A6,A12,FINSEQ_2:57;
end;
A13: dom p3 = Seg len p3 by FINSEQ_1:def 3;
i <= len p by A1,FINSEQ_3:25;
then
A14: i =len p1 by FINSEQ_1:17
.=len p3+ len <*x*> by A4,FINSEQ_1:22
.= len p3 + 1 by FINSEQ_1:39;
then
A15: x =p1.i by A4,FINSEQ_1:42
.=a by A5,A3,FINSEQ_1:def 7;
A16: for k st k in Seg len p3 holds p3.k=0.K
proof
let k;
assume
A17: k in Seg len p3;
then k <= len p3 by FINSEQ_1:1;
then
A18: i<> k by A14,NAT_1:13;
A19: k in dom p3 by A17,FINSEQ_1:def 3;
then
A20: k in dom p1 by A4,FINSEQ_2:15;
thus p3.k=p1.k by A4,A19,FINSEQ_1:def 7
.=p.k by A5,A20,FINSEQ_1:def 7
.=0.K by A2,A5,A18,A20,FINSEQ_2:15;
end;
A21: now
let j be Nat;
assume
A22: j in dom p3;
hence p3.j =0.K by A16,A13
.= (len p3 |->0.K).j by A13,A22,FINSEQ_2:57;
end;
len (len p3 |->0.K)=len p3 by CARD_1:def 7;
then
A23: p3=len p3 |->0.K by A21,FINSEQ_2:9;
len (len p2 |->0.K)=len p2 by CARD_1:def 7;
then p2=len p2 |->0.K by A11,FINSEQ_2:9;
then Sum p=Sum(p3^<*x*>) + Sum(len p2 |->0.K) by A5,A4,RLVECT_1:41
.=Sum(p3^<*x*>) + 0.K by Th11
.=Sum(p3^<*x*>) by RLVECT_1:4
.=Sum(len p3 |->0.K) + x by A23,FVSUM_1:71
.=0.K + a by A15,Th11
.=p.i by RLVECT_1:4;
hence thesis;
end;
theorem Th13:
for p,q being FinSequence of K holds len (mlt(p,q))=min(len p, len q)
proof
let p,q be FinSequence of K;
reconsider r=mlt(p,q) as FinSequence of K;
r=(the multF of K).:(p,q) by FVSUM_1:def 7;
hence thesis by FINSEQ_2:71;
end;
theorem Th14:
for K being Ring
for p,q being FinSequence of K for i st 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 K be Ring;
let p,q be FinSequence of K;
let i;
assume that
A1: 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 by FINSEQ_1:def 3;
reconsider j1=j as Element of NAT by ORDINAL1:def 12;
dom(mlt(p,q)) = Seg len (mlt(p,q)) & len (mlt(p,q))=min(len p,len q) by Th13,
FINSEQ_1:def 3;
then
A5: j in (dom p) /\ (dom q) by A3,A4,FINSEQ_2:2;
then
A6: j in dom q by XBOOLE_0:def 4;
then reconsider b=q.j1 as Element of K by FINSEQ_2:11;
thus i=j implies mlt(p,q).j=(q.i)
proof
reconsider b=q.j1 as Element of K by A6,FINSEQ_2:11;
assume
A7: i=j;
hence mlt(p,q).j=(1.K)*b by A1,A3,FVSUM_1:60
.=q.i by A7;
end;
assume
A8: i<>j;
j in dom p by A5,XBOOLE_0:def 4;
then p.j=0.K by A2,A8;
hence mlt(p,q).j=(0.K)*b by A3,FVSUM_1:60
.=0.K;
end;
theorem Th15:
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));
then j in Seg width B by ZFMISC_1:87;
then
A2: (Line(B,i)).j = B*(i,j) by MATRIX_0:def 7;
hence i=j implies (Line((1.(K,n)),i)).j=1.K by A1,MATRIX_1:def 3;
thus thesis by A1,A2,MATRIX_1:def 3;
end;
theorem Th16:
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));
then i in dom B by ZFMISC_1:87;
then
A2: (Col(B,j)).i = B*(i,j) by MATRIX_0:def 8;
hence i=j implies (Col((1.(K,n)),j)).i=1.K by A1,MATRIX_1:def 3;
thus thesis by A1,A2,MATRIX_1:def 3;
end;
theorem Th17:
for K being Ring
for p,q being FinSequence 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 K be Ring;
let p,q be FinSequence of K;
let i;
assume that
A1: i in dom p & i in dom q and
A2: p.i=1.K & for k st k in dom p & k<>i holds p.k=0.K;
reconsider r=mlt(p,q) as FinSequence of K;
A3: for k st k in dom r & k<>i holds r.k=0.K by A2,Th14;
A4: dom p = Seg len p & dom q = Seg len q by FINSEQ_1:def 3;
dom (mlt(p,q)) = Seg len (mlt(p,q)) & len (mlt(p,q))=min(len p,len q) by Th13
,FINSEQ_1:def 3;
then dom p /\ dom q = dom (mlt(p,q)) by A4,FINSEQ_2:2;
then
A5: i in dom r by A1,XBOOLE_0:def 4;
then r.i=q.i by A2,Th14;
hence thesis by A5,A3,Th12;
end;
theorem
for K being Ring
for A being Matrix of n,K holds 1.(K,n)*A=A
proof
let K be Ring;
let A be Matrix of n,K;
set B=1.(K,n);
A1: len B=n by MATRIX_0:24;
A2: len A=n by MATRIX_0:24;
A3: width B=n by MATRIX_0:24;
then
A4: len (B*A)=len (B) by A2,Def4;
A5: now
A6: dom A = Seg len A by FINSEQ_1:def 3;
let i,j;
assume
A7: [i,j] in Indices (B*A);
A8: dom (B*A) = Seg len (B*A) & Indices (B*A)=[:dom (B*A),Seg width(B*A)
:] by FINSEQ_1:def 3;
then
A9: i in Seg width B by A1,A3,A4,A7,ZFMISC_1:87;
then i in Seg len(Line(B,i)) by MATRIX_0:def 7;
then
A10: i in dom (Line(B,i)) by FINSEQ_1:def 3;
A11: dom B = Seg len B by FINSEQ_1:def 3;
then
A12: i in dom B by A4,A7,A8,ZFMISC_1:87;
then [i,i] in [:dom B,Seg width B:] by A9,ZFMISC_1:87;
then [i,i] in Indices B;
then
A13: (Line(B,i)).i=1.K by Th15;
A14: now
let k;
assume that
A15: k in dom (Line (B,i)) and
A16: k<>i;
k in Seg len (Line (B,i)) by A15,FINSEQ_1:def 3;
then k in Seg width B by MATRIX_0:def 7;
then [i,k] in [:dom B,Seg width B:] by A12,ZFMISC_1:87;
then [i,k] in Indices B;
hence (Line(B,i)).k=0.K by A16,Th15;
end;
i in Seg len (Col(A,j)) by A3,A2,A9,MATRIX_0:def 8;
then
A17: i in dom (Col(A,j)) by FINSEQ_1:def 3;
thus (B*A)*(i,j)= Line(B,i) "*" Col(A,j) by A3,A2,A7,Def4
.=Sum(mlt(Line(B,i),Col(A,j))) by FVSUM_1:def 9
.=Col(A,j).i by A10,A17,A14,A13,Th17
.=A*(i,j) by A1,A2,A6,A11,A12,MATRIX_0:def 8;
end;
width (B*A)=width A by A3,A2,Def4;
hence thesis by A1,A2,A4,A5,MATRIX_0:21;
end;
theorem
for K being commutative Ring
for A being Matrix of n,K holds A*(1.(K,n))=A
proof
let K be commutative Ring;
let A be Matrix of n,K;
set B=1.(K,n);
A1: width B=n by MATRIX_0:24;
A2: width A=n by MATRIX_0:24;
A3: len B=n by MATRIX_0:24;
then
A4: width (A*B)=width B by A2,Def4;
A5: now
let i,j;
assume
A6: [i,j] in Indices (A*B);
then A7: j in Seg width B by A4,ZFMISC_1:87;
then j in Seg len (Col(B,j)) by A3,A1,MATRIX_0:def 8;
then
A8: j in dom (Col(B,j)) by FINSEQ_1:def 3;
A9: j in Seg width A by A1,A2,A4,A6,ZFMISC_1:87;
A10: now
let k;
assume that
A11: k in dom (Col(B,j)) and
A12: k<>j;
k in Seg len (Col(B,j)) by A11,FINSEQ_1:def 3;
then k in Seg len B by MATRIX_0:def 8;
then k in dom B by FINSEQ_1:def 3;
then [k,j] in [:dom B,Seg width B:] by A7,ZFMISC_1:87;
then [k,j] in Indices B;
hence (Col(B,j)).k=0.K by A12,Th16;
end;
j in dom B by A3,A1,A7,FINSEQ_1:def 3;
then [j,j] in [:dom B,Seg width B:] by A1,A2,A9,ZFMISC_1:87;
then [j,j] in Indices B;
then
A13: (Col(B,j)).j=1.K by Th16;
j in Seg len (Line(A,i)) by A1,A2,A7,MATRIX_0:def 7;
then
A14: j in dom (Line(A,i)) by FINSEQ_1:def 3;
thus (A*B)*(i,j)= Line(A,i) "*" Col(B,j) by A3,A2,A6,Def4
.=Col(B,j) "*" Line(A,i) by FVSUM_1:90
.=Sum(mlt(Col(B,j),Line(A,i))) by FVSUM_1:def 9
.=Line(A,i).j by A8,A14,A10,A13,Th17
.=A*(i,j) by A9,MATRIX_0:def 7;
end;
len (A*B)=len A by A3,A2,Def4;
hence thesis by A1,A2,A4,A5,MATRIX_0:21;
end;
theorem
for K being Field
for a,b being Element of K holds <*<*a*>*> * <*<*b*>*> =<*<*a*b*>*>
proof
let K be Field;
let a,b be Element of K;
reconsider A=<*<*a*>*> as Matrix of 1,K;
reconsider B=<*<*b*>*> as Matrix of 1,K;
reconsider C=A*B as Matrix of K;
A1: len Line(A,1)=width A by MATRIX_0:def 7
.=1 by MATRIX_0:24;
A2: width A=1 by MATRIX_0:24;
then 1 in Seg width A by FINSEQ_1:2,TARSKI:def 1;
then Line(A,1).1=<*<*a*>*>*(1,1) by MATRIX_0:def 7
.=a by MATRIX_0:49;
then
A3: Line(<*<*a*>*>,1)=<*a*> by A1,FINSEQ_1:40;
A4: len B=1 by MATRIX_0:24;
then 1 in Seg len B by FINSEQ_1:2,TARSKI:def 1;
then 1 in dom B by FINSEQ_1:def 3;
then
A5: Col(B,1).1=<*<*b*>*>*(1,1) by MATRIX_0:def 8
.=b by MATRIX_0:49;
len A =1 by MATRIX_0:24;
then
A6: len C=1 by A2,A4,Def4;
width B=1 by MATRIX_0:24;
then
A7: width C=1 by A2,A4,Def4;
then reconsider C as Matrix of 1,K by A6,MATRIX_0:51;
Seg len C = dom C by FINSEQ_1:def 3;
then
A8: Indices C=[:Seg 1,Seg 1:] by A6,A7;
len Col(B,1)=len B by MATRIX_0:def 8
.=1 by MATRIX_0:24;
then
A9: Col(<*<*b*>*>,1)=<*b*> by A5,FINSEQ_1:40;
now
let i,j;
assume
A10: [i,j] in Indices C;
then j in Seg 1 by A8,ZFMISC_1:87;
then
A11: j=1 by FINSEQ_1:2,TARSKI:def 1;
i in Seg 1 by A8,A10,ZFMISC_1:87;
then
A12: i=1 by FINSEQ_1:2,TARSKI:def 1;
hence C*(i,j)=<*a*> "*" <*b*> by A2,A4,A3,A9,A10,A11,Def4
.=a * b by FVSUM_1:88
.=<*<*a*b*>*>*(i,j) by A12,A11,MATRIX_0:49;
end;
hence thesis by MATRIX_0:27;
end;
theorem
for K being Field
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 K be Field;
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: width A=2 by MATRIX_0:24;
2 in{1,2} by TARSKI:def 2;
then
A2: Line(A,2).2=A*(2,2) by A1,FINSEQ_1:2,MATRIX_0:def 7
.=d1 by MATRIX_0:50;
A3: len Line(A,2)=width A by MATRIX_0:def 7
.=2 by MATRIX_0:24;
1 in {1,2} by TARSKI:def 2;
then Line(A,2).1=A*(2,1) by A1,FINSEQ_1:2,MATRIX_0:def 7
.=c1 by MATRIX_0:50;
then
A4: Line(A,2)=<*c1,d1*> by A3,A2,FINSEQ_1:44;
2 in{1,2} by TARSKI:def 2;
then
A5: Line(A,1).2=A*(1,2) by A1,FINSEQ_1:2,MATRIX_0:def 7
.=b1 by MATRIX_0:50;
A6: len Line(A,1)=width A by MATRIX_0:def 7
.=2 by MATRIX_0:24;
1 in {1,2} by TARSKI:def 2;
then Line(A,1).1=A*(1,1) by A1,FINSEQ_1:2,MATRIX_0:def 7
.=a1 by MATRIX_0:50;
then
A7: Line(A,1)=<*a1,b1*> by A6,A5,FINSEQ_1:44;
A8: len Col(B,2)=len B by MATRIX_0:def 8
.=2 by MATRIX_0:24;
A9: len Col(B,1)=len B by MATRIX_0:def 8
.=2 by MATRIX_0:24;
reconsider C=A*B as Matrix of K;
A10: len B=2 by MATRIX_0:24;
width B=2 by MATRIX_0:24;
then
A11: width C=2 by A1,A10,Def4;
len A =2 by MATRIX_0:24;
then
A12: len C=2 by A1,A10,Def4;
then reconsider C as Matrix of 2,K by A11,MATRIX_0:51;
A13: Seg len B = dom B by FINSEQ_1:def 3;
2 in {1,2} by TARSKI:def 2;
then
A14: Col(B,2).2=B*(2,2) by A10,A13,FINSEQ_1:2,MATRIX_0:def 8
.=d2 by MATRIX_0:50;
1 in {1,2} by TARSKI:def 2;
then Col(B,2).1=B*(1,2) by A10,A13,FINSEQ_1:2,MATRIX_0:def 8
.=b2 by MATRIX_0:50;
then
A15: Col(B,2)=<*b2,d2*> by A8,A14,FINSEQ_1:44;
2 in {1,2} by TARSKI:def 2;
then
A16: Col(B,1).2=B*(2,1) by A10,A13,FINSEQ_1:2,MATRIX_0:def 8
.=c2 by MATRIX_0:50;
1 in {1,2} by TARSKI:def 2;
then Col(B,1).1=B*(1,1) by A10,A13,FINSEQ_1:2,MATRIX_0:def 8
.=a2 by MATRIX_0:50;
then
A17: Col(B,1)=<*a2,c2*> by A9,A16,FINSEQ_1:44;
dom C = Seg len C by FINSEQ_1:def 3;
then
A18: Indices C=[:Seg 2,Seg 2:] by A12,A11;
now
let i,j;
assume
A19: [i,j] in Indices C;
then
A20: i in Seg 2 & j in Seg 2 by A18,ZFMISC_1:87;
now
per cases by A20,FINSEQ_1:2,TARSKI:def 2;
case
i=1 & j=1;
hence C*(1,1)=<*a1,b1*> "*" <*a2,c2*> by A1,A10,A7,A17,A19,Def4
.=a1 * a2+ b1*c2 by FVSUM_1:89
.=D*(1,1) by MATRIX_0:50;
end;
case
i=1 & j=2;
hence C*(1,2)=<*a1,b1*> "*" <*b2,d2*> by A1,A10,A7,A15,A19,Def4
.=a1 * b2+ b1*d2 by FVSUM_1:89
.=D*(1,2) by MATRIX_0:50;
end;
case
i=2 & j=1;
hence C*(2,1)=<*c1,d1*> "*" <*a2,c2*> by A1,A10,A4,A17,A19,Def4
.=c1 * a2+ d1*c2 by FVSUM_1:89
.=D*(2,1) by MATRIX_0:50;
end;
case
i=2 & j=2;
hence C*(2,2)=<*c1,d1*> "*" <*b2,d2*> by A1,A10,A4,A15,A19,Def4
.=c1 * b2+ d1*d2 by FVSUM_1:89
.=D*(2,2) by MATRIX_0:50;
end;
end;
hence C*(i,j)=D*(i,j);
end;
hence thesis by MATRIX_0:27;
end;
theorem
for K being Field
for A,B being Matrix of K st width A=len B & width B<>0 holds (A*B) @=
(B @)*(A @)
proof
let K be Field;
let A,B be Matrix of K;
assume that
A1: width A=len B and
A2: width B<>0;
A3: len (B@)=width B by MATRIX_0:def 6;
len (A@)=width A by MATRIX_0:def 6;
then
A4: width (B@)=len (A@) by A1,A2,MATRIX_0:54;
then
A5: width ((B@)*(A@))=width (A@) by Def4;
width (A*B)>0 by A1,A2,Def4;
then
A6: width ((A*B)@)=len (A*B) by MATRIX_0:54
.=len A by A1,Def4;
A7: width (B@*A@)=width (A@) by A4,Def4;
A8: len (B@*A@)=len (B@) by A4,Def4
.=width B by MATRIX_0:def 6;
A9: len ((B@)*(A@))=len (B@) by A4,Def4;
A10: now
let i,j;
assume
A11: [i,j] in Indices ((B@)*(A@));
dom((B@)*(A@))=dom(B@) by A9,FINSEQ_3:29;
then
A12: [i,j] in [:dom (B@),Seg width (A@):] by A5,A11;
per cases;
suppose
width A=0;
hence ((B@)*(A@))*(i,j)=((A*B)@)*(i,j) by A1,A2,MATRIX_0:def 3;
end;
suppose
width A>0;
then width (A@)= len A by MATRIX_0:54;
then Seg width (A@) = dom A by FINSEQ_1:def 3;
then
A13: j in dom A by A12,ZFMISC_1:87;
then
A14: Col(A@,j)=Line(A,j) by MATRIX_0:58;
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;
Seg width B = dom (B@) by A3,FINSEQ_1:def 3;
then
A16: i in Seg width B by A12,ZFMISC_1:87;
then i in Seg width (A*B) by A1,Def4;
then [j,i] in [:dom(A*B),Seg width (A*B):] by A15,ZFMISC_1:87;
then
A17: [j,i]in Indices (A*B);
Line(B@,i)=Col(B,i) by A16,MATRIX_0:59;
hence ((B@)*(A@))*(i,j)= Col(B,i) "*" Line(A,j) by A4,A11,A14,Def4
.= Line(A,j) "*" Col(B,i) by FVSUM_1:90
.=(A*B)*(j,i) by A1,A17,Def4
.=((A*B)@)*(i,j) by A17,MATRIX_0:def 6;
end;
end;
A18: width (A@)=len A
proof
per cases;
suppose
width A=0;
hence thesis by A1,A2,MATRIX_0:def 3;
end;
suppose
width A>0;
hence thesis by MATRIX_0:54;
end;
end;
len ((A*B)@)=width (A*B) by MATRIX_0:def 6
.=width B by A1,Def4;
hence thesis by A6,A8,A7,A10,A18,MATRIX_0: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 & Y c= J by FINSUB_1:def 5;
then [:X,Y:] c=[:I,J:] by ZFMISC_1:96;
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:79;
end;
theorem Th23:
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 is having_a_unity )& G is commutative holds F $$ ([:X,Y:],G*(f,g))=F$$([:Y
,X:],G*(g,f))
proof
deffunc F(object,object) = [$2,$1];
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 is
having_a_unity );
consider h being Function such that
A2: dom h=[:J,I:] &
for x,y being object st x in J & y in I holds h.(x,y)= F(x,y)
from FUNCT_3:sch 2;
now
let z1,z2 be object;
assume that
A3: z1 in dom h and
A4: z2 in dom h and
A5: h.z1=h.z2;
consider x2,y2 being object such that
A6: z2=[x2,y2] by A2,A4,RELAT_1:def 1;
x2 in J & y2 in I by A2,A4,A6,ZFMISC_1:87;
then
A7: h.(x2,y2)=[y2,x2] by A2;
consider x1,y1 being object such that
A8: z1=[x1,y1] by A2,A3,RELAT_1:def 1;
x1 in J & y1 in I by A2,A3,A8,ZFMISC_1:87;
then
A9: h.(x1,y1)=[y1,x1] by A2;
then y1=y2 by A5,A8,A6,A7,XTUPLE_0:1;
hence z1=z2 by A5,A8,A6,A9,A7,XTUPLE_0:1;
end;
then
A10: h is one-to-one by FUNCT_1:def 4;
A11: for x st x in [:J,I:] holds h.x in [:I,J:]
proof
let x;
assume
A12: x in[:J,I:];
then consider y,z being object such that
A13: x=[y,z] by RELAT_1:def 1;
A14: y in J & z in I by A12,A13,ZFMISC_1:87;
then h.(y,z)=[z,y] by A2;
hence thesis by A13,A14,ZFMISC_1:87;
end;
assume
A15: G is commutative;
A16: G*(g,f)=(G*(f,g))*h
proof
reconsider G as Function of [:D,D:],D;
A17: dom (G*(g,f))=[:J,I:] by FUNCT_2:def 1;
A18: dom (G*(f,g))=[:I,J:] by FUNCT_2:def 1;
A19: for x being object
holds x in dom (G*(g,f)) iff x in dom h & h.x in dom (G*(f,g))
proof
let x be object;
thus x in dom (G*(g,f)) implies x in dom h & h.x in dom (G*(f,g))
proof
assume
A20: x in dom (G*(g,f));
then consider y,z being object such that
A21: x=[y,z] by RELAT_1:def 1;
A22: y in J & z in I by A17,A20,A21,ZFMISC_1:87;
then h.(y,z)=[z,y] by A2;
hence thesis by A2,A18,A21,A22,ZFMISC_1:87;
end;
assume that
A23: x in dom h and
h.x in dom (G*(f,g));
thus thesis by A2,A23,FUNCT_2:def 1;
end;
for x being object st x in dom (G*(g,f))
holds (G*(g,f)).x = (G*(f,g)).(h.x)
proof
let x be object;
assume
A24: x in dom (G*(g,f));
then consider y,z being object such that
A25: x=[y,z] by RELAT_1:def 1;
reconsider z as Element of I by A17,A24,A25,ZFMISC_1:87;
reconsider y as Element of J by A17,A24,A25,ZFMISC_1:87;
A26: [z,y] in dom (G*(f,g)) by A18,ZFMISC_1:87;
A27: [y,z] in dom (G*(g,f)) by A17,ZFMISC_1:87;
thus (G*(f,g)).(h.x) = (G*(f,g)).(h.(y,z)) by A25
.= (G*(f,g)).(z,y) by A2
.=G.(f.z,g.y) by A26,FINSEQOP:77
.=G.(g.y,f.z) by A15
.=(G*(g,f)).(y,z) by A27,FINSEQOP:77
.=(G*(g,f)).x by A25;
end;
hence thesis by A19,FUNCT_1:10;
end;
A28: X c= I & Y c=J by FINSUB_1:def 5;
for y being object holds y in [:X,Y:] iff y in h.:([:Y,X:])
proof
let y be object;
thus y in [:X,Y:] implies y in h.:([:Y,X:])
proof
assume
A29: y in [:X,Y:];
then consider y1,x1 being object such that
A30: y=[y1,x1] by RELAT_1:def 1;
A31: y1 in X & x1 in Y by A29,A30,ZFMISC_1:87;
then
A32: [x1,y1] in [:Y,X:] & [x1,y1] in dom h by A28,A2,ZFMISC_1:87;
h.(x1,y1)=y by A28,A2,A30,A31;
hence thesis by A32,FUNCT_1:def 6;
end;
assume y in h.:([:Y,X:]);
then consider x being object such that
x in dom h and
A33: x in [:Y,X:] and
A34: y = h.x by FUNCT_1:def 6;
consider x1,y1 being object such that
A35: x=[x1,y1] by A33,RELAT_1:def 1;
A36: x1 in Y & y1 in X by A33,A35,ZFMISC_1:87;
y = h.(x1,y1) by A34,A35;
then y=[y1,x1] by A28,A2,A36;
hence thesis by A36,ZFMISC_1:87;
end;
then
A37: h.:([:Y,X:])=[:X,Y:] by TARSKI:2;
reconsider h as Function of [:J,I:],[:I,J:] by A2,A11,FUNCT_2:3;
F $$ ([:X,Y:],G*(f,g))=F $$ ([:Y,X:],(G*(f,g))*h) by A1,A10,A37,SETWOP_2:6
.=F $$ ([:Y,X:],G*(g,f)) by A16;
hence thesis;
end;
theorem Th24:
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 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;
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:87;
reconsider z=g.y as Element of D;
reconsider u=[x,y] as Element of [:I,J:] by ZFMISC_1:87;
A4: dom <:f, dom f --> z:> = dom f /\ dom (dom f --> z) by FUNCT_3:def 7
.= dom f /\ dom f by FUNCOP_1:13
.=dom f;
rng f c= D & rng (dom f --> z) c=D by RELAT_1:def 19;
then
A5: [:rng f,rng (dom f --> z):] c= [:D,D:] by ZFMISC_1:96;
dom f=I by FUNCT_2:def 1;
then
A6: x in dom <:f, dom f --> z:> by A4;
dom G =[:D,D:] & rng<:f, dom f --> z:> c= [:rng f,rng (dom f --> z):]
by FUNCT_2:def 1,FUNCT_3:51;
then x in dom (G * <:f, dom f --> z:>) by A6,A5,RELAT_1:27,XBOOLE_1:1;
then
A7: x in dom (G[:](f,z))by FUNCOP_1:def 4;
A8: F$$({.x.},G[:](f,F$$({.y.},g)))=(G[:](f,F$$({.y.},g))).x by A1,SETWISEO:17
.=(G[:](f,g.y)).x by A1,SETWISEO:17
.= G.(f.x,g.y) by A7,FUNCOP_1:27;
F $$([:{.x.},{.y.}:],G*(f,g))= F $$({.u.},G*(f,g)) by ZFMISC_1:29
.= G*(f,g).(x,y) by A1,SETWISEO:17
.=G.(f.x,g.y) by A2,A3,FINSEQOP:77;
hence F $$([:{.x.},{.y.}:],G*(f,g))=F$$({.x.},G[:](f,F$$({.y.},g))) by A8;
end;
hence thesis;
end;
theorem Th25:
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 is
having_a_unity & F is having_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 that
A1: F is commutative and
A2: F is associative and
A3: F is having_a_unity and
A4: F is having_an_inverseOp and
A5: 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)));
A6: P[{}.J]
proof
set z=the_unity_wrt F;
reconsider T={}.[:I,J:] as Element of Fin [:I,J:];
A7: T=[:{x},{}.J:] by ZFMISC_1:90;
A8: dom <:f, dom f --> z:> = dom f /\ dom (dom f --> z) by FUNCT_3:def 7
.= dom f /\ dom f by FUNCOP_1:13
.=dom f;
rng f c= D & rng (dom f --> z) c=D by RELAT_1:def 19;
then
A9: [:rng f,rng (dom f --> z):] c= [:D,D:] by ZFMISC_1:96;
dom f=I by FUNCT_2:def 1;
then
A10: x in dom <:f, dom f --> z:> by A8;
dom G =[:D,D:] & rng<:f, dom f --> z:> c= [:rng f,rng (dom f --> z)
:] by FUNCT_2:def 1,FUNCT_3:51;
then x in dom (G*<:f, dom f --> z:>) by A10,A9,RELAT_1:27,XBOOLE_1:1;
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,A2,A3,SETWISEO:31
.=(G[:](f,the_unity_wrt F)).x by A1,A2,SETWISEO:17
.= G.(f.x,the_unity_wrt F) by A11,FUNCOP_1:27
.=the_unity_wrt F by A2,A3,A4,A5,FINSEQOP:66;
hence thesis by A1,A2,A3,A7,SETWISEO:31;
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;
per cases;
suppose
y in Y1;
then Y1 \/ {y} = Y1 by ZFMISC_1:40;
hence thesis by A13;
end;
suppose
not y in Y1;
then
A14: Y1 misses {y} by ZFMISC_1:50;
then
A15: [:{x},Y1:] misses [:{x},s:] by ZFMISC_1:104;
thus F$$([:{.x.},Y1 \/ {.y.}:],G*(f,g)) =F$$([:{.x.},Y1:] \/ [:{.x.},s
:],G*(f,g)) by ZFMISC_1:97
.=F.(F$$([:{.x.},Y1:],G*(f,g)),F$$([:{.x.},s:],G*(f,g))) by A1,A2,A3
,A15,SETWOP_2:4
.=F.(F$$({.x.},G[:](f,F$$(Y1,g))),F$$({.x.},G[:](f,F$$(s,g)))) by A1
,A2,A13,Th24
.=F$$({.x.},F.:(G[:](f,F$$(Y1,g)),G[:](f,F$$(s,g)))) by A1,A2,A3,
SETWOP_2:10
.=F$$({.x.},G[:](f,F.(F$$(Y1,g),F$$(s,g)))) by A5,FINSEQOP:36
.=F$$({.x.},G[:](f,F$$(Y1 \/ {.y.},g))) by A1,A2,A3,A14,SETWOP_2:4;
end;
end;
thus for Y being Element of Fin J holds P[Y] from SETWISEO:sch 4(A6,A12);
end;
hence thesis;
end;
theorem Th26:
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 is having_a_unity & F is commutative & F is
associative & F is having_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 is having_a_unity & F is commutative & F is associative and
A2: F is having_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: 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;
reconsider s={.x.} as Element of Fin I;
assume
A4: F$$([:X1,Y:],G*(f,g))=F$$(X1,G[:](f,F$$(Y,g)));
now
per cases;
case
x in X1;
then X1 \/ {x} = X1 by ZFMISC_1:40;
hence thesis by A4;
end;
case
not x in X1;
then
A5: X1 misses {x} by ZFMISC_1:50;
then
A6: [:X1,Y:] misses [:s,Y:] by ZFMISC_1:104;
thus F$$([:X1 \/ {.x.},Y:],G*(f,g)) =F$$([:X1,Y:] \/ [:s,Y:],G*(f,g))
by ZFMISC_1:97
.=F.(F $$([:X1,Y:],G*(f,g)),F $$([:s,Y:],G*(f,g))) by A1,A6,
SETWOP_2:4
.=F.(F$$(X1,G[:](f,F$$(Y,g))),F$$(s,G[:](f,F$$(Y,g)))) by A1,A2,A4
,Th25
.=F$$(X1 \/ {.x.},G[:](f,F$$(Y,g))) by A1,A5,SETWOP_2:4;
end;
end;
hence thesis;
end;
A7: P[{}.I]
proof
reconsider T={}.[:I,J:] as Element of Fin [:I,J:];
T=[:{}.I,Y:] by ZFMISC_1:90;
then F $$([:{}.I,Y:],G*(f,g))= the_unity_wrt F by A1,SETWISEO:31;
hence thesis by A1,SETWISEO:31;
end;
for X1 being Element of Fin I holds P[X1] from SETWISEO:sch 4(A7,A3 );
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 & 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 that
A1: F is commutative associative and
A2: 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,A2
,Th23
.=F$$({.y.},G[:](g,F$$({.x.},f))) by A1,Th24
.=F$$({.y.},G[;] (F$$({.x.},f),g)) by A2,FUNCOP_1:64;
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 is having_a_unity & F is commutative associative &
F is having_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 is having_a_unity & F is commutative & F is associative and
A2: F is having_an_inverseOp & G is_distributive_wrt F and
A3: G is commutative;
thus F $$ ([:X,Y:],G*(f,g))=F$$([:Y,X:],G*(g,f)) by A1,A3,Th23
.=F$$(Y,G[:](g,F$$(X,f))) by A1,A2,Th26
.=F$$(Y,G[;](F$$(X,f),g)) by A3,FUNCOP_1:64;
end;
theorem Th29:
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 is having_a_unity commutative associative 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 that
A1: F is having_a_unity and
A2: F is commutative & F is associative;
now
let x be Element of I;
assume
A3: for i being Element of I holds g.i=F$$(Y,(curry f).i);
deffunc F(object) = [x,$1];
consider h being Function such that
A4: dom h = J &
for y being object st y in J holds h.y = F(y) from FUNCT_1:sch 3;
A5: dom ((curry f).x) = J & dom (f *h)=J & rng h c= [:I,J:]
proof
A6: dom f=[:I,J:] by FUNCT_2:def 1;
then ex g being Function st 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:29;
hence dom ((curry f).x)=J;
now
let y be object;
assume y in rng h;
then consider z being object such that
A7: z in dom h and
A8: y = h.z by FUNCT_1:def 3;
y=[x,z] by A4,A7,A8;
hence y in dom f by A4,A6,A7,ZFMISC_1:87;
end;
then rng h c= dom f by TARSKI:def 3;
hence thesis by A4,FUNCT_2:def 1,RELAT_1:27;
end;
A9: for y being object st y in J holds ((curry f).x).y=(f*h).y
proof
let y be object;
dom f=[:I,J:] by FUNCT_2:def 1;
then
A10: ex g being Function st 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:29;
assume
A11: y in J;
hence (f*h).y=f.(h.y) by A5,FUNCT_1:12
.= f.(x,y) by A4,A11
.=((curry f).x).y by A11,A10;
end;
for y being object holds y in [:{x},Y:] iff y in h.:(Y)
proof
let y be object;
thus y in [:{x},Y:] implies y in h.:(Y)
proof
assume
A12: y in [:{x},Y:];
then consider y1,x1 being object such that
A13: y=[y1,x1] by RELAT_1:def 1;
A14: y1 in {x} by A12,A13,ZFMISC_1:87;
A15: Y c= J & x1 in Y by A12,A13,FINSUB_1:def 5,ZFMISC_1:87;
then h.x1=[x,x1] by A4
.=y by A13,A14,TARSKI:def 1;
hence thesis by A4,A15,FUNCT_1:def 6;
end;
assume y in h.:Y;
then consider z being object such that
A16: z in dom h and
A17: z in Y and
A18: y = h.z by FUNCT_1:def 6;
y=[x,z] by A4,A16,A18;
hence thesis by A17,ZFMISC_1:105;
end;
then
A19: h.:Y=[:{x},Y:] by TARSKI:2;
now
let x1,x2 be object;
assume that
A20: x1 in dom h and
A21: x2 in dom h and
A22: h.x1=h.x2;
[x,x1]=h.x2 by A4,A20,A22
.=[x,x2] by A4,A21;
hence x1=x2 by XTUPLE_0:1;
end;
then
A23: h is one-to-one by FUNCT_1:def 4;
reconsider h as Function of J,[:I,J:] by A4,A5,FUNCT_2:2;
thus F$$([:{.x.},Y:],f)=F$$(Y,f*h) by A1,A2,A23,A19,SETWOP_2:6
.=F $$ (Y,(curry f).x) by A5,A9,FUNCT_1:2
.=g.x by A3
.=F$$({.x.},g) by A2,SETWISEO:17;
end;
hence thesis;
end;
theorem Th30:
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 is having_a_unity & F is commutative & F is associative 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 that
A1: for i being Element of I holds g.i=F$$(Y,(curry f).i) and
A2: F is having_a_unity & F is commutative & F is associative;
defpred P[Element of Fin I] means F$$([:$1,Y:],f)=F$$($1,g);
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;
per cases;
suppose
x in X1;
then X1 \/ {x} = X1 by ZFMISC_1:40;
hence thesis by A4;
end;
suppose
not x in X1;
then
A5: X1 misses {x} by ZFMISC_1:50;
then
A6: [:X1,Y:] misses [:s,Y:] by ZFMISC_1:104;
thus F$$([:X1 \/ {.x.},Y:],f) =F$$([:X1,Y:] \/ [:s,Y:],f)by ZFMISC_1:97
.=F.(F $$([:X1,Y:],f),F $$([:s,Y:],f)) by A2,A6,SETWOP_2:4
.=F.(F$$(X1,g),F$$(s,g)) by A1,A2,A4,Th29
.=F$$(X1 \/ {.x.},g) by A2,A5,SETWOP_2:4;
end;
end;
A7: P[{}.I]
proof
reconsider T={}.[:I,J:] as Element of Fin [:I,J:];
T=[:{}.I,Y:] by ZFMISC_1:90;
then F $$([:{}.I,Y:],f)= the_unity_wrt F by A2,SETWISEO:31;
hence thesis by A2,SETWISEO:31;
end;
for X1 being Element of Fin I holds P[X1] from SETWISEO:sch 4(A7,A3 );
hence thesis;
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 J,D for X being Element of Fin I
st F is having_a_unity & F is commutative & F is associative 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 that
A1: F is having_a_unity and
A2: F is commutative & F is associative;
now
let y be Element of J;
assume
A3: for j being Element of J holds g.j=F$$(X,(curry' f).j);
deffunc F(object) = [$1,y];
consider h being Function such that
A4: dom h = I &
for x being object st x in I holds h.x = F(x) from FUNCT_1:sch 3;
A5: dom ((curry' f).y) =I & dom (f *h)=I & rng h c= [:I,J:]
proof
A6: dom f=[:I,J:] by FUNCT_2:def 1;
then ex g being Function st 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:32;
hence dom ((curry' f).y)=I;
now
let x be object;
assume x in rng h;
then consider z being object such that
A7: z in dom h and
A8: x = h.z by FUNCT_1:def 3;
x=[z,y] by A4,A7,A8;
hence x in dom f by A4,A6,A7,ZFMISC_1:87;
end;
then rng h c= dom f by TARSKI:def 3;
hence thesis by A4,FUNCT_2:def 1,RELAT_1:27;
end;
A9: for x being object st x in I holds ((curry' f).y).x=(f*h).x
proof
let x be object;
dom f=[:I,J:] by FUNCT_2:def 1;
then
A10: ex g being Function st 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:32;
assume
A11: x in I;
hence (f*h).x=f.(h.x) by A5,FUNCT_1:12
.= f.(x,y) by A4,A11
.=((curry' f).y).x by A11,A10;
end;
for x being object holds x in [:X,{y}:] iff x in h.:(X)
proof
let x be object;
thus x in [:X,{y}:] implies x in h.:(X)
proof
assume
A12: x in [:X,{y}:];
then consider x1,y1 being object such that
A13: x=[x1,y1] by RELAT_1:def 1;
A14: y1 in {y} by A12,A13,ZFMISC_1:87;
A15: X c= I & x1 in X by A12,A13,FINSUB_1:def 5,ZFMISC_1:87;
then h.x1=[x1,y] by A4
.=x by A13,A14,TARSKI:def 1;
hence thesis by A4,A15,FUNCT_1:def 6;
end;
assume x in h.:(X);
then consider z being object such that
A16: z in dom h and
A17: z in X and
A18: x = h.z by FUNCT_1:def 6;
x=[z,y] by A4,A16,A18;
hence thesis by A17,ZFMISC_1:106;
end;
then
A19: h.:X=[:X,{y}:] by TARSKI:2;
now
let x1,x2 be object;
assume that
A20: x1 in dom h and
A21: x2 in dom h and
A22: h.x1=h.x2;
[x1,y]=h.x2 by A4,A20,A22
.=[x2,y] by A4,A21;
hence x1=x2 by XTUPLE_0:1;
end;
then
A23: h is one-to-one by FUNCT_1:def 4;
reconsider h as Function of I,[:I,J:] by A4,A5,FUNCT_2:2;
thus F$$([:X,{.y.}:],f)=F$$(X,f*h) by A1,A2,A23,A19,SETWOP_2:6
.=F $$ (X,(curry' f).y) by A5,A9,FUNCT_1:2
.=g.y by A3
.=F$$({.y.},g) by A2,SETWISEO:17;
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 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 is having_a_unity & F is commutative & F is associative 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 that
A1: for j being Element of J holds g.j=F$$(X,(curry' f).j) and
A2: F is having_a_unity & F is commutative & F is associative;
defpred P[Element of Fin J] means F$$([:X,$1:],f)=F$$($1,g);
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;
per cases;
suppose
y in Y1;
then Y1 \/ {y} = Y1 by ZFMISC_1:40;
hence thesis by A4;
end;
suppose
not y in Y1;
then
A5: Y1 misses {y} by ZFMISC_1:50;
then
A6: [:X,Y1:] misses [:X,s:] by ZFMISC_1:104;
thus F$$([:X,Y1 \/ {.y.}:],f) =F$$([:X,Y1:] \/ [:X,s:],f)by ZFMISC_1:97
.=F.(F $$([:X,Y1:],f),F $$([:X,s:],f)) by A2,A6,SETWOP_2:4
.=F.(F$$(Y1,g),F$$(s,g)) by A1,A2,A4,Th31
.=F$$(Y1 \/ {.y.},g) by A2,A5,SETWOP_2:4;
end;
end;
A7: P[{}.J]
proof
reconsider T={}.[:I,J:] as Element of Fin [:I,J:];
T=[:X,{}.J:] by ZFMISC_1:90;
then F $$([:X,{}.J:],f)= the_unity_wrt F by A2,SETWISEO:31;
hence thesis by A2,SETWISEO:31;
end;
for Y1 being Element of Fin J holds P[Y1] from SETWISEO:sch 4(A7,A3 );
hence thesis;
end;
theorem
for K being commutative Ring
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 K be commutative Ring;
let A,B,C be Matrix of K;
assume that
A1: width A=len B and
A2: width B=len C;
A3: len (B*C)=width A by A1,A2,Def4;
A4: width (B*C)=width C by A2,Def4;
then
A5: width (A*(B*C))=width C by A3,Def4;
dom(B*C)=dom B by A1,A3,FINSEQ_3:29;
then
A6: Indices (B*C)=[:dom B,Seg width C:] by A4;
A7: Seg len B = dom B by FINSEQ_1:def 3;
A8: len (A*(B*C))=len A by A3,Def4;
then dom(A*(B*C))=dom A by FINSEQ_3:29;
then
A9: Indices (A*(B*C))=[:dom A,Seg width C:] by A5;
0.K is_a_unity_wrt (the addF of K) by FVSUM_1:6;
then
A10: the addF of K is having_a_unity by SETWISEO:def 2;
A11: width (A*B)=len C by A1,A2,Def4;
then
A12: width ((A*B)*C)=width C by Def4;
A13: len (A*B)=len A by A1,Def4;
then dom(A*B)=dom A by FINSEQ_3:29;
then
A14: Indices (A*B)=[:dom A,Seg width B:] by A2,A11;
A15: len ((A*B)*C)=len A by A13,A11,Def4;
then
A16: dom((A*B)*C)=dom A by FINSEQ_3:29;
then
A17: Indices((A*B)*C)=[:dom A,Seg width C:] by A12;
A18: Indices ((A*B)*C)=[:dom A,Seg width C:] by A12,A16;
now
reconsider Y=findom B as Element of Fin NAT;
reconsider X=findom C as Element of Fin NAT;
let i,j;
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
A19: for k1 being Element of NAT for k2 being Element of NAT holds f.(
k1,k2) = F(k1,k2) from BINOP_1:sch 4;
A20: for k be Element of NAT st k in NAT holds ((curry f).k) |dom B =(C*(k,
j)) * mlt(Line(A,i),Col(B,k))
proof
let k be Element of NAT;
assume k in NAT;
A21: {k} c=NAT by ZFMISC_1:31;
reconsider a=C*(k,j) as Element of K;
A22: dom curry f = NAT by FUNCT_2:def 1;
dom f=[:NAT,NAT:] by FUNCT_2:def 1;
then
A23: dom((curry f).k)=proj2 ( [:NAT,NAT:]/\ [:{k},proj2 [:NAT,NAT:]:])by A22,
FUNCT_5:31
.= proj2([:{k},NAT:]/\[:NAT,NAT:] ) by FUNCT_5:9
.= proj2 [:{k},NAT:] by A21,ZFMISC_1:101
.= NAT by FUNCT_5:9;
then
A24: dom(((curry f).k) |dom B)=NAT /\ dom B by RELAT_1:61
.=dom B by XBOOLE_1:28;
reconsider p=mlt(Line(A,i),Col(B,k)) as FinSequence of K;
A25: len mlt(Line(A,i),Col(B,k))= len ((the multF of K).: (Line(A,i),Col
(B,k))) by FVSUM_1:def 7;
len (Line(A,i))= len B by A1,MATRIX_0:def 7
.= len (Col(B,k)) by MATRIX_0:def 8;
then
A26: len ((the multF of K).:(Line(A,i),Col(B,k))) =len (Line(A,i)) by
FINSEQ_2:72
.= len B by A1,MATRIX_0:def 7;
dom (a multfield)=the carrier of K by FUNCT_2:def 1;
then (a*p)=(a multfield)* p & rng p c=dom (a multfield) by FINSEQ_1:def 4
,FVSUM_1:def 6;
then
A27: dom (a*p) = dom p by RELAT_1:27;
A28: dom ((the multF of K).:(Line(A,i),Col(B,k)))= Seg len ((the multF
of K).:(Line(A,i),Col(B,k))) by FINSEQ_1:def 3;
A29: now
let l be object;
assume
A30: l in dom B;
then reconsider l9=l as Element of NAT;
A31: l in dom(a*p) by A25,A26,A27,A30,FINSEQ_3:29;
l9 in dom p by A25,A26,A30,FINSEQ_3:29;
then reconsider b=p.l9 as Element of K by FINSEQ_2:11;
A32: l9 in dom( (the multF of K) .: (Line(A,i),Col(B,k)) ) by A26,A28,A30,
FINSEQ_1:def 3;
thus (((curry f).k) |dom B).l=((curry f).k).l9 by A30,FUNCT_1:49
.= f.(k,l9) by A22,A23,FUNCT_5:31
.=(A* (i,l9))*(B* (l9,k))*(C* (k,j)) by A19
.=(the multF of K). ((the multF of K).((Line(A,i).l9),(B*(l9,k))),
(C*(k,j))) by A1,A7,A30,MATRIX_0:def 7
.=(the multF of K). ((the multF of K).((Line(A,i).l9),(Col(B,k).l9
)),(C*(k,j))) by A30,MATRIX_0:def 8
.=(the multF of K). (( (the multF of K) .: (Line(A,i),Col(B,k)) ).
l9,(C*(k,j))) by A32,FUNCOP_1:22
.= b*a by FVSUM_1:def 7
.=(C*(k,j) * mlt(Line(A,i),Col(B,k))).l by A31,FVSUM_1:50;
end;
dom (C*(k,j)*mlt(Line(A,i),Col(B,k)))=dom B by A25,A26,A27,FINSEQ_3:29;
hence thesis by A24,A29,FUNCT_1:2;
end;
A33: 0.K = the_unity_wrt (the addF of K) by FVSUM_1:7;
deffunc F9( Element of NAT) = (the addF of K)$$(X,(curry' f).$1);
deffunc F( Element of NAT) = (the addF of K)$$(Y,(curry f).$1);
consider g being sequence of the carrier of K such that
A34: for k being Element of NAT holds g.k = F(k) from FUNCT_2:sch 4;
A35: dom (g|dom C)=dom g /\ dom C by RELAT_1:61
.= NAT /\ dom C by FUNCT_2:def 1
.=dom C by XBOOLE_1:28;
len (Line((A*B),i))=width (A*B) by MATRIX_0:def 7
.=len C by A1,A2,Def4
.=len (Col(C,j)) by MATRIX_0:def 8;
then
A36: len ((the multF of K).:(Line((A*B),i),Col(C,j)))=len (Col(C,j)) by
FINSEQ_2:72
.=len C by MATRIX_0:def 8;
assume
A37: [i,j] in Indices ((A*B)*C);
then
A38: i in dom A by A17,ZFMISC_1:87;
A39: now
let k9 be object;
assume
A40: k9 in dom C;
then reconsider k=k9 as Element of NAT;
A41: k in dom ((the multF of K).:(Line(A*B,i),Col(C,j))) by A36,A40,
FINSEQ_3:29;
reconsider p=mlt(Line(A,i),Col(B,k)) as FinSequence of K;
reconsider a=C*(k,j) as Element of K;
dom (a multfield)=the carrier of K by FUNCT_2:def 1;
then (a*p)=(a multfield)* p & rng p c=dom (a multfield) by FINSEQ_1:def 4
,FVSUM_1:def 6;
then
A42: dom (a*p)=dom p by RELAT_1:27;
len (Line(A,i))= len B by A1,MATRIX_0:def 7
.= len (Col(B,k)) by MATRIX_0:def 8;
then len ((the multF of K).:(Line(A,i),Col(B,k))) =len (Line(A,i)) by
FINSEQ_2:72
.= len B by A1,MATRIX_0:def 7;
then len B = len p by FVSUM_1:def 7;
then
A43: dom (C*(k,j)*mlt(Line(A,i),Col(B,k)))=dom B by A42,FINSEQ_3:29;
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:21;
then
A44: [#](C*(k,j)*mlt(Line(A,i),Col(B,k)),0.K) | dom B= ((curry f).k) | dom
B by A20;
k in Seg width B by A2,A40,FINSEQ_1:def 3;
then
A45: [i,k] in Indices (A*B) by A14,A38,ZFMISC_1:87;
A46: k in Seg width (A*B) by A11,A40,FINSEQ_1:def 3;
thus (g|dom C).k9=g.k by A35,A40,FUNCT_1:47
.=(the addF of K)$$(Y,(curry f).k) by A34
.=(the addF of K)$$(Y,[#](C*(k,j)*mlt(Line(A,i),Col(B,k)),0.K)) by A44,
FVSUM_1:8,SETWOP_2:7
.=(the addF of K)$$ (a*p) by A10,A33,A43,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:73
.= C*(k,j) *( Line(A,i) "*" Col(B,k)) by FVSUM_1:def 9
.=((A*B)*(i,k))*(C*(k,j)) by A1,A45,Def4
.= (the multF of K).(Line(A*B,i).k,C*(k,j)) by A46,MATRIX_0:def 7
.= (the multF of K).(Line(A*B,i).k,Col(C,j).k) by A40,MATRIX_0:def 8
.= ((the multF of K).:(Line(A*B,i),Col(C,j))).k by A41,FUNCOP_1:22
.=(mlt(Line(A*B,i),Col(C,j))).k9 by FVSUM_1:def 7;
end;
A47: len ((the multF of K).:(Line((A*B),i),Col(C,j)))= len (mlt(Line((A*B)
,i),Col(C,j))) by FVSUM_1:def 7;
then
A48: dom C = dom mlt(Line(A*B,i),Col(C,j)) by A36,FINSEQ_3:29;
dom mlt(Line(A*B,i),Col(C,j)) = dom C by A36,A47,FINSEQ_3:29;
then
A49: [#](mlt(Line(A*B,i),Col(C,j)),0.K) | dom C=mlt(Line(A*B,i),Col(C,j ))
by SETWOP_2:21;
len (Col((B*C),j))=len (B*C) by MATRIX_0:def 8
.=width A by A1,A2,Def4
.=len (Line(A,i)) by MATRIX_0:def 7;
then
A50: len
((the multF of K).:(Line(A,i),Col(B*C,j)))=len (Line(A,i)) by FINSEQ_2:72
.=width A by MATRIX_0:def 7;
A51: len ((the multF of K).:(Line(A,i),Col(B*C,j)))= len (mlt(Line(A,i),
Col(B*C,j))) by FVSUM_1:def 7;
then
A52: dom (mlt(Line(A,i),Col(B*C,j))) = Y by A1,A50,FINSEQ_3:29;
dom mlt(Line(A,i),Col(B*C,j)) = dom B by A1,A50,A51,FINSEQ_3:29;
then
A53: [#](mlt(Line(A,i),Col(B*C,j)),0.K) | dom B=mlt(Line(A,i),Col(B*C,j ))
by SETWOP_2:21;
consider h being sequence of (the carrier of K) such that
A54: for k being Element of NAT holds h.k = F9(k) from FUNCT_2:sch 4;
A55: dom (h|dom B)=dom h /\ dom B by RELAT_1:61
.= NAT /\ dom B by FUNCT_2:def 1
.=dom B by XBOOLE_1:28;
A56: j in Seg width C by A17,A37,ZFMISC_1:87;
A57: now
let k9 be object;
assume
A58: k9 in dom B;
then reconsider k=k9 as Element of NAT;
A59: k in Seg width A by A1,A58,FINSEQ_1:def 3;
A60: k in dom(B*C) by A1,A3,A58,FINSEQ_3:29;
A61: [k,j] in Indices (B*C) by A6,A56,A58,ZFMISC_1:87;
reconsider p=mlt(Line(B,k),Col(C,j)) as FinSequence of K;
reconsider a=A*(i,k) as Element of K;
A62: len mlt(Line(B,k),Col(C,j))= len ((the multF of K).:(Line(B,k),Col(
C,j))) by FVSUM_1:def 7;
dom f=[:NAT,NAT:] by FUNCT_2:def 1;
then
A63: ex G being Function st 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:32;
then
A64: dom(((curry' f).k) |dom C)=NAT /\ dom C by RELAT_1:61
.=dom C by XBOOLE_1:28;
A65: k in dom ((the multF of K).: (Line(A,i),Col(B*C,j)))by A1,A50,A58,
FINSEQ_3:29;
len (Line(B,k))= len C by A2,MATRIX_0:def 7
.= len (Col(C,j)) by MATRIX_0:def 8;
then
A66: len ((the multF of K).:(Line(B,k),Col(C,j))) =len (Line(B,k)) by
FINSEQ_2:72
.= len C by A2,MATRIX_0:def 7;
dom (a multfield)=the carrier of K by FUNCT_2:def 1;
then (a*p)=(a multfield)* p & rng p c=dom (a multfield) by FINSEQ_1:def 4
,FVSUM_1:def 6;
then
A67: dom (a*p)=dom p by RELAT_1:27;
then
A68: dom (A*(i,k)*mlt(Line(B,k),Col(C,j)))=dom C by A62,A66,FINSEQ_3:29;
A69: now
let l be object;
assume
A70: l in dom C;
then reconsider l9=l as Element of NAT;
A71: l9 in dom ((the multF of K) .: (Line(B,k),Col(C,j))) by A66,A70,
FINSEQ_3:29;
l9 in dom p by A62,A66,A70,FINSEQ_3:29;
then reconsider b=p.l9 as Element of K by FINSEQ_2:11;
A72: l9 in Seg width B by A2,A70,FINSEQ_1:def 3;
A73: l in dom(a*p) by A62,A66,A67,A70,FINSEQ_3:29;
thus (((curry' f).k) |dom C).l=((curry' f).k).l9 by A70,FUNCT_1:49
.= f.(l9,k) by A63
.=(A* (i,k))*(B* (k,l9))*(C* (l9,j)) by A19
.=(A* (i,k))*((B* (k,l9))*(C* (l9,j))) by GROUP_1:def 3
.=(the multF of K). (A*(i,k), (the multF of K).(( Line(B,k) ).l9,
( C*(l9,j)))) by A72,MATRIX_0:def 7
.=(the multF of K). (A*(i,k),(the multF of K).((Line(B,k).l9),(Col
(C,j)).l9)) by A70,MATRIX_0:def 8
.=(the multF of K). (A*(i,k),( (the multF of K) .: (Line(B,k),Col(
C,j))).l9) by A71,FUNCOP_1:22
.=a*b by FVSUM_1:def 7
.=(A*(i,k)*mlt(Line(B,k),Col(C,j))).l by A73,FVSUM_1:50;
end;
[#](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 A68,SETWOP_2:21;
then
A74: [#](A*(i,k)*mlt(Line(B,k),Col(C,j)),0.K) | dom C= ((curry' f).k) |
dom C by A64,A68,A69,FUNCT_1:2;
thus (h|dom B).k9=h.k by A55,A58,FUNCT_1:47
.=(the addF of K)$$(X,(curry' f).k) by A54
.=(the addF of K)$$(X,[#](A*(i,k)*mlt(Line(B,k),Col(C,j)),0.K)) by A74,
FVSUM_1:8,SETWOP_2:7
.=(the addF of K)$$ (a*p) by A10,A33,A68,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:73
.= A*(i,k) *( Line(B,k) "*" Col(C,j)) by FVSUM_1:def 9
.= A*(i,k)*((B*C)*(k,j)) by A2,A61,Def4
.= (the multF of K).(Line(A,i).k,(B*C)*(k,j)) by A59,MATRIX_0:def 7
.= (the multF of K).(Line(A,i).k,Col(B*C,j).k) by A60,MATRIX_0:def 8
.= ((the multF of K).:(Line(A,i),Col(B*C,j))).k by A65,FUNCOP_1:22
.=(mlt(Line(A,i),Col(B*C,j))).k9 by FVSUM_1:def 7;
end;
dom mlt(Line(A,i),Col(B*C,j))=dom B by A1,A50,A51,FINSEQ_3:29;
then
A75: h|dom B=mlt(Line(A,i),Col(B*C,j)) by A55,A57,FUNCT_1:2;
dom mlt(Line(A*B,i),Col(C,j))=dom C by A36,A47,FINSEQ_3:29;
then
A76: g|dom C=mlt(Line(A*B,i),Col(C,j)) by A35,A39,FUNCT_1:2;
thus ((A*B)*C)*(i,j)=Line(A*B,i) "*" Col(C,j) by A11,A37,Def4
.=Sum(mlt(Line(A*B,i),Col(C,j))) by FVSUM_1:def 9
.=(the addF of K) $$(mlt(Line(A*B,i),Col(C,j)))by FVSUM_1:def 8
.=(the addF of K) $$(findom C, [#](mlt(Line(A*B,i),Col(C,j)),0.K)) by A10
,A33,A48,SETWOP_2:def 2
.=(the addF of K)$$(X,g) by A10,A49,A76,SETWOP_2:7
.=(the addF of K)$$([:X,Y:],f) by A10,A34,Th30
.=(the addF of K)$$(Y,h) by A10,A54,Th32
.=(the addF of K)$$(findom (mlt(Line(A,i),Col(B*C,j))), [#](mlt(Line(A
,i),Col(B*C,j)),the_unity_wrt(the addF of K))) by A10,A33,A53,A75,A52,
SETWOP_2:7
.=(the addF of K)$$(mlt(Line(A,i),Col(B*C,j))) by A10,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 9
.=(A*(B*C))*(i,j) by A3,A9,A18,A37,Def4;
end;
hence thesis by A8,A5,A15,A12,MATRIX_0: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 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);
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
A1: for k be Nat st k in Seg n1 ex x being Element of K st P[k,x]
proof
reconsider p as Function of Seg n,Seg n by MATRIX_1:def 12;
let k be Nat;
assume k in Seg n1;
then p.k in Seg n by FUNCT_2:5;
then reconsider j=p.k as Element of NAT;
reconsider x=M*(k,j)as Element of K;
take x;
thus thesis;
end;
consider t being FinSequence of K such that
A2: dom t = Seg n1 and
A3: for k be Nat st k in Seg n1 holds P[k,t.k] from FINSEQ_1:sch 5(A1);
take t;
thus len t= n by A2,FINSEQ_1:def 3;
let i,j;
assume i in dom t & j=p.i;
hence thesis by A2,A3;
end;
uniqueness
proof
for p1,p2 being FinSequence 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 K;
assume that
A4: len p1=n and
A5: for i,j st i in dom p1 & j=p.i holds p1.i=M*(i,j) and
A6: len p2=n and
A7: for i,j st i in dom p2 & j=p.i holds p2.i= M*(i,j);
A8: dom p2= Seg n by A6,FINSEQ_1:def 3;
A9: dom p1 = Seg n by A4,FINSEQ_1:def 3;
for i be Nat st i in Seg n holds p1.i = p2.i
proof
reconsider p as Function of Seg n,Seg n by MATRIX_1:def 12;
let i be Nat;
assume
A10: i in Seg n;
then p.i in Seg n by FUNCT_2:5;
then reconsider j=p.i as Element of NAT;
p1.i=M*(i,j) by A5,A9,A10;
hence thesis by A7,A8,A10;
end;
hence thesis by A9,A8,FINSEQ_1:13;
end;
hence thesis;
end;
end;
definition
let n; let K be Ring;
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 multF of K)
$$ Path_matrix(p,M),p);
existence
proof
deffunc V(Element of Permutations n) = -((the multF 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
FUNCT_2:sch 4;
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 multF
of K) $$ Path_matrix(p,M),p) and
A3: for p being Element of Permutations(n) holds f2.p = -((the multF
of K) $$ Path_matrix(p,M),p);
now
let p be Element of Permutations(n);
f1.p = -((the multF of K) $$ Path_matrix(p,M),p) by A2;
hence f1.p=f2.p by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let n;
let K be Ring;
let M be Matrix of n,K;
func Det M -> Element of K equals
(the addF of K) $$ (In(Permutations(n), Fin Permutations n),Path_product(M));
coherence;
end;
reserve a for Element of K;
theorem
for K be Ring,
a being Element of K holds
Det <*<*a*>*> =a
proof
let K be Ring,
a be Element of K;
set M=<*<*a*>*>;
A1: (Path_product M).(idseq 1)=a
proof
reconsider p = idseq 1 as Element of Permutations(1) by MATRIX_1:def 12;
A2: -(a,p)=a
proof
reconsider q = id Seg 1 as Element of Permutations(1) by MATRIX_1:def 12;
len Permutations 1 = 1 by MATRIX_1:9;
then q is even by MATRIX_1:16;
hence thesis by MATRIX_1:def 16;
end;
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:2,TARSKI:def 1;
then 1=p.1 by A4,FUNCT_1:18;
then Path_matrix(p,M).1=M*(1,1) by A5,Def7;
then Path_matrix(p,M).1=a by MATRIX_0:49;
then
A6: Path_matrix(p,M)=<*a*> by A3,FINSEQ_1:40;
(Path_product M).p = -((the multF of K) $$ Path_matrix(p,M),p) & <*a*>
=1|->a by Def8,FINSEQ_2:59;
hence thesis by A6,A2,FINSOP_1:16;
end;
Permutations 1 in Fin Permutations 1 by FINSUB_1:def 5; then
In (Permutations 1, Fin Permutations 1) = Permutations 1
by SUBSET_1:def 8; then
In (Permutations 1, Fin Permutations 1) = {idseq 1} &
idseq 1 in Permutations 1 by MATRIX_1:10,TARSKI:def 1;
hence thesis by A1,SETWISEO:17;
end;
definition
let n;
let K;
let M be Matrix of n,K;
func diagonal_of_Matrix M -> FinSequence of K means
len it = n & for i st i in Seg n holds it.i=M*(i,i);
existence
proof
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
deffunc V(Nat) = M*($1,$1);
consider z being FinSequence of K such that
A1: len z=n1 & for i be Nat st i in dom z holds z.i=V(i) from FINSEQ_2
:sch 1;
take z;
dom z = Seg n1 by A1,FINSEQ_1:def 3;
hence thesis by A1;
end;
uniqueness
proof
let p1,p2 be FinSequence of K;
assume that
A2: len p1 = n and
A3: for i st i in Seg n holds p1.i=M*(i,i) and
A4: len p2 = n and
A5: for i st i in Seg n holds p2.i=M*(i,i);
A6: now
let i be Nat;
assume
A7: i in Seg n;
then p1.i=M*(i,i) by A3;
hence p1.i = p2.i by A5,A7;
end;
dom p1 = Seg n & dom p2= Seg n by A2,A4,FINSEQ_1:def 3;
hence thesis by A6,FINSEQ_1:13;
end;
end;