begin
definition
let D be non
empty set ;
let M be
Matrix of
D;
existence
ex b1 being Matrix of D st
( len b1 = width M & ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b1 * (i,j) = M * (j,i) ) )
uniqueness
for b1, b2 being Matrix of D st len b1 = width M & ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b1 * (i,j) = M * (j,i) ) & len b2 = width M & ( for i, j being Nat holds
( [i,j] in Indices b2 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b2 * (i,j) = M * (j,i) ) holds
b1 = b2
end;
Lm1:
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 )
Lm2:
for n being Element of NAT
for K being non empty set
for A being Matrix of n,K holds A @ is Matrix of n,K
definition
let K be non
empty doubleLoopStr ;
let n be
Nat;
coherence
n -tuples_on (n -tuples_on the carrier of K) is set
;
coherence
n |-> (n |-> (0. K)) is Matrix of n,K
by Th10;
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 ) )
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
let A be
Matrix of
n,
K;
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))
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
let B be
Matrix of
n,
K;
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))
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
end;
definition
let F be non
empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ;
let n be
Nat;
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) )
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
end;
begin