:: by Nobuyuki Tamura and Yatsuka Nakamura

::

:: Received July 17, 2007

:: Copyright (c) 2007-2017 Association of Mizar Users

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)

proof end;

theorem Th1: :: MATRIXR2:1

for x, y being FinSequence of REAL st len x = len y & x + y = 0* (len x) holds

( x = - y & y = - x )

( x = - y & y = - x )

proof end;

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

proof end;

theorem Th2: :: MATRIXR2:2

for D being non empty set

for i, j being Nat

for A being Matrix of D

for p being FinSequence of D st p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A holds

A * (i,j) = p . j

for i, j being Nat

for A being Matrix of D

for p being FinSequence of D st p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A holds

A * (i,j) = p . j

proof end;

theorem Th3: :: MATRIXR2:3

for i, j being Nat

for a being Real

for A being Matrix of REAL st [i,j] in Indices A holds

(a * A) * (i,j) = a * (A * (i,j))

for a being Real

for A being Matrix of REAL st [i,j] in Indices A holds

(a * A) * (i,j) = a * (A * (i,j))

proof end;

theorem :: MATRIXR2:4

for n being Nat

for A, B being Matrix of n,REAL holds

( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n )

for A, B being Matrix of n,REAL holds

( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n )

proof end;

theorem Th6: :: MATRIXR2:6

for A, B being Matrix of REAL st len A = len B & width A = width B holds

( len (A - B) = len A & width (A - B) = width A & ( for i, j being Nat st [i,j] in Indices A holds

(A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) ) )

( len (A - B) = len A & width (A - B) = width A & ( for i, j being Nat st [i,j] in Indices A holds

(A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) ) )

proof end;

definition

let n be Nat;

let A, B be Matrix of n,REAL;

:: original: *

redefine func A * B -> Matrix of n,REAL;

coherence

A * B is Matrix of n,REAL ;

end;
let A, B be Matrix of n,REAL;

:: original: *

redefine func A * B -> Matrix of n,REAL;

coherence

A * B is Matrix of n,REAL ;

theorem Th7: :: MATRIXR2:7

for A, B being Matrix of REAL st len A = len B & width A = width B & len A > 0 holds

A + (B - B) = A

A + (B - B) = A

proof end;

theorem :: MATRIXR2:8

for A, B being Matrix of REAL st len A = len B & width A = width B & len A > 0 holds

(A + B) - B = A

(A + B) - B = A

proof end;

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))

proof end;

theorem Th10: :: MATRIXR2:10

for A being Matrix of REAL

for i, j being Nat st [i,j] in Indices A holds

(- A) * (i,j) = - (A * (i,j))

for i, j being Nat st [i,j] in Indices A holds

(- A) * (i,j) = - (A * (i,j))

proof end;

theorem Th14: :: MATRIXR2:14

for n being Nat

for K being Field

for A being Matrix of K st n > 0 & len A > 0 holds

(0. (K,n,(len A))) * A = 0. (K,n,(width A))

for K being Field

for A being Matrix of K st n > 0 & len A > 0 holds

(0. (K,n,(len A))) * A = 0. (K,n,(width A))

proof end;

theorem Th15: :: MATRIXR2:15

for K being Field

for A, C being Matrix of K st len A = width C & len C > 0 & len A > 0 holds

(- C) * A = - (C * A)

for A, C being Matrix of K st len A = width C & len C > 0 & len A > 0 holds

(- C) * A = - (C * A)

proof end;

theorem Th16: :: MATRIXR2:16

for K being Field

for A, B, C being Matrix of K st len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 holds

(B - C) * A = (B * A) - (C * A)

for A, B, C being Matrix of K st len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 holds

(B - C) * A = (B * A) - (C * A)

proof end;

theorem :: MATRIXR2:17

theorem Th18: :: MATRIXR2:18

for K being Field

for m being Nat

for A, C being Matrix of K st width A > 0 & len A > 0 holds

