:: Transpose Matrices and Groups of Permutations
:: by Katarzyna Jankowska
::
:: Received May 20, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

definition
let n, m be Nat;
let a be set ;
func (n,m) --> a -> tabular FinSequence equals :: MATRIX_2:def 1
n |-> (m |-> a);
coherence
n |-> (m |-> a) is tabular FinSequence by MATRIX_1:2;
end;

:: deftheorem defines --> MATRIX_2:def 1 :
for n, m being Nat
for a being set holds (n,m) --> a = n |-> (m |-> a);

definition
let D be non empty set ;
let n, m be Nat;
let d be Element of D;
:: original: -->
redefine func (n,m) --> d -> Matrix of n,m,D;
coherence
(n,m) --> d is Matrix of n,m,D by MATRIX_1:10;
end;

theorem Th1: :: MATRIX_2:1
for i, j, n, m being Nat
for D being non empty set
for a being Element of D st [i,j] in Indices ((n,m) --> a) holds
((n,m) --> a) * (i,j) = a
proof end;

theorem :: MATRIX_2:2
for n being Nat
for K being Field
for a9, b9 being Element of K holds ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9)
proof end;

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

:: deftheorem defines ][ MATRIX_2:def 2 :
for a, b, c, d being set holds (a,b) ][ (c,d) = <*<*a,b*>,<*c,d*>*>;

theorem Th3: :: MATRIX_2:3
for x1, x2, y1, y2 being set holds
( len ((x1,x2) ][ (y1,y2)) = 2 & width ((x1,x2) ][ (y1,y2)) = 2 & Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):] )
proof end;

