begin
Lm1:
for F1, F2 being FinSequence of REAL
for j being Element of NAT st len F1 = len F2 holds
(F1 - F2) . j = (F1 . j) - (F2 . j)
theorem Th1:
Lm2:
for D being non empty set
for i being Element of NAT
for A being Matrix of st 1 <= i & i <= len A holds
Line A,i = A . i
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
begin
theorem Th6:
theorem Th7:
theorem
Lm3:
for i, j being Element of NAT
for A being Matrix of st [i,j] in Indices A holds
(- A) * i,j = - (A * i,j)
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem
theorem Th14:
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
begin
:: deftheorem defines Det MATRIXR2:def 1 :
theorem
for
A being
Matrix of 2, holds
Det A = ((A * 1,1) * (A * 2,2)) - ((A * 1,2) * (A * 2,1))
theorem Th33:
theorem Th34:
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,
theorem Th36:
theorem Th37:
for
D being non
empty set for
A being
Matrix of 3, 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, 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))
theorem
Lm4:
idseq 0 is Permutation of Seg 0
by FINSEQ_2:65;
theorem Th40:
theorem Th41:
theorem
theorem Th43:
theorem
theorem Th45:
theorem Th46:
begin
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem
for
n,
m,
k being
Element of
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
Element of
NAT st
[i,j] in Indices (B * A) holds
(B * A) * i,
j = ((Line B,i) * A) . j
theorem Th61:
theorem
begin
:: deftheorem defines 1_Rmatrix MATRIXR2:def 2 :
theorem Th63:
theorem Th64:
theorem Th65:
theorem
theorem Th67:
theorem Th68:
theorem
theorem Th70:
theorem Th71:
theorem Th72:
:: deftheorem defines 0_Rmatrix MATRIXR2:def 3 :
theorem
:: deftheorem defines Base_FinSeq MATRIXR2:def 4 :
theorem Th74:
theorem Th75:
theorem Th76:
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*> )
theorem Th78:
begin
:: deftheorem Def5 defines invertible MATRIXR2:def 5 :
:: deftheorem Def6 defines Inv MATRIXR2:def 6 :
theorem
theorem Th80:
theorem
theorem
theorem
theorem
theorem
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
theorem
theorem
theorem
theorem Th93:
theorem
theorem Th95:
theorem Th96:
theorem