Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### The abstract of the Mizar article:

### Matrices. Abelian Group of Matrices

**by****Katarzyna Jankowska**- Received June 8, 1991
- MML identifier: MATRIX_1

- [ Mizar article, MML identifier index ]

environ vocabulary VECTSP_1, FINSEQ_1, RLVECT_1, RELAT_1, BOOLE, FINSEQ_2, FUNCOP_1, CARD_1, TREES_1, FUNCT_1, QC_LANG1, INCSP_1, GROUP_1, ARYTM_1, BINOP_1, MATRIX_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, NAT_1, STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FUNCOP_1, FINSEQ_2, BINOP_1, FINSEQOP, RLVECT_1, VECTSP_1, CARD_1; constructors BINOP_1, FINSEQOP, VECTSP_1, XREAL_0, XCMPLX_0, MEMBERED, XBOOLE_0; clusters FINSEQ_1, VECTSP_1, STRUCT_0, FINSEQ_2, RELSET_1, GROUP_1, ARYTM_3, RELAT_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements NUMERALS, SUBSET, BOOLE; begin reserve x,y,z,y1,y2 for set, i,j,k,l,n,m for Nat, D for non empty set, K for non empty doubleLoopStr, s,t,v for FinSequence, a,a1,a2,b1,b2,d for Element of D, p,p1,p2,q,r for FinSequence of D, F for add-associative right_zeroed right_complementable Abelian (non empty doubleLoopStr); definition let f be FinSequence; attr f is tabular means :: MATRIX_1:def 1 ex n being Nat st for x st x in rng f ex s st s=x & len s = n; end; definition cluster tabular FinSequence; end; theorem :: MATRIX_1:1 <*<*d*>*> is tabular; theorem :: MATRIX_1:2 m |-> (n |-> x) is tabular; theorem :: MATRIX_1:3 for s holds <*s*> is tabular; theorem :: MATRIX_1:4 for s1,s2 be FinSequence st len s1 =n & len s2 = n holds <*s1,s2*> is tabular ; theorem :: MATRIX_1:5 {} is tabular; theorem :: MATRIX_1:6 <*{},{}*> is tabular; theorem :: MATRIX_1:7 <*<*a1*>,<*a2*>*> is tabular; theorem :: MATRIX_1:8 <*<*a1,a2*>,<*b1,b2*>*> is tabular; definition let f be Relation; attr f is empty-yielding means :: MATRIX_1:def 2 for s being set st s in rng f holds Card s = 0; end; definition let D be set; cluster tabular FinSequence of D*; end; definition let D be set; mode Matrix of D is tabular FinSequence of D*; end; definition let D be non empty set; cluster non empty-yielding Matrix of D; end; theorem :: MATRIX_1:9 s is Matrix of D iff ex n st for x st x in rng s ex p st x = p & len p = n; definition let D,m,n; mode Matrix of m,n,D -> Matrix of D means :: MATRIX_1:def 3 len it = m & for p st p in rng it holds len p = n; end; definition let D,n; mode Matrix of n,D is Matrix of n,n,D; end; definition let K be non empty 1-sorted; mode Matrix of K is Matrix of the carrier of K; let n; mode Matrix of n,K is Matrix of n,n,the carrier of K; let m; mode Matrix of n,m,K is Matrix of n,m,the carrier of K; end; theorem :: MATRIX_1:10 m |-> (n |-> a) is Matrix of m,n,D; theorem :: MATRIX_1:11 for p being FinSequence of D holds <*p*> is Matrix of 1,len p,D; theorem :: MATRIX_1:12 for p1,p2 st len p1 =n & len p2 = n holds <*p1,p2*> is Matrix of 2,n,D; theorem :: MATRIX_1:13 {} is Matrix of 0,m,D; theorem :: MATRIX_1:14 <*{}*> is Matrix of 1,0,D; theorem :: MATRIX_1:15 <*<*a*>*> is Matrix of 1,D; theorem :: MATRIX_1:16 <*{},{}*> is Matrix of 2,0,D; theorem :: MATRIX_1:17 <*<*a1,a2*>*> is Matrix of 1,2,D; theorem :: MATRIX_1:18 <*<*a1*>,<*a2*>*> is Matrix of 2,1,D; theorem :: MATRIX_1:19 <*<*a1,a2*>,<*b1,b2*>*> is Matrix of 2,D; reserve M,M1,M2 for Matrix of D; definition let M be tabular FinSequence; func width M -> Nat means :: MATRIX_1:def 4 ex s st s in rng M & len s = it if len M > 0 otherwise it = 0; end; theorem :: MATRIX_1:20 len M > 0 implies for n holds M is Matrix of len M, n, D iff n = width M; definition let M be tabular FinSequence; func Indices M -> set equals :: MATRIX_1:def 5 [:dom M,Seg width M:]; end; definition let D be set; let M be Matrix of D; let i,j; assume [i,j] in Indices M; func M*(i,j) -> Element of D means :: MATRIX_1:def 6 ex p being FinSequence of D st p= M.i & it =p.j; end; theorem :: MATRIX_1:21 len M1 =len M2 & width M1= width M2 & (for i,j st [i,j] in Indices M1 holds M1*(i,j) = M2*(i,j)) implies M1 = M2; scheme MatrixLambda { D() -> non empty set, n() -> Nat, m() -> Nat, f(set,set) -> Element of D()} : ex M being Matrix of n(),m(),D() st for i,j st [i,j] in Indices M holds M*(i,j) = f(i,j); scheme MatrixEx { D() -> non empty set, n() -> Nat, m() -> Nat, P[set,set,set] } : ex M being Matrix of n(),m(),D() st for i,j st [i,j] in Indices M holds P[i,j,M*(i,j)] provided for i,j st [i,j] in [:Seg n(), Seg m():] for x1,x2 being Element of D() st P[i,j,x1] & P[i,j,x2] holds x1 = x2 and for i,j st [i,j] in [:Seg n(), Seg m():] ex x being Element of D() st P[i,j,x]; canceled; theorem :: MATRIX_1:23 for M being Matrix of 0,m,D holds len M=0 & width M = 0 & Indices M = {}; theorem :: MATRIX_1:24 n > 0 implies for M being Matrix of n,m,D holds len M=n & width M = m & Indices M = [:Seg n, Seg m:]; theorem :: MATRIX_1:25 for M being Matrix of n,D holds len M=n & width M =n & Indices M = [:Seg n, Seg n:]; theorem :: MATRIX_1:26 for M being Matrix of n,m,D holds len M = n & Indices M=[:Seg n,Seg width M:]; theorem :: MATRIX_1:27 for M1,M2 being Matrix of n,m,D holds Indices M1=Indices M2; theorem :: MATRIX_1:28 for M1,M2 being Matrix of n,m,D st (for i,j st [i,j] in Indices M1 holds M1*(i,j) = M2*(i,j)) holds M1 = M2; theorem :: MATRIX_1:29 for M1 being Matrix of n,D holds for i,j st [i,j] in Indices M1 holds [j,i] in Indices M1; definition let D; let M be Matrix of D; func M@ -> Matrix of D means :: MATRIX_1:def 7 len it = width M & (for i,j holds [i,j] in Indices it iff [j,i] in Indices M) & for i,j st [j,i] in Indices M holds it*(i,j) = M*(j,i); end; definition let D,M,i; func Line(M,i) -> FinSequence of D means :: MATRIX_1:def 8 len it = width M & for j st j in Seg width M holds it.j = M*(i,j); func Col(M,i) -> FinSequence of D means :: MATRIX_1:def 9 len it = len M & for j st j in dom M holds it.j = M*(j,i); end; definition let D; let M be Matrix of D; let i; redefine func Line(M,i) -> Element of (width M)-tuples_on D; func Col(M,i) -> Element of (len M)-tuples_on D; end; reserve A,B for Matrix of n,K; definition let K,n; func n-Matrices_over K -> set equals :: MATRIX_1:def 10 n-tuples_on (n-tuples_on the carrier of K); func 0.(K,n) -> Matrix of n,K equals :: MATRIX_1:def 11 n |-> (n |-> 0.K); func 1.(K,n) -> Matrix of n,K means :: MATRIX_1:def 12 (for i st [i,i] in Indices it holds it*(i,i) = 1_ K) & for i,j st [i,j] in Indices it & i <> j holds it*(i,j) = 0.K; let A; func -A -> Matrix of n,K means :: MATRIX_1:def 13 for i,j holds [i,j] in Indices A implies it*(i,j) = -(A*(i,j)); let B; func A+B -> Matrix of n,K means :: MATRIX_1:def 14 for i,j holds [i,j] in Indices A implies it*(i,j) = A*(i,j) + B*(i,j); end; definition let K,n; cluster n-Matrices_over K -> non empty; end; theorem :: MATRIX_1:30 [i,j] in Indices (0.(K,n)) implies (0.(K,n))*(i,j)= 0.K; theorem :: MATRIX_1:31 x is Element of n-Matrices_over K iff x is Matrix of n,K; definition let K,n; mode Diagonal of n,K -> Matrix of n,K means :: MATRIX_1:def 15 for i,j st [i,j] in Indices it & it*(i,j) <> 0.K holds i=j; end; reserve A,A',B,B',C for Matrix of n,F; theorem :: MATRIX_1:32 A + B = B + A; theorem :: MATRIX_1:33 (A + B) + C = A + (B + C); theorem :: MATRIX_1:34 A + 0.(F,n)= A; theorem :: MATRIX_1:35 A + (-A) = 0.(F,n); definition let F,n; func n-G_Matrix_over F -> strict AbGroup means :: MATRIX_1:def 16 the carrier of it = n-Matrices_over F & (for A,B holds (the add of it).(A,B) = A+B) & the Zero of it = 0.(F,n); end;

Back to top