A * (0. (K,(width A),m)) = 0. (K,(len A),m)

for m being Nat

for A, C being Matrix of K st width A > 0 & len A > 0 holds

A * (0. (K,(width A),m)) = 0. (K,(len A),m)

proof end;

theorem Th19: :: MATRIXR2:19

for K being Field

for A, C being Matrix of K st width A = len C & len A > 0 & len C > 0 holds

A * (- C) = - (A * C)

for A, C being Matrix of K st width A = len C & len A > 0 & len C > 0 holds

A * (- C) = - (A * C)

proof end;

theorem Th20: :: MATRIXR2:20

for K being Field

for A, B, C being Matrix of K st len B = len C & width B = width C & len B = width A & len B > 0 & len A > 0 holds

A * (B - C) = (A * B) - (A * C)

for A, B, C being Matrix of K st len B = len C & width B = width C & len B = width A & len B > 0 & len A > 0 holds

A * (B - C) = (A * B) - (A * C)

proof end;

theorem :: MATRIXR2:21

theorem Th22: :: MATRIXR2:22

for A, B, C being Matrix of REAL st len A = len B & width A = width B & len C = len A & width C = width A & ( for i, j being Nat st [i,j] in Indices A holds

C * (i,j) = (A * (i,j)) - (B * (i,j)) ) holds

C = A - B

C * (i,j) = (A * (i,j)) - (B * (i,j)) ) holds

C = A - B

proof end;

theorem Th23: :: MATRIXR2:23

for x1, x2 being FinSequence of REAL st len x1 = len x2 holds

LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2)

LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2)

proof end;

theorem Th24: :: MATRIXR2:24

for x1, x2 being FinSequence of REAL st len x1 = len x2 & len x1 > 0 holds

ColVec2Mx (x1 - x2) = (ColVec2Mx x1) - (ColVec2Mx x2)

ColVec2Mx (x1 - x2) = (ColVec2Mx x1) - (ColVec2Mx x2)

proof end;

theorem Th25: :: MATRIXR2:25

for A, B being Matrix of REAL st len A = len B & width A = width B holds

for i being Nat st 1 <= i & i <= len A holds

Line ((A - B),i) = (Line (A,i)) - (Line (B,i))

for i being Nat st 1 <= i & i <= len A holds

Line ((A - B),i) = (Line (A,i)) - (Line (B,i))

proof end;

theorem Th26: :: MATRIXR2:26

for A, B being Matrix of REAL st len A = len B & width A = width B holds

for i being Nat st 1 <= i & i <= width A holds

Col ((A - B),i) = (Col (A,i)) - (Col (B,i))

for i being Nat st 1 <= i & i <= width A holds

Col ((A - B),i) = (Col (A,i)) - (Col (B,i))

proof end;

theorem :: MATRIXR2:27

for k, n, m, l being Nat

for A being Matrix of n,k,REAL

for B being Matrix of k,m,REAL

for C being Matrix of m,l,REAL st n > 0 & k > 0 & m > 0 holds

(A * B) * C = A * (B * C)

for A being Matrix of n,k,REAL

for B being Matrix of k,m,REAL

for C being Matrix of m,l,REAL st n > 0 & k > 0 & m > 0 holds

(A * B) * C = A * (B * C)

proof end;

theorem Th31: :: MATRIXR2:31

for n, m being Nat

for A being Matrix of REAL st len A = n & width A = m holds

(- A) + A = 0_Rmatrix (n,m)

for A being Matrix of REAL st len A = n & width A = m holds

(- A) + A = 0_Rmatrix (n,m)

proof end;

definition

let n be Nat;

let A be Matrix of n,REAL;

:: original: MXR2MXF

redefine func MXR2MXF A -> Matrix of n,F_Real;

coherence

MXR2MXF A is Matrix of n,F_Real ;

end;
let A be Matrix of n,REAL;

:: original: MXR2MXF

redefine func MXR2MXF A -> Matrix of n,F_Real;

coherence

