environ
vocabularies HIDDEN, NUMBERS, NAT_1, XBOOLE_0, ALGSTR_0, FINSEQ_1, SUBSET_1, RLVECT_1, RELAT_1, FINSEQ_2, TARSKI, STRUCT_0, TREES_1, ZFMISC_1, FUNCT_1, SUPINF_2, MESFUNC1, ARYTM_1, ARYTM_3, VECTSP_1, BINOP_1, MATRIX_1, XXREAL_0, FUNCOP_1, CARD_1, FUNCT_2, GROUP_1, ABIAN, INT_1, CARD_3, FINSET_1, FUNCSDOM;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, NAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, CARD_3, MATRIX_0, STRUCT_0, ALGSTR_0, BINOP_1, FINSEQOP, RLVECT_1, VECTSP_1, XXREAL_0, PARTFUN1, NAT_D, GROUP_1, GROUP_4, FINSET_1, FINSUB_1, FINSEQ_3, FINSEQ_4;
definitions TARSKI, RLVECT_1, ALGSTR_0, STRUCT_0;
theorems FINSEQ_1, FINSEQ_2, FUNCOP_1, ZFMISC_1, BINOP_1, RLVECT_1, ORDINAL1, CARD_1, MATRIX_0, TARSKI, GROUP_1, FUNCT_2, FINSET_1, GROUP_4, FRAENKEL, RELAT_1, XBOOLE_0, NAT_D;
schemes BINOP_1, MATRIX_0, XBOOLE_0;
registrations RELAT_1, FINSEQ_2, STRUCT_0, VECTSP_1, ORDINAL1, XXREAL_0, XBOOLE_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, GROUP_1, CARD_1;
constructors HIDDEN, BINOP_1, XXREAL_0, FINSEQOP, VECTSP_1, RLVECT_1, RELSET_1, CARD_3, FUNCT_6, CARD_2, WELLORD2, NAT_1, MATRIX_0, PRE_POLY, GROUP_1, RELAT_2, PARTFUN1, FINSUB_1, NAT_D, FINSEQ_4, GROUP_4;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities FINSEQ_2, STRUCT_0, ALGSTR_0;
expansions ;
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 MATRIX_0:10;
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;