:: Abelian Group of Matrices
:: by Katarzyna Jankowska
::
:: Received June 8, 1991
:: Copyright (c) 1991-2015 Association of Mizar Users


definition
let K be non empty 1-sorted ;
mode Matrix of K is Matrix of the carrier of K;
let n be Nat;
mode Matrix of n,K is Matrix of n,n, the carrier of K;
let m be Nat;
mode Matrix of n,m,K is Matrix of n,m, the carrier of K;
end;

definition
let K be non empty doubleLoopStr ;
let n be Nat;
func n -Matrices_over K -> set equals :: MATRIX_1:def 1
n -tuples_on (n -tuples_on the carrier of K);
coherence
n -tuples_on (n -tuples_on the carrier of K) is set ;
func 0. (K,n) -> Matrix of n,K equals :: MATRIX_1:def 2
n |-> (n |-> (0. K));
coherence
n |-> (n |-> (0. K)) is Matrix of n,K by MATRIX_0:10;
func 1. (K,n) -> Matrix of n,K means :Def3: :: MATRIX_1:def 3
( ( for i being Nat st [i,i] in Indices it holds
it * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices it & i <> j holds
it * (i,j) = 0. K ) );
existence
ex b1 being Matrix of n,K st
( ( for i being Nat st [i,i] in Indices b1 holds
b1 * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices b1 & i <> j holds
b1 * (i,j) = 0. K ) )
proof end;
uniqueness
for b1, b2 being Matrix of n,K st ( for i being Nat st [i,i] in Indices b1 holds
b1 * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices b1 & i <> j holds
b1 * (i,j) = 0. K ) & ( for i being Nat st [i,i] in Indices b2 holds
b2 * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices b2 & i <> j holds
b2 * (i,j) = 0. K ) holds
b1 = b2
proof end;
let A be Matrix of n,K;
func - A -> Matrix of n,K means :Def4: :: MATRIX_1:def 4
 for i, j being Nat st [i,j] in Indices A holds
it * (i,j) = - (A * (i,j));
existence
ex b1 being Matrix of n,K st
for i, j being Nat st [i,j] in Indices A holds
b1 * (i,j) = - (A * (i,j))
proof end;
uniqueness
for b1, b2 being Matrix of n,K st ( for i, j being Nat st [i,j] in Indices A holds
b1 * (i,j) = - (A * (i,j)) ) & ( for i, j being Nat st [i,j] in Indices A holds
b2 * (i,j) = - (A * (i,j)) ) holds
b1 = b2
proof end;
let B be Matrix of n,K;
func A + B -> Matrix of n,K means :Def5: :: MATRIX_1:def 5
 for i, j being Nat st [i,j] in Indices A holds
it * (i,j) = (A * (i,j)) + (B * (i,j));
existence
ex b1 being Matrix of n,K st
for i, j being Nat st [i,j] in Indices A holds
b1 * (i,j) = (A * (i,j)) + (B * (i,j))
proof end;
uniqueness
for b1, b2 being Matrix of n,K st ( for i, j being Nat st [i,j] in Indices A holds
b1 * (i,j) = (A * (i,j)) + (B * (i,j)) ) & ( for i, j being Nat st [i,j] in Indices A holds
b2 * (i,j) = (A * (i,j)) + (B * (i,j)) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines -Matrices_over MATRIX_1:def 1 :
for K being non empty doubleLoopStr
for n being Nat holds n -Matrices_over K = n -tuples_on (n -tuples_on the carrier of K);

:: deftheorem defines 0. MATRIX_1:def 2 :
for K being non empty doubleLoopStr
for n being Nat holds 0. (K,n) = n |-> (n |-> (0. K));

:: deftheorem Def3 defines 1. MATRIX_1:def 3 :
for K being non empty doubleLoopStr
for n being Nat
for b3 being Matrix of n,K holds
( b3 = 1. (K,n) iff ( ( for i being Nat st [i,i] in Indices b3 holds
b3 * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices b3 & i <> j holds
b3 * (i,j) = 0. K ) ) );

:: deftheorem Def4 defines - MATRIX_1:def 4 :
for K being non empty doubleLoopStr
for n being Nat
for A, b4 being Matrix of n,K holds
( b4 = - A iff for i, j being Nat st [i,j] in Indices A holds
b4 * (i,j) = - (A * (i,j)) );

:: deftheorem Def5 defines + MATRIX_1:def 5 :
for K being non empty doubleLoopStr
for n being Nat
for A, B, b5 being Matrix of n,K holds
( b5 = A + B iff for i, j being Nat st [i,j] in Indices A holds
b5 * (i,j) = (A * (i,j)) + (B * (i,j)) );

registration
let K be non empty doubleLoopStr ;
let n be Nat;
cluster n -Matrices_over K -> non empty ;
coherence
not n -Matrices_over K is empty ;
end;

theorem Th1: :: MATRIX_1:1
for i, j, n being Nat
for K being non empty doubleLoopStr st [i,j] in Indices (0. (K,n)) holds
(0. (K,n)) * (i,j) = 0. K
proof end;

theorem Th2: :: MATRIX_1:2
for x being object
for n being Nat
for K being non empty doubleLoopStr holds
( x is Element of n -Matrices_over K iff x is Matrix of n,K )
proof end;

definition
let K be non empty ZeroStr ;
let M be Matrix of K;
attr M is diagonal means :def6: :: MATRIX_1:def 6
 for i, j being Nat st [i,j] in Indices M & M * (i,j) <> 0. K holds
i = j;
end;

:: deftheorem def6 defines diagonal MATRIX_1:def 6 :
for K being non empty ZeroStr
for M being Matrix of K holds
( M is diagonal iff for i, j being Nat st [i,j] in Indices M & M * (i,j) <> 0. K holds
i = j );

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

theorem Th3: :: MATRIX_1:3
for n being Nat
for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for A, B being Matrix of n,F holds A + B = B + A
proof end;

theorem Th4: :: MATRIX_1:4
for n being Nat
for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for A, B, C being Matrix of n,F holds (A + B) + C = A + (B + C)
proof end;

theorem Th5: :: MATRIX_1:5
for n being Nat
for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for A being Matrix of n,F holds A + (0. (F,n)) = A
proof end;

theorem Th6: :: MATRIX_1:6
for n being Nat
for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for A being Matrix of n,F holds A + (- A) = 0. (F,n)
proof end;

definition
let F be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ;
let n be Nat;
func n -G_Matrix_over F -> strict AbGroup means :: MATRIX_1:def 7
( the carrier of it = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of it . (A,B) = A + B ) & 0. it = 0. (F,n) );
existence
ex b1 being strict AbGroup st
( the carrier of b1 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of b1 . (A,B) = A + B ) & 0. b1 = 0. (F,n) )
proof end;
uniqueness
for b1, b2 being strict AbGroup st the carrier of b1 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of b1 . (A,B) = A + B ) & 0. b1 = 0. (F,n) & the carrier of b2 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of b2 . (A,B) = A + B ) & 0. b2 = 0. (F,n) holds
b1 = b2
proof end;
end;

