:: Calculation of Matrices of Field Elements. Part {I}
:: by Yatsuka Nakamura and Hiroshi Yamazaki
::
:: Received August 8, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users


definition
let K be Field;
let M1, M2 be Matrix of K;
func M1 - M2 -> Matrix of K equals :: MATRIX_4:def 1
M1 + (- M2);
coherence
M1 + (- M2) is Matrix of K ;
end;

:: deftheorem defines - MATRIX_4:def 1 :
for K being Field
for M1, M2 being Matrix of K holds M1 - M2 = M1 + (- M2);

theorem Th1: :: MATRIX_4:1
for K being Field
for M being Matrix of K holds - (- M) = M
proof end;

theorem Th2: :: MATRIX_4:2
for K being Field
for M being Matrix of K holds M + (- M) = 0. (K,(len M),(width M))
proof end;

theorem :: MATRIX_4:3
for K being Field
for M being Matrix of K holds M - M = 0. (K,(len M),(width M)) by Th2;

theorem :: MATRIX_4:4
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M1 + M3 = M2 + M3 holds
M1 = M2
proof end;

theorem :: MATRIX_4:5
for K being Field
for M1, M2 being Matrix of K holds M1 - (- M2) = M1 + M2 by Th1;

theorem :: MATRIX_4:6
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 & M1 = M1 + M2 holds
M2 = 0. (K,(len M1),(width M1))
proof end;

theorem Th7: :: MATRIX_4:7
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 & M1 - M2 = 0. (K,(len M1),(width M1)) holds
M1 = M2
proof end;

theorem Th8: :: MATRIX_4:8
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 & M1 + M2 = 0. (K,(len M1),(width M1)) holds
M2 = - M1
proof end;

theorem Th9: :: MATRIX_4:9
for n, m being Nat
for K being Field holds - (0. (K,n,m)) = 0. (K,n,m)
proof end;

theorem :: MATRIX_4:10
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 & M2 - M1 = M2 holds
M1 = 0. (K,(len M1),(width M1))
proof end;

theorem Th11: :: MATRIX_4:11
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
M1 = M1 - (M2 - M2)
proof end;

theorem Th12: :: MATRIX_4:12
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
- (M1 + M2) = (- M1) + (- M2)
proof end;

theorem :: MATRIX_4:13
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
M1 - (M1 - M2) = M2
proof end;

theorem Th14: :: MATRIX_4:14
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M1 - M3 = M2 - M3 holds
M1 = M2
proof end;

theorem Th15: :: MATRIX_4:15
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M3 - M1 = M3 - M2 holds
M1 = M2
proof end;

theorem Th16: :: MATRIX_4:16
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds
(M1 - M2) - M3 = (M1 - M3) - M2
proof end;

theorem :: MATRIX_4:17
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds
M1 - M3 = (M1 - M2) - (M3 - M2)
proof end;

theorem Th18: :: MATRIX_4:18
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds
(M3 - M1) - (M3 - M2) = M2 - M1
proof end;

theorem :: MATRIX_4:19
for K being Field
for M1, M2, M3, M4 being Matrix of K st len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 - M2 = M3 - M4 holds
M1 - M3 = M2 - M4
proof end;

theorem Th20: :: MATRIX_4:20
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
M1 = M1 + (M2 - M2)
proof end;

theorem Th21: :: MATRIX_4:21
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
M1 = (M1 + M2) - M2
proof end;

theorem Th22: :: MATRIX_4:22
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
M1 = (M1 - M2) + M2
proof end;

theorem :: MATRIX_4:23
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds
M1 + M3 = (M1 + M2) + (M3 - M2)
proof end;

theorem :: MATRIX_4:24
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds
(M1 + M2) - M3 = (M1 - M3) + M2
proof end;

theorem :: MATRIX_4:25
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds
(M1 - M2) + M3 = (M3 - M2) + M1
proof end;

theorem Th26: :: MATRIX_4:26
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds
M1 + M3 = (M1 + M2) - (M2 - M3)
proof end;

theorem :: MATRIX_4:27
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds
M1 - M3 = (M1 + M2) - (M3 + M2)
proof end;

theorem Th28: :: MATRIX_4:28
for K being Field
for M1, M2, M3, M4 being Matrix of K st len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 + M2 = M3 + M4 holds
M1 - M3 = M4 - M2
proof end;

theorem :: MATRIX_4:29
for K being Field
for M1, M2, M3, M4 being Matrix of K st len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 - M3 = M4 - M2 holds
M1 + M2 = M3 + M4
proof end;

theorem :: MATRIX_4:30
for K being Field
for M1, M2, M3, M4 being Matrix of K st len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 + M2 = M3 - M4 holds
M1 + M4 = M3 - M2
proof end;

theorem Th31: :: MATRIX_4:31
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds
M1 - (M2 + M3) = (M1 - M2) - M3
proof end;

