:: The Product of Matrices of Elements of a Field and Determinants
:: by Katarzyna Zawadzka
::
:: Received May 17, 1993
:: Copyright (c) 1993-2016 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;
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
:: MATRIX_3:def 1
n |-> (m |-> 0.K);
end;
definition
let K be Ring;
let A be Matrix of K;
func -A -> Matrix of K means
:: MATRIX_3:def 2
len it= len A & width it =width A & for
i,j holds [i,j] in Indices A implies it*(i,j)= -(A*(i,j));
end;
definition
let K be Ring;
let A,B be Matrix of K;
func A+B -> Matrix of K means
:: MATRIX_3:def 3
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);
end;
theorem :: MATRIX_3:1
for i,j st [i,j] in Indices (0.(K,n,m)) holds (0.(K,n,m))*(i,j)= 0.K;
theorem :: MATRIX_3:2
for A,B being Matrix of K st len A= len B & width A=width B holds A +
B = B + A;
theorem :: MATRIX_3:3
for A,B,C being Matrix of K st len A=len B & width A=width B holds (A
+ B) + C= A + (B + C);
theorem :: MATRIX_3:4
for A being Matrix of n,m,K holds A + 0.(K,n,m)= A;
theorem :: MATRIX_3:5
for A being Matrix of n,m,K holds A + (-A) = 0.(K,n,m);
definition
let K be Ring;
let A,B be Matrix of K;
assume
width A=len B;
func A*B -> Matrix of K means
:: MATRIX_3:def 4
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);
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;
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
:: MATRIX_3:def 5
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));
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
:: MATRIX_3:def 6
a*M;
end;
theorem :: MATRIX_3:6
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;
theorem :: MATRIX_3:7
for i,l st [i,l] in Indices (1.(K,n)) & l=i holds (Line(1.(K,n),i)).l= 1.K;
theorem :: MATRIX_3:8
for i,l st [i,l] in Indices (1.(K,n)) & l<>i holds (Line(1.(K,n),i)).l =0.K;
theorem :: MATRIX_3:9
for l,j st [l,j] in Indices (1.(K,n)) & l=j holds (Col(1.(K,n),j)).l= 1.K;
theorem :: MATRIX_3:10
for l,j st [l,j] in Indices (1.(K,n)) & l<>j holds (Col(1.(K,n),j)).l= 0.K;
theorem :: MATRIX_3:11
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;
theorem :: MATRIX_3:12
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;
theorem :: MATRIX_3:13
for p,q being FinSequence of K holds len (mlt(p,q))=min(len p, len q);
theorem :: MATRIX_3:14
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);
theorem :: MATRIX_3:15
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);
theorem :: MATRIX_3:16
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);
theorem :: MATRIX_3:17
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;
theorem :: MATRIX_3:18
for K being Ring
for A being Matrix of n,K holds 1.(K,n)*A=A;
theorem :: MATRIX_3:19
for K being commutative Ring
for A being Matrix of n,K holds A*(1.(K,n))=A;
theorem :: MATRIX_3:20
for K being Field
for a,b being Element of K holds <*<*a*>*> * <*<*b*>*> =<*<*a*b*>*>;
theorem :: MATRIX_3:21
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);
theorem :: MATRIX_3:22
for K being Field
for A,B being Matrix of K st width A=len B & width B<>0 holds (A*B) @=
(B @)*(A @);
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:];
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;
end;
theorem :: MATRIX_3:23
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));
theorem :: MATRIX_3:24
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)));
theorem :: MATRIX_3:25
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)));
theorem :: MATRIX_3:26
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)));
theorem :: MATRIX_3:27
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));
theorem :: MATRIX_3:28
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));
theorem :: MATRIX_3:29
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);
theorem :: MATRIX_3:30
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);
theorem :: MATRIX_3:31
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);
theorem :: MATRIX_3:32
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);
theorem :: MATRIX_3:33
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);
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
:: MATRIX_3:def 7
len it=n & for i,j st i in dom it & j=p.i holds it.i=M*(i,j);
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
:: MATRIX_3:def 8
for p being Element of Permutations(n) holds it.p = -((the multF of K)
$$ Path_matrix(p,M),p);
end;
definition
let n;
let K be Ring;
let M be Matrix of n,K;
func Det M -> Element of K equals
:: MATRIX_3:def 9
(the addF of K) $$ (In(Permutations(n), Fin Permutations n),Path_product(M));
end;
reserve a for Element of K;
theorem :: MATRIX_3:34
for K be Ring,
a being Element of K holds
Det <*<*a*>*> =a;
definition
let n;
let K;
let M be Matrix of n,K;
func diagonal_of_Matrix M -> FinSequence of K means
:: MATRIX_3:def 10
len it = n & for i st i in Seg n holds it.i=M*(i,i);
end;