:: by Yatsuka Nakamura , Nobuyuki Tamura and Wenpai Chang

::

:: Received February 20, 2006

:: Copyright (c) 2006-2012 Association of Mizar Users

begin

theorem :: MATRIXR1:1

theorem :: MATRIXR1:2

theorem :: MATRIXR1:4

theorem :: MATRIXR1:7

theorem :: MATRIXR1:8

theorem :: MATRIXR1:9

theorem :: MATRIXR1:11

theorem :: MATRIXR1:12

theorem :: MATRIXR1:13

begin

theorem Th16: :: MATRIXR1:16

for K being non empty multMagma

for p being FinSequence of K

for a being Element of K holds len (a * p) = len p

for p being FinSequence of K

for a being Element of K holds len (a * p) = len p

proof end;

theorem Th17: :: MATRIXR1:17

for r being Real

for fr being Element of F_Real

for p being FinSequence of REAL

for fp being FinSequence of F_Real st r = fr & p = fp holds

r * p = fr * fp

for fr being Element of F_Real

for p being FinSequence of REAL

for fp being FinSequence of F_Real st r = fr & p = fp holds

r * p = fr * fp

proof end;

theorem :: MATRIXR1:18

for K being Field

for a being Element of K

for A being Matrix of K holds Indices (a * A) = Indices A

for a being Element of K

for A being Matrix of K holds Indices (a * A) = Indices A

proof end;

theorem Th19: :: MATRIXR1:19

for i being Nat

for K being Field

for a being Element of K

for M being Matrix of K st 1 <= i & i <= width M holds

Col ((a * M),i) = a * (Col (M,i))

for K being Field

for a being Element of K

for M being Matrix of K st 1 <= i & i <= width M holds

Col ((a * M),i) = a * (Col (M,i))

proof end;

theorem :: MATRIXR1:20

for K being Field

for a being Element of K

for M being Matrix of K

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

Line ((a * M),i) = a * (Line (M,i))

for a being Element of K

for M being Matrix of K

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

Line ((a * M),i) = a * (Line (M,i))

proof end;

theorem :: MATRIXR1:21

for K being Field

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

ex C being Matrix of K st

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

C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) )

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

ex C being Matrix of K st

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

C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) )

proof end;

theorem Th22: :: MATRIXR1:22

for K being Field

for a being Element of K

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

A * (a * B) = a * (A * B)

for a being Element of K

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

A * (a * B) = a * (A * B)

proof end;

theorem :: MATRIXR1:23

for D1, D2 being set

for A being Matrix of D1

for B being Matrix of D2 st A = B holds

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

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

for A being Matrix of D1

for B being Matrix of D2 st A = B holds

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

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

proof end;

definition
end;

:: deftheorem defines + MATRIXR1:def 3 :

for A, B being Matrix of REAL holds A + B = MXF2MXR ((MXR2MXF A) + (MXR2MXF B));

for A, B being Matrix of REAL holds A + B = MXF2MXR ((MXR2MXF A) + (MXR2MXF B));

theorem Th25: :: MATRIXR1:25

for A, B being Matrix of REAL 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;

theorem Th26: :: MATRIXR1:26

for A, B, C being Matrix of REAL st 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;

:: deftheorem defines - MATRIXR1:def 4 :

for A being Matrix of REAL holds - A = MXF2MXR (- (MXR2MXF A));

for A being Matrix of REAL holds - A = MXF2MXR (- (MXR2MXF A));

definition

let A, B be Matrix of REAL;

coherence

MXF2MXR ((MXR2MXF A) - (MXR2MXF B)) is Matrix of REAL ;

coherence

MXF2MXR ((MXR2MXF A) * (MXR2MXF B)) is Matrix of REAL ;

end;
coherence

MXF2MXR ((MXR2MXF A) - (MXR2MXF B)) is Matrix of REAL ;

coherence

MXF2MXR ((MXR2MXF A) * (MXR2MXF B)) is Matrix of REAL ;

:: deftheorem defines - MATRIXR1:def 5 :

for A, B being Matrix of REAL holds A - B = MXF2MXR ((MXR2MXF A) - (MXR2MXF B));

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

for A, B being Matrix of REAL holds A * B = MXF2MXR ((MXR2MXF A) * (MXR2MXF B));

definition

let a be real number ;

let A be Matrix of REAL;

ex b_{1} being Matrix of REAL st

for ea being Element of F_Real st ea = a holds

b_{1} = MXF2MXR (ea * (MXR2MXF A))

for b_{1}, b_{2} being Matrix of REAL st ( for ea being Element of F_Real st ea = a holds

b_{1} = MXF2MXR (ea * (MXR2MXF A)) ) & ( for ea being Element of F_Real st ea = a holds

b_{2} = MXF2MXR (ea * (MXR2MXF A)) ) holds

b_{1} = b_{2}

end;
let A be Matrix of REAL;

func a * A -> Matrix of REAL means :Def7: :: MATRIXR1:def 7

for ea being Element of F_Real st ea = a holds

