:: Abelian Group of Matrices
:: by Katarzyna Jankowska
::
:: Received June 8, 1991
:: Copyright (c) 1991-2019 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;
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, PRE_POLY, GROUP_1,
RELAT_2, PARTFUN1, FINSUB_1, NAT_D, FINSEQ_4, GROUP_4;
registrations RELAT_1, FINSEQ_2, STRUCT_0, VECTSP_1, ORDINAL1, XXREAL_0,
XBOOLE_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, GROUP_1,
CARD_1;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions TARSKI, RLVECT_1, ALGSTR_0, STRUCT_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;
schemes BINOP_1, MATRIX_0, XBOOLE_0;
begin
reserve x,y,z for object,
i,j,n,m for Nat,
D for non empty set,
K for non empty doubleLoopStr,
s,t 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 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,n;
func n-Matrices_over K -> set equals
n-tuples_on (n-tuples_on the carrier of K);
coherence;
func 0.(K,n) -> Matrix of n,K equals
n |-> (n |-> 0.K);
coherence by MATRIX_0:10;
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;
let A;
func -A -> Matrix of n,K means
:Def4:
for i,j holds [i,j] in Indices A implies it*(i,j) = -(A*(i,j));
existence
proof
deffunc F(Nat,Nat) = -(A*($1,$2));
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
consider M being Matrix of n1,K such that
A14: for i,j st [i,j] in Indices M holds M*(i,j) = F(i,j) from
MATRIX_0:sch 1;
Indices A=[:Seg n,Seg n:] by MATRIX_0:24;
then
A15: Indices A = Indices M by MATRIX_0:24;
reconsider M as Matrix of n,K;
take M;
thus thesis by A14,A15;
end;
uniqueness
proof
let M1,M2 be Matrix of n,K;
assume that
A16: for i,j st [i,j] in Indices A holds M1*(i,j) =-(A*(i,j)) and
A17: for i,j st [i,j] in Indices A holds M2*(i,j) =-(A*(i,j));
A18: now
let i,j;
assume
A19: [i,j] in Indices A;
then M1*(i,j) = -(A*(i,j)) by A16;
hence M1*(i,j)=M2*(i,j) by A17,A19;
end;
Indices M1=[:Seg n,Seg n:] by MATRIX_0:24;
then Indices A = Indices M1 by MATRIX_0:24;
hence thesis by A18,MATRIX_0:27;
end;
let B;
func A+B -> Matrix of n,K means
:Def5:
for i,j holds [i,j] in Indices A implies it*(i,j) = A*(i,j) + B*(i,j);
existence
proof
deffunc F(Nat,Nat) = A*($1,$2) + B*($1,$2);
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
consider M being Matrix of n1,K such that
A20: for i,j st [i,j] in Indices M holds M*(i,j)= F(i,j) from
MATRIX_0:sch 1;
Indices A=[:Seg n,Seg n:] by MATRIX_0:24;
then
A21: Indices A = Indices M by MATRIX_0:24;
reconsider M as Matrix of n,K;
take M;
thus thesis by A20,A21;
end;
uniqueness
proof
let M1,M2 be Matrix of n,K;
assume that
A22: for i,j st [i,j] in Indices A holds M1*(i,j)=A*(i,j) + B*(i,j) and
A23: for i,j st [i,j] in Indices A holds M2*(i,j) = A*(i,j) + B*(i,j);
A24: now
let i,j;
assume
A25: [i,j] in Indices A;
then M1*(i,j)=(A*(i,j) + B*(i,j)) by A22;
hence M1*(i,j)=M2*(i,j) by A23,A25;
end;
Indices M1=[:Seg n,Seg n:] by MATRIX_0:24;
then Indices A = Indices M1 by MATRIX_0:24;
hence thesis by A24,MATRIX_0:27;
end;
end;
registration
let K,n;
cluster n-Matrices_over K -> non empty;
coherence;
end;
theorem Th1:
[i,j] in Indices (0.(K,n)) implies (0.(K,n))*(i,j)= 0.K
proof
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, K;
cluster diagonal for Matrix of n,K;
existence
proof
take 1.(K,n);
let i,j;
thus thesis by Def3;
end;
end;
reserve A,A9,B,B9,C for Matrix of n,F;
theorem Th3:
A + B = B + A
proof
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,Def5
.=(B + A)*(i,j) by A2,A1,A3,Def5;
end;
hence thesis by MATRIX_0:27;
end;
theorem Th4:
(A + B) + C = A + (B + C)
proof
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,Def5
.=(A*(i,j) + B*(i,j)) + C*(i,j) by A1,A4,Def5
.=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,Def5
.=(A + ( B + C))*(i,j) by A1,A4,Def5;
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) by RLVECT_1:4;
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 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, K;
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 upper_triangular lower_triangular for diagonal Matrix of n,K;
coherence by def6;
end;
registration
let n, K;
cluster lower_triangular upper_triangular for Matrix of n,K;
existence
proof
set M = the diagonal Matrix of n,K;
take M;
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,
q,r for FinSequence of D,
a9,b9 for Element of K;
definition
let IT be set;
attr IT is permutational means :Def3:
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
:Def4:
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 Def3;
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 Def3;
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;
coherence by ORDINAL1:def 12;
end;
definition
let P be permutational non empty set;
redefine mode Element of P -> Permutation of Seg len P;
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 Def3;
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 Def4;
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 Def3;
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 Def4,ORDINAL1:def 12;
hence thesis by A1,FINSEQ_1:def 3;
end;
hence thesis;
end;
definition
let n;
func Permutations n -> set means
:Def5:
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;
assume
A2: x is Permutation of Seg n;
then x in Funcs(Seg n,Seg n) by FUNCT_2:9;
hence thesis by A1,A2;
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 Def3;
x in P iff x is Permutation of Seg n by A1,FUNCT_2:9;
hence thesis by Def5;
end;
end;
theorem
len Permutations(n)=n
proof
set x = the Element of Permutations(n);
reconsider q=x as Permutation of Seg n by Def5;
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 Def4;
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 Def5;
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 Def5;
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
:Def6:
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 Def5;
reconsider z=p*q as Element of Permutations(n) by Def5;
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 Def6;
hence the carrier of Group_of_Perm(n) is non empty;
end;
end;
theorem Th5:
idseq n is Element of Group_of_Perm(n)
proof
the carrier of Group_of_Perm(n) = Permutations(n) by Def6;
hence thesis by Def5;
end;
theorem Th6:
p *(idseq n)=p & (idseq n)*p=p
proof
A1: Seg n = {} implies Seg n= {};
p is Permutation of Seg n by Def5;
then
A2: rng p= Seg n by FUNCT_2:def 3;
p is Function of Seg n,Seg n by Def5;
then dom p= Seg n by A1,FUNCT_2:def 1;
hence thesis by A2,RELAT_1:52,54;
end;
theorem Th7:
p *p"=idseq n & p"*p=idseq n
proof
p is Permutation of Seg n by Def5;
hence thesis by FUNCT_2:61;
end;
theorem Th8:
p" is Element of Group_of_Perm(n)
proof
reconsider p as Permutation of Seg n by Def5;
p" is Element of Permutations(n) by Def5;
hence thesis by Def6;
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 Th5;
take e;
reconsider e9=idseq n as Element of Permutations(n) by Def5;
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 Def6;
reconsider r=q as Permutation of Seg n by Def5;
reconsider f=r" as Element of Permutations(n) by Def5;
reconsider g=f as Element of Group_of_Perm(n) by Th8;
take g;
A3: g * p= q*f by Def6
.=e by Th7;
p * g= f*q by Def6
.=e by Th7;
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 Def6;
A4: e * p =p9 * e9 by Def6
.=p by Th6;
p * e =e9 * p9 by Def6
.=p by Th6;
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 Def6;
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 Def5;
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 Def5;
A7: r9 * q9 is Element of Permutations(n) by A5,Def5;
(p * q) * r =(the multF of Group_of_Perm n).((q9*p9),r9) by Def6
.=r9*(q9 *p9 ) by A6,Def6
.=(r9 *q9) * p9 by RELAT_1:36
.=(the multF of Group_of_Perm n).(p9,(r9*q9)) by A7,Def6
.=p *(q* r) by Def6;
hence thesis;
end;
hence thesis by A1,GROUP_1:1;
end;
end;
theorem Th9:
idseq n= 1_Group_of_Perm(n)
proof
reconsider e=idseq n as Element of Group_of_Perm(n) by Th5;
reconsider e9=idseq n as Element of Permutations(n) by Def5;
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 Def6;
A1: e * p =p9 * e9 by Def6
.=p by Th6;
p * e =e9 * p9 by Def6
.=p by Th6;
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 Th9;
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 Def5;
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;