MXR2MXF A is Matrix of n,F_Real ;

:: deftheorem defines Det MATRIXR2:def 1 :

for n being Nat

for A being Matrix of n,REAL holds Det A = Det (MXR2MXF A);

for n being Nat

for A being Matrix of n,REAL holds Det A = Det (MXR2MXF A);

theorem :: MATRIXR2:32

for A being Matrix of 2,REAL holds Det A = ((A * (1,1)) * (A * (2,2))) - ((A * (1,2)) * (A * (2,1)))

proof end;

theorem Th33: :: MATRIXR2:33

for n being Nat

for s1, s2, s3 being FinSequence st len s1 = n & len s2 = n & len s3 = n holds

<*s1,s2,s3*> is tabular

for s1, s2, s3 being FinSequence st len s1 = n & len s2 = n & len s3 = n holds

<*s1,s2,s3*> is tabular

proof end;

theorem Th34: :: MATRIXR2:34

for D being non empty set

for n being Nat

for p1, p2, p3 being FinSequence of D st len p1 = n & len p2 = n & len p3 = n holds

<*p1,p2,p3*> is Matrix of 3,n,D

for n being Nat

for p1, p2, p3 being FinSequence of D st len p1 = n & len p2 = n & len p3 = n holds

<*p1,p2,p3*> is Matrix of 3,n,D

proof end;

theorem Th35: :: MATRIXR2:35

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

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

proof end;

theorem Th36: :: MATRIXR2:36

for D being non empty set

for n being Nat

for A being Matrix of n,D

for p being FinSequence of D

for i being Nat st p = A . i & i in Seg n holds

len p = n

for n being Nat

for A being Matrix of n,D

for p being FinSequence of D

for i being Nat st p = A . i & i in Seg n holds

len p = n

proof end;

theorem Th37: :: MATRIXR2:37

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))*>*>

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))*>*>

proof end;

theorem :: MATRIXR2:38

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)))

proof end;

Lm4: idseq 0 is Permutation of (Seg 0)

by FINSEQ_2:55;

:: Removing condition n>=1 from MATRIX7:37

theorem :: MATRIXR2:44

:: Removing condition n>0 from MATRIX11:62

theorem Th45: :: MATRIXR2:45

for n being Nat

for K being Field

for A, B being Matrix of n,K holds Det (A * B) = (Det A) * (Det B)

for K being Field

for A, B being Matrix of n,K holds Det (A * B) = (Det A) * (Det B)

proof end;

theorem :: MATRIXR2:47

for x, y being FinSequence of REAL

for A being Matrix of REAL st len x = len A & len y = len x & len x > 0 holds

(x - y) * A = (x * A) - (y * A)

for A being Matrix of REAL st len x = len A & len y = len x & len x > 0 holds

(x - y) * A = (x * A) - (y * A)

proof end;

theorem :: MATRIXR2:48

for x, y being FinSequence of REAL

for A being Matrix of REAL st len x = width A & len y = len x & len x > 0 & len A > 0 holds

A * (x - y) = (A * x) - (A * y)

for A being Matrix of REAL st len x = width A & len y = len x & len x > 0 & len A > 0 holds

A * (x - y) = (A * x) - (A * y)

proof end;

theorem :: MATRIXR2:49

for x being FinSequence of REAL

for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds

(- x) * A = - (x * A)

for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds

(- x) * A = - (x * A)

proof end;

theorem :: MATRIXR2:50

for x being FinSequence of REAL

for A being Matrix of REAL st len x = width A & len x > 0 holds

A * (- x) = - (A * x)

for A being Matrix of REAL st len x = width A & len x > 0 holds

A * (- x) = - (A * x)

proof end;

theorem :: MATRIXR2:51

for x being FinSequence of REAL

for A being Matrix of REAL st len x = len A & len x > 0 holds

x * (- A) = - (x * A)

for A being Matrix of REAL st len x = len A & len x > 0 holds

x * (- A) = - (x * A)

