environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, VECTSP_1, FINSEQ_1, ARYTM_1, FUNCT_1, FINSEQ_2, ARYTM_3, EUCLID, MATRIX_1, XXREAL_0, INCSP_1, RELAT_1, TREES_1, TARSKI, MATRIXR1, CARD_1, NAT_1, REAL_1, SUPINF_2, QC_LANG1, ZFMISC_1, FVSUM_1, MATRIX_3, FUNCT_2, MESFUNC1, GROUP_1, ABIAN, BINOP_1, ALGSTR_0, SETWISEO, CARD_3, RVSUM_1, FUNCT_4, AFINSQ_1, PRALG_1, PARTFUN1, MATRIXR2, MATRIX_0, FUNCT_7, FUNCSDOM, FINSUB_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, XXREAL_0, ZFMISC_1, ORDINAL1, NUMBERS, ENUMSET1, SETWOP_2, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, PARTFUN1, BINOP_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCT_7, STRUCT_0, ALGSTR_0, MATRIX_0, MATRIX_1, FVSUM_1, FINSEQ_7, SETWISEO, GROUP_1, FINSUB_1, MATRIX_3, MATRIX_6, MATRIXR1, EUCLID, MATRIX_7, MATRIX_4, RVSUM_1, VECTSP_1, MATRPROB;
definitions TARSKI, MATRIX_0;
theorems MATRIX_3, VECTSP_1, MATRIX_0, MATRIX_4, GROUP_1, XREAL_0, FUNCT_1, FINSEQ_1, NAT_1, FINSEQ_7, FINSEQ_2, TARSKI, FINSOP_1, FVSUM_1, SETWISEO, XBOOLE_0, ENUMSET1, XCMPLX_0, ZFMISC_1, MATRIX_7, MATRIXR1, FINSEQ_3, XXREAL_0, RVSUM_1, MATRIX10, MATRIX11, MATRPROB, FINSEQ_4, MATRIX_9, MATRIXC1, PARTFUN1, FUNCT_7, CARD_1, MATRIX_1, FINSUB_1, SUBSET_1;
schemes FINSEQ_4;
registrations FINSEQ_2, NAT_1, RELSET_1, MEMBERED, STRUCT_0, VECTSP_1, NUMBERS, XXREAL_0, MATRIX_1, FINSEQ_1, FVSUM_1, FINSET_1, XBOOLE_0, VALUED_0, CARD_1, MATRIX_0, MATRIX_6, XREAL_0, VECTSP_2, ORDINAL1;
constructors HIDDEN, FVSUM_1, BINOP_2, FINSEQ_7, SETWISEO, FINSOP_1, FINSEQ_4, MATRIX_7, MATRIXR1, MATRIX_6, REAL_1, RVSUM_1, EUCLID, RELSET_1, MATRIX_4, BINOP_1, VECTSP_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities MATRIX_0, STRUCT_0, RLVECT_1, VECTSP_1, MATRIXR1, FINSEQ_1, VALUED_1;
expansions TARSKI, MATRIX_0, FINSEQ_1;
Lm1:
for F1, F2 being FinSequence of REAL
for j being Nat st len F1 = len F2 holds
(F1 - F2) . j = (F1 . j) - (F2 . j)
Lm2:
for D being non empty set
for i being Nat
for A being Matrix of D st 1 <= i & i <= len A holds
Line (A,i) = A . i
Lm3:
for i, j being Nat
for A being Matrix of REAL st [i,j] in Indices A holds
(- A) * (i,j) = - (A * (i,j))
theorem Th35:
for
D being non
empty set for
a1,
a2,
a3,
b1,
b2,
b3,
c1,
c2,
c3 being
Element of
D holds
<*<*a1,a2,a3*>,<*b1,b2,b3*>,<*c1,c2,c3*>*> is
Matrix of 3,
D
theorem Th37:
for
D being non
empty set for
A being
Matrix of 3,
D holds
A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>,<*(A * (2,1)),(A * (2,2)),(A * (2,3))*>,<*(A * (3,1)),(A * (3,2)),(A * (3,3))*>*>
theorem
for
A being
Matrix of 3,
REAL holds
Det A = (((((((A * (1,1)) * (A * (2,2))) * (A * (3,3))) - (((A * (1,3)) * (A * (2,2))) * (A * (3,1)))) - (((A * (1,1)) * (A * (2,3))) * (A * (3,2)))) + (((A * (1,2)) * (A * (2,3))) * (A * (3,1)))) - (((A * (1,2)) * (A * (2,1))) * (A * (3,3)))) + (((A * (1,3)) * (A * (2,1))) * (A * (3,2)))
Lm4:
idseq 0 is Permutation of (Seg 0)
by FINSEQ_2:55;
theorem
for
k,
n,
m being
Nat for
B being
Matrix of
n,
m,
REAL for
A being
Matrix of
m,
k,
REAL st
n > 0 holds
for
i,
j being
Nat st
[i,j] in Indices (B * A) holds
(B * A) * (
i,
j)
= ((Line (B,i)) * A) . j
theorem
(
Base_FinSeq (1,1)
= <*1*> &
Base_FinSeq (2,1)
= <*1,0*> &
Base_FinSeq (2,2)
= <*0,1*> &
Base_FinSeq (3,1)
= <*1,0,0*> &
Base_FinSeq (3,2)
= <*0,1,0*> &
Base_FinSeq (3,3)
= <*0,0,1*> )