begin
theorem
theorem
theorem Th3:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th14:
theorem
begin
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem
theorem
theorem Th22:
:: deftheorem defines MXR2MXF MATRIXR1:def 1 :
for A being Matrix of REAL holds MXR2MXF A = A;
:: deftheorem defines MXF2MXR MATRIXR1:def 2 :
for A being Matrix of F_Real holds MXF2MXR A = A;
theorem
theorem
:: deftheorem defines + MATRIXR1:def 3 :
for A, B being Matrix of REAL holds A + B = MXF2MXR ((MXR2MXF A) + (MXR2MXF B));
theorem Th25:
theorem Th26:
:: deftheorem defines - MATRIXR1:def 4 :
for A being Matrix of REAL holds - A = MXF2MXR (- (MXR2MXF A));
:: deftheorem defines - MATRIXR1:def 5 :
for A, B being Matrix of REAL holds A - B = MXF2MXR ((MXR2MXF A) - (MXR2MXF B));
:: deftheorem defines * MATRIXR1:def 6 :
for A, B being Matrix of REAL holds A * B = MXF2MXR ((MXR2MXF A) * (MXR2MXF B));
:: deftheorem Def7 defines * MATRIXR1:def 7 :
for a being real number
for A, b3 being Matrix of REAL holds
( b3 = a * A iff for ea being Element of F_Real st ea = a holds
b3 = MXF2MXR (ea * (MXR2MXF A)) );
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem
theorem
theorem
theorem
:: deftheorem defines 0_Rmatrix MATRIXR1:def 8 :
for n, m being Nat holds 0_Rmatrix (n,m) = MXF2MXR (0. (F_Real,n,m));
theorem
theorem Th36:
theorem
theorem
theorem
theorem Th40:
theorem
theorem
theorem
theorem
:: deftheorem Def9 defines ColVec2Mx MATRIXR1:def 9 :
for x being FinSequence of REAL st len x > 0 holds
for b2 being Matrix of REAL holds
( b2 = ColVec2Mx x iff ( len b2 = len x & width b2 = 1 & ( for j being Nat st j in dom x holds
b2 . j = <*(x . j)*> ) ) );
theorem
theorem Th46:
theorem Th47:
:: deftheorem Def10 defines LineVec2Mx MATRIXR1:def 10 :
for x being FinSequence of REAL
for b2 being Matrix of REAL holds
( b2 = LineVec2Mx x iff ( width b2 = len x & len b2 = 1 & ( for j being Nat st j in dom x holds
b2 * (1,j) = x . j ) ) );
theorem
theorem Th49:
theorem Th50:
theorem
:: deftheorem defines * MATRIXR1:def 11 :
for M being Matrix of REAL
for x being FinSequence of REAL holds M * x = Col ((M * (ColVec2Mx x)),1);
:: deftheorem defines * MATRIXR1:def 12 :
for M being Matrix of REAL
for x being FinSequence of REAL holds x * M = Line (((LineVec2Mx x) * M),1);
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem
theorem
theorem Th59:
theorem
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem
theorem