it = MXF2MXR (ea * (MXR2MXF A));

existence for ea being Element of F_Real st ea = a holds

it = MXF2MXR (ea * (MXR2MXF A));

ex b

for ea being Element of F_Real st ea = a holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def7 defines * MATRIXR1:def 7 :

for a being real number

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

( b_{3} = a * A iff for ea being Element of F_Real st ea = a holds

b_{3} = MXF2MXR (ea * (MXR2MXF A)) );

for a being real number

for A, b

( b

b

theorem Th29: :: MATRIXR1:29

for a being Real

for A being Matrix of REAL

for i2, j2 being Nat st [i2,j2] in Indices A holds

(a * A) * (i2,j2) = a * (A * (i2,j2))

for A being Matrix of REAL

for i2, j2 being Nat st [i2,j2] in Indices A holds

(a * A) * (i2,j2) = a * (A * (i2,j2))

proof end;

theorem :: MATRIXR1:31

for a being Real

for i being Nat

for A being Matrix of REAL st len A > 0 & i in dom A holds

( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds

(a * A) . i = a * q ) )

for i being Nat

for A being Matrix of REAL st len A > 0 & i in dom A holds

( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds

(a * A) . i = a * q ) )

proof end;

:: deftheorem defines 0_Rmatrix MATRIXR1:def 8 :

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

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

theorem Th36: :: MATRIXR1:36

for n, m being Nat

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

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

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

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

proof end;

theorem :: MATRIXR1:37

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

B = 0_Rmatrix ((len A),(width A))

B = 0_Rmatrix ((len A),(width A))

proof end;

theorem :: MATRIXR1:38

for A, B being Matrix of REAL st len A = len B & width A = width B & A + B = 0_Rmatrix ((len A),(width A)) holds

B = - A

B = - A

proof end;

theorem :: MATRIXR1:39

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

A = 0_Rmatrix ((len A),(width A))

A = 0_Rmatrix ((len A),(width A))

proof end;

theorem :: MATRIXR1:41

for a being Real

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

(a * A) * B = a * (A * B)

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

(a * A) * B = a * (A * B)

proof end;

theorem :: MATRIXR1:43

for a being real number

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

a * (A + B) = (a * A) + (a * B)

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

a * (A + B) = (a * A) + (a * B)

proof end;

definition

let x be FinSequence of REAL ;

assume A1: len x > 0 ;

ex b_{1} being Matrix of REAL st

( len b_{1} = len x & width b_{1} = 1 & ( for j being Nat st j in dom x holds

b_{1} . j = <*(x . j)*> ) )

for b_{1}, b_{2} being Matrix of REAL st len b_{1} = len x & width b_{1} = 1 & ( for j being Nat st j in dom x holds

b_{1} . j = <*(x . j)*> ) & len b_{2} = len x & width b_{2} = 1 & ( for j being Nat st j in dom x holds

b_{2} . j = <*(x . j)*> ) holds

b_{1} = b_{2}

end;
assume A1: len x > 0 ;

func ColVec2Mx x -> Matrix of REAL means :Def9: :: MATRIXR1:def 9

( len it = len x & width it = 1 & ( for j being Nat st j in dom x holds

it . j = <*(x . j)*> ) );

