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