:: A Theory of Matrices of Real Elements
:: by Yatsuka Nakamura , Nobuyuki Tamura and Wenpai Chang
::
:: Received February 20, 2006
:: Copyright (c) 2006-2021 Association of Mizar Users

theorem :: MATRIXR1:1

for r1, r2 being Real
for fr1, fr2 being Element of F_Real st r1 = fr1 & r2 = fr2 holds
r1 + r2 = fr1 + fr2 ;

theorem :: MATRIXR1:2

for r1, r2 being Real
for fr1, fr2 being Element of F_Real st r1 = fr1 & r2 = fr2 holds
r1 * r2 = fr1 * fr2 ;

theorem Th3: :: MATRIXR1:3

for F being FinSequence of REAL holds
( F + (- F) = 0* (len F) & F - F = 0* (len F) )

proof end;

theorem :: MATRIXR1:4

for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
F1 - F2 = F1 + (- F2) ;

theorem :: MATRIXR1:5

for F being FinSequence of REAL holds F - (0* (len F)) = F

proof end;

theorem :: MATRIXR1:6

for F being FinSequence of REAL holds (0* (len F)) - F = - F

proof end;

theorem :: MATRIXR1:7

for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
F1 - (- F2) = F1 + F2 ;

theorem :: MATRIXR1:8

for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
- (F1 - F2) = F2 - F1 by RVSUM_1:35;

theorem :: MATRIXR1:9

for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
- (F1 - F2) = (- F1) + F2 by RVSUM_1:36;

theorem :: MATRIXR1:10

for F1, F2 being FinSequence of REAL st len F1 = len F2 & F1 - F2 = 0* (len F1) holds
F1 = F2

proof end;

theorem :: MATRIXR1:11

for F1, F2, F3 being FinSequence of REAL st len F1 = len F2 & len F2 = len F3 holds
(F1 - F2) - F3 = F1 - (F2 + F3) by RVSUM_1:39;

theorem :: MATRIXR1:12

for F1, F2, F3 being FinSequence of REAL st len F1 = len F2 & len F2 = len F3 holds
F1 + (F2 - F3) = (F1 + F2) - F3 by RVSUM_1:40;

theorem :: MATRIXR1:13

for F1, F2, F3 being FinSequence of REAL st len F1 = len F2 & len F2 = len F3 holds
F1 - (F2 - F3) = (F1 - F2) + F3 by RVSUM_1:41;

theorem Th14: :: MATRIXR1:14

for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
F1 = (F1 + F2) - F2

proof end;

theorem :: MATRIXR1:15

for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
F1 = (F1 - F2) + F2

proof end;

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

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

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

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

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

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

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)

proof end;

definition

let A be Matrix of REAL;

func MXR2MXF A -> Matrix of F_Real equals :: MATRIXR1:def 1
A;

coherence
A is Matrix of F_Real ;

end;

:: deftheorem defines MXR2MXF MATRIXR1:def 1 :
for A being Matrix of REAL holds MXR2MXF A = A;

definition

let A be Matrix of F_Real;

func MXF2MXR A -> Matrix of REAL equals :: MATRIXR1:def 2
A;

coherence
A is Matrix of REAL ;

end;

:: deftheorem defines MXF2MXR MATRIXR1:def 2 :
for A being Matrix of F_Real holds MXF2MXR A = A;

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)

proof end;

theorem :: MATRIXR1:24

for K being Field
for A, B being Matrix of K holds Indices (A + B) = Indices A

proof end;

definition

let A, B be Matrix of REAL;

func A + B -> Matrix of REAL equals :: MATRIXR1:def 3
MXF2MXR ((MXR2MXF A) + (MXR2MXF B));

coherence
MXF2MXR ((MXR2MXF A) + (MXR2MXF B)) is Matrix of REAL ;

end;

:: deftheorem defines + MATRIXR1:def 3 :
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)) ) )

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

proof end;

definition

let A be Matrix of REAL;

func - A -> Matrix of REAL equals :: MATRIXR1:def 4
MXF2MXR (- (MXR2MXF A));

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

end;

:: deftheorem defines - MATRIXR1:def 4 :
for A being Matrix of REAL holds - A = MXF2MXR (- (MXR2MXF A));

definition

let A, B be Matrix of REAL;

func A - B -> Matrix of REAL equals :: MATRIXR1:def 5
MXF2MXR ((MXR2MXF A) - (MXR2MXF B));

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

func A * B -> Matrix of REAL equals :: MATRIXR1:def 6
MXF2MXR ((MXR2MXF A) * (MXR2MXF B));

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

end;

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

definition

let a be Real;
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
ex b₁ being Matrix of REAL st
for ea being Element of F_Real st ea = a holds
b₁ = MXF2MXR (ea * (MXR2MXF A))

proof end;

