:: Abelian Group of Matrices
:: by Katarzyna Jankowska
::
:: Received June 8, 1991
:: Copyright (c) 1991-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, ALGSTR_0, FINSEQ_1, SUBSET_1,
RLVECT_1, RELAT_1, FINSEQ_2, TARSKI, STRUCT_0, TREES_1,
ZFMISC_1, FUNCT_1, SUPINF_2, MESFUNC1, ARYTM_1, ARYTM_3,
VECTSP_1, BINOP_1, MATRIX_1, XXREAL_0, FUNCOP_1, CARD_1,
FUNCT_2, GROUP_1, ABIAN, INT_1, CARD_3, FINSET_1, FUNCSDOM,
MATRIX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS,
RELAT_1, NAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, CARD_3,
MATRIX_0, STRUCT_0, ALGSTR_0, BINOP_1, FINSEQOP, RLVECT_1,
VECTSP_1, XXREAL_0, PARTFUN1, NAT_D, GROUP_1, GROUP_4, FINSET_1,
FINSUB_1, FINSEQ_3, FINSEQ_4;
constructors BINOP_1, XXREAL_0, FINSEQOP, VECTSP_1, RLVECT_1,
RELSET_1, CARD_3, FUNCT_6, CARD_2, WELLORD2, NAT_1, MATRIX_0,
STRUCT_0, PRE_POLY, GROUP_1, RELAT_2, PARTFUN1, FINSUB_1, NAT_D,
FINSEQ_4, GROUP_4;
registrations FINSEQ_2, STRUCT_0, VECTSP_1, ORDINAL1, XXREAL_0,
XBOOLE_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1,
GROUP_1, CARD_1, RLVECT_1;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions TARSKI, RLVECT_1, ALGSTR_0, STRUCT_0, MATRIX_0;
equalities FINSEQ_2, STRUCT_0, ALGSTR_0;
theorems FINSEQ_1, FINSEQ_2, FUNCOP_1, ZFMISC_1, BINOP_1, RLVECT_1,
ORDINAL1, CARD_1, MATRIX_0, TARSKI, GROUP_1, FUNCT_2, FINSET_1,
GROUP_4, FRAENKEL, RELAT_1, XBOOLE_0, NAT_D, NAT_1;
schemes BINOP_1, MATRIX_0, XBOOLE_0;
begin
reserve x,y,z for object,
i,j,n,m for Nat,
K for non empty addMagma,
F for add-associative right_zeroed right_complementable Abelian
non empty addLoopStr;
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;
reserve A,B for Matrix of n,K;
definition
let K be 1-sorted;
let n;
func n-Matrices_over K -> set equals
n-tuples_on (n-tuples_on the carrier of K);
coherence;
end;
definition
let K be non empty ZeroStr;
let n;
func 0.(K,n) -> Matrix of n,K equals
n |-> (n |-> 0.K);
coherence by MATRIX_0:10;
end;
definition
let K be non empty ZeroOneStr;
let n;
func 1.(K,n) -> Matrix of n,K means
:Def3:
(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;
existence
proof
defpred P[set,set,set] means ($1 = $2 implies $3 = 1.K) & ($1 <> $2
implies $3 = 0.K);
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
A1: for i,j st [i,j] in [:Seg n1, Seg n1:] ex x being Element of K st P[i, j,x]
proof
let i,j;
assume [i,j] in [:Seg n1, Seg n1:];
i = j implies P[i,j,1.K];
hence thesis;
end;
consider M being Matrix of n1,K such that
A2: for i,j st [i,j] in Indices M holds P[i,j,M*(i,j)] from MATRIX_0:sch 2(A1);
reconsider M as Matrix of n,K;
take M;
thus thesis by A2;
end;
uniqueness
proof
let M1,M2 be Matrix of n,K;
assume that
A3: for i st [i,i] in Indices M1 holds M1*(i,i) = 1.K and
A4: for i,j st [i,j] in Indices M1 & i <> j holds M1*(i,j) = 0.K and
A5: for i st [i,i] in Indices M2 holds M2*(i,i) = 1.K and
A6: for i,j st [i,j] in Indices M2 & i <> j holds M2*(i,j) = 0.K;
A7: Indices M1 =Indices M2 by MATRIX_0:26;
A8: now
let i,j;
assume
A9: [i,j] in Indices M1;
A10: now
assume
A11: i<>j;
then M1*(i,j)=0.K by A4,A9;
hence M1*(i,j)=M2*(i,j) by A7,A6,A9,A11;
end;
now
assume
A12: i=j;
then M1*(i,j)=1.K by A3,A9;
hence M1*(i,j)=M2*(i,j) by A7,A5,A9,A12;
end;
hence M1*(i,j)=M2*(i,j) by A10;
end;
A13: len M2=n & width M2=n by MATRIX_0:24;
len M1=n & width M1=n by MATRIX_0:24;
hence thesis by A8,A13,MATRIX_0:21;
end;
end;
definition
let K be non empty addLoopStr;
let A be Matrix of K;
func -A -> Matrix of K means
:Def2:
len it = len A & width it = width A &
for i,j holds [i,j] in Indices A implies it*(i,j)= -(A*(i,j));
existence
proof
set n = len A;
deffunc F(Nat,Nat) = -(A*($1,$2));
consider M being Matrix of len A,width A,K such that
A1: for i,j st [i,j] in Indices M holds M*(i,j) = F(i,j)
from MATRIX_0:sch 1;
reconsider A1=A as Matrix of n,width A,K by MATRIX_0:51;
A2: Indices A1=[:Seg n,Seg width A:] by MATRIX_0:25;
A3: now
per cases by NAT_1:3;
case n > 0;
hence len M=len A & width M=width A & Indices A = Indices M
by A2,MATRIX_0:23;
end;
case
A4: n = 0;
then len M=0 by MATRIX_0:def 2;
then
A5: width M=0 by MATRIX_0:def 3;
width A=0 by A4,MATRIX_0:def 3;
hence len M=len A & width M=width A & Indices A = Indices M
by A2,A5,MATRIX_0:25;
end;
end;
take M;
thus thesis by A1,A3;
end;
uniqueness
proof
let M1,M2 be Matrix of K;
set n=len A;
assume that
A6: len M1= len A & width M1 =width A and
A7: for i,j st [i,j] in Indices A holds M1*(i,j) =-(A*(i,j)) and
A8: len M2= len A & width M2 =width A and
A9: for i,j st [i,j] in Indices A holds M2*(i,j) =-(A*(i,j));
reconsider M2 as Matrix of n,width A,K by A8,MATRIX_0:51;
reconsider M1 as Matrix of n,width A,K by A6,MATRIX_0:51;
reconsider A1=A as Matrix of n,width A,K by MATRIX_0:51;
A10: Indices A1=[:Seg n,Seg width A:] by MATRIX_0:25;
A11: Indices M1=[:Seg n,Seg width M1:] & Indices M2=[:Seg n,Seg width M2:]
by MATRIX_0:25;
A12: now
per cases by NAT_1:3;
case
A13: n > 0;
then Indices M1=[:Seg n,Seg width A:] by MATRIX_0:23;
hence Indices A = Indices M1 & Indices M1= Indices M2
by A10,A13,MATRIX_0:23;
end;
case
A14: n = 0;
then len M1=0 by MATRIX_0:def 2;
then
A15: width M1=0 by MATRIX_0:def 3;
len M2=0 by A14,MATRIX_0:def 2;
hence Indices A = Indices M1 & Indices M1 = Indices M2
by A10,A11,A14,A15,MATRIX_0:def 3;
end;
end;
now
let i,j;
assume
A16: [i,j] in Indices A;
then M1*(i,j) = -(A*(i,j)) by A7;
hence M1*(i,j)=M2*(i,j) by A9,A16;
end;
hence thesis by A12,MATRIX_0:27;
end;
end;
registration
let K be non empty addLoopStr;
let A be Matrix of K;
cluster -A -> (len A,width A)-size;
coherence
proof
thus len -A = len A by Def2;
A2: width -A = width A by Def2;
-A is Matrix of len -A,width -A,K by MATRIX_0:51;
hence thesis by A2,MATRIX_0:def 2;
end;
end;
registration
let m,n be Nat;
let K be non empty addLoopStr;
let A be Matrix of m,n,K;
cluster -A -> (m,n)-size;
coherence
proof
A1: width (-A) = width A & len A = m by MATRIX_0:def 2,Def2;
A2: len (-A) = len A by Def2;
per cases by NAT_1:3;
suppose
A3: m = 0;
then -A = {} by A2,MATRIX_0:def 2;
hence thesis by A3,MATRIX_0:13;
end;
suppose m > 0;
then width A = n by MATRIX_0:23;
hence thesis by A1;
end;
end;
end;
definition
let m,n be Nat;
let K be non empty addLoopStr;
let A be Matrix of m,n,K;
redefine func -A -> Matrix of m,n,K means :: redefines - (MATRIX_1, definition)
:Def4:
for i,j holds [i,j] in Indices A implies it*(i,j) = -(A*(i,j));
coherence;
compatibility
proof
let M be Matrix of m,n,K;
thus M = -A implies
for i,j holds [i,j] in Indices A implies M*(i,j) = -(A*(i,j)) by Def2;
assume
A1: for i,j holds [i,j] in Indices A implies M*(i,j) = -(A*(i,j));
A2: Indices M = Indices A by MATRIX_0:26;
A6: len M = m by MATRIX_0:def 2;
A3: len -A = m by MATRIX_0:def 2;
A4: now
per cases by NAT_1:3;
suppose
A5: m = 0;
hence width M = 0 by MATRIX_0:22
.= width -A by A5,MATRIX_0:22;
end;
suppose
A8: m > 0;
hence width M = n by A6,MATRIX_0:20
.= width -A by A3,A8,MATRIX_0:20;
end;
end;
for i,j st [i,j] in Indices M holds M*(i,j) = (-A)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices M;
hence M*(i,j) = -(A*(i,j)) by A1,A2
.= (-A)*(i,j) by A2,A5,Def2;
end;
hence M = -A by A6,A3,A4,MATRIX_0:21;
end;
end;
definition
let K be non empty addMagma;
let A,B be Matrix of K;
func A+B -> Matrix of K means
:Def3a:
len it = len A & width it = width A &
for i,j holds [i,j] in Indices A implies it*(i,j) = A*(i,j) + B*(i,j);
existence
proof
set n=len A;
reconsider A1=A as Matrix of len A,width A,K by MATRIX_0:51;
deffunc F(Nat,Nat) = A*($1,$2) + B*($1,$2);
consider M being Matrix of len A,width A,K such that
A1: for i,j st [i,j] in Indices M holds M*(i,j) = F(i,j)
from MATRIX_0:sch 1;
A2: Indices A1=[:Seg len A,Seg width A:] by MATRIX_0:25;
A3: now
per cases by NAT_1:3;
case n > 0;
hence len M=len A & width M=width A & Indices A = Indices M
by A2,MATRIX_0:23;
end;
case
A4: n = 0;
then len M=0 by MATRIX_0:def 2;
then
A5: width M=0 by MATRIX_0:def 3;
width A=0 by A4,MATRIX_0:def 3;
hence len M=len A & width M=width A & Indices A = Indices M
by A2,A5,MATRIX_0:25;
end;
end;
take M;
thus thesis by A1,A3;
end;
uniqueness
proof
set n = len A;
let M1,M2 be Matrix of K;
assume that
A6: len M1 =len A & width M1=width A and
A7: for i,j st [i,j] in Indices A holds M1*(i,j)=A*(i,j) + B*(i,j) and
A8: len M2 =len A & width M2=width A and
A9: for i,j st [i,j] in Indices A holds M2*(i,j) = A*(i,j) + B*(i,j);
reconsider M2 as Matrix of n,width A,K by A8,MATRIX_0:51;
reconsider M1 as Matrix of n,width A,K by A6,MATRIX_0:51;
reconsider A1=A as Matrix of n,width A,K by MATRIX_0:51;
A10: Indices A1=[:Seg n,Seg width A:] by MATRIX_0:25;
A11: Indices M1=[:Seg n,Seg width M1:] & Indices M2=[:Seg n,Seg width M2:]
by MATRIX_0:25;
A12: now
per cases by NAT_1:3;
case
A13: n > 0;
then Indices M1=[:Seg n,Seg width A:] by MATRIX_0:23;
hence Indices A = Indices M1 & Indices M1= Indices M2
by A10,A13,MATRIX_0:23;
end;
case
A14: n = 0;
then len M1=0 by MATRIX_0:def 2;
then
A15: width M1=0 by MATRIX_0:def 3;
len M2=0 by A14,MATRIX_0:def 2;
hence Indices A = Indices M1 & Indices M1= Indices M2
by A10,A11,A14,A15,MATRIX_0:def 3;
end;
end;
now
let i,j;
assume
A16: [i,j] in Indices A;
then M1*(i,j)=(A*(i,j) + B*(i,j)) by A7;
hence M1*(i,j)=M2*(i,j) by A9,A16;
end;
hence thesis by A12,MATRIX_0:27;
end;
end;
registration
let K be non empty addMagma;
let A,B be Matrix of K;
cluster A+B -> (len A,width A)-size;
coherence
proof
thus len(A+B) = len A by Def3a;
A2: width(A+B) = width A by Def3a;
A+B is Matrix of len(A+B),width(A+B),K by MATRIX_0:51;
hence thesis by A2,MATRIX_0:def 2;
end;
end;
registration
let m,n;
let K be non empty addMagma;
let A be Matrix of m,n,K;
let B be Matrix of K;
cluster A+B -> (m,n)-size;
coherence
proof
A1: width (A+B) = width A & len A = m by MATRIX_0:def 2,Def3a;
A2: len (A+B) = len A by Def3a;
per cases by NAT_1:3;
suppose
A3: m = 0;
then A+B = {} by A2,MATRIX_0:def 2;
hence thesis by A3,MATRIX_0:13;
end;
suppose m > 0;
then width A = n by MATRIX_0:23;
hence thesis by A1;
end;
end;
end;
definition
let K be non empty addLoopStr;
let A,B be Matrix of K;
func A-B -> Matrix of K equals
A + -B;
coherence;
end;
registration
let K be non empty addLoopStr;
let A,B be Matrix of K;
cluster A-B -> (len A,width A)-size;
coherence;
end;
registration
let m,n be Nat;
let K be non empty addLoopStr;
let A be Matrix of m,n,K;
let B be Matrix of K;
cluster A-B -> (m,n)-size;
coherence;
end;
definition
let m,n be Nat;
let K be non empty addMagma;
let A,B be Matrix of m,n,K;
redefine func A+B -> Matrix of m,n,K means :: redefines + (MATRIX_1, definition)
:Def5:
for i,j holds [i,j] in Indices A implies it*(i,j) = A*(i,j) + B*(i,j);
coherence;
compatibility
proof
let M be Matrix of m,n,K;
thus M = A+B implies
for i,j holds [i,j] in Indices A implies M*(i,j) = (A*(i,j))+(B*(i,j))
by Def3a;
assume
A1: for i,j holds [i,j] in Indices A implies M*(i,j) = (A*(i,j))+(B*(i,j));
A2: Indices M = Indices A by MATRIX_0:26;
A3: len M = m by MATRIX_0:def 2;
A5: len(A+B) = m by MATRIX_0:def 2;
A4: now
per cases by NAT_1:3;
suppose
A6: m = 0;
hence width M = 0 by MATRIX_0:22
.= width(A+B) by A6,MATRIX_0:22;
end;
suppose
A7: m > 0;
hence width M = n by A3,MATRIX_0:20
.= width(A+B) by A5,A7,MATRIX_0:20;
end;
end;
for i,j st [i,j] in Indices M holds M*(i,j) = (A+B)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices M;
hence M*(i,j) = (A*(i,j))+(B*(i,j)) by A1,A2
.= (A+B)*(i,j) by A2,A5,Def3a;
end;
hence M = A+B by A3,A5,A4,MATRIX_0:21;
end;
end;
definition
let m,n;
let K be non empty addLoopStr;
let A,B be Matrix of m,n,K;
redefine func A-B -> Matrix of m,n,K means :: redefines - (MATRIX_1, definition)
for i,j holds [i,j] in Indices A implies it*(i,j) = A*(i,j) - B*(i,j);
coherence;
compatibility
proof
let M be Matrix of m,n,K;
thus M = A-B implies
for i,j holds [i,j] in Indices A implies M*(i,j) = A*(i,j)-B*(i,j)
proof
assume
A1: M = A-B;
let i,j such that
A2: [i,j] in Indices A;
A3: Indices A = Indices B by MATRIX_0:26;
thus M*(i,j) = A*(i,j)+(-B)*(i,j) by A1,A2,Def3a
.= A*(i,j)-B*(i,j) by A2,A3,Def4;
end;
assume
A4: for i,j holds [i,j] in Indices A implies M*(i,j) = A*(i,j)-B*(i,j);
now
let i,j such that
A5: [i,j] in Indices M;
A7: Indices M = Indices B by MATRIX_0:26;
A6: Indices M = Indices A by MATRIX_0:26;
hence M*(i,j) = A*(i,j)-B*(i,j) by A4,A5
.= A*(i,j)+(-B)*(i,j) by A5,A7,Def4
.= (A-B)*(i,j) by A5,A6,Def3a;
end;
hence thesis by MATRIX_0:27;
end;
end;
registration
let K,n;
cluster n-Matrices_over K -> non empty;
coherence;
end;
theorem Th1:
for K being non empty addLoopStr holds
[i,j] in Indices (0.(K,n)) implies (0.(K,n))*(i,j)= 0.K
proof
let K be non empty addLoopStr;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
set M = 0.(K,n);
assume
A1: [i,j] in Indices M;
then
A2: [i,j] in [:Seg n,Seg n:] by MATRIX_0:24;
then j in Seg n by ZFMISC_1:87;
then
A3: (n1 |-> 0.K).j= 0.K by FUNCOP_1:7;
i in Seg n by A2,ZFMISC_1:87;
then M.i= n1 |-> 0.K by FUNCOP_1:7;
hence thesis by A1,A3,MATRIX_0:def 5;
end;
theorem Th2:
x is Element of n-Matrices_over K iff x is Matrix of n,K
proof
thus x is Element of (n-Matrices_over K) implies x is Matrix of n,K
proof
assume x is Element of (n-Matrices_over K);
then reconsider
x as Element of n-tuples_on (n-tuples_on the carrier of K);
A1: len x=n by CARD_1:def 7;
ex m st for y st y in rng x ex q being FinSequence of K st y=q & len q =m
proof
take n;
let y;
A2: rng x c= (n-tuples_on the carrier of K) by FINSEQ_1:def 4;
assume y in rng x;
then reconsider q=y as Element of n-tuples_on the carrier of K by A2;
reconsider q as FinSequence of K;
take q;
thus thesis by CARD_1:def 7;
end;
then reconsider x as Matrix of the carrier of K by MATRIX_0:9;
for q be FinSequence of K st q in rng x holds len q = n
proof
let q be FinSequence of K;
A3: rng x c= n-tuples_on the carrier of K by FINSEQ_1:def 4;
assume q in rng x;
then reconsider q as Element of n-tuples_on the carrier of K by A3;
len q=n by CARD_1:def 7;
hence thesis;
end;
hence thesis by A1,MATRIX_0:def 2;
end;
assume x is Matrix of n,K;
then reconsider x as Matrix of n,K;
A4: len x = n by MATRIX_0:def 2;
then reconsider x as Element of n-tuples_on ((the carrier of K)*) by
FINSEQ_2:92;
rng x c= n-tuples_on the carrier of K
proof
let y be object;
assume
A5: y in rng x;
rng x c= (the carrier of K)* by FINSEQ_1:def 4;
then reconsider p=y as FinSequence of K by A5,FINSEQ_1:def 11;
len p =n by A5,MATRIX_0:def 2;
then p is Element of n-tuples_on the carrier of K by FINSEQ_2:92;
hence thesis;
end;
then x is FinSequence of n-tuples_on the carrier of K by FINSEQ_1:def 4;
hence thesis by A4,FINSEQ_2:92;
end;
definition
let K be non empty ZeroStr;
let M be Matrix of K;
attr M is diagonal means :Def6:
for i,j st [i,j] in Indices M & M*(i,j) <> 0.K holds i=j;
end;
registration
let n; let K be non empty ZeroOneStr;
cluster diagonal for Matrix of n,K;
existence
proof
take 1.(K,n);
let i,j;
thus thesis by Def3;
end;
end;
reserve A,B,C for Matrix of n,F;
theorem Th3:
for A,B being Matrix of m,n,F holds A + B = B + A
proof
let A,B be Matrix of m,n,F;
A1: Indices A = Indices (A + B) by MATRIX_0:26;
A2: Indices A= Indices B by MATRIX_0:26;
now
let i,j;
assume
A3: [i,j] in Indices (A + B);
hence (A + B)*(i,j)=A*(i,j) + B*(i,j) by A1,Def3a
.=(B + A)*(i,j) by A2,A1,A3,Def3a;
end;
hence thesis by MATRIX_0:27;
end;
theorem Th4:
for A,B,C being Matrix of m,n,F holds (A + B) + C = A + (B + C)
proof
let A,B,C be Matrix of m,n,F;
A1: Indices A= Indices ((A + B) +C) by MATRIX_0:26;
A2: Indices A= Indices (A + B) by MATRIX_0:26;
A3: Indices A= Indices B by MATRIX_0:26;
now
let i,j;
assume
A4: [i,j] in Indices ((A + B) + C);
hence ((A + B)+C)*(i,j)=(A+B)*(i,j) + C*(i,j) by A1,A2,Def3a
.=(A*(i,j) + B*(i,j)) + C*(i,j) by A1,A4,Def3a
.=A*(i,j) + (B*(i,j) + C*(i,j)) by RLVECT_1:def 3
.=A*(i,j) + ( B + C)*(i,j) by A3,A1,A4,Def3a
.=(A + ( B + C))*(i,j) by A1,A4,Def3a;
end;
hence thesis by MATRIX_0:27;
end;
theorem Th5:
A + 0.(F,n)= A
proof
A1: Indices A= Indices (A+0.(F,n)) by MATRIX_0:26;
A2: Indices A= Indices (0.(F,n)) by MATRIX_0:26;
now
let i,j;
assume
A3: [i,j] in Indices (A+ 0.(F,n));
hence (A+ 0.(F,n)) *(i,j)=A*(i,j) + 0.(F,n)*(i,j) by A1,Def5
.=A*(i,j) +0.F by A1,A2,A3,Th1
.=A*(i,j);
end;
hence thesis by MATRIX_0:27;
end;
theorem Th6:
A + (-A) = 0.(F,n)
proof
A1: Indices A= Indices (A + (-A)) by MATRIX_0:26;
A2: Indices A= Indices 0.(F,n) by MATRIX_0:26;
now
let i,j;
assume
A3: [i,j] in Indices (A + (-A));
hence (A + (-A))*(i,j)=A*(i,j)+ (-A)*(i,j) by A1,Def5
.=A*(i,j)+ (-A*(i,j)) by A1,A3,Def4
.=0.F by RLVECT_1:def 10
.=(0.(F,n))*(i,j) by A2,A1,A3,Th1;
end;
hence thesis by MATRIX_0:27;
end;
definition
let F,n;
func n-G_Matrix_over F -> strict AbGroup means
the carrier of it = n-Matrices_over F &
(for A,B holds (the addF of it).(A,B) = A+B) &
0.it = 0.(F,n);
existence
proof
reconsider A0=0.(F,n) as Element of n-Matrices_over F;
defpred P[Element of n-Matrices_over F, Element of n-Matrices_over F,
Element of n-Matrices_over F] means ex A,B st $1=A & $2=B & $3 = A + B;
A1: for a,b being Element of n-Matrices_over F ex c being Element of n
-Matrices_over F st P[a,b,c]
proof
let a,b be Element of (n-Matrices_over F);
reconsider B=b as Matrix of n,F by Th2;
reconsider A=a as Matrix of n,F by Th2;
reconsider c = A+B as Element of n-Matrices_over F by Th2;
take c;
thus thesis;
end;
consider h being BinOp of n-Matrices_over F such that
A2: for a,b being Element of n-Matrices_over F holds P[a,b,h.(a,b)]
from BINOP_1:sch 3(A1);
set G=addLoopStr (# n-Matrices_over F,h,A0 #);
A3: h.(A,B)=A+B
proof
A is Element of (n-Matrices_over F) & B is Element of (n-Matrices_over F)
by Th2;
then ex A9,B9 being Matrix of n,F st A=A9 & B=B9 & h.(A,B)= A9 + B9
by A2;
hence thesis;
end;
A4: for a being Element of n-Matrices_over F ex b being Element of n
-Matrices_over F st ex A st a=A & b= -A
proof
let a be Element of n-Matrices_over F;
reconsider A=a as Matrix of n,F by Th2;
reconsider b=-A as Element of n-Matrices_over F by Th2;
take b;
thus thesis;
end;
G is Abelian add-associative right_zeroed right_complementable
proof
thus G is Abelian
proof
let a,b be Element of G;
reconsider A=a,B=b as Matrix of n,F by Th2;
thus a+b=A+B by A3
.=B+A by Th3
.=b+a by A3;
end;
hereby
let a,b,c be Element of G;
reconsider A=a,B=b,C=c as Matrix of n,F by Th2;
thus (a+b)+c =h.(A+B,C) by A3
.=(A+B)+C by A3
.=A+(B+C) by Th4
.=h.(A,B+C) by A3
.=a+(b+c) by A3;
end;
hereby
let a be Element of G;
reconsider A=a as Matrix of n,F by Th2;
thus a+0.G=A + 0.(F,n) by A3
.=a by Th5;
end;
let a be Element of G;
consider b being Element of n-Matrices_over F such that
A5: ex A st a=A & b= -A by A4;
consider A such that
A6: a=A and
A7: b= -A by A5;
reconsider b = -A as Element of G by A7;
take b;
thus a+b=A+-A by A3,A6
.=0.G by Th6;
end;
then reconsider G as strict AbGroup;
take G;
thus thesis by A3;
end;
uniqueness
proof
thus for G1,G2 being strict AbGroup st the carrier of G1 = n-Matrices_over
F & (for A,B holds (the addF of G1).(A,B) = A+B) & 0.G1 = 0.(F,n) & the carrier
of G2 = n-Matrices_over F & (for A,B holds (the addF of G2).(A,B) = A+B) & 0.G2
= 0.(F,n) holds G1=G2
proof
let G1,G2 be strict AbGroup;
assume that
A8: the carrier of G1 = n-Matrices_over F and
A9: for A,B holds (the addF of G1).(A,B) = A+B and
A10: 0.G1 = 0.(F,n) & the carrier of G2 = n-Matrices_over F and
A11: for A,B holds (the addF of G2).(A,B) = A+B and
A12: 0.G2 = 0.(F,n);
now
let a,b be Element of G1;
reconsider A = a, B = b as Matrix of n,F by A8,Th2;
thus (the addF of G1).(a,b)= A+B by A9
.= (the addF of G2).(a,b) by A11;
end;
hence thesis by A8,A10,A12,BINOP_1:2;
end;
end;
end;
begin :: taken from MATRIX_2
reserve i,j,n for Nat,
K for Field,
a,b for Element of K;
definition
let n;
let K be non empty ZeroStr;
let M be Matrix of n,K;
attr M is upper_triangular means
for i,j st [i,j] in Indices M & i>j holds M*(i,j) = 0.K;
attr M is lower_triangular means
for i,j st [i,j] in Indices M & i<j holds M*(i,j) = 0.K;
end;
registration
let n; let K be non empty ZeroOneStr;
cluster -> upper_triangular lower_triangular for diagonal Matrix of n,K;
coherence by Def6;
end;
registration
let n; let K be non empty ZeroOneStr;
cluster lower_triangular upper_triangular for Matrix of n,K;
existence
proof
take the diagonal Matrix of n,K;
thus thesis;
end;
end;
theorem
((n,n)-->a) + ((n,n)-->b) = (n,n)-->(a+b)
proof
A1: Indices ((n,n)-->a) = Indices ((n,n)-->(a+b)) by MATRIX_0:26;
A2: Indices ((n,n)-->a) = Indices ((n,n)-->b) by MATRIX_0:26;
now
let i,j;
assume
A3: [i,j] in Indices ((n,n)-->(a+b));
then ((n,n)-->a)*(i,j)=a by A1,MATRIX_0:46;
then ((n,n)-->a)*(i,j) +((n,n)-->b)*(i,j)=a+b by A2,A1,A3,MATRIX_0:46;
hence ((n,n)-->a)*(i,j) +((n,n)-->b)*(i,j)=((n,n)-->(a+b))*(i,j)
by A3,MATRIX_0:46;
end;
hence thesis by A1,Def5;
end;
begin :: Sets of Permutations
reserve x,y,x1,x2,y1,y2 for set,
i,j,k,l,n,m for Nat,
D for non empty set,
K for Field,
s,s2 for FinSequence,
a,b,c,d for Element of D;
definition
let IT be set;
attr IT is permutational means :Def10:
ex n st for x st x in IT holds x is Permutation of Seg n;
end;
registration
cluster permutational non empty for set;
existence
proof
set n = the Nat;
set p = the Permutation of Seg n;
take P={p};
thus P is permutational
proof
take n;
let x;
assume x in P;
hence thesis by TARSKI:def 1;
end;
thus thesis;
end;
end;
definition
let P be permutational non empty set;
func len P -> Nat means
:Def11:
ex s st s in P & it = len s;
existence
proof
set x = the Element of P;
consider n such that
A1: for y st y in P holds y is Permutation of Seg n by Def10;
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider q = x as Permutation of Seg n by A1;
A2: dom q=Seg n by FUNCT_2:52;
then reconsider q as FinSequence by FINSEQ_1:def 2;
take n,q;
thus thesis by A2,FINSEQ_1:def 3;
end;
uniqueness
proof
let n1,n2 be Nat;
given s1 be FinSequence such that
A3: s1 in P and
A4: n1=len s1;
consider n such that
A5: for y st y in P holds y is Permutation of Seg n by Def10;
s1 is Function of Seg n,Seg n by A3,A5;
then n in NAT & dom s1=Seg n by FUNCT_2:52,ORDINAL1:def 12;
then
A6: len s1=n by FINSEQ_1:def 3;
given s2 such that
A7: s2 in P and
A8: n2=len s2;
s2 is Permutation of Seg n by A7,A5;
then dom s2=Seg n by FUNCT_2:52;
hence thesis by A4,A8,A6,FINSEQ_1:def 3;
end;
end;
definition
let P be permutational non empty set;
redefine func len P -> Element of NAT; :: redefines len (MATRIX_1, definition)
coherence by ORDINAL1:def 12;
end;
definition
let P be permutational non empty set;
redefine mode Element of P -> Permutation of Seg len P; :: redefines Element (SUBSET_1, definition)
coherence
proof
let x be Element of P;
consider n such that
A1: for y st y in P holds y is Permutation of Seg n by Def10;
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider q=x as Permutation of Seg n by A1;
A2: dom q=Seg n by FUNCT_2:52;
then reconsider q as FinSequence by FINSEQ_1:def 2;
len q=n by A2,FINSEQ_1:def 3;
then Seg (len P) = Seg n by Def11;
hence thesis by A1;
end;
end;
theorem
ex P being permutational non empty set st len P = n
proof
set p = the Permutation of Seg n;
set P = {p};
now
take n;
let x;
assume x in P;
hence x is Permutation of Seg n by TARSKI:def 1;
end;
then reconsider P as permutational non empty set by Def10;
take P;
len P = n
proof
set x = the Element of P;
reconsider y=x as Function of Seg n,Seg n by TARSKI:def 1;
A1: dom y=Seg n by FUNCT_2:52;
then reconsider s=y as FinSequence by FINSEQ_1:def 2;
n in NAT & len P= len s by Def11,ORDINAL1:def 12;
hence thesis by A1,FINSEQ_1:def 3;
end;
hence thesis;
end;
definition
let n;
func Permutations n -> set means
:Def12:
x in it iff x is Permutation of Seg n;
existence
proof
defpred P[object] means $1 is Permutation of Seg n;
consider P being set such that
A1: for x being object holds x in P iff x in Funcs(Seg n,Seg n) & P[x]
from XBOOLE_0:sch 1;
take P;
let x;
thus x in P implies x is Permutation of Seg n by A1;
thus thesis by A1,FUNCT_2:9;
end;
uniqueness
proof
let P1,P2 be set;
assume that
A3: for x holds x in P1 iff x is Permutation of Seg n and
A4: for x holds x in P2 iff x is Permutation of Seg n;
A5: now
let x be object;
assume x in P2;
then x is Permutation of Seg n by A4;
hence x in P1 by A3;
end;
now
let x be object;
assume x in P1;
then x is Permutation of Seg n by A3;
hence x in P2 by A4;
end;
hence thesis by A5,TARSKI:2;
end;
end;
registration
let n;
cluster Permutations(n) -> permutational non empty;
coherence
proof
defpred P[object] means $1 is Permutation of Seg n;
consider P being set such that
A1: for x being object holds x in P iff x in Funcs(Seg n,Seg n) & P[x] from
XBOOLE_0:sch 1;
idseq n in Funcs(Seg n,Seg n) by FUNCT_2:9;
then reconsider P as non empty set by A1;
now
take n;
let x;
assume x in P;
hence x is Permutation of Seg n by A1;
end;
then reconsider P as permutational non empty set by Def10;
x in P iff x is Permutation of Seg n by A1,FUNCT_2:9;
hence thesis by Def12;
end;
end;
theorem
len Permutations(n) = n
proof
set x = the Element of Permutations(n);
reconsider q=x as Permutation of Seg n by Def12;
A1: dom q=Seg n by FUNCT_2:52;
then reconsider q as FinSequence by FINSEQ_1:def 2;
n in NAT by ORDINAL1:def 12;
then len q=n by A1,FINSEQ_1:def 3;
hence thesis by Def11;
end;
theorem
Permutations 1 = {idseq 1}
proof
A1: Permutations 1 c={idseq 1}
proof
let p be object;
assume p in Permutations 1;
then reconsider q=p as Permutation of Seg 1 by Def12;
A2: dom q=Seg 1 by FUNCT_2:52;
rng q = Seg 1 & 1 in {1} by FUNCT_2:def 3,TARSKI:def 1;
then q.1 in Seg 1 by FINSEQ_1:2,FUNCT_2:4;
then
A3: q.1=1 by FINSEQ_1:2,TARSKI:def 1;
reconsider q as FinSequence by A2,FINSEQ_1:def 2;
len q= 1 by A2,FINSEQ_1:def 3;
then q = idseq 1 by A3,FINSEQ_1:40,FINSEQ_2:50;
hence thesis by TARSKI:def 1;
end;
{idseq 1} c= Permutations(1)
proof
let x be object;
assume x in {idseq 1};
then x= idseq 1 by TARSKI:def 1;
hence thesis by Def12;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
begin :: Group of Permutations
reserve p,q for Element of Permutations(n);
definition let n;
func Group_of_Perm(n) -> strict multMagma means
:Def13:
the carrier of it = Permutations(n) &
for q,p be Element of Permutations(n) holds (the multF of it).(q,p) = p*q;
existence
proof
defpred P[Element of Permutations(n),Element of Permutations(n),set] means
$3 = $2*$1;
A1: for q,p being Element of Permutations(n) ex z being Element of
Permutations(n) st P[q,p,z]
proof
let q,p be Element of Permutations(n);
reconsider p,q as Permutation of Seg n by Def12;
reconsider z=p*q as Element of Permutations(n) by Def12;
take z;
thus thesis;
end;
consider o being BinOp of Permutations(n) such that
A2: for q,p being Element of Permutations(n) holds P[q,p,o.(q,p)] from
BINOP_1:sch 3(A1);
take multMagma(# Permutations(n),o#);
thus thesis by A2;
end;
uniqueness
proof
let G1,G2 be strict multMagma;
assume that
A3: the carrier of G1 = Permutations(n) and
A4: for q,p be Element of Permutations(n) holds (the multF of G1).(q,p
)=p*q and
A5: the carrier of G2 = Permutations(n) and
A6: for q,p be Element of Permutations(n) holds (the multF of G2).(q,p )=p*q;
now
let q,p be Element of G1;
reconsider q9 = q, p9 = p as Element of Permutations(n) by A3;
thus (the multF of G1).(q,p)=p9*q9 by A4
.=(the multF of G2).(q,p) by A6;
end;
hence thesis by A3,A5,BINOP_1:2;
end;
end;
registration
let n;
cluster Group_of_Perm(n) -> non empty;
coherence
proof
the carrier of Group_of_Perm(n) = Permutations(n) by Def13;
hence the carrier of Group_of_Perm(n) is non empty;
end;
end;
theorem Th11:
idseq n is Element of Group_of_Perm(n)
proof
the carrier of Group_of_Perm(n) = Permutations(n) by Def13;
hence thesis by Def12;
end;
theorem Th12:
p *(idseq n)=p & (idseq n)*p=p
proof
A1: Seg n = {} implies Seg n= {};
p is Permutation of Seg n by Def12;
then
A2: rng p= Seg n by FUNCT_2:def 3;
p is Function of Seg n,Seg n by Def12;
then dom p= Seg n by A1,FUNCT_2:def 1;
hence thesis by A2,RELAT_1:52,54;
end;
theorem Th13:
p *p"=idseq n & p"*p=idseq n
proof
p is Permutation of Seg n by Def12;
hence thesis by FUNCT_2:61;
end;
theorem Th14:
p" is Element of Group_of_Perm(n)
proof
reconsider p as Permutation of Seg n by Def12;
p" is Element of Permutations(n) by Def12;
hence thesis by Def13;
end;
registration
let n;
cluster Group_of_Perm(n) -> associative Group-like;
coherence
proof
A1: ex e being Element of Group_of_Perm(n) st for p being Element of
Group_of_Perm(n) holds p * e = p & e * p = p & ex g being Element of
Group_of_Perm(n) st p * g = e & g * p = e
proof
reconsider e=idseq n as Element of Group_of_Perm(n) by Th11;
take e;
reconsider e9=idseq n as Element of Permutations(n) by Def12;
A2: for p being Element of Group_of_Perm(n) holds ex g being Element of
Group_of_Perm(n) st p * g= e & g * p=e
proof
let p be Element of Group_of_Perm(n);
reconsider q=p as Element of Permutations(n) by Def13;
reconsider r=q as Permutation of Seg n by Def12;
reconsider f=r" as Element of Permutations(n) by Def12;
reconsider g=f as Element of Group_of_Perm(n) by Th14;
take g;
A3: g * p= q*f by Def13
.=e by Th13;
p * g= f*q by Def13
.=e by Th13;
hence thesis by A3;
end;
for p being Element of Group_of_Perm(n) holds p * e =p & e* p=p
proof
let p be Element of Group_of_Perm(n);
reconsider p9=p as Element of Permutations(n) by Def13;
A4: e * p =p9 * e9 by Def13
.=p by Th12;
p * e =e9 * p9 by Def13
.=p by Th12;
hence thesis by A4;
end;
hence thesis by A2;
end;
for p,q,r being Element of Group_of_Perm(n) holds (p * q) * r = p * (q * r)
proof
let p,q,r be Element of Group_of_Perm(n);
reconsider p9=p,q9=q,r9=r as Element of Permutations(n) by Def13;
A5: q9*p9 is Permutation of Seg n & r9*q9 is Permutation of Seg n
proof
reconsider p9,q9,r9 as Permutation of Seg n by Def12;
q9*p9 is Permutation of Seg n & r9*q9 is Permutation of Seg n;
hence thesis;
end;
then
A6: q9 * p9 is Element of Permutations(n) by Def12;
A7: r9 * q9 is Element of Permutations(n) by A5,Def12;
(p * q) * r =(the multF of Group_of_Perm n).((q9*p9),r9) by Def13
.=r9*(q9 *p9 ) by A6,Def13
.=(r9 *q9) * p9 by RELAT_1:36
.=(the multF of Group_of_Perm n).(p9,(r9*q9)) by A7,Def13
.=p *(q* r) by Def13;
hence thesis;
end;
hence thesis by A1,GROUP_1:1;
end;
end;
theorem Th15:
idseq n= 1_Group_of_Perm(n)
proof
reconsider e=idseq n as Element of Group_of_Perm(n) by Th11;
reconsider e9=idseq n as Element of Permutations(n) by Def12;
for p being Element of Group_of_Perm(n) holds p * e=p & e* p=p
proof
let p be Element of Group_of_Perm(n);
reconsider p9=p as Element of Permutations(n) by Def13;
A1: e * p =p9 * e9 by Def13
.=p by Th12;
p * e =e9 * p9 by Def13
.=p by Th12;
hence thesis by A1;
end;
hence thesis by GROUP_1:4;
end;
definition
let n;
let p be Permutation of Seg n;
attr p is being_transposition means
ex i,j st i in dom p & j in dom p & i<>j
& p.i=j & p.j=i & for k st k <>i & k<>j & k in dom p holds p.k=k;
end;
definition
let n;
let IT be Permutation of Seg n;
attr IT is even means
ex l be FinSequence of Group_of_Perm(n) st (len l) mod 2 = 0 &
IT = Product l &
for i st i in dom l ex q st l.i = q & q is being_transposition;
end;
notation
let n;
let IT be Permutation of Seg n;
antonym IT is odd for IT is even;
end;
theorem
id Seg n is even
proof
set l=<*>the carrier of Group_of_Perm n;
0=2 * 0 + 0;
then
A1: (len l) mod 2=0 by NAT_D:def 2;
Product <*> the carrier of Group_of_Perm(n)=1_Group_of_Perm(n) by GROUP_4:8;
then
A2: idseq n=Product l by Th15;
for i st i in dom l ex q st l.i=q & q is being_transposition;
hence thesis by A1,A2;
end;
definition
let K be Ring;
let n be Nat;
let x be Element of K;
let p be Element of Permutations(n);
func -(x,p) -> Element of K equals
x if p is even otherwise -x;
correctness;
end;
registration let n;
cluster Permutations n -> finite;
coherence
proof
A1: Permutations n c= Funcs(Seg n,Seg n)
proof
let x be object;
assume x in Permutations n;
then x is Function of Seg n,Seg n by Def12;
hence thesis by FUNCT_2:9;
end;
Funcs(Seg n,Seg n) is finite by FRAENKEL:6;
hence thesis by A1,FINSET_1:1;
end;
end;