:: Calculation of Matrices of Field Elements. Part {I}
:: by Yatsuka Nakamura and Hiroshi Yamazaki
::
:: Received August 8, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users
begin
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
Element
of
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
Element
of
NAT
holds
(
M
is
Matrix
of
n
,
width
M
,
D
iff
n
=
len
M
)
by
MATRIX_1:20
,
MATRIX_1:def 2
;
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
)
)
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
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;