:: by Yatsuka Nakamura and Hiroshi Yamazaki

::

:: Received August 8, 2003

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

begin

:: deftheorem defines - MATRIX_4:def 1 :

for K being Field

for M1, M2 being Matrix of K holds M1 - M2 = M1 + (- M2);

for K being Field

for M1, M2 being Matrix of K holds M1 - M2 = M1 + (- M2);

theorem :: MATRIX_4:3

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

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

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

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

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

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

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)

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)

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

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

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

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

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)

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

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

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)

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

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

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)

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

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

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)

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)

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

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

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

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

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

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)

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)

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

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

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)

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

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

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)

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

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

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

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)

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

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

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

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)

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

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

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

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

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

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

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

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

theorem Th59: :: MATRIX_4:59

for i being Nat

for K being Field

for j being Element of NAT

for A, B being Matrix of K st width A = width B & ex j being Element of NAT st [i,j] in Indices A holds

Line ((A + B),i) = (Line (A,i)) + (Line (B,i))

for K being Field

for j being Element of NAT

for A, B being Matrix of K st width A = width B & ex j being Element of 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))

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)

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)

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)

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 Element of 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

for n, m, k being Element of 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;