theorem :: MATRIX_4:32
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds
M1 - (M2 - M3) = (M1 - M2) + M3
proof end;

theorem :: MATRIX_4:33
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds
M1 - (M2 - M3) = M1 + (M3 - M2)
proof end;

theorem :: MATRIX_4:34
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
M1 - M3 = (M1 - M2) + (M2 - M3)
proof end;

theorem :: MATRIX_4:35
for K being Field
for M1, M2, M3 being Matrix of K st - M1 = - M2 holds
M1 = M2
proof end;

theorem :: MATRIX_4:36
for K being Field
for M being Matrix of K st - M = 0. (K,(len M),(width M)) holds
M = 0. (K,(len M),(width M))
proof end;

theorem :: MATRIX_4:37
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 & M1 + (- M2) = 0. (K,(len M1),(width M1)) holds
M1 = M2
proof end;

theorem Th38: :: MATRIX_4:38
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
M1 = (M1 + M2) + (- M2)
proof end;

theorem :: MATRIX_4:39
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
M1 = M1 + (M2 + (- M2))
proof end;

theorem :: MATRIX_4:40
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
M1 = ((- M2) + M1) + M2
proof end;

theorem :: MATRIX_4:41
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
- ((- M1) + M2) = M1 + (- M2)
proof end;

theorem :: MATRIX_4:42
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
M1 + M2 = - ((- M1) + (- M2))
proof end;

theorem :: MATRIX_4:43
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
- (M1 - M2) = M2 - M1
proof end;

theorem Th44: :: MATRIX_4:44
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
(- M1) - M2 = (- M2) - M1
proof end;

theorem :: MATRIX_4:45
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
M1 = (- M2) - ((- M1) - M2)
proof end;

theorem Th46: :: MATRIX_4:46
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds
((- M1) - M2) - M3 = ((- M1) - M3) - M2
proof end;

theorem Th47: :: MATRIX_4:47
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds
((- M1) - M2) - M3 = ((- M2) - M3) - M1
proof end;

theorem :: MATRIX_4:48
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds
((- M1) - M2) - M3 = ((- M3) - M2) - M1
proof end;

theorem :: MATRIX_4:49
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds
(M3 - M1) - (M3 - M2) = - (M1 - M2)
proof end;

theorem :: MATRIX_4:50
for K being Field
for M being Matrix of K holds (0. (K,(len M),(width M))) - M = - M
proof end;

theorem :: MATRIX_4:51
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
M1 + M2 = M1 - (- M2) by Th1;

theorem :: MATRIX_4:52
for K being Field
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
M1 = M1 - (M2 + (- M2))
proof end;

theorem :: MATRIX_4:53
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M1 - M3 = M2 + (- M3) holds
M1 = M2
proof end;

theorem :: MATRIX_4:54
for K being Field
for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M3 - M1 = M3 + (- M2) holds
M1 = M2
proof end;

theorem Th55: :: MATRIX_4:55
for K being set
for A, B being Matrix of K st len A = len B & width A = width B holds
Indices A = Indices B
proof end;

theorem Th56: :: MATRIX_4:56
for K being Field
for x, y, z being FinSequence of K st len x = len y & len y = len z holds
mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z))
proof end;

theorem Th57: :: MATRIX_4:57
for K being Field
for x, y, z being FinSequence of K st len x = len y & len y = len z holds
mlt (z,(x + y)) = (mlt (z,x)) + (mlt (z,y))
proof end;

theorem :: MATRIX_4:58
for D being non empty set
for M being Matrix of D st len M > 0 holds
for n being Nat holds
( M is Matrix of n, width M,D iff n = len M ) by MATRIX_0:20, MATRIX_0:def 2;

theorem Th59: :: MATRIX_4:59
for i being Nat
for K being Field
for j being Nat
for A, B being Matrix of K st width A = width B & ex j being Nat st [i,j] in Indices A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
proof end;

theorem Th60: :: MATRIX_4:60
for K being Field
for j being Nat
for A, B being Matrix of K st len A = len B & ex i being Nat st [i,j] in Indices A holds
Col ((A + B),j) = (Col (A,j)) + (Col (B,j))
proof end;

theorem Th61: :: MATRIX_4:61
for V1 being Field
for P1, P2 being FinSequence of V1 st len P1 = len P2 holds
Sum (P1 + P2) = (Sum P1) + (Sum P2)
proof end;

theorem :: MATRIX_4:62
for K being Field
for A, B, C being Matrix of K st len B = len C & width B = width C & width A = len B & len A > 0 & len B > 0 holds
A * (B + C) = (A * B) + (A * C)
proof end;

theorem :: MATRIX_4:63
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)
proof end;

theorem :: MATRIX_4:64
for K being Field
for n, m, k being Nat
for M1 being Matrix of n,m,K
for M2 being Matrix of m,k,K st width M1 = len M2 & 0 < len M1 & 0 < len M2 holds
M1 * M2 is Matrix of n,k,K
proof end;