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 D 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 REAL 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 :
for n being Element of NAT
for A being Matrix of n, REAL holds Det A = Det (MXR2MXF A);
theorem
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,
D
theorem Th36:
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)))
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 :
for n being Element of NAT holds 1_Rmatrix n = MXF2MXR (1. (F_Real,n));
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 :
for n being Element of NAT holds 0_Rmatrix n = 0_Rmatrix (n,n);
theorem
:: deftheorem defines Base_FinSeq MATRIXR2:def 4 :
for n, i being Nat holds Base_FinSeq (n,i) = (n |-> 0) +* (i,1);
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 :
for n being Element of NAT
for A being Matrix of n, REAL holds
( A is invertible iff ex B being Matrix of n, REAL st
( B * A = 1_Rmatrix n & A * B = 1_Rmatrix n ) );
:: deftheorem Def6 defines Inv MATRIXR2:def 6 :
for n being Element of NAT
for A being Matrix of n, REAL st A is invertible holds
for b3 being Matrix of n, REAL holds
( b3 = Inv A iff ( b3 * A = 1_Rmatrix n & A * b3 = 1_Rmatrix n ) );
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