theorem Th4: :: MATRIX_2:4
for x1, x2, y1, y2 being set holds
( [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 end;

definition
let D be non empty set ;
let a be Element of D;
:: original: <*
redefine func <*a*> -> Element of 1 -tuples_on D;
coherence
<*a*> is Element of 1 -tuples_on D by FINSEQ_2:98;
end;

definition
let D be non empty set ;
let n be Nat;
let p be Element of n -tuples_on D;
:: original: <*
redefine func <*p*> -> Matrix of 1,n,D;
coherence
<*p*> is Matrix of 1,n,D
proof end;
end;

theorem :: MATRIX_2:5
for D being non empty set
for a being Element of D holds
( [1,1] in Indices <*<*a*>*> & <*<*a*>*> * (1,1) = a )
proof end;

definition
let D be non empty set ;
let a, b, c, d be Element of D;
:: original: ][
redefine func (a,b) ][ (c,d) -> Matrix of 2,D;
coherence
(a,b) ][ (c,d) is Matrix of 2,D by MATRIX_1:19;
end;

theorem :: MATRIX_2:6
for D being non empty set
for a, b, c, d being Element of D holds
( ((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 end;

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
attr M is upper_triangular means :Def3: :: MATRIX_2:def 3
 for i, j being Nat st [i,j] in Indices M & i > j holds
M * (i,j) = 0. K;
attr M is lower_triangular means :: MATRIX_2:def 4
 for i, j being Nat st [i,j] in Indices M & i < j holds
M * (i,j) = 0. K;
end;

:: deftheorem Def3 defines upper_triangular MATRIX_2:def 3 :
for n being Nat
for K being Field
for M being Matrix of n,K holds
( M is upper_triangular iff for i, j being Nat st [i,j] in Indices M & i > j holds
M * (i,j) = 0. K );

:: deftheorem defines lower_triangular MATRIX_2:def 4 :
for n being Nat
for K being Field
for M being Matrix of n,K holds
( M is lower_triangular iff for i, j being Nat st [i,j] in Indices M & i < j holds
M * (i,j) = 0. K );

registration
let n be Nat;
let K be Field;
cluster diagonal -> upper_triangular lower_triangular for Matrix of n,n, the carrier of K;
coherence
for b1 being Diagonal of n,K holds
( b1 is upper_triangular & b1 is lower_triangular )
proof end;
end;

registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular upper_triangular lower_triangular for Matrix of n,n, the carrier of K;
existence
ex b1 being Matrix of n,K st
( b1 is lower_triangular & b1 is upper_triangular )
proof end;
end;

definition
let n be Nat;
let K be Field;
mode Upper_Triangular_Matrix of n,K is upper_triangular Matrix of n,K;
mode Lower_Triangular_Matrix of n,K is lower_triangular Matrix of n,K;
end;

theorem :: MATRIX_2:7
for n being Nat
for D being non empty set
for M being Matrix of D st len M = n holds
M is Matrix of n, width M,D
proof end;

begin

theorem Th8: :: MATRIX_2:8
for n, m being Nat
for D being non empty set
for M being Matrix of n,m,D
for k being Nat st k in Seg n holds
M . k = Line (M,k)
proof end;

Lm1: for K being Field
for M being Matrix of K
for k being Nat st k in dom M holds
M . k = Line (M,k)
proof end;

definition
let i be Nat;
let K be Field;
let M be Matrix of K;
func DelCol (M,i) -> Matrix of K means :: MATRIX_2:def 5
( len it = len M & ( for k being Nat st k in dom M holds
it . k = Del ((Line (M,k)),i) ) );
existence
ex b1 being Matrix of K st
( len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del ((Line (M,k)),i) ) )
proof end;
uniqueness
for b1, b2 being Matrix of K st len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del ((Line (M,k)),i) ) & len b2 = len M & ( for k being Nat st k in dom M holds
b2 . k = Del ((Line (M,k)),i) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines DelCol MATRIX_2:def 5 :
for i being Nat
for K being Field
for M, b4 being Matrix of K holds
( b4 = DelCol (M,i) iff ( len b4 = len M & ( for k being Nat st k in dom M holds
b4 . k = Del ((Line (M,k)),i) ) ) );

theorem Th9: :: MATRIX_2:9
for D being non empty set
for M1, M2 being Matrix of D st M1 @ = M2 @ & len M1 = len M2 holds
M1 = M2
proof end;

theorem Th10: :: MATRIX_2:10
for D being non empty set
for M being Matrix of D st width M > 0 holds
( len (M @) = width M & width (M @) = len M )
proof end;

theorem :: MATRIX_2:11
for D being non empty set
for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 & M1 @ = M2 @ holds
M1 = M2
proof end;

theorem :: MATRIX_2:12
for D being non empty set
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 end;

theorem Th13: :: MATRIX_2:13
for D being non empty set
for M being Matrix of D st len M > 0 & width M > 0 holds
(M @) @ = M
proof end;

theorem Th14: :: MATRIX_2:14
for D being non empty set
for M being Matrix of D
for i being Nat st i in dom M holds
Line (M,i) = Col ((M @),i)
proof end;

theorem :: MATRIX_2:15
for D being non empty set
for M being Matrix of D
for j being Nat st j in Seg (width M) holds
Line ((M @),j) = Col (M,j)
proof end;

theorem :: MATRIX_2:16
for D being non empty set
for M being Matrix of D
for i being Nat st i in dom M holds
M . i = Line (M,i)
proof end;

notation
let K be Field;
let i be Nat;
let M be Matrix of K;
synonym DelLine (M,i) for Del (i,K);
end;

registration
let K be Field;
let i be Nat;
let M be Matrix of K;
cluster DelLine (,M) -> tabular ;
coherence
DelLine (,M) is tabular
proof end;
end;

definition
let K be Field;
let i be Nat;
let M be Matrix of K;
:: original: DelLine
redefine func DelLine (M,i) -> Matrix of K;
coherence
DelLine (,M) is Matrix of K by FINSEQ_3:105;
end;

definition
let i, j, n be Nat;
let K be Field;
let M be Matrix of n,K;
func Deleting (M,i,j) -> Matrix of K equals :: MATRIX_2:def 6
 DelCol ((DelLine (M,i)),j);
coherence
DelCol ((DelLine (M,i)),j) is Matrix of K ;
end;

:: deftheorem defines Deleting MATRIX_2:def 6 :
for i, j, n being Nat
for K being Field
for M being Matrix of n,K holds Deleting (M,i,j) = DelCol ((DelLine (M,i)),j);

begin

definition
let IT be set ;
attr IT is permutational means :Def7: :: MATRIX_2:def 7
 ex n being Nat st
for x being set st x in IT holds
x is Permutation of (Seg n);
end;

:: deftheorem Def7 defines permutational MATRIX_2:def 7 :
for IT being set holds
( IT is permutational iff ex n being Nat st
for x being set st x in IT holds
x is Permutation of (Seg n) );

registration
cluster non empty permutational for set ;
existence
ex b1 being set st
( b1 is permutational & not b1 is empty )
proof end;
end;

definition
let P be non empty permutational set ;
func len P -> Nat means :Def8: :: MATRIX_2:def 8
 ex s being FinSequence st
( s in P & it = len s );
existence
ex b1 being Nat ex s being FinSequence st
( s in P & b1 = len s )
proof end;
uniqueness
for b1, b2 being Nat st ex s being FinSequence st
( s in P & b1 = len s ) & ex s being FinSequence st
( s in P & b2 = len s ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines len MATRIX_2:def 8 :
for P being non empty permutational set
for b2 being Nat holds
( b2 = len P iff ex s being FinSequence st
( s in P & b2 = len s ) );

definition
let P be non empty permutational set ;
:: original: len
redefine func len P -> Element of NAT ;
coherence
len P is Element of NAT by ORDINAL1:def 12;
end;

definition
let P be non empty permutational set ;
:: original: Element
redefine mode Element of P -> Permutation of (Seg (len P));
coherence
for b1 being Element of P holds b1 is Permutation of (Seg (len P))
proof end;
end;

theorem :: MATRIX_2:17
for n being Nat ex P being non empty permutational set st len P = n
proof end;

definition
let n be Nat;
func Permutations n -> set means :Def9: :: MATRIX_2:def 9
 for x being set holds
( x in it iff x is Permutation of (Seg n) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is Permutation of (Seg n) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Permutation of (Seg n) ) ) & ( for x being set holds
( x in b2 iff x is Permutation of (Seg n) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines Permutations MATRIX_2:def 9 :
for n being Nat
for b2 being set holds
( b2 = Permutations n iff for x being set holds
( x in b2 iff x is Permutation of (Seg n) ) );

registration
let n be Nat;
cluster Permutations n -> non empty permutational ;
coherence
( Permutations n is permutational & not Permutations n is empty )
proof end;
end;

theorem :: MATRIX_2:18
for n being Nat holds len (Permutations n) = n
proof end;

theorem :: MATRIX_2:19
Permutations 1 = {(idseq 1)}
proof end;

begin

definition
let n be Nat;
func Group_of_Perm n -> strict multMagma means :Def10: :: MATRIX_2:def 10
( the carrier of it = Permutations n & ( for q, p being Element of Permutations n holds the multF of it . (q,p) = p * q ) );
existence
ex b1 being strict multMagma st
( the carrier of b1 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b1 . (q,p) = p * q ) )
proof end;
uniqueness
for b1, b2 being strict multMagma st the carrier of b1 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b1 . (q,p) = p * q ) & the carrier of b2 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b2 . (q,p) = p * q ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines Group_of_Perm MATRIX_2:def 10 :
for n being Nat
for b2 being strict multMagma holds
( b2 = Group_of_Perm n iff ( the carrier of b2 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b2 . (q,p) = p * q ) ) );

registration
let n be Nat;
cluster Group_of_Perm n -> non empty strict ;
coherence
not Group_of_Perm n is empty
proof end;
end;

theorem Th20: :: MATRIX_2:20
for n being Nat holds idseq n is Element of (Group_of_Perm n)
proof end;

theorem Th21: :: MATRIX_2:21
for n being Nat
for p being Element of Permutations n holds
( p * (idseq n) = p & (idseq n) * p = p )
proof end;

theorem Th22: :: MATRIX_2:22
for n being Nat
for p being Element of Permutations n holds
( p * (p ") = idseq n & (p ") * p = idseq n )
proof end;

theorem Th23: :: MATRIX_2:23
for n being Nat
for p being Element of Permutations n holds p " is Element of (Group_of_Perm n)
proof end;

registration
let n be Nat;
cluster Group_of_Perm n -> strict Group-like associative ;
coherence
( Group_of_Perm n is associative & Group_of_Perm n is Group-like )
proof end;
end;

theorem Th24: :: MATRIX_2:24
for n being Nat holds idseq n = 1_ (Group_of_Perm n)
proof end;

definition
let n be Nat;
let p be Permutation of (Seg n);
attr p is being_transposition means :: MATRIX_2:def 11
 ex i, j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) );
end;

:: deftheorem defines being_transposition MATRIX_2:def 11 :
for n being Nat
for p being Permutation of (Seg n) holds
( p is being_transposition iff ex i, j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) ) );