:: deftheorem defines -G_Matrix_over MATRIX_1:def 7 :
for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for n being Nat
for b3 being strict AbGroup holds
( b3 = n -G_Matrix_over F iff ( the carrier of b3 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of b3 . (A,B) = A + B ) & 0. b3 = 0. (F,n) ) );

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
attr M is upper_triangular means :: MATRIX_1:def 8
 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_1:def 9
 for i, j being Nat st [i,j] in Indices M & i < j holds
M * (i,j) = 0. K;
end;

:: deftheorem defines upper_triangular MATRIX_1:def 8 :
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_1:def 9 :
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 tabular V144( the carrier of K,n,n) diagonal -> diagonal upper_triangular lower_triangular for FinSequence of the carrier of K * ;
coherence
for b1 being diagonal Matrix of n,K holds
( b1 is upper_triangular & b1 is lower_triangular ) by def6;
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 V144( the carrier of K,n,n) upper_triangular lower_triangular for FinSequence of the carrier of K * ;
existence
ex b1 being Matrix of n,K st
( b1 is lower_triangular & b1 is upper_triangular )
proof end;
end;

theorem :: MATRIX_1:7
for n being Nat
for K being Field
for a, b being Element of K holds ((n,n) --> a) + ((n,n) --> b) = (n,n) --> (a + b)
proof end;

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

:: deftheorem Def3 defines permutational MATRIX_1:def 10 :
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 :Def4: :: MATRIX_1:def 11
 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 Def4 defines len MATRIX_1:def 11 :
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_1:8
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 :Def5: :: MATRIX_1:def 12
 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 Def5 defines Permutations MATRIX_1:def 12 :
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_1:9
for n being Nat holds len (Permutations n) = n
proof end;

theorem :: MATRIX_1:10
Permutations 1 = {(idseq 1)}
proof end;

definition
let n be Nat;
func Group_of_Perm n -> strict multMagma means :Def6: :: MATRIX_1:def 13
( 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 Def6 defines Group_of_Perm MATRIX_1:def 13 :
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 Th5: :: MATRIX_1:11
for n being Nat holds idseq n is Element of (Group_of_Perm n)
proof end;

theorem Th6: :: MATRIX_1:12
for n being Nat
for p being Element of Permutations n holds
( p * (idseq n) = p & (idseq n) * p = p )
proof end;

theorem Th7: :: MATRIX_1:13
for n being Nat
for p being Element of Permutations n holds
( p * (p ") = idseq n & (p ") * p = idseq n )
proof end;

theorem Th8: :: MATRIX_1:14
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 Th9: :: MATRIX_1:15
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_1:def 14
 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_1:def 14 :
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 :: MATRIX_1:def 15
 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 defines even MATRIX_1:def 15 :
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_1:16
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_1:def 16
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_1:def 16 :
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 ) );

registration
let n be Nat;
cluster Permutations n -> finite ;
coherence
Permutations n is finite
proof end;
end;