The abstract of the Mizar article:

Transpose Matrices and Groups of Permutations

by

Katarzyna Jankowska

Received May 20, 1992

MML identifier: MATRIX_2

[ Mizar article, MML identifier index ]

environ

 vocabulary VECTSP_1, FINSEQ_1, RELAT_1, FUNCT_1, FUNCOP_1, MATRIX_1, FINSEQ_2,
      TREES_1, RLVECT_1, BOOLE, CARD_1, INCSP_1, QC_LANG1, FUNCT_2, BINOP_1,
      GROUP_1, NAT_1, ARYTM_1, FINSET_1, FINSUB_1, MATRIX_2, CARD_3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, RELAT_1, FUNCT_1,
      PARTFUN1, FUNCT_2, STRUCT_0, NAT_1, GROUP_1, GROUP_4, BINOP_1, RLVECT_1,
      VECTSP_1, FINSEQ_1, CARD_1, MATRIX_1, FINSET_1, FINSUB_1, FINSEQ_2,
      FINSEQ_4, FINSEQOP;
 constructors NAT_1, GROUP_4, BINOP_1, MATRIX_1, FINSEQOP, FINSEQ_4, MEMBERED,
      PARTFUN1, RELAT_2, XBOOLE_0;
 clusters FUNCT_1, GROUP_1, MATRIX_1, FINSET_1, RELSET_1, STRUCT_0, FINSEQ_1,
      FINSEQ_2, XREAL_0, ARYTM_3, FUNCT_2, ZFMISC_1, PARTFUN1, XBOOLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


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;

scheme SeqDEx{D()->non empty set,A()->Nat,P[set,set]}:
  ex p being FinSequence of D() st dom p = Seg A() &
                     for k st k in Seg A() holds P[k,p.k]
 provided
 for k st k in Seg A() ex x being Element of D() st P[k,x];

definition let n,m; let a be set;
 func (n,m) --> a -> tabular FinSequence equals
:: MATRIX_2:def 1
   n |-> (m |-> a);
end;

 definition
  let D,n,m;let d;
  redefine func (n,m) --> d ->Matrix of n,m,D;
 end;

theorem :: MATRIX_2:1
 [i,j] in Indices ((n,m)-->a) implies ((n,m)-->a) *(i,j)=a;

 reserve a',b' for Element of K;

theorem :: MATRIX_2:2
  ((n,n)-->a') + ((n,n)-->b')= (n,n)-->(a'+b');