proof end;

theorem :: MATRIXR2:52

for x being FinSequence of REAL

for A being Matrix of REAL st len x = width A & len A > 0 & len x > 0 holds

(- A) * x = - (A * x)

for A being Matrix of REAL st len x = width A & len A > 0 & len x > 0 holds

(- A) * x = - (A * x)

proof end;

theorem :: MATRIXR2:53

for a being Real

for x being FinSequence of REAL

for A being Matrix of REAL st width A = len x & len x > 0 holds

A * (a * x) = a * (A * x)

for x being FinSequence of REAL

for A being Matrix of REAL st width A = len x & len x > 0 holds

A * (a * x) = a * (A * x)

proof end;

theorem :: MATRIXR2:54

for x being FinSequence of REAL

for A, B being Matrix of REAL st len x = len A & len A = len B & width A = width B & len A > 0 holds

x * (A - B) = (x * A) - (x * B)

for A, B being Matrix of REAL st len x = len A & len A = len B & width A = width B & len A > 0 holds

x * (A - B) = (x * A) - (x * B)

proof end;

theorem :: MATRIXR2:55

for x being FinSequence of REAL

for A, B being Matrix of REAL st len x = width A & len A = len B & width A = width B & len x > 0 & len A > 0 holds

(A - B) * x = (A * x) - (B * x)

for A, B being Matrix of REAL st len x = width A & len A = len B & width A = width B & len x > 0 & len A > 0 holds

(A - B) * x = (A * x) - (B * x)

proof end;

theorem Th56: :: MATRIXR2:56

for x being FinSequence of REAL

for A being Matrix of REAL st len A = len x holds

(LineVec2Mx x) * A = LineVec2Mx (x * A)

for A being Matrix of REAL st len A = len x holds

(LineVec2Mx x) * A = LineVec2Mx (x * A)

proof end;

theorem Th57: :: MATRIXR2:57

for x being FinSequence of REAL

for A, B being Matrix of REAL st len x = len A & width A = len B holds

x * (A * B) = (x * A) * B

for A, B being Matrix of REAL st len x = len A & width A = len B holds

x * (A * B) = (x * A) * B

proof end;

theorem Th58: :: MATRIXR2:58

for x being FinSequence of REAL

for A being Matrix of REAL st width A = len x & len x > 0 & len A > 0 holds

A * (ColVec2Mx x) = ColVec2Mx (A * x)

for A being Matrix of REAL st width A = len x & len x > 0 & len A > 0 holds

A * (ColVec2Mx x) = ColVec2Mx (A * x)

proof end;

theorem Th59: :: MATRIXR2:59

for x being FinSequence of REAL

for A, B being Matrix of REAL st len x = width B & width A = len B & len x > 0 & len B > 0 holds

(A * B) * x = A * (B * x)

for A, B being Matrix of REAL st len x = width B & width A = len B & len x > 0 & len B > 0 holds

(A * B) * x = A * (B * x)

proof end;

theorem :: MATRIXR2:60

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

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

proof end;

theorem Th61: :: MATRIXR2:61

for n being Nat

for A, B being Matrix of n,REAL

for i, j being Nat st [i,j] in Indices (B * A) holds

(B * A) * (i,j) = ((Line (B,i)) * A) . j

for A, B being Matrix of n,REAL

for i, j being Nat st [i,j] in Indices (B * A) holds

(B * A) * (i,j) = ((Line (B,i)) * A) . j

proof end;

theorem :: MATRIXR2:62

for n being Nat

for A, B being Matrix of n,REAL st n > 0 holds

for i, j being Nat st [i,j] in Indices (A * B) holds

(A * B) * (i,j) = (A * (Col (B,j))) . i

for A, B being Matrix of n,REAL st n > 0 holds

for i, j being Nat st [i,j] in Indices (A * B) holds

(A * B) * (i,j) = (A * (Col (B,j))) . i

proof end;

:: deftheorem defines 1_Rmatrix MATRIXR2:def 2 :

