:: Transpose Matrices and Groups of Permutations
:: by Katarzyna Jankowska
::
:: Received May 20, 1992
:: Copyright (c) 1992-2012 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, FINSEQ_1, SUBSET_1, FUNCOP_1,
MATRIX_1, FINSEQ_2, RELAT_1, XXREAL_0, CARD_1, TREES_1, FUNCT_1, ARYTM_3,
ZFMISC_1, SUPINF_2, INCSP_1, FINSEQ_3, STRUCT_0, QC_LANG1, TARSKI,
FUNCT_2, ALGSTR_0, BINOP_1, GROUP_1, ABIAN, INT_1, CARD_3, ARYTM_1,
FINSET_1, FINSUB_1, MATRIX_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
FINSEQ_1, FUNCT_2, STRUCT_0, ALGSTR_0, ORDINAL1, NAT_1, NAT_D, GROUP_1,
GROUP_4, BINOP_1, VECTSP_1, MATRIX_1, FINSET_1, FINSUB_1, FINSEQ_2,
FINSEQ_3, FINSEQ_4, NUMBERS, XXREAL_0;
constructors RELAT_2, PARTFUN1, BINOP_1, FINSUB_1, XXREAL_0, NAT_1, NAT_D,
FINSEQOP, FINSEQ_4, GROUP_4, MATRIX_1, VECTSP_1, RELSET_1, PRE_POLY;
registrations XBOOLE_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XXREAL_0, NAT_1,
FINSEQ_1, FINSEQ_2, STRUCT_0, GROUP_1, MATRIX_1, ORDINAL1, CARD_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions STRUCT_0, FINSEQ_2, MATRIX_1, TARSKI, ALGSTR_0;
theorems FINSEQ_1, FINSEQ_2, FINSEQ_3, TARSKI, GROUP_1, FUNCT_1, FUNCT_2,
ZFMISC_1, NAT_1, BINOP_1, FINSUB_1, FINSET_1, GROUP_4, FRAENKEL,
MATRIX_1, RELAT_1, XBOOLE_0, FUNCOP_1, ORDINAL1, NAT_D, CARD_1;
schemes BINOP_1, MATRIX_1, XBOOLE_0;
begin :: Some Examples of Matrices
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 n,m;
let a be set;
func (n,m) --> a -> tabular FinSequence equals
n |-> (m |-> a);
coherence by MATRIX_1:2;
end;
definition
let D,n,m;
let d;
redefine func (n,m) --> d -> Matrix of n,m,D;
coherence by MATRIX_1:10;
end;
theorem Th1:
[i,j] in Indices ((n,m)-->a) implies ((n,m)-->a) * (i,j)=a
proof
reconsider m1=m as Element of NAT by ORDINAL1:def 12;
set M=(n,m)-->a;
assume
A1: [i,j] in Indices M;
then i in dom M by ZFMISC_1:87;
then i in Seg len M by FINSEQ_1:def 3;
then
A2: i in Seg n by MATRIX_1:def 2;
then
A3: n > 0;
j in Seg width M by A1,ZFMISC_1:87;
then j in Seg m by A3,MATRIX_1:23;
then
A4: (m1|->a).j = a by FUNCOP_1:7;
M.i=m1|->a by A2,FUNCOP_1:7;
hence thesis by A1,A4,MATRIX_1:def 5;
end;
theorem
((n,n)-->a9) + ((n,n)-->b9)= (n,n)-->(a9+b9)
proof
A1: Indices ((n,n)-->a9) =Indices ((n,n)-->(a9+b9)) by MATRIX_1:26;
A2: Indices ((n,n)-->a9) =Indices ((n,n)-->b9) by MATRIX_1:26;
now
let i,j;
assume
A3: [i,j] in Indices ((n,n)-->(a9+b9));
then ((n,n)-->a9)*(i,j)=a9 by A1,Th1;
then ((n,n)-->a9)*(i,j) +((n,n)-->b9)*(i,j)=a9+b9 by A2,A1,A3,Th1;
hence
((n,n)-->a9)*(i,j) +((n,n)-->b9)*(i,j)=((n,n)-->(a9+b9))*(i,j) by A3,Th1;
end;
hence thesis by A1,MATRIX_1:def 13;
end;
definition
let a,b,c,d be set;
func (a,b)][(c,d) ->tabular FinSequence equals
<*<*a,b*>,<*c,d*>*>;
correctness
proof
len <*a,b*>=2 & len <*c,d*>=2 by FINSEQ_1:44;
hence thesis by MATRIX_1:4;
end;
end;
theorem Th3:
len (x1,x2)][(y1,y2)=2 & width (x1,x2)][(y1,y2)=2 & Indices (x1,
x2)][(y1,y2)=[:Seg 2,Seg 2:]
proof
set M = (x1,x2)][(y1,y2);
thus
A1: len M=2 by FINSEQ_1:44;
rng M = { <*x1,x2*>,<*y1,y2*>} by FINSEQ_2:127;
then
A2: <*x1,x2*> in rng M by TARSKI:def 2;
len <*x1,x2*>=2 by FINSEQ_1:44;
hence width M=2 by A1,A2,MATRIX_1:def 3;
hence thesis by A1,FINSEQ_1:def 3;
end;
theorem Th4:
[1,1] in Indices (x1,x2)][(y1,y2) & [1,2] in Indices (x1,x2)][(y1
,y2) & [2,1] in Indices (x1,x2)][(y1,y2) & [2,2] in Indices (x1,x2)][(y1,y2)
proof
A1: 2 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
Indices (x1,x2)][(y1,y2)=[:Seg 2,Seg 2:] & 1 in Seg 2 by Th3,FINSEQ_1:2
,TARSKI:def 2;
hence thesis by A1,ZFMISC_1:87;
end;
definition
let D;
let a be Element of D;
redefine func <*a*> -> Element of 1-tuples_on D;
coherence by FINSEQ_2:98;
end;
definition
let D;
let n;
let p be Element of n-tuples_on D;
redefine func <*p*> -> Matrix of 1,n,D;
coherence
proof
len p = n by CARD_1:def 7;
hence thesis by MATRIX_1:11;
end;
end;
theorem
[1,1] in Indices <*<*a*>*> & <*<*a*>*>*(1,1)=a
proof
set M=<*<*a*>*>;
Indices M= [:Seg 1,Seg 1:] & 1 in Seg 1 by FINSEQ_1:2,MATRIX_1:24
,TARSKI:def 1;
hence
A1: [1,1] in Indices <*<*a*>*> by ZFMISC_1:87;
M.1= <*a*> & <*a*>.1=a by FINSEQ_1:40;
hence thesis by A1,MATRIX_1:def 5;
end;
definition
let D;
let a,b,c,d be Element of D;
redefine func (a,b)][(c,d) -> Matrix of 2,D;
coherence by MATRIX_1:19;
end;
theorem
(a,b)][(c,d)*(1,1)=a & (a,b)][(c,d)*(1,2)=b & (a,b)][(c,d)*(2,1)=c & (
a,b)][(c,d)*(2,2)=d
proof
set M=(a,b)][(c,d);
A1: M.1= <*a,b*> & M.2=<*c,d*> by FINSEQ_1:44;
A2: <*a,b*>.1=a & <*a,b*>.2=b by FINSEQ_1:44;
A3: [2,1] in Indices M & [2,2] in Indices M by Th4;
A4: <*c,d*>.1=c & <*c,d*>.2=d by FINSEQ_1:44;
[1,1] in Indices M & [1,2] in Indices M by Th4;
hence thesis by A1,A2,A4,A3,MATRIX_1:def 5;
end;
definition
let n, K;
let M be Matrix of n,K;
attr M is upper_triangular means
:Def3:
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 of n,K;
coherence
proof
let M be Diagonal of n,K;
for i,j st [i,j] in Indices M & i>j holds M*(i,j) = 0.K by MATRIX_1:def 14;
hence M is upper_triangular by Def3;
thus for i,j st [i,j] in Indices M & in;
hence contradiction by A1;
end;
suppose
A3: ex p be FinSequence of D st p in rng M & not len p=m;
consider k such that
A4: for x st x in rng M ex q st x = q & len q = k by MATRIX_1:9;
consider p be FinSequence of D such that
A5: p in rng M and
A6: len p<>m by A3;
reconsider x=p as set;
A7: ex q st x = q & len q = k by A5,A4;
now
per cases;
suppose
n= 0;
then M={} by A1;
hence len p= m by A5,RELAT_1:38;
end;
suppose
n>0;
then consider s being FinSequence such that
A8: s in rng M and
A9: len s = width M by A1,MATRIX_1:def 3;
reconsider y=s as set;
ex r st y = r & len r = k by A4,A8;
hence len p= m by A7,A9;
end;
end;
hence contradiction by A6;
end;
end;
begin :: Deleting of Rows and Columns in a Matrix
theorem Th8:
for M be Matrix of n,m,D holds for k st k in Seg n holds M.k= Line(M,k)
proof
let M be Matrix of n,m,D;
let k;
assume
A1: k in Seg n;
len M = n & dom M = Seg len M by FINSEQ_1:def 3,MATRIX_1:25;
then
A2: M.k in rng M by A1,FUNCT_1:def 3;
per cases;
suppose
n=0;
hence thesis by A1;
end;
suppose
A3: 0 < n;
consider l such that
A4: for x st x in rng M ex p be FinSequence of D st x = p & len p = l
by MATRIX_1:9;
consider p being FinSequence of D such that
A5: M.k = p and
len p= l by A2,A4;
A6: width M=m by A3,MATRIX_1:23;
A7: for j st j in Seg width M holds p.j = M*(k,j)
proof
let j;
assume j in Seg width M;
then [k,j] in [:Seg n,Seg m:] by A1,A6,ZFMISC_1:87;
then [k,j] in Indices M by A3,MATRIX_1:23;
then ex q being FinSequence of D st q=M.k & M*(k,j)=q.j by MATRIX_1:def 5
;
hence thesis by A5;
end;
len p=width M by A2,A6,A5,MATRIX_1:def 2;
hence thesis by A5,A7,MATRIX_1:def 7;
end;
end;
Lm1: for M be Matrix of K holds for k st k in dom M holds M.k=Line(M,k)
proof
let M be Matrix of K;
let k;
assume
A1: k in dom M;
then 1 <= k & k <= len M by FINSEQ_3:25;
then reconsider N = M as Matrix of len M, width M, K by MATRIX_1:20;
k in Seg len N by A1,FINSEQ_1:def 3;
hence thesis by Th8;
end;
definition
let i, K;
let M be Matrix of K;
func DelCol(M,i) -> Matrix of K means
len it=len M & for k st k in dom M holds it.k=Del(Line(M,k),i);
existence
proof
per cases;
suppose
A1: not i in Seg width M;
take M;
thus len M = len M;
let k such that
A2: k in dom M;
len Line(M,k) = width M by MATRIX_1:def 7;
then
A3: not i in dom Line(M,k) by A1,FINSEQ_1:def 3;
thus M.k = Line(M,k) by A2,Lm1
.= Del(Line(M,k),i) by A3,FINSEQ_3:104;
end;
suppose
A4: i in Seg width M;
defpred P[Nat,Nat,Element of K] means $3=Del(Line(M,$1),i).$2;
per cases;
suppose
A5: len M=0;
then Seg len M = {};
hence thesis by A4,A5,MATRIX_1:def 3;
end;
suppose
A6: len M>0;
set n1=width M;
per cases;
suppose
n1=0;
hence thesis by A4;
end;
suppose
n1>0;
then consider m being Nat such that
A7: n1=m+1 by NAT_1:6;
reconsider m as Element of NAT by ORDINAL1:def 12;
A8: for k st k in dom M holds len (Del(Line(M,k),i))=m
proof
let k;
assume k in dom M;
A9: len Line(M,k) = n1 by MATRIX_1:def 7;
then i in dom Line(M,k) by A4,FINSEQ_1:def 3;
then ex l being Nat st len Line(M,k)=l+1 & len Del(Line(M,k),i)=l
by FINSEQ_3:104;
hence thesis by A7,A9;
end;
A10: for k,l st [k,l] in [:Seg len M, Seg m:] ex x being Element of
K st P[k,l,x]
proof
let k,l;
assume
A11: [k,l] in [:Seg len M, Seg m:];
reconsider p=Del(Line(M,k),i) as FinSequence of K by FINSEQ_3:105;
dom M = Seg len M by FINSEQ_1:def 3;
then k in dom M by A11,ZFMISC_1:87;
then
A12: len p = m by A8;
A13: dom p = Seg len p by FINSEQ_1:def 3;
l in Seg m by A11,ZFMISC_1:87;
then reconsider x=p.l as Element of (the carrier of K) by A12,A13,
FINSEQ_2:11;
take x;
thus thesis;
end;
consider N being Matrix of len M,m,K such that
A14: for k,l st [k,l] in Indices N holds P[k,l,N*(k,l)] from
MATRIX_1:sch 2(A10);
dom M = Seg len M by FINSEQ_1:def 3;
then
A15: Indices N = [:dom M, Seg m :] by A6,MATRIX_1:23;
A16: for k,l st k in dom M & l in Seg m holds N*(k,l)=Del(Line(M,k), i).l
proof
let k,l;
assume k in dom M & l in Seg m;
then [k,l] in Indices N by A15,ZFMISC_1:87;
hence thesis by A14;
end;
A17: width N = m by A6,MATRIX_1:23;
reconsider N as Matrix of K;
take N;
for k st k in dom M holds N.k=Del(Line(M,k),i)
proof
let k;
assume
A18: k in dom M;
then k in Seg len M by FINSEQ_1:def 3;
then
A19: N.k=Line(N,k) by Th8;
reconsider s=N.k as FinSequence;
A20: len s= m by A17,A19,MATRIX_1:def 7;
then
A21: dom s = Seg m by FINSEQ_1:def 3;
A22: now
let j be Nat;
assume
A23: j in dom s;
then Line(N,k).j=N*(k,j) by A17,A21,MATRIX_1:def 7;
hence s.j=Del(Line(M,k),i).j by A16,A18,A19,A21,A23;
end;
len Del (Line(M,k),i)=m by A8,A18;
hence thesis by A20,A22,FINSEQ_2:9;
end;
hence thesis by A6,MATRIX_1:23;
end;
end;
end;
end;
uniqueness
proof
let M1,M2 be Matrix of K;
assume that
A24: len M1=len M and
A25: for k st k in dom M holds M1.k=Del(Line(M,k),i) and
A26: len M2=len M and
A27: for k st k in dom M holds M2.k=Del(Line(M,k),i);
A28: dom M1 = dom M by A24,FINSEQ_3:29;
now
let k be Nat;
assume
A29: k in dom M1;
hence M1.k=Del(Line(M,k),i) by A25,A28
.=M2.k by A27,A28,A29;
end;
hence thesis by A24,A26,FINSEQ_2:9;
end;
end;
theorem Th9:
for M1,M2 being Matrix of D st M1@=M2@ & len M1=len M2 holds M1 = M2
proof
let M1,M2 be Matrix of D;
assume that
A1: M1@=M2@ and
A2: len M1=len M2;
len (M1@) = width M1 by MATRIX_1:def 6;
then
A3: width M1=width M2 by A1,MATRIX_1:def 6;
A4: Indices M2=[:dom M2,Seg width M2:];
for i,j st [i,j] in Indices M1 holds M1*(i,j) = M2*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices M1;
dom M1 = Seg len M2 by A2,FINSEQ_1:def 3
.= dom M2 by FINSEQ_1:def 3;
then M2@*(j,i) = M2*(i,j) by A3,A4,A5,MATRIX_1:def 6;
hence thesis by A1,A5,MATRIX_1:def 6;
end;
hence thesis by A2,A3,MATRIX_1:21;
end;
theorem Th10:
for M being Matrix of D st width M > 0 holds len (M@)=width M &
width (M@)=len M
proof
let M be Matrix of D;
assume
A1: width M>0;
thus len (M@)=width M by MATRIX_1:def 6;
per cases;
suppose
len M=0;
hence thesis by A1,MATRIX_1:def 3;
end;
suppose
A2: len M>0;
for i,j being set holds [i,j]in [:dom (M@),Seg width (M@):] iff [i,j]
in [:Seg width M,dom M:]
proof
let i,j be set;
thus [i,j] in [:dom (M@),Seg width (M@):] implies [i,j] in [:Seg width M
,dom M:]
proof
assume
A3: [i,j]in [:dom (M@),Seg width (M@):];
then i in dom (M@) & j in Seg width (M@) by ZFMISC_1:87;
then reconsider i,j as Nat;
[i,j] in Indices (M@) by A3;
then [j,i] in Indices M by MATRIX_1:def 6;
hence thesis by ZFMISC_1:88;
end;
assume
A4: [i,j] in [:Seg width M,dom M:];
then i in Seg width M & j in dom M by ZFMISC_1:87;
then reconsider i,j as Nat;
[j,i] in Indices M by A4,ZFMISC_1:88;
then [i,j] in Indices (M@) by MATRIX_1:def 6;
hence thesis;
end;
then
dom M = Seg len M & [:Seg width M,dom M:]=[:dom (M@),Seg width (M@):]
by FINSEQ_1:def 3,ZFMISC_1:89;
then dom M=Seg width (M@) by A1,A2,ZFMISC_1:110;
hence thesis by FINSEQ_1:def 3;
end;
end;
theorem
for M1,M2 being Matrix of D st width M1>0 & width M2>0 & M1@=M2@ holds M1=M2
proof
let M1,M2 be Matrix of D;
assume width M1>0 & width M2>0;
then
A1: width (M1@)=len M1 & width (M2@)=len M2 by Th10;
assume M1@=M2@;
hence thesis by A1,Th9;
end;
theorem
for M1,M2 being Matrix of D st width M1>0 & width M2>0 holds M1=M2 iff
M1@=M2@ & width M1 = width M2
proof
let M1,M2 be Matrix of D;
assume that
A1: width M1>0 and
A2: width M2>0;
thus M1=M2 implies M1@=M2@ & width (M1) =width (M2);
assume that
A3: M1@=M2@ and
A4: width (M1) =width (M2);
len M1=width (M1@) by A1,Th10;
then
A5: len M1=len M2 by A2,A3,Th10;
A6: Indices M2=[:dom M2,Seg width M2:];
for i,j st [i,j] in Indices M1 holds M1*(i,j) = M2*(i,j)
proof
let i,j;
assume
A7: [i,j] in Indices M1;
dom M1 = Seg len M2 by A5,FINSEQ_1:def 3
.= dom M2 by FINSEQ_1:def 3;
then M2@*(j,i)=M2*(i,j) by A4,A6,A7,MATRIX_1:def 6;
hence thesis by A3,A7,MATRIX_1:def 6;
end;
hence thesis by A4,A5,MATRIX_1:21;
end;
theorem Th13:
for M being Matrix of D st len M>0 & width M>0 holds (M@)@=M
proof
let M be Matrix of D;
assume that
A1: len M>0 and
A2: width M>0;
set N=M@;
A3: width N= len M by A2,Th10;
A4: len (N@) = width N by MATRIX_1:def 6;
A5: len N = width M by MATRIX_1:def 6;
dom M = Seg len M & dom (N@) = Seg len (N@) by FINSEQ_1:def 3;
then
A6: Indices (N@)=Indices M by A1,A5,A3,A4,Th10;
A7: for i,j st [i,j] in Indices (N@) holds (N@)*(i,j) = M*(i,j)
proof
let i,j;
assume
A8: [i,j] in Indices (N@);
then [j,i] in Indices N by MATRIX_1:def 6;
then (N@)*(i,j)=N*(j,i) by MATRIX_1:def 6;
hence thesis by A6,A8,MATRIX_1:def 6;
end;
width N>0 by A1,A2,Th10;
then width (N@)=width M by A5,Th10;
hence thesis by A3,A4,A7,MATRIX_1:21;
end;
theorem Th14:
for M being Matrix of D holds for i st i in dom M holds Line(M,i )=Col(M@,i)
proof
let M be Matrix of D;
let i;
A1: len (M@)=width M by MATRIX_1:def 6;
len Col(M@,i) = len (M@) by MATRIX_1:def 8;
then
A2: len Col(M@,i)=width M by MATRIX_1:def 6;
then
A3: dom Col(M@,i) = Seg width M by FINSEQ_1:def 3;
assume
A4: i in dom M;
A5: now
let j be Nat;
A6: dom (M@) = Seg len (M@) by FINSEQ_1:def 3;
assume
A7: j in dom Col(M@,i);
then Line(M,i).j=M*(i,j) & [i,j] in Indices M by A4,A3,MATRIX_1:def 7
,ZFMISC_1:87;
hence Line(M,i).j=M@*(j,i) by MATRIX_1:def 6
.=Col(M@,i).j by A1,A3,A7,A6,MATRIX_1:def 8;
end;
len Line(M,i) = width M by MATRIX_1:def 7;
hence thesis by A2,A5,FINSEQ_2:9;
end;
theorem
for M being Matrix of D holds for j st j in Seg width M holds Line(M@,
j)=Col(M,j)
proof
let M be Matrix of D;
let j;
assume
A1: j in Seg width M;
then j in Seg len (M@) by MATRIX_1:def 6;
then
A2: j in dom (M@) by FINSEQ_1:def 3;
per cases;
suppose
A3: len M=0;
then Seg len M = {};
hence thesis by A1,A3,MATRIX_1:def 3;
end;
suppose
A4: len M>0;
per cases;
suppose
width M=0;
hence thesis by A1;
end;
suppose
width M>0;
then (M@)@=M by A4,Th13;
hence thesis by A2,Th14;
end;
end;
end;
theorem
for M being Matrix of D holds for i st i in dom M holds M.i=Line(M,i)
proof
let M be Matrix of D;
let i;
assume
A1: i in dom M;
then
A2: M.i in rng M by FUNCT_1:def 3;
rng M c= D* by FINSEQ_1:def 4;
then reconsider p=M.i as FinSequence of D by A2,FINSEQ_1:def 11;
M<> {} by A1;
then M is Matrix of len M,width M,D by MATRIX_1:20;
then
A3: len p = width M by A2,MATRIX_1:def 2;
A4: len Line(M,i)= width M by MATRIX_1:def 7;
then
A5: dom Line(M,i) = Seg width M by FINSEQ_1:def 3;
A6: for j st j in Seg (width M) holds M*(i,j) =p.j
proof
let j;
assume j in Seg(width M);
then [i,j] in Indices M by A1,ZFMISC_1:87;
then ex q being FinSequence of D st q=M.i & q.j=M*(i,j) by MATRIX_1:def 5;
hence thesis;
end;
now
let j be Nat;
assume
A7: j in dom Line(M,i);
hence (Line(M,i)).j=M*(i,j) by A5,MATRIX_1:def 7
.=p.j by A6,A5,A7;
end;
hence thesis by A3,A4,FINSEQ_2:9;
end;
notation
let K, i;
let M be Matrix of K;
synonym DelLine(M,i) for Del(M,i);
end;
registration
let K, i;
let M be Matrix of K;
cluster DelLine(M,i) -> tabular;
coherence
proof
consider n being Nat such that
A1: for x st x in rng M ex s being FinSequence st s=x & len s = n by
MATRIX_1:def 1;
take n;
let x;
A2: rng DelLine(M,i) c= rng M by FINSEQ_3:106;
assume x in rng DelLine(M,i);
hence thesis by A1,A2;
end;
end;
definition
let K, i;
let M be Matrix of K;
redefine func DelLine(M,i) -> Matrix of K;
coherence by FINSEQ_3:105;
end;
definition
let i,j,n,K;
let M be Matrix of n,K;
func Deleting(M,i,j) -> Matrix of K equals
DelCol(DelLine(M,i),j);
coherence;
end;
begin :: Sets of Permutations
definition
let IT be set;
attr IT is permutational means
:Def7:
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
:Def8:
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 Def7;
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 Def7;
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 Def7;
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 Def8;
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 Def7;
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 Def8,ORDINAL1:def 12;
hence thesis by A1,FINSEQ_1:def 3;
end;
hence thesis;
end;
definition
let n;
func Permutations n -> set means
:Def9:
x in it iff x is Permutation of Seg n;
existence
proof
defpred P[set] means $1 is Permutation of Seg n;
consider P being set such that
A1: for x 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;
assume x in P2;
then x is Permutation of Seg n by A4;
hence x in P1 by A3;
end;
now
let x;
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:1;
end;
end;
registration
let n;
cluster Permutations(n) -> permutational non empty;
coherence
proof
defpred P[set] means $1 is Permutation of Seg n;
consider P being set such that
A1: for x 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 Def7;
x in P iff x is Permutation of Seg n
proof
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;
hence thesis by Def9;
end;
end;
theorem
len Permutations(n)=n
proof
set x = the Element of Permutations(n);
reconsider q=x as Permutation of Seg n by Def9;
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 Def8;
end;
theorem
Permutations 1 = {idseq 1}
proof
A1: Permutations 1 c={idseq 1}
proof
let p be set;
assume p in Permutations 1;
then reconsider q=p as Permutation of Seg 1 by Def9;
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;
assume x in {idseq 1};
then x= idseq 1 by TARSKI:def 1;
hence thesis by Def9;
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
:Def10:
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 Def9;
reconsider z=p*q as Element of Permutations(n) by Def9;
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 Def10;
hence the carrier of Group_of_Perm(n) is non empty;
end;
end;
theorem Th20:
idseq n is Element of Group_of_Perm(n)
proof
the carrier of Group_of_Perm(n) = Permutations(n) by Def10;
hence thesis by Def9;
end;
theorem Th21:
p *(idseq n)=p & (idseq n)*p=p
proof
A1: Seg n = {} implies Seg n= {};
p is Permutation of Seg n by Def9;
then
A2: rng p= Seg n by FUNCT_2:def 3;
p is Function of Seg n,Seg n by Def9;
then dom p= Seg n by A1,FUNCT_2:def 1;
hence thesis by A2,RELAT_1:52,54;
end;
theorem Th22:
p *p"=idseq n & p"*p=idseq n
proof
p is Permutation of Seg n by Def9;
hence thesis by FUNCT_2:61;
end;
theorem Th23:
p" is Element of Group_of_Perm(n)
proof
reconsider p as Permutation of Seg n by Def9;
p" is Element of Permutations(n) by Def9;
hence thesis by Def10;
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 Th20;
take e;
reconsider e9=idseq n as Element of Permutations(n) by Def9;
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 Def10;
reconsider r=q as Permutation of Seg n by Def9;
reconsider f=r" as Element of Permutations(n) by Def9;
reconsider g=f as Element of Group_of_Perm(n) by Th23;
take g;
A3: g * p= q*f by Def10
.=e by Th22;
p * g= f*q by Def10
.=e by Th22;
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 Def10;
A4: e * p =p9 * e9 by Def10
.=p by Th21;
p * e =e9 * p9 by Def10
.=p by Th21;
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 Def10;
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 Def9;
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 Def9;
A7: r9 * q9 is Element of Permutations(n) by A5,Def9;
(p * q) * r =(the multF of Group_of_Perm n).((q9*p9),r9) by Def10
.=r9*(q9 *p9 ) by A6,Def10
.=(r9 *q9) * p9 by RELAT_1:36
.=(the multF of Group_of_Perm n).(p9,(r9*q9)) by A7,Def10
.=p *(q* r) by Def10;
hence thesis;
end;
hence thesis by A1,GROUP_1:1;
end;
end;
theorem Th24:
idseq n= 1_Group_of_Perm(n)
proof
reconsider e=idseq n as Element of Group_of_Perm(n) by Th20;
reconsider e9=idseq n as Element of Permutations(n) by Def9;
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 Def10;
A1: e * p =p9 * e9 by Def10
.=p by Th21;
p * e =e9 * p9 by Def10
.=p by Th21;
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
:Def12:
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 Th24;
for i st i in dom l ex q st l.i=q & q is being_transposition;
hence thesis by A1,A2,Def12;
end;
definition
let K,n;
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;
definition
let X be set;
assume
A1: X is finite;
func FinOmega X -> Element of Fin X equals
X;
coherence by A1,FINSUB_1:def 5;
end;
theorem
Permutations n is finite
proof
A1: Permutations n c= Funcs(Seg n,Seg n)
proof
let x;
assume x in Permutations n;
then x is Function of Seg n,Seg n by Def9;
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;