:: Abelian Group of Matrices
:: by Katarzyna Jankowska
::
:: Received June 8, 1991
:: Copyright (c) 1991-2012 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 set
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 :: 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 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 Function-like FinSequence-like tabular V151( 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;

definition
let K be non empty doubleLoopStr ;
let n be Nat;
mode Diagonal of n,K is diagonal Matrix of n,K;
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) ) );