for n being Nat holds 1_Rmatrix n = MXF2MXR (1. (F_Real,n));

for n being Nat holds 1_Rmatrix n = MXF2MXR (1. (F_Real,n));

theorem Th63: :: MATRIXR2:63

for n being Nat holds

( ( for i being Nat st [i,i] in Indices (1_Rmatrix n) holds

(1_Rmatrix n) * (i,i) = 1 ) & ( for i, j being Nat st [i,j] in Indices (1_Rmatrix n) & i <> j holds

(1_Rmatrix n) * (i,j) = 0 ) )

( ( for i being Nat st [i,i] in Indices (1_Rmatrix n) holds

(1_Rmatrix n) * (i,i) = 1 ) & ( for i, j being Nat st [i,j] in Indices (1_Rmatrix n) & i <> j holds

(1_Rmatrix n) * (i,j) = 0 ) )

proof end;

theorem :: MATRIXR2:69

:: deftheorem defines 0_Rmatrix MATRIXR2:def 3 :

for n being Nat holds 0_Rmatrix n = 0_Rmatrix (n,n);

for n being Nat holds 0_Rmatrix n = 0_Rmatrix (n,n);

:: deftheorem defines Base_FinSeq MATRIXR2:def 4 :

for n, i being Nat holds Base_FinSeq (n,i) = (n |-> 0) +* (i,1);

for n, i being Nat holds Base_FinSeq (n,i) = (n |-> 0) +* (i,1);

theorem :: MATRIXR2:77

( 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*> )

proof end;

:: deftheorem defines invertible MATRIXR2:def 5 :

for n being 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 ) );

for n being 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 ) );

definition

let n be Nat;

let A be Matrix of n,REAL;

assume A1: A is invertible ;

ex b_{1} being Matrix of n,REAL st

( b_{1} * A = 1_Rmatrix n & A * b_{1} = 1_Rmatrix n )
by A1;

uniqueness

for b_{1}, b_{2} being Matrix of n,REAL st b_{1} * A = 1_Rmatrix n & A * b_{1} = 1_Rmatrix n & b_{2} * A = 1_Rmatrix n & A * b_{2} = 1_Rmatrix n holds

b_{1} = b_{2}

end;
let A be Matrix of n,REAL;

assume A1: A is invertible ;

func Inv A -> Matrix of n,REAL means :Def6: :: MATRIXR2:def 6

( it * A = 1_Rmatrix n & A * it = 1_Rmatrix n );

existence ( it * A = 1_Rmatrix n & A * it = 1_Rmatrix n );

ex b

( b

uniqueness

for b

b

proof end;

:: deftheorem Def6 defines Inv MATRIXR2:def 6 :

for n being Nat

for A being Matrix of n,REAL st A is invertible holds

for b_{3} being Matrix of n,REAL holds

( b_{3} = Inv A iff ( b_{3} * A = 1_Rmatrix n & A * b_{3} = 1_Rmatrix n ) );

for n being Nat

for A being Matrix of n,REAL st A is invertible holds

for b

( b

registration
end;

theorem Th80: :: MATRIXR2:80

for n being Nat

for A, B1, B2 being Matrix of n,REAL st B1 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n holds

( B1 = B2 & A is invertible )

for A, B1, B2 being Matrix of n,REAL st B1 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n holds

( B1 = B2 & A is invertible )

proof end;

theorem :: MATRIXR2:83

for n being Nat

for A, B being Matrix of n,REAL st A is invertible & B is invertible holds

( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) )

for A, B being Matrix of n,REAL st A is invertible & B is invertible holds

( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) )

proof end;

theorem Th87: :: MATRIXR2:87

for n being Nat

for x, y being FinSequence of REAL

for A being Matrix of n,REAL st A is invertible & len x = n & len y = n & n > 0 holds

( A * x = y iff x = (Inv A) * y )

for x, y being FinSequence of REAL

