environ
vocabularies HIDDEN, NUMBERS, NAT_1, SUBSET_1, FINSEQ_2, MATRIX_1, ARYTM_3, FINSEQ_1, TREES_1, RELAT_1, CARD_1, XXREAL_0, ZFMISC_1, XCMPLX_0, COMPLFLD, MATRIX_5, ARYTM_1, COMPLEX1, QC_LANG1, FUNCT_1, RVSUM_1, BINOP_2, TARSKI, XBOOLE_0, CARD_3, INCSP_1, FUNCOP_1, SETWISEO, ORDINAL4, PARTFUN1, MATRIXC1, FUNCT_7;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, FUNCT_1, RELSET_1, FUNCT_2, ZFMISC_1, NAT_D, PARTFUN1, BINOP_1, FUNCOP_1, NAT_1, FINSEQ_1, FINSEQOP, SEQ_4, COMPLEX1, RVSUM_1, FINSEQ_2, BINOP_2, MATRIX_5, MATRIX_0, MATRIX_3, MATRIX_4, RLVECT_1, COMPLSP2, SETWOP_2, COMPLFLD, STRUCT_0, GROUP_1;
definitions ;
theorems FINSEQ_1, FUNCT_1, NAT_1, MATRIX_0, FINSEQ_2, COMPLEX1, BINOP_2, FINSEQ_3, XCMPLX_0, ZFMISC_1, SEQ_4, FINSEQOP, COMPLSP2, FUNCOP_1, FUNCT_2, FINSOP_1, SETWOP_2, FINSEQ_5, XREAL_1, MATRIX_3, COMPLFLD, MATRIX_4, MATRIX_5, NUMBERS, XBOOLE_1, ORDINAL1, PARTFUN1, XXREAL_0, XREAL_0, CARD_1;
schemes MATRIX_0, FINSEQ_2, FINSEQ_1, FUNCT_2, NAT_1;
registrations XBOOLE_0, FUNCT_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, BINOP_2, FINSEQ_2, COMPLFLD, MATRIX_0, VALUED_0, RELSET_1, XREAL_0, ORDINAL1, MEMBERED;
constructors HIDDEN, SETWISEO, FINSOP_1, MATRIX_3, MATRIX_4, MATRIX_5, SEQ_4, BINOP_2, BINOP_1, RVSUM_1, NAT_D, RELSET_1, COMPLSP2, PRE_POLY, REAL_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities MATRIX_0, RVSUM_1, VALUED_1;
expansions ;
definition
let M be
Matrix of
COMPLEX;
existence
ex b1 being Matrix of COMPLEX st
( len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = (M * (i,j)) *' ) )
uniqueness
for b1, b2 being Matrix of COMPLEX st len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = (M * (i,j)) *' ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b2 * (i,j) = (M * (i,j)) *' ) holds
b1 = b2
involutiveness
for b1, b2 being Matrix of COMPLEX st len b1 = len b2 & width b1 = width b2 & ( for i, j being Nat st [i,j] in Indices b2 holds
b1 * (i,j) = (b2 * (i,j)) *' ) holds
( len b2 = len b1 & width b2 = width b1 & ( for i, j being Nat st [i,j] in Indices b1 holds
b2 * (i,j) = (b1 * (i,j)) *' ) )
end;
Lm1:
for a being Element of COMPLEX
for F being FinSequence of COMPLEX holds a * F = (multcomplex [;] (a,(id COMPLEX))) * F
Lm2:
for a, b being Element of COMPLEX holds (multcomplex [;] (a,(id COMPLEX))) . b = a * b
definition
let x,
y be
FinSequence of
COMPLEX ;
let M be
Matrix of
COMPLEX;
assume that A1:
len x = len M
and A2:
len y = width M
;
existence
ex b1 being Matrix of COMPLEX st
( len b1 = len x & width b1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) )
uniqueness
for b1, b2 being Matrix of COMPLEX st len b1 = len x & width b1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) & len b2 = len x & width b2 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b2 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) holds
b1 = b2
end;