:: 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 b1 being Matrix of REAL st
for ea being Element of F_Real st ea = a holds
b1 = MXF2MXR (ea * (MXR2MXF A))
proof end;
uniqueness
for b1, b2 being Matrix of REAL st ( for ea being Element of F_Real st ea = a holds
b1 = MXF2MXR (ea * (MXR2MXF A)) ) & ( for ea being Element of F_Real st ea = a holds
b2 = MXF2MXR (ea * (MXR2MXF A)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines * MATRIXR1:def 7 :
for a being Real
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: :: 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 b1 being Matrix of REAL st
( len b1 = len x & width b1 = 1 & ( for j being Nat st j in dom x holds
b1 . j = <*(x . j)*> ) )
proof end;
uniqueness
for b1, b2 being Matrix of REAL st len b1 = len x & width b1 = 1 & ( for j being Nat st j in dom x holds
b1 . j = <*(x . j)*> ) & len b2 = len x & width b2 = 1 & ( for j being Nat st j in dom x holds
b2 . j = <*(x . j)*> ) holds
b1 = b2
proof end;
end;

:: 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 :: 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 b1 being Matrix of REAL st
( width b1 = len x & len b1 = 1 & ( for j being Nat st j in dom x holds
b1 * (1,j) = x . j ) )
proof end;
uniqueness
for b1, b2 being Matrix of REAL st width b1 = len x & len b1 = 1 & ( for j being Nat st j in dom x holds
b1 * (1,j) = x . j ) & width b2 = len x & len b2 = 1 & ( for j being Nat st j in dom x holds
b2 * (1,j) = x . j ) holds
b1 = b2
proof end;
end;

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