for A being Matrix of n,REAL st A is invertible & len x = n & len y = n & n > 0 holds

( A * x = y iff x = (Inv A) * y )

proof end;

theorem Th89: :: MATRIXR2:89

for n being Nat

for x, y being FinSequence of REAL

for A being Matrix of n,REAL st A is invertible & len x = n & len y = n holds

( x * A = y iff x = y * (Inv A) )

for x, y being FinSequence of REAL

for A being Matrix of n,REAL st A is invertible & len x = n & len y = n holds

( x * A = y iff x = y * (Inv A) )

proof end;

theorem :: MATRIXR2:90

for n being Nat

for A being Matrix of n,REAL st n > 0 & A is invertible holds

for y being FinSequence of REAL st len y = n holds

ex x being FinSequence of REAL st

( len x = n & A * x = y )

for A being Matrix of n,REAL st n > 0 & A is invertible holds

for y being FinSequence of REAL st len y = n holds

ex x being FinSequence of REAL st

( len x = n & A * x = y )

proof end;

theorem :: MATRIXR2:91

for n being Nat

for A being Matrix of n,REAL st A is invertible holds

for y being FinSequence of REAL st len y = n holds

ex x being FinSequence of REAL st

( len x = n & x * A = y )

for A being Matrix of n,REAL st A is invertible holds

for y being FinSequence of REAL st len y = n holds

ex x being FinSequence of REAL st

( len x = n & x * A = y )

proof end;

theorem :: MATRIXR2:92

for n being Nat

for A being Matrix of n,REAL

for x, y being FinSequence of REAL st len x = n & len y = n & x * A = y holds

for j being Nat st 1 <= j & j <= n holds

y . j = |(x,(Col (A,j)))|

for A being Matrix of n,REAL

for x, y being FinSequence of REAL st len x = n & len y = n & x * A = y holds

for j being Nat st 1 <= j & j <= n holds

y . j = |(x,(Col (A,j)))|

proof end;

theorem Th93: :: MATRIXR2:93

for n being Nat

for A being Matrix of n,REAL st ( for y being FinSequence of REAL st len y = n holds

ex x being FinSequence of REAL st

( len x = n & x * A = y ) ) holds

ex B being Matrix of n,REAL st B * A = 1_Rmatrix n

for A being Matrix of n,REAL st ( for y being FinSequence of REAL st len y = n holds

ex x being FinSequence of REAL st

( len x = n & x * A = y ) ) holds

ex B being Matrix of n,REAL st B * A = 1_Rmatrix n

proof end;

theorem :: MATRIXR2:94

for n being Nat

for x being FinSequence of REAL

for A being Matrix of n,REAL st n > 0 & len x = n holds

(A @) * x = x * A

for x being FinSequence of REAL

for A being Matrix of n,REAL st n > 0 & len x = n holds

(A @) * x = x * A

proof end;

theorem Th95: :: MATRIXR2:95

for n being Nat

for x being FinSequence of REAL

for A being Matrix of n,REAL st n > 0 & len x = n holds

x * (A @) = A * x

for x being FinSequence of REAL

for A being Matrix of n,REAL st n > 0 & len x = n holds

x * (A @) = A * x

proof end;

theorem Th96: :: MATRIXR2:96

for n being Nat

for A being Matrix of n,REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds

ex x being FinSequence of REAL st

( len x = n & A * x = y ) ) holds

ex B being Matrix of n,REAL st A * B = 1_Rmatrix n

for A being Matrix of n,REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds

ex x being FinSequence of REAL st

( len x = n & A * x = y ) ) holds

ex B being Matrix of n,REAL st A * B = 1_Rmatrix n

proof end;

theorem :: MATRIXR2:97

for n being Nat

for A being Matrix of n,REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds

ex x1, x2 being FinSequence of REAL st

( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) ) holds

A is invertible

for A being Matrix of n,REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds

ex x1, x2 being FinSequence of REAL st

( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) ) holds

A is invertible

proof end;