definition
 let a,b,c,d be set;
 func (a,b)][(c,d) ->tabular FinSequence equals
:: MATRIX_2:def 2
 <*<*a,b*>,<*c,d*>*>;
 end;

theorem :: MATRIX_2:3
len (x1,x2)][(y1,y2)=2 & width (x1,x2)][(y1,y2)=2 &
        Indices (x1,x2)][(y1,y2)=[:Seg 2,Seg 2:];

theorem :: MATRIX_2:4
 [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);

definition let D;let a be Element of D;
 redefine func <*a*> -> Element of 1-tuples_on D;
end;

 definition let D;let n;let p be Element of n-tuples_on D;
 redefine func <*p*> -> Matrix of 1,n,D;
 end;

theorem :: MATRIX_2:5
   [1,1] in Indices <*<*a*>*> & <*<*a*>*>*(1,1)=a;

 definition let D;let a,b,c,d be Element of D;
  redefine func (a,b)][(c,d) -> Matrix of 2,D;
  end;

theorem :: MATRIX_2:6
   (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;

definition let n;let K be Field;
mode Upper_Triangular_Matrix of n,K -> Matrix of n,K means
:: MATRIX_2:def 3
   for i,j st [i,j] in Indices it holds
          (i>j implies it*(i,j) = 0.K );
end;

definition let n;let K;
mode Lower_Triangular_Matrix of n,K -> Matrix of n,K means
:: MATRIX_2:def 4
   for i,j st [i,j] in Indices it holds
          (i<j implies it*(i,j) = 0.K );
end;

theorem :: MATRIX_2:7
  for M being Matrix of D st len M=n holds M is Matrix of n,width M,D;

begin :: Deleting of Rows and Columns in a Matrix

definition let i; let p be FinSequence;
func Del(p,i) -> FinSequence equals
:: MATRIX_2:def 5
   p * Sgm ((dom p) \ {i});
end;

theorem :: MATRIX_2:8
for p being FinSequence holds
  (i in dom p implies ex m st len p = m + 1 & len Del(p,i) = m) &
  (not i in dom p implies Del(p,i) = p);

theorem :: MATRIX_2:9
 for p being FinSequence of D holds Del(p,i) is FinSequence of D;

theorem :: MATRIX_2:10
for M be Matrix of n,m,K holds
  for k st k in Seg n holds M.k=Line(M,k);

definition let i;
let K;
let M be Matrix of K;
assume i in Seg (width M);
func DelCol(M,i) -> Matrix of K means
:: MATRIX_2:def 6
  len it=len M & for k st k in dom M holds it.k=Del(Line(M,k),i);
end;

theorem :: MATRIX_2:11
 for M1,M2 being Matrix of D st M1@=M2@ & len M1=len M2
      holds M1 = M2;

theorem :: MATRIX_2:12
for M being Matrix of D st width M > 0
        holds len (M@)=width M & width (M@)=len M;

theorem :: MATRIX_2:13
   for M1,M2 being Matrix of D st width M1>0 & width M2>0 &
     M1@=M2@ & width (M1@) =width (M2@)
     holds M1=M2;

theorem :: MATRIX_2:14
 for M1,M2 being Matrix of D st width M1>0 & width M2>0 holds
     M1=M2 iff M1@=M2@ & width M1 = width M2;

theorem :: MATRIX_2:15
for M being Matrix of D st len M>0 & width M>0 holds (M@)@=M;

theorem :: MATRIX_2:16
for M being Matrix of D holds
       for i st i in dom M holds Line(M,i)=Col(M@,i);

theorem :: MATRIX_2:17
for M being Matrix of D holds
       for j st j in Seg(width M) holds Line(M@,j)=Col(M,j);

theorem :: MATRIX_2:18
for M being Matrix of D holds for i st i in dom M holds M.i=Line(M,i);

definition let i; let K;let M be Matrix of K;
assume i in dom M & width M>0;
func DelLine(M,i) -> Matrix of K means
:: MATRIX_2:def 7
     it={} if len M=1 otherwise
     width it=width M &
     for k st k in Seg (width M) holds Col(it,k)=Del(Col(M,k),i);
end;

definition let i,j; let n;let K;let M be Matrix of n,K;
func Deleting(M,i,j) -> Matrix of K equals
:: MATRIX_2:def 8
    {} if n=1 otherwise
     DelCol((DelLine(M,i)),j);
end;

begin :: Sets of Permutations

definition let IT be set;
  attr IT is permutational means
:: MATRIX_2:def 9
 ex n st for x st x in IT holds x is Permutation of Seg n;
end;

definition
 cluster permutational non empty set;
end;

definition let P be permutational non empty set;
func len P -> Nat means
:: MATRIX_2:def 10
 ex s st s in P & it=len s;
 end;

definition let P be permutational non empty set;
redefine mode Element of P -> Permutation of Seg len P;
 end;

theorem :: MATRIX_2:19
   ex P being permutational non empty set st len P =n;

definition let n;
func Permutations(n) -> set means
:: MATRIX_2:def 11
x in it iff x is Permutation of Seg n;
end;

definition let n;
cluster Permutations(n) -> permutational non empty;
end;

theorem :: MATRIX_2:20
  len Permutations(n)=n;

theorem :: MATRIX_2:21
  Permutations(1)={idseq 1};

definition let n;let p be Element of Permutations(n);
func len p -> Nat means
:: MATRIX_2:def 12
 ex s being FinSequence st s=p & it=len s;
end;

theorem :: MATRIX_2:22
  for p being Element of Permutations(n) holds len p= n;

begin :: Group of Permutations

reserve p,q for Element of Permutations(n);

definition let n;
 func Group_of_Perm(n) -> strict HGrStr means
:: MATRIX_2:def 13
 the carrier of it = Permutations(n) &
  for q,p be Element of Permutations(n) holds (the mult of it).(q,p)=p*q;
end;

definition let n;
 cluster Group_of_Perm(n) -> non empty;
end;

theorem :: MATRIX_2:23
 idseq n is Element of Group_of_Perm(n);

theorem :: MATRIX_2:24
  p *(idseq n)=p & (idseq n)*p=p;

theorem :: MATRIX_2:25
 p *p"=idseq n & p"*p=idseq n;

theorem :: MATRIX_2:26
p" is Element of Group_of_Perm(n);

 definition let n;
  mode permutation of n is Element of Permutations(n);
  cluster Group_of_Perm(n) -> associative Group-like;
 end;

canceled;

theorem :: MATRIX_2:28
 idseq n= 1.Group_of_Perm(n);

definition let n;let p be Permutation of Seg n;
 attr p is being_transposition means
:: MATRIX_2:def 14
     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;
  synonym p is_transposition;
end;

definition let n;
  let IT be Permutation of Seg n;
  attr IT is even means
:: MATRIX_2:def 15
ex l be FinSequence of the carrier 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_transposition;
 antonym IT is odd;
end;

theorem :: MATRIX_2:29
  id Seg n is even;

definition
 let K,n;let x be Element of K;
 let p be Element of Permutations(n);
func -(x,p)-> Element of K equals
:: MATRIX_2:def 16
     x if p is even otherwise -x;
end;

definition let X be set;
assume X is finite;
func FinOmega(X) -> Element of Fin X equals
:: MATRIX_2:def 17
   X;
end;

theorem :: MATRIX_2:30
   Permutations(n) is finite;