:: The Product of Matrices of Elements of a Field and Determinants
:: by Katarzyna Zawadzka
::
:: Received May 17, 1993
:: Copyright (c) 1993-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, 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, MATRIX_0;
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,
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 non empty ZeroStr;
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
::$CD 2
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 MATRIX_1:def 6;
then
A4: width (A+B)=width (B+A) by A2,MATRIX_1:def 6;
A5: len A=len (A+B) by MATRIX_1:def 6;
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,MATRIX_1:def 6
.=( B + A)*(i,j) by A7,A6,A9,MATRIX_1:def 6;
end;
len (A+B)=len (B+A) by A1,A5,MATRIX_1:def 6;
hence thesis by A4,A8,MATRIX_0:21;
end;
theorem
for K being Ring
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 K be Ring;
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 MATRIX_1:def 6;
A6: width (A+B)=width A by MATRIX_1:def 6;
A7: len (A+(B+C))=len A & width (A+(B+C))=width A by MATRIX_1:def 6;
A8: len (A+B)=len A by MATRIX_1:def 6;
A9: len ((A+B)+C)=len (A+B) by MATRIX_1:def 6;
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,MATRIX_1:def 6
.=(A*(i,j) + B*(i,j)) + C*(i,j) by A4,A10,A12,MATRIX_1:def 6
.=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,MATRIX_1:def 6
.=(A + (B + C))*(i,j) by A4,A10,A12,MATRIX_1:def 6;
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 MATRIX_1:def 6;
A3: Indices A=[:Seg n,Seg m:] by A1,MATRIX_0:23;
A4: len A= len (A+0.(K,n,m)) by MATRIX_1:def 6;
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,MATRIX_1:def 6
.=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 MATRIX_1:def 6;
A10: len A= len (A+0.(K,n,m)) by MATRIX_1:def 6;
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 MATRIX_1:def 4;
A2: len (A+ -A)=len A by MATRIX_1:def 6;
A3: width (A+ -A)=width A by MATRIX_1:def 6;
A4: len -A=len A by MATRIX_1:def 4;
A5: now
per cases;
case
A6: n > 0;
then len (A+ -A)=n & width (A + -A) =m by 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) = [:Seg 0,Seg 0 qua set:] by A9,A11;
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,MATRIX_1:def 6;
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 MATRIX_1:def 6
.=A*(i,j)+ (-A*(i,j)) by A15,MATRIX_1:def 4
.=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 non empty doubleLoopStr;
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;
registration
let n,k,m;
let K be non empty doubleLoopStr;
let A be Matrix of n,k,K;
let B be Matrix of width A,m,K;
cluster A*B -> (len A,width B)-size;
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;
registration
let n;
let K be non empty doubleLoopStr;
let A,B be Matrix of n,K;
cluster A*B -> (n,n)-size;
coherence
proof
A1: len A = n & len B = n & width A = n & width B = n by MATRIX_0:24;
then len (A*B)=len A & width (A*B)=width B by Def4;
hence thesis by A1,MATRIX_0:51;
end;
end;
definition
let K be non empty multMagma;
let M be Matrix of K;
let a be Element of K;
func a*M -> Matrix of K means
:Def5:
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 non empty multMagma;
let M be Matrix of K;
let a be Element of K;
func M*a -> Matrix of K means
:Def6:
len it = len M & width it = width M &
for i,j st [i,j] in Indices M holds it*(i,j) = (M*(i,j))*a;
existence
proof
deffunc F(Nat,Nat) = (M*($1,$2))*a;
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)=(M*(i,j))*a 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)=(M*(i,j))*a;
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)=(M*(i,j))*a by A7,A10
.=B*(i,j) by A9,A11,A10;
end;
hence thesis by A5,A6,A8,MATRIX_0:21;
end;
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 Nat
for K being add-associative right_zeroed right_complementable
non empty addLoopStr holds
Sum (n |-> 0.K) = 0.K
proof
let n be 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 holds (j in dom mlt(p,q) implies
(i=j implies mlt(p,q).j = q.i) &
(i<>j implies mlt(p,q).j = 0.K)) & (j in dom mlt(q,p) implies
(i=j implies mlt(q,p).j = q.i) &
(i<>j implies mlt(q,p).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;
thus j in dom mlt(p,q) implies
(i=j implies mlt(p,q).j = q.i) &
(i<>j implies mlt(p,q).j = 0.K)
proof
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;
thus j in dom mlt(q,p) implies
(i=j implies mlt(q,p).j = q.i) &
(i<>j implies mlt(q,p).j = 0.K)
proof
assume
A9: j in dom mlt(q,p);
A10: 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(q,p)) = Seg len (mlt(q,p)) & len (mlt(q,p))=min(len q,len p)
by Th13, FINSEQ_1:def 3;
then
A11: j in (dom q) /\ (dom p) by A9,A10,FINSEQ_2:2;
then
A12: 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(q,p).j=(q.i)
proof
reconsider b=q.j1 as Element of K by A12,FINSEQ_2:11;
assume
A13: i=j;
hence mlt(q,p).j=b*(1.K) by A1,A9,FVSUM_1:60
.=q.i by A13;
end;
assume
A14: i<>j;
j in dom p by A11,XBOOLE_0:def 4;
then p.j=0.K by A2,A14;
hence mlt(q,p).j=b*(0.K) by A9,FVSUM_1:60
.=0.K;
end;
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 & Sum(mlt(q,p)) = 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;
thus Sum(mlt(p,q))=q.i
proof
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;
thus Sum(mlt(q,p))=q.i
proof
reconsider r=mlt(q,p) as FinSequence of K;
A6: for k st k in dom r & k<>i holds r.k=0.K by A2,Th14;
A7: dom p = Seg len p & dom q = Seg len q by FINSEQ_1:def 3;
dom (mlt(q,p)) = Seg len (mlt(q,p)) & len (mlt(q,p))=min(len q,len p)
by Th13,FINSEQ_1:def 3;
then dom q /\ dom p = dom (mlt(q,p)) by A7,FINSEQ_2:2;
then
A8: i in dom r by A1,XBOOLE_0:def 4;
then r.i=q.i by A2,Th14;
hence thesis by A8,A6,Th12;
end;
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 Ring
for A being Matrix of n,K holds A*1.(K,n)=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: width A=n & width B=n by MATRIX_0:24;
then
A3: len (A*B)=len (A) & width(A*B) = width(B) by A1,Def4;
A4: now
let i,j;
assume
A5: [i,j] in Indices (A*B);
then
A6: j in Seg len B & j in Seg width B by A1,A2,A3,ZFMISC_1:87;
then j in Seg len(Col(B,j)) by MATRIX_0:def 8;
then
A7: j in dom (Col(B,j)) by FINSEQ_1:def 3;
dom B = Seg len B by FINSEQ_1:def 3;
then j in dom B by A6;
then [j,j] in [:dom B,Seg width B:] by A6,ZFMISC_1:87;
then [j,j] in Indices B;
then
A8: (Col(B,j)).j=1.K by Th16;
A9: for k st k in dom (Col(B,j)) & k <> j holds (Col(B,j)).k = 0.K
proof
let k;
assume that
A10: k in dom (Col (B,j)) and
A11: k<>j;
k in Seg len (Col (B,j)) by A10,FINSEQ_1:def 3; then
k in dom B by MATRIX_0:def 8, FINSEQ_1:def 3;
then [k,j] in [:dom B,Seg width B:] by A6,ZFMISC_1:87;
then [k,j] in Indices B;
hence (Col(B,j)).k=0.K by A11,Th16;
end;
j in Seg(len (Line(A,i))) by A2,A6,MATRIX_0:def 7;
then
A12: j in dom (Line(A,i)) by FINSEQ_1:def 3;
thus (A*B)*(i,j)= Line(A,i) "*" Col(B,j) by A2,A1,A5,Def4
.=Sum(mlt(Line(A,i),Col(B,j))) by FVSUM_1:def 9
.=Line(A,i).j by A7,A12,A9,A8,Th17
.=A*(i,j) by A2,A6,MATRIX_0:def 7;
end;
width (A*B)=width A by A2,A1,Def4;
hence thesis by A3,A4,MATRIX_0:21;
end;
theorem
for K being Ring
for a,b being Element of K holds <*<*a*>*> * <*<*b*>*> =<*<*a*b*>*>
proof
let K be Ring;
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;
reconsider C as Matrix of 1,K;
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 Ring
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 Ring;
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;
reconsider C as Matrix of 2,K;
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 commutative Ring
for A,B being Matrix of K st width A=len B & width B<>0 holds
(A*B) @ = (B @) * (A @)
proof
let K be commutative Ring;
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:]; :: redefines [: (ZFMISC_1, definition)
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; :: redefines * (FINSEQOP, definition)
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;
Lm2:
for K being Ring
for a being Element of K
for p1,p2 being FinSequence of the carrier of K st
len p1 = len p2 &
(for i being Element of NAT, k being Element of K st
i in dom p1 & k = p1.i holds (p2.i) = k * a) holds
Sum(p2) = (Sum p1) * a
proof
let K be Ring;
let a be Element of K;
defpred P[FinSequence of the carrier of K] means
for p2 being FinSequence of the carrier of K st
len $1 = len p2 &
(for i being Element of NAT, k being Element of K st
i in dom $1 & k = $1.i holds (p2.i) = k * a) holds
Sum(p2) = (Sum $1) * a;
A1: P[ <*> the carrier of K ]
proof
A2: Sum(<*> the carrier of K) = 0.K by RLVECT_1:43;
now
let p2 be FinSequence of the carrier of K;
assume len (<*> the carrier of K) = len p2;
then p2 = <*> the carrier of K;
hence Sum(p2) = Sum(<*> the carrier of K) * a by A2;
end;
hence thesis;
end;
A3: for p being FinSequence of the carrier of K
for x being Element of the carrier of K st P[p] holds
P[p ^ <*x*>]
proof
let p be FinSequence of the carrier of K;
let x be Element of the carrier of K;
assume A4: P[p];
for p2 being FinSequence of the carrier of K st
(len (p ^ <*x*>) = len p2) & (for i being Element of NAT,
k being Element of K st i in dom (p ^ <*x*>) &
k = (p ^ <*x*>).i holds (p2.i) = k * a) holds
Sum(p2) = (Sum (p ^ <*x*>)) * a
proof
let p2 be FinSequence of the carrier of K;
assume that
A5: len (p ^ <*x*>) = len p2 and
A6: for i being Element of NAT,
k being Element of K st i in dom (p ^ <*x*>) &
k = (p ^ <*x*>).i holds (p2.i) = k * a;
len p2 <> 0 by A5;
then consider q being FinSequence of the carrier of K,
d being Element of K such that
A7: p2 = q ^ <* d *> by FINSEQ_2:19;
(len q) + 1 = len p2 by A7,FINSEQ_2:16
.= (len p) + 1 by A5, FINSEQ_2:16;
then
A8: len p = len q by XCMPLX_1:2;
for i being Element of NAT, k being Element of K
st i in dom p & k = p.i holds q.i = k * a
proof
let i be Element of NAT;
let k be Element of K;
assume that
A9: i in dom p and
A10: k = p.i;
A11: i in dom (p ^ <*x*>) by A9,FINSEQ_2:15;
i in Seg (len p) by A9, FINSEQ_1:def 3; then
A12: 1 <= i & i <= len p by FINSEQ_1:1;
then
A13: (p ^ <*x*>).i= k by A10, FINSEQ_1:64;
thus q.i = (q ^ <*d*>).i by A12,A8,FINSEQ_1:64
.= k * a by A7,A13,A6,A11;
end; then
A14: Sum q = (Sum p) * a by A4,A8;
set p1 = p ^ <*x*>;
reconsider i1 = (len p) + 1 as Element of NAT;
len <*x*> = 1 by FINSEQ_1:40;
then dom <*x*> = Seg 1 by FINSEQ_1:def 3;
then 1 in dom <*x*> by FINSEQ_1:3;
then (len p) + 1 in dom (p1) & x = p1.((len p) + 1) by FINSEQ_1:28,42;
then i1 in dom p1 & x = p1.i1;
then
A15: p2.i1 = x * a by A6;
d = p2.i1 by A7,A8,FINSEQ_1:42;
then
A16: d = x*a by A15;
thus Sum(p2) = (Sum q) + d by A7,FVSUM_1:71
.= ((Sum p) + x) * a by A14, A16, VECTSP_1:def 3
.= (Sum (p ^ <*x*>)) * a by FVSUM_1:71;
end;
hence P[p ^ <*x*>];
end;
thus for p being FinSequence of the carrier of K holds P[p]
from FINSEQ_2:sch 2(A1,A3);
end;
theorem
for K being 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 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;
A6: len (A*(B*C))=len A by A3,Def4;
then
A7: Indices (A*(B*C))=[:dom A,Seg width C:] by A5,FINSEQ_3:29;
A8: width (A*B)=len C by A1,A2,Def4;
then
A9: width ((A*B)*C)=width C by Def4;
len (A*B)=len A by A1,Def4;
then
A10: len ((A*B)*C)=len A by A8,Def4;
then
A11: Indices((A*B)*C)=[:dom A,Seg width C:] by A9,FINSEQ_3:29;
A12: width ((A*B)*C) = width(A*(B*C)) by A5,A8,Def4;
A13: len ((A*B)*C) = len(A*(B*C)) by A6,A10;
for i,j being Nat st [i,j] in Indices ((A*B)*C) holds
((A*B)*C) * (i,j) = (A*(B*C)) * (i,j)
proof
let i,j be Nat;
assume [i,j] in Indices ((A*B)*C);
then
A14: [i,j] in Indices ((A*B)*C) & [i,j] in Indices (A*(B*C)) by A7,A11;
reconsider X=findom B as Element of Fin NAT;
reconsider Y=findom C as Element of Fin NAT;
deffunc F(Element of NAT ,Element of NAT) =
(A* (i,$1))*((B* ($1,$2))*(C* ($2,j)));
consider f being Function of [:NAT,NAT:],the carrier of K such that
A15: for k1 being Element of NAT for k2 being Element of NAT holds f.(
k1,k2) = F(k1,k2) from BINOP_1:sch 4;
A16: for k be Element of NAT st k in NAT holds
((curry f).k) | (dom C) = (A*(i,k)) * (mlt(Line(B,k),Col(C,j)))
proof
let k be Element of NAT;
assume k in NAT;
A17: {k} c= NAT by ZFMISC_1:31;
A18: dom (curry f) = NAT by FUNCT_2:def 1;
dom f = [:NAT,NAT:] by FUNCT_2:def 1;
then
A19: dom ((curry f) . k) = proj2 ([:NAT,NAT:] /\ [:{k},(proj2 [:NAT,NAT:]):])
by A18, FUNCT_5:31
.= proj2 ([:{k},NAT:] /\ [:NAT,NAT:]) by FUNCT_5:9
.= proj2 [:{k},NAT:] by A17, ZFMISC_1:101
.= NAT by FUNCT_5:9;
then
A20: dom (((curry f).k) | (dom C)) = NAT /\ (dom C) by RELAT_1:61
.= dom C by XBOOLE_1:28;
reconsider a = A * (i,k) as Element of K;
reconsider p = mlt ((Line (B,k)),(Col (C,j))) as FinSequence of K;
A21: len (mlt ((Line (B,k)),(Col (C,j)))) =
len ((the multF of K) .: ((Line (B,k)),(Col (C,j)))) by FVSUM_1:def 7;
len (Line (B,k)) = len C by A2, MATRIX_0:def 7
.= len (Col (C,j)) by MATRIX_0:def 8;
then
A22: 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
A23: dom (a * p) = dom p by RELAT_1:27;
then
A24: dom ((A*(i,k)) * (mlt(Line(B,k),Col(C,j)))) =
dom C by A21,A22, FINSEQ_3:29;
for l being object st l in dom C
holds (((curry f).k) | (dom C)).l =
((A*(i,k)) * (mlt(Line(B,k),Col(C,j)))).l
proof
let l be object;
assume
A25: l in dom C;
then reconsider l9 = l as Element of NAT;
A26: l in dom(a * p) by A21,A22,A23,A25,FINSEQ_3:29;
l9 in dom (p) by A21,A22,A25,FINSEQ_3:29;
then reconsider b = p.l9 as Element of K by FINSEQ_2:11;
dom ((the multF of K) .: ((Line (B,k)),(Col (C,j)))) =
Seg (len ((the multF of K) .: ((Line (B,k)),(Col (C,j)))))
by FINSEQ_1:def 3;
then
A27: l9 in dom ((the multF of K) .: ((Line (B,k)),(Col (C,j))))
by A22,A25,FINSEQ_1:def 3;
A28: Seg len C = dom C by FINSEQ_1:def 3;
thus (((curry f).k) | (dom C)).l = ((curry f).k).l9 by A25,FUNCT_1:49
.= f.(k,l9) by A18,A19,FUNCT_5:31
.= (A * (i,k)) * ((B * (k,l9)) * (C * (l9,j))) by A15
.= (the multF of K).(A * (i,k),
(the multF of K).((Line(B,k)).l9, C * (l9,j)))
by A2,A28,A25, MATRIX_0:def 7
.= (the multF of K).(A * (i,k), (the multF of K).((Line(B,k)).l9,
(Col(C,j)).l9)) by A25, MATRIX_0:def 8
.= (the multF of K).(A * (i,k),
((the multF of K) .: ((Line(B,k)), (Col(C,j)))).l9)
by A27, FUNCOP_1:22
.= a * b by FVSUM_1:def 7
.= ((A*(i,k)) * (mlt(Line(B,k),Col(C,j)))).l
by A26, FVSUM_1:50;
end;
hence ((curry f).k) | (dom C) = (A*(i,k)) * (mlt(Line(B,k),Col(C,j)))
by A20, A24, FUNCT_1:2;
end;
deffunc H2(Element of NAT) = (the addF of K) $$ (Y,((curry f) . $1));
deffunc H3(Element of NAT) = (the addF of K) $$ (X,((curry' f) . $1));
consider g being sequence of the carrier of K such that
A29: for k being Element of NAT holds g . k = H2(k)
from FUNCT_2:sch 4;
A30: dom (g | (dom B)) = (dom g) /\ (dom B) by RELAT_1:61
.= NAT /\ (dom B) by FUNCT_2:def 1
.= dom B 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
A31: 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;
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
A32: 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;
A33: i in dom A by A11,A14,ZFMISC_1:87;
A34: 0. K = the_unity_wrt the addF of K by FVSUM_1:7;
0.K is_a_unity_wrt the addF of K by FVSUM_1:6;
then
A35: the addF of K is having_a_unity by SETWISEO:def 2;
A36: for k9 being object st k9 in dom B
holds (g | (dom B)).k9 = (mlt(Line(A, i), Col(B * C, j))).k9
proof
let k9 be object;
assume
A37: k9 in dom B;
then reconsider k = k9 as Element of NAT;
A38: k in dom ((the multF of K) .: (Line(A,i), Col(B * C,j)))
by A1,A32,A37,FINSEQ_3:29;
reconsider p = mlt(Line(B,k),Col(C,j)) as FinSequence of K;
reconsider a = A * (i,k) 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
A39: dom (a * p) = dom p by RELAT_1:27;
len (Line (B,k)) = len C by A2,MATRIX_0:def 7
.= len (Col (C,j)) by MATRIX_0:def 8;
then 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;
then len C = len p by FVSUM_1:def 7;
then
A40: dom ((A * (i,k)) * (mlt (Line(B,k),Col(C,j)))) = dom C
by A39, FINSEQ_3:29;
then ([#] (((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:21;
then
A41: ([#] (((A * (i,k)) * (mlt (Line(B,k),Col(C,j)))), 0.K))
| (dom C) = ((curry f).k) | (dom C) by A16;
[i,j] in Indices (A*(B*C)) by A14;
then j in Seg (width C) by A5,ZFMISC_1:87;
then
A42: j in Seg (width (B * C)) by A4;
dom(B*C)=dom B by A1,A3,FINSEQ_3:29;
then k in dom(B*C) by A37;
then
A43: [k,j] in Indices(B * C) by A42,ZFMISC_1:87;
k in Seg (width A) by A1,A37,FINSEQ_1:def 3;
then i in dom A & k in Seg (width A) by A33;
then
A44: A * (i,k) = (Line(A,i)).k by MATRIX_0:def 7;
dom(B*C)=dom B by A1,A3,FINSEQ_3:29;
then k in dom (B * C) & j in Seg (width (B * C)) by A37,A42;
then
A45: (B * C) * (k,j) = (Col(B * C,j)).k by MATRIX_0:def 8;
thus (g | (dom B)).k9 = g.k by A30,A37,FUNCT_1:47
.= (the addF of K) $$ (Y,((curry f).k)) by A29
.= (the addF of K) $$ (Y,([#] (((A * (i,k)) *
(mlt (Line(B,k),Col(C,j)))), 0.K))) by A41, FVSUM_1:8, SETWOP_2:7
.= (the addF of K) $$ (a * p) by A40,A35,A34,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,A43,Def4
.= ((the multF of K) .: (Line(A,i), Col(B * C,j))).k
by A38, A44, A45, FUNCOP_1:22
.= (mlt(Line(A, i), Col(B * C, j))).k9 by FVSUM_1:def 7;
end;
consider h being sequence of the carrier of K such that
A46: for l being Element of NAT holds h . l = H3(l)
from FUNCT_2:sch 4;
A47: dom (h | (dom C)) = (dom h) /\ (dom C) by RELAT_1:61
.= NAT /\ (dom C) by FUNCT_2:def 1
.= dom C by XBOOLE_1:28 ;
A48: for l9 being object st l9 in dom C
holds (h | (dom C)).l9 = (mlt(Line(A * B, i), Col(C, j))).l9
proof
let l9 be object;
assume
A49: l9 in dom C;
then reconsider l = l9 as Element of NAT;
A50: for k being Element of NAT
holds ((curry' f).l).k = ((A*(i,k)*(B*(k,l))) * (C*(l,j)))
proof
let k be Element of NAT;
thus ((curry' f).l).k = f.(k,l) by FUNCT_5:70
.= (A*(i,k)) * ((B*(k,l))*(C*(l,j))) by A15
.= (A*(i,k)*(B*(k,l))) * (C*(l,j)) by GROUP_1:def 3;
end;
reconsider p1=mlt(Line(A,i),Col(B,l)) as FinSequence of the carrier of K;
A51: len(Line(A,i)) = len B by A1,MATRIX_0:def 7
.= len(Col(B,l)) by MATRIX_0:def 8;
A52: len (mlt(Line(A,i),Col(B,l))) =
len ((the multF of K) .: (Line(A,i),Col(B,l))) by FVSUM_1:def 7
.= len (Line(A,i)) by A51,FINSEQ_2:72
.= len B by A1, MATRIX_0:def 7;
dom B = Seg (len B) by FINSEQ_1:def 3;
then reconsider p2 = (((curry' f).l)) | (dom B)
as FinSequence of K by FINSEQ_2:27;
A53: dom p2 = (dom ((curry' f).l)) /\ (dom B) by RELAT_1:61
.= NAT /\ (dom B) by FUNCT_2:def 1
.= dom B by XBOOLE_1:28;
then
A54: findom p2 = X;
then
A55: len p1 = len p2 by A52,FINSEQ_3:29;
A56: [#](p2, 0.K) | (dom B) = p2 by A53,SETWOP_2:21;
for i2 being Element of NAT
for k being Element of K
st i2 in dom p1 & k = p1.i2
holds p2.i2 = k * (C*(l,j))
proof
let i2 be Element of NAT;
let k be Element of K;
assume that
A57: i2 in dom p1 and
A58: k = p1.i2;
A59: i2 in dom(mlt(Line(A,i),Col(B,l))) by A57;
A60: A*(i,i2) = Line(A,i).i2 & Col(B,l).i2 = B*(i2,l)
proof
A61: len (Line(A,i)) = width A by MATRIX_0:def 7
.= len (Col(B,l)) by A1, MATRIX_0:def 8;
width A = len (Line(A,i)) by MATRIX_0:def 7
.= len((the multF of K) .: (Line(A,i),Col(B,l))) by A61,FINSEQ_2:72
.= len (mlt(Line(A,i),Col(B,l))) by FVSUM_1:def 7;
then
A62: i2 in Seg(width A) by A57,FINSEQ_1:def 3;
hence A*(i,i2) = Line(A,i).i2 by MATRIX_0:def 7;
width A = len B by A1;
then Seg(width A) = Seg(len B);
then i2 in Seg(len B) by A62;
then i2 in dom B by FINSEQ_1:def 3;
hence Col(B,l).i2 = B*(i2,l) by MATRIX_0:def 8;
end;
p1.i2 = (A*(i,i2)) * (B*(i2,l)) by A60,A59,FVSUM_1:60;
then
A63: k = (A*(i,i2)) * (B*(i2,l)) by A58;
dom p1 = dom p2 by A55,FINSEQ_3:29;
then i2 in dom p2 by A57;
then
A64: i2 in dom B by A53;
thus p2.i2 = ((curry' f).l).i2 by A64, FUNCT_1:49
.= k * (C*(l,j)) by A63,A50;
end;
then
A65: Sum(p2) = (Sum p1) * (C*(l,j)) by A55,Lm2;
width(A*B) = width B by A1,Def4;
then
A66: Seg(width(A*B)) = dom C by A2, FINSEQ_1:def 3;
then
A67: l in Seg(width(A*B)) by A49;
A68: [i,l] in Indices(A*B)
proof
dom A = Seg(len A) by FINSEQ_1:def 3
.= Seg (len (A*B)) by A1,Def4
.= dom(A*B) by FINSEQ_1:def 3;
then i in dom (A*B) by A33;
hence thesis by A67, ZFMISC_1:87;
end;
A69: ((A * B) * (i,l)) * (C*(l,j)) = mlt(Line(A*B,i),Col(C,j)).l
proof
A70: (A*B)*(i,l)=Line(A*B,i).l by A67, MATRIX_0:def 7;
A71: C*(l,j) = Col(C,j).l by A67,A66,MATRIX_0:def 8;
A72: len(Line(A*B,i)) = width(A*B) by MATRIX_0:def 7
.= len(Col(C,j)) by A8, MATRIX_0:def 8;
len C = len (Col(C,j)) by MATRIX_0:def 8
.= len ((the multF of K) .: (Line(A*B,i),Col(C,j)))
by A72,FINSEQ_2:72
.= len (mlt(Line(A*B,i),Col(C,j))) by FVSUM_1:def 7;
then l in dom(mlt(Line(A*B,i),Col(C,j))) by A49,FINSEQ_3:29;
hence thesis by A70,A71,FVSUM_1:60;
end;
thus (h | (dom C)).l9 = h.l by A47,A49,FUNCT_1:47
.= (the addF of K) $$ (X,((curry' f) . l)) by A46
.= (the addF of K) $$ (X,[#](p2, 0.K)) by A56, FVSUM_1:8, SETWOP_2:7
.= (the addF of K) $$ (p2) by A34,A54, FVSUM_1:8, SETWOP_2:def 2
.= Sum p2 by FVSUM_1:def 8
.= (Line(A,i) "*" Col(B,l)) * (C*(l,j)) by A65,FVSUM_1:def 9
.= mlt(Line(A*B,i), Col(C,j)).l9 by A1,A68,A69,Def4;
end;
A73: 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
A74: dom (mlt ((Line (A,i)),(Col ((B * C),j)))) = X
by A1, A32, FINSEQ_3:29;
A75: dom (mlt ((Line (A,i)),(Col ((B * C),j)))) = dom B
by A1, A32, A73, FINSEQ_3:29;
then
A76: ([#] ((mlt ((Line (A,i)),(Col ((B * C),j)))),(0. K))) | (dom B) =
mlt ((Line (A,i)),(Col ((B * C),j))) by SETWOP_2:21;
A77: g | (dom B) = mlt ((Line(A,i)),(Col(B*C, j))) by A30,A36,A75, FUNCT_1:2;
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
A78: dom C = dom (mlt ((Line ((A * B),i)),(Col (C,j)))) by A31, FINSEQ_3:29;
then
A79: h | (dom C) = mlt (Line(A * B, i), Col(C,j)) by A47, A48, FUNCT_1:2;
A80: 0. K = the_unity_wrt the addF of K by FVSUM_1:7;
dom (mlt ((Line ((A * B),i)),(Col (C,j)))) = dom C by A78;
then
A81: ([#] ((mlt ((Line ((A * B),i)),(Col (C,j)))),(0. K))) | (dom C) =
mlt ((Line ((A * B),i)),(Col (C,j))) by SETWOP_2:21;
thus ((A * B) * C) * (i,j) = (Line ((A * B),i)) "*" (Col (C,j))
by A8,A14,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 A35,A80,A78,SETWOP_2:def 2
.= (the addF of K) $$ (Y,h) by A35, A81, A79, SETWOP_2:7
.= (the addF of K) $$ ([:X,Y:],f) by A35, A46, Th32
.= (the addF of K) $$ (X,g) by A35, A29, Th30
.= (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 A35, A80, A74,A76, A77, SETWOP_2:7
.= (the addF of K) $$ (mlt ((Line (A,i)),(Col ((B * C),j))))
by A35, 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, A14, Def4;
end;
hence thesis by A12,A13,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 16;
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 16;
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 16;
A2: -(a,p)=a
proof
reconsider q = id Seg 1 as Element of Permutations(1) by MATRIX_1:def 16;
len Permutations 1 = 1 by MATRIX_1:9;
then q is even by MATRIX_1:16;
hence thesis by MATRIX_1:def 20;
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;
theorem
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 by Lm1;
:: inserted 2025-05-11
theorem Lm100:
for K being commutative non empty multMagma
for M being Matrix of K
for a being Element of K
holds a*M = M*a
proof
let K be commutative non empty multMagma;
let M be Matrix of K;
let a be Element of K;
A1: len (a*M) = len M by Def5
.= len (M*a) by Def6;
A2: width (a*M) = width M by Def5
.= width (M*a) by Def6;
for i,j being Nat st [i,j] in Indices (a*M)
holds (a*M) * (i,j) = (M*a) * (i,j)
proof
let i,j be Nat;
assume A3: [i,j] in Indices (a*M);
A4: [i,j] in Indices M
proof
A5: dom (a*M) = Seg (len (a*M)) by FINSEQ_1:def 3
.= Seg (len M) by Def5
.= dom M by FINSEQ_1:def 3;
width (a*M) = width M by Def5;
then [:dom(M),Seg(width M):] = Indices (a*M) by A5;
then Indices M = Indices(a*M);
hence thesis by A3;
end;
thus (a*M) * (i,j) = a * (M*(i,j)) by A4,Def5
.= (M*a) * (i,j) by A4,Def6;
end;
hence a*M = M*a by A1,A2,MATRIX_0:21;
end;
:: inserted 2025-05-11
definition
let K be commutative non empty multMagma;
let M be Matrix of K;
let a be Element of K;
redefine func M*a -> Matrix of K equals a*M; :: redefines * (MATRIX_3, definition)
correctness by Lm100;
end;
:: inserted 2025-05-11
registration
let m,n be Nat;
let K be non empty multMagma;
let M be Matrix of m,n,K;
let a be Element of K;
cluster a*M -> (m,n)-size;
coherence
proof
A1: len (a * M) = len M by Def5
.= m by MATRIX_0:25;
for p being FinSequence of the carrier of K
st p in rng (a * M) holds len p = n
proof
let p be FinSequence of the carrier of K;
assume A2: p in rng (a * M);
then consider i being object such that
A3: i in dom (a * M) & p = (a * M).i by FUNCT_1:def 3;
per cases;
suppose len M = 0;
then len (a * M) = 0 by Def5;
then Seg (len (a * M)) = {};
then dom (a * M) = {} by FINSEQ_1:def 3;
hence thesis by A3;
end;
suppose A4: len M > 0;
then a4: len (a * M) > 0 by Def5;
len M = m by MATRIX_0:25;
then A6: len (a*M) = m by Def5;
m > 0 by A4, MATRIX_0:25;
then width M = n by MATRIX_0:23;
then width (a*M) = n by Def5;
then a*M is Matrix of m,n,the carrier of K by a4,A6,MATRIX_0:20;
then a*M is m,n-size;
hence thesis by A2,MATRIX_0:def 2;
end;
end;
hence thesis by A1, MATRIX_0:def 2;
end;
cluster M*a -> (m,n)-size;
coherence
proof
A1: len (M * a) = len M by Def6
.= m by MATRIX_0:25;
for p being FinSequence of the carrier of K
st p in rng (M * a) holds len p = n
proof
let p be FinSequence of the carrier of K;
assume A2: p in rng (M * a);
then consider i being object such that
A3: i in dom (M * a) & p = (M * a).i by FUNCT_1:def 3;
per cases;
suppose len M = 0;
then len (M * a) = 0 by Def6;
then Seg (len (M * a)) = {};
then dom (M * a) = {} by FINSEQ_1:def 3;
hence thesis by A3;
end;
suppose A4: len M > 0;
then a4: len (M * a) > 0 by Def6;
len M = m by MATRIX_0:25;
then A6: len (M*a) = m by Def6;
m > 0 by A4, MATRIX_0:25;
then width M = n by MATRIX_0:23;
then width (M*a) = n by Def6;
then M*a is Matrix of m,n,the carrier of K by a4,A6,MATRIX_0:20;
then M*a is m,n-size;
hence thesis by A2,MATRIX_0:def 2;
end;
end;
hence thesis by A1, MATRIX_0:def 2;
end;
end;
registration
let K be well-unital non empty multLoopStr_0;
let A be Matrix of K;
reduce (1.K)*A to A;
reducibility
proof
A1: len A = len A & width A = width A;
for i,j being Nat st [i,j] in Indices A holds A*(i,j) = (1.K)*(A*(i,j));
hence thesis by A1,Def5;
end;
reduce A*(1.K) to A;
reducibility
proof
A1: len A = len A & width A = width A;
for i,j being Nat st [i,j] in Indices A holds A*(i,j) = (A*(i,j))*(1.K);
hence thesis by A1,Def6;
end;
end;
theorem
for K being add-associative right_zeroed right_complementable
well-unital left-distributive non empty doubleLoopStr
for A being Matrix of K holds (-1.K)*A = -A
proof
let K be add-associative right_zeroed right_complementable
well-unital left-distributive non empty doubleLoopStr;
let A be Matrix of K;
A1: len -A = len A & width -A = width A by MATRIX_1:def 4;
now
let i,j be Nat;
assume [i,j] in Indices A;
hence (-A)*(i,j) = -(1.K*(A*(i,j))) by MATRIX_1:def 4
.= (-1.K)*(A*(i,j)) by VECTSP_1:9;
end;
hence thesis by A1,Def5;
end;
theorem
for K being add-associative right_zeroed right_complementable
well-unital right-distributive non empty doubleLoopStr
for A being Matrix of K holds A*(-1.K) = -A
proof
let K be add-associative right_zeroed right_complementable
well-unital right-distributive non empty doubleLoopStr;
let A be Matrix of K;
A1: len -A = len A & width -A = width A by MATRIX_1:def 4;
now
let i,j be Nat;
assume [i,j] in Indices A;
hence (-A)*(i,j) = -((A*(i,j))*1.K) by MATRIX_1:def 4
.= (A*(i,j))*(-1.K) by VECTSP_1:8;
end;
hence thesis by A1,Def6;
end;