environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, NAT_1, MATRIX_1, RELAT_1, XXREAL_0, CARD_1, ARYTM_3, LATTICE3, FUNCT_4, FINSEQ_1, TREES_1, COMPLEX1, ARYTM_1, FUNCOP_1, QC_LANG1, VECTSP_1, REAL_1, MATRIXR1, ZFMISC_1, MATRIX10, FUNCT_7;
notations HIDDEN, COMPLEX1, TARSKI, ZFMISC_1, SUBSET_1, FINSEQ_1, MATRIX_0, ORDINAL1, FUNCT_7, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, MATRIXR1, RLVECT_1, VECTSP_1, STRUCT_0, MATRIX_3, GROUP_1, MATRIX_1;
definitions ;
theorems MATRIX_0, MATRIX_3, MATRIXR1, XREAL_1, ABSVALUE, VECTSP_1, MATRIX_4, FINSEQ_1, FINSEQ_3, COMPLEX1, MATRIXC1, XXREAL_0, XREAL_0;
schemes MATRIX_0;
registrations RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, VECTSP_1, ORDINAL1;
constructors HIDDEN, XXREAL_0, REAL_1, BINOP_2, MEMBERED, COMPLEX1, MATRIX_3, MATRIX_4, MATRIXR1, RELSET_1, FUNCT_7, NUMBERS;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
equalities MATRIX_0, MATRIXR1;
expansions ;
definition
let M be
Matrix of
REAL;
existence
ex b1 being Matrix of REAL 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 REAL 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
end;
Lm1:
1 in REAL
by XREAL_0:def 1;
Lm2:
- 1 in REAL
by XREAL_0:def 1;
registration
let n be
Nat;
coherence
for b1 being Matrix of n,REAL st b1 = (n,n) --> 1 holds
b1 is Positive
by MATRIX_0:46, Lm1;
coherence
for b1 being Matrix of n,REAL st b1 = (n,n) --> (- 1) holds
b1 is Negative
coherence
for b1 being Matrix of n,REAL st b1 = (n,n) --> (- 1) holds
b1 is Nonpositive
by MATRIX_0:46, Lm2;
coherence
for b1 being Matrix of n,REAL st b1 = (n,n) --> 1 holds
b1 is Nonnegative
by MATRIX_0:46, Lm1;
end;
Lm3:
for n being Nat
for M1, M2 being Matrix of n,REAL holds
( len M1 = len M2 & width M1 = width M2 )