existence ( len it = len x & width it = 1 & ( for j being Nat st j in dom x holds

it . j = <*(x . j)*> ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def9 defines ColVec2Mx MATRIXR1:def 9 :

for x being FinSequence of REAL st len x > 0 holds

for b_{2} being Matrix of REAL holds

( b_{2} = ColVec2Mx x iff ( len b_{2} = len x & width b_{2} = 1 & ( for j being Nat st j in dom x holds

b_{2} . j = <*(x . j)*> ) ) );

for x being FinSequence of REAL st len x > 0 holds

for b

( b

b

theorem :: MATRIXR1:45

for x being FinSequence of REAL

for M being Matrix of REAL st len x > 0 holds

( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) )

for M being Matrix of REAL st len x > 0 holds

( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) )

proof end;

theorem Th46: :: MATRIXR1:46

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 Th47: :: MATRIXR1:47

for a being Real

for x being FinSequence of REAL st len x > 0 holds

ColVec2Mx (a * x) = a * (ColVec2Mx x)

for x being FinSequence of REAL st len x > 0 holds

ColVec2Mx (a * x) = a * (ColVec2Mx x)

proof end;

definition

let x be FinSequence of REAL ;

ex b_{1} being Matrix of REAL st

( width b_{1} = len x & len b_{1} = 1 & ( for j being Nat st j in dom x holds

b_{1} * (1,j) = x . j ) )

for b_{1}, b_{2} being Matrix of REAL st width b_{1} = len x & len b_{1} = 1 & ( for j being Nat st j in dom x holds

b_{1} * (1,j) = x . j ) & width b_{2} = len x & len b_{2} = 1 & ( for j being Nat st j in dom x holds

b_{2} * (1,j) = x . j ) holds

b_{1} = b_{2}

end;
func LineVec2Mx x -> Matrix of REAL means :Def10: :: MATRIXR1:def 10

( width it = len x & len it = 1 & ( for j being Nat st j in dom x holds

it * (1,j) = x . j ) );

existence ( width it = len x & len it = 1 & ( for j being Nat st j in dom x holds

it * (1,j) = x . j ) );

ex b

( width b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def10 defines LineVec2Mx MATRIXR1:def 10 :

for x being FinSequence of REAL

for b_{2} being Matrix of REAL holds

( b_{2} = LineVec2Mx x iff ( width b_{2} = len x & len b_{2} = 1 & ( for j being Nat st j in dom x holds

b_{2} * (1,j) = x . j ) ) );

for x being FinSequence of REAL

for b

( b

b

theorem :: MATRIXR1:48

for x being FinSequence of REAL

for M being Matrix of REAL holds

( M = LineVec2Mx x iff ( Line (M,1) = x & len M = 1 ) )

for M being Matrix of REAL holds

( M = LineVec2Mx x iff ( Line (M,1) = x & len M = 1 ) )

proof end;

theorem Th49: :: MATRIXR1:49

for x being FinSequence of REAL st len x > 0 holds

( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x )

( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x )

proof end;

theorem Th50: :: MATRIXR1:50

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;

definition

let M be Matrix of REAL;

let x be FinSequence of REAL ;

coherence

Col ((M * (ColVec2Mx x)),1) is FinSequence of REAL ;

coherence

Line (((LineVec2Mx x) * M),1) is FinSequence of REAL ;

end;
let x be FinSequence of REAL ;

coherence

Col ((M * (ColVec2Mx x)),1) is FinSequence of REAL ;

coherence

Line (((LineVec2Mx x) * M),1) is FinSequence of REAL ;

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

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

for M being Matrix of REAL

for x being FinSequence of REAL holds x * M = Line (((LineVec2Mx x) * M),1);

theorem Th52: :: MATRIXR1:52

for x being FinSequence of REAL

for A being Matrix of REAL st len A > 0 & width A > 0 & ( len A = len x or width (A @) = len x ) holds

(A @) * x = x * A

for A being Matrix of REAL st len A > 0 & width A > 0 & ( len A = len x or width (A @) = len x ) holds

(A @) * x = x * A

proof end;

theorem Th53: :: MATRIXR1:53

for x being FinSequence of REAL

for A being Matrix of REAL st len A > 0 & width A > 0 & ( width A = len x or len (A @) = len x ) holds

A * x = x * (A @)

for A being Matrix of REAL st len A > 0 & width A > 0 & ( width A = len x or len (A @) = len x ) holds

A * x = x * (A @)

proof end;

theorem Th54: :: MATRIXR1:54

for A, B being Matrix of REAL st len A = len 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 Th55: :: MATRIXR1:55

for A, B being Matrix of REAL st 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 Th56: :: MATRIXR1:56

for a being Real

for M being Matrix of REAL

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

Col ((a * M),i) = a * (Col (M,i))

for M being Matrix of REAL

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

Col ((a * M),i) = a * (Col (M,i))

proof end;

theorem :: MATRIXR1:57

for x1, x2 being FinSequence of REAL

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

A * (x1 + x2) = (A * x1) + (A * x2)

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

A * (x1 + x2) = (A * x1) + (A * x2)

proof end;

theorem :: MATRIXR1:58

for x1, x2 being FinSequence of REAL

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

(x1 + x2) * A = (x1 * A) + (x2 * A)

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

(x1 + x2) * A = (x1 * A) + (x2 * A)

proof end;

theorem Th59: :: MATRIXR1:59

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 :: MATRIXR1:60

for a being Real

for x being FinSequence of REAL

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

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

for x being FinSequence of REAL

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

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

proof end;

theorem Th61: :: MATRIXR1:61

for x being FinSequence of REAL

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

len (A * x) = len A

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

len (A * x) = len A

proof end;

theorem Th62: :: MATRIXR1:62

for x being FinSequence of REAL

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

len (x * A) = width A

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

len (x * A) = width A

proof end;

theorem Th63: :: MATRIXR1:63

for x being FinSequence of REAL

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

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

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

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

proof end;

theorem Th64: :: MATRIXR1:64

for x being FinSequence of REAL

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

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

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

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

proof end;

theorem :: MATRIXR1:65

for n, m being Element of NAT

for x being FinSequence of REAL st len x = m & n > 0 & m > 0 holds

(0_Rmatrix (n,m)) * x = 0* n

for x being FinSequence of REAL st len x = m & n > 0 & m > 0 holds

(0_Rmatrix (n,m)) * x = 0* n

proof end;

theorem :: MATRIXR1:66

for n, m being Element of NAT

for x being FinSequence of REAL st len x = n & n > 0 holds

x * (0_Rmatrix (n,m)) = 0* m

for x being FinSequence of REAL st len x = n & n > 0 holds

x * (0_Rmatrix (n,m)) = 0* m

proof end;