definition
let n be Nat;
let IT be Permutation of (Seg n);
attr IT is even means :Def12: :: MATRIX_2:def 12
 ex l being FinSequence of (Group_of_Perm n) st
( (len l) mod 2 = 0 & IT = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) );
end;

:: deftheorem Def12 defines even MATRIX_2:def 12 :
for n being Nat
for IT being Permutation of (Seg n) holds
( IT is even iff ex l being FinSequence of (Group_of_Perm n) st
( (len l) mod 2 = 0 & IT = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) ) );

notation
let n be Nat;
let IT be Permutation of (Seg n);
antonym odd IT for even ;
end;

theorem :: MATRIX_2:25
for n being Nat holds id (Seg n) is even
proof end;

definition
let K be Field;
let n be Nat;
let x be Element of K;
let p be Element of Permutations n;
func - (x,p) -> Element of K equals :: MATRIX_2:def 13
x if p is even
otherwise - x;
correctness
coherence
( ( p is even implies x is Element of K ) & ( not p is even implies - x is Element of K ) );
consistency
for b1 being Element of K holds verum;
;
end;

:: deftheorem defines - MATRIX_2:def 13 :
for K being Field
for n being Nat
for x being Element of K
for p being Element of Permutations n holds
( ( p is even implies - (x,p) = x ) & ( not p is even implies - (x,p) = - x ) );

definition
let X be set ;
assume A1: X is finite ;
func FinOmega X -> Element of Fin X equals :: MATRIX_2:def 14
X;
coherence
X is Element of Fin X by A1, FINSUB_1:def 5;
end;

:: deftheorem defines FinOmega MATRIX_2:def 14 :
for X being set st X is finite holds
FinOmega X = X;

theorem :: MATRIX_2:26
for n being Nat holds Permutations n is finite
proof end;