uniqueness
for b₁, b₂ being Matrix of REAL st ( for ea being Element of F_Real st ea = a holds
b₁ = MXF2MXR (ea * (MXR2MXF A)) ) & ( for ea being Element of F_Real st ea = a holds
b₂ = MXF2MXR (ea * (MXR2MXF A)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines * MATRIXR1:def 7 :
for a being Real
for A, b₃ being Matrix of REAL holds
( b₃ = a * A iff for ea being Element of F_Real st ea = a holds
b₃ = MXF2MXR (ea * (MXR2MXF A)) );

theorem Th27: :: MATRIXR1:27

for a being Real
for A being Matrix of REAL holds
( len (a * A) = len A & width (a * A) = width A )

proof end;

theorem Th28: :: MATRIXR1:28

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

proof end;

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

proof end;

theorem Th30: :: MATRIXR1:30

for a being Real
for A being Matrix of REAL st width A > 0 holds
(a * A) @ = a * (A @)

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

proof end;

theorem :: MATRIXR1:32

for A being Matrix of REAL holds 1 * A = A

proof end;

theorem :: MATRIXR1:33

for A being Matrix of REAL holds A + A = 2 * A

proof end;

theorem :: MATRIXR1:34

for A being Matrix of REAL holds (A + A) + A = 3 * A

proof end;

definition

let n, m be Nat;

func 0_Rmatrix (n,m) -> Matrix of REAL equals :: MATRIXR1:def 8
MXF2MXR (0. (F_Real,n,m));

coherence
MXF2MXR (0. (F_Real,n,m)) is Matrix of REAL ;

end;

:: deftheorem defines 0_Rmatrix MATRIXR1:def 8 :
for n, m being Nat holds 0_Rmatrix (n,m) = MXF2MXR (0. (F_Real,n,m));

theorem :: MATRIXR1:35

for A, B being Matrix of REAL holds A - (- B) = A + B

proof end;

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 )

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

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

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

proof end;

theorem Th40: :: MATRIXR1:40

for a being Real
for A, B being Matrix of REAL st width A = len B holds
A * (a * B) = a * (A * B)

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)

proof end;

theorem :: MATRIXR1:42

for M being Matrix of REAL holds M + (0_Rmatrix ((len M),(width M))) = M

proof end;

theorem :: MATRIXR1:43

for a being Real
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;

theorem :: MATRIXR1:44

for A being Matrix of REAL st len A > 0 holds
0 * A = 0_Rmatrix ((len A),(width A))

proof end;

definition

let x be FinSequence of REAL ;
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
ex b₁ being Matrix of REAL st
( len b₁ = len x & width b₁ = 1 & ( for j being Nat st j in dom x holds
b₁ . j = <*(x . j)*> ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of REAL st len b₁ = len x & width b₁ = 1 & ( for j being Nat st j in dom x holds
b₁ . j = <*(x . j)*> ) & len b₂ = len x & width b₂ = 1 & ( for j being Nat st j in dom x holds
b₂ . j = <*(x . j)*> ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines ColVec2Mx MATRIXR1:def 9 :
for x being FinSequence of REAL st len x > 0 holds
for b₂ being Matrix of REAL holds
( b₂ = ColVec2Mx x iff ( len b₂ = len x & width b₂ = 1 & ( for j being Nat st j in dom x holds
b₂ . j = <*(x . j)*> ) ) );

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

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)

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)

proof end;

definition

let x be FinSequence of REAL ;

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
ex b₁ being Matrix of REAL st
( width b₁ = len x & len b₁ = 1 & ( for j being Nat st j in dom x holds
b₁ * (1,j) = x . j ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of REAL st width b₁ = len x & len b₁ = 1 & ( for j being Nat st j in dom x holds
b₁ * (1,j) = x . j ) & width b₂ = len x & len b₂ = 1 & ( for j being Nat st j in dom x holds
b₂ * (1,j) = x . j ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines LineVec2Mx MATRIXR1:def 10 :
for x being FinSequence of REAL
for b₂ being Matrix of REAL holds
( b₂ = LineVec2Mx x iff ( width b₂ = len x & len b₂ = 1 & ( for j being Nat st j in dom x holds
b₂ * (1,j) = x . j ) ) );

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

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 )

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)

proof end;

theorem :: MATRIXR1:51

for a being Real
for x being FinSequence of REAL holds LineVec2Mx (a * x) = a * (LineVec2Mx x)

proof end;

definition

let M be Matrix of REAL;
let x be FinSequence of REAL ;

func M * x -> FinSequence of REAL equals :: MATRIXR1:def 11
Col ((M * (ColVec2Mx x)),1);

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

func x * M -> FinSequence of REAL equals :: MATRIXR1:def 12
Line (((LineVec2Mx x) * M),1);

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

end;

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

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

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

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

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

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)

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)

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)

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)

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

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

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)

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)

proof end;

theorem :: MATRIXR1:65

for n, m being Nat
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 Nat
for x being FinSequence of REAL st len x = n & n > 0 holds
x * (0_Rmatrix (n,m)) = 0* m

proof end;