:: A Theory of Matrices of Complex Elements
:: by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received December 10, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users
begin
theorem
:: MATRIX_5:1
1
=
1_
F_Complex
by
COMPLEX1:def 4
,
COMPLFLD:8
;
theorem
:: MATRIX_5:2
0.
F_Complex
=
0
by
COMPLFLD:7
;
definition
let
A
be
Matrix
of
COMPLEX
;
func
COMPLEX2Field
A
->
Matrix
of
F_Complex
equals
:: MATRIX_5:def 1
A
;
coherence
A
is
Matrix
of
F_Complex
by
COMPLFLD:def 1
;
end;
::
deftheorem
defines
COMPLEX2Field
MATRIX_5:def 1 :
for
A
being
Matrix
of
COMPLEX
holds
COMPLEX2Field
A
=
A
;
definition
let
A
be
Matrix
of
F_Complex
;
func
Field2COMPLEX
A
->
Matrix
of
COMPLEX
equals
:: MATRIX_5:def 2
A
;
coherence
A
is
Matrix
of
COMPLEX
by
COMPLFLD:def 1
;
end;
::
deftheorem
defines
Field2COMPLEX
MATRIX_5:def 2 :
for
A
being
Matrix
of
F_Complex
holds
Field2COMPLEX
A
=
A
;
theorem
:: MATRIX_5:3
for
A
,
B
being
Matrix
of
COMPLEX
st
COMPLEX2Field
A
=
COMPLEX2Field
B
holds
A
=
B
;
theorem
:: MATRIX_5:4
for
A
,
B
being
Matrix
of
F_Complex
st
Field2COMPLEX
A
=
Field2COMPLEX
B
holds
A
=
B
;
theorem
:: MATRIX_5:5
for
A
being
Matrix
of
COMPLEX
holds
A
=
Field2COMPLEX
(
COMPLEX2Field
A
)
;
theorem
:: MATRIX_5:6
for
A
being
Matrix
of
F_Complex
holds
A
=
COMPLEX2Field
(
Field2COMPLEX
A
)
;
definition
let
A
,
B
be
Matrix
of
COMPLEX
;
func
A
+
B
->
Matrix
of
COMPLEX
equals
:: MATRIX_5:def 3
Field2COMPLEX
(
(
COMPLEX2Field
A
)
+
(
COMPLEX2Field
B
)
)
;
coherence
Field2COMPLEX
(
(
COMPLEX2Field
A
)
+
(
COMPLEX2Field
B
)
)
is
Matrix
of
COMPLEX
;
end;
::
deftheorem
defines
+
MATRIX_5:def 3 :
for
A
,
B
being
Matrix
of
COMPLEX
holds
A
+
B
=
Field2COMPLEX
(
(
COMPLEX2Field
A
)
+
(
COMPLEX2Field
B
)
)
;
definition
let
A
be
Matrix
of
COMPLEX
;
func
-
A
->
Matrix
of
COMPLEX
equals
:: MATRIX_5:def 4
Field2COMPLEX
(
-
(
COMPLEX2Field
A
)
)
;
coherence
Field2COMPLEX
(
-
(
COMPLEX2Field
A
)
)
is
Matrix
of
COMPLEX
;
end;
::
deftheorem
defines
-
MATRIX_5:def 4 :
for
A
being
Matrix
of
COMPLEX
holds
-
A
=
Field2COMPLEX
(
-
(
COMPLEX2Field
A
)
)
;
definition
let
A
,
B
be
Matrix
of
COMPLEX
;
func
A
-
B
->
Matrix
of
COMPLEX
equals
:: MATRIX_5:def 5
Field2COMPLEX
(
(
COMPLEX2Field
A
)
-
(
COMPLEX2Field
B
)
)
;
coherence
Field2COMPLEX
(
(
COMPLEX2Field
A
)
-
(
COMPLEX2Field
B
)
)
is
Matrix
of
COMPLEX
;
func
A
*
B
->
Matrix
of
COMPLEX
equals
:: MATRIX_5:def 6
Field2COMPLEX
(
(
COMPLEX2Field
A
)
*
(
COMPLEX2Field
B
)
)
;
coherence
Field2COMPLEX
(
(
COMPLEX2Field
A
)
*
(
COMPLEX2Field
B
)
)
is
Matrix
of
COMPLEX
;
end;
::
deftheorem
defines
-
MATRIX_5:def 5 :
for
A
,
B
being
Matrix
of
COMPLEX
holds
A
-
B
=
Field2COMPLEX
(
(
COMPLEX2Field
A
)
-
(
COMPLEX2Field
B
)
)
;
::
deftheorem
defines
*
MATRIX_5:def 6 :
for
A
,
B
being
Matrix
of
COMPLEX
holds
A
*
B
=
Field2COMPLEX
(
(
COMPLEX2Field
A
)
*
(
COMPLEX2Field
B
)
)
;
definition
let
x
be
complex
number
;
let
A
be
Matrix
of
COMPLEX
;
func
x
*
A
->
Matrix
of
COMPLEX
means
:
Def7
:
:: MATRIX_5:def 7
for
ea
being
Element
of
F_Complex
st
ea
=
x
holds
it
=
Field2COMPLEX
(
ea
*
(
COMPLEX2Field
A
)
)
;
existence
ex
b
1
being
Matrix
of
COMPLEX
st
for
ea
being
Element
of
F_Complex
st
ea
=
x
holds
b
1
=
Field2COMPLEX
(
ea
*
(
COMPLEX2Field
A
)
)
proof
end;
uniqueness
for
b
1
,
b
2
being
Matrix
of
COMPLEX
st ( for
ea
being
Element
of
F_Complex
st
ea
=
x
holds
b
1
=
Field2COMPLEX
(
ea
*
(
COMPLEX2Field
A
)
)
) & ( for
ea
being
Element
of
F_Complex
st
ea
=
x
holds
b
2
=
Field2COMPLEX
(
ea
*
(
COMPLEX2Field
A
)
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def7
defines
*
MATRIX_5:def 7 :
for
x
being
complex
number
for
A
,
b
3
being
Matrix
of
COMPLEX
holds
(
b
3
=
x
*
A
iff for
ea
being
Element
of
F_Complex
st
ea
=
x
holds
b
3
=
Field2COMPLEX
(
ea
*
(
COMPLEX2Field
A
)
)
);
theorem
:: MATRIX_5:7
for
A
being
Matrix
of
COMPLEX
holds
(
len
A
=
len
(
COMPLEX2Field
A
)
&
width
A
=
width
(
COMPLEX2Field
A
)
) ;
theorem
:: MATRIX_5:8
for
A
being
Matrix
of
F_Complex
holds
(
len
A
=
len
(
Field2COMPLEX
A
)
&
width
A
=
width
(
Field2COMPLEX
A
)
) ;
theorem
Th9
:
:: MATRIX_5:9
for
K
being
Field
for
M
being
Matrix
of
K
holds
(
1_
K
)
*
M
=
M
proof
end;
theorem
:: MATRIX_5:10
for
M
being
Matrix
of
COMPLEX
holds 1
*
M
=
M
proof
end;
theorem
:: MATRIX_5:11
for
K
being
Field
for
a
,
b
being
Element
of
K
for
M
being
Matrix
of
K
holds
a
*
(
b
*
M
)
=
(
a
*
b
)
*
M
proof
end;
theorem
Th12
:
:: MATRIX_5:12
for
K
being
Field
for
a
,
b
being
Element
of
K
for
M
being
Matrix
of
K
holds
(
a
+
b
)
*
M
=
(
a
*
M
)
+
(
b
*
M
)
proof
end;
theorem
:: MATRIX_5:13
for
M
being
Matrix
of
COMPLEX
holds
M
+
M
=
2
*
M
proof
end;
theorem
:: MATRIX_5:14
for
M
being
Matrix
of
COMPLEX
holds
(
M
+
M
)
+
M
=
3
*
M
proof
end;
definition
let
n
,
m
be
Nat
;
func
0_Cx
(
n
,
m
)
->
Matrix
of
COMPLEX
equals
:: MATRIX_5:def 8
Field2COMPLEX
(
0.
(
F_Complex
,
n
,
m
)
)
;
coherence
Field2COMPLEX
(
0.
(
F_Complex
,
n
,
m
)
)
is
Matrix
of
COMPLEX
;
end;
::
deftheorem
defines
0_Cx
MATRIX_5:def 8 :
for
n
,
m
being
Nat
holds
0_Cx
(
n
,
m
)
=
Field2COMPLEX
(
0.
(
F_Complex
,
n
,
m
)
)
;
theorem
:: MATRIX_5:15
for
n
,
m
being
Element
of
NAT
holds
COMPLEX2Field
(
0_Cx
(
n
,
m
)
)
=
0.
(
F_Complex
,
n
,
m
) ;
theorem
:: MATRIX_5:16
for
M1
,
M2
being
Matrix
of
COMPLEX
st
len
M1
=
len
M2
&
width
M1
=
width
M2
&
M1
=
M1
+
M2
holds
M2
=
0_Cx
(
(
len
M1
)
,
(
width
M1
)
)
proof
end;
theorem
:: MATRIX_5:17
for
M1
,
M2
being
Matrix
of
COMPLEX
st
len
M1
=
len
M2
&
width
M1
=
width
M2
&
M1
+
M2
=
0_Cx
(
(
len
M1
)
,
(
width
M1
)
) holds
M2
=
-
M1
proof
end;
theorem
:: MATRIX_5:18
for
M1
,
M2
being
Matrix
of
COMPLEX
st
len
M1
=
len
M2
&
width
M1
=
width
M2
&
M2
-
M1
=
M2
holds
M1
=
0_Cx
(
(
len
M1
)
,
(
width
M1
)
)
proof
end;
theorem
:: MATRIX_5:19
for
M
being
Matrix
of
COMPLEX
holds
M
+
(
0_Cx
(
(
len
M
)
,
(
width
M
)
)
)
=
M
proof
end;
theorem
Th20
:
:: MATRIX_5:20
for
K
being
Field
for
b
being
Element
of
K
for
M1
,
M2
being
Matrix
of
K
st
len
M1
=
len
M2
&
width
M1
=
width
M2
holds
b
*
(
M1
+
M2
)
=
(
b
*
M1
)
+
(
b
*
M2
)
proof
end;
theorem
:: MATRIX_5:21
for
M1
,
M2
being
Matrix
of
COMPLEX
for
a
being
complex
number
st
len
M1
=
len
M2
&
width
M1
=
width
M2
holds
a
*
(
M1
+
M2
)
=
(
a
*
M1
)
+
(
a
*
M2
)
proof
end;
theorem
Th22
:
:: MATRIX_5:22
for
K
being
Field
for
M1
,
M2
being
Matrix
of
K
st
width
M1
=
len
M2
&
len
M1
>
0
&
len
M2
>
0
holds
(
0.
(
K
,
(
len
M1
)
,
(
width
M1
)
)
)
*
M2
=
0.
(
K
,
(
len
M1
)
,
(
width
M2
)
)
proof
end;
theorem
:: MATRIX_5:23
for
M1
,
M2
being
Matrix
of
COMPLEX
st
width
M1
=
len
M2
&
len
M1
>
0
&
len
M2
>
0
holds
(
0_Cx
(
(
len
M1
)
,
(
width
M1
)
)
)
*
M2
=
0_Cx
(
(
len
M1
)
,
(
width
M2
)
)
proof
end;
theorem
Th24
:
:: MATRIX_5:24
for
K
being
Field
for
M1
being
Matrix
of
K
st
len
M1
>
0
holds
(
0.
K
)
*
M1
=
0.
(
K
,
(
len
M1
)
,
(
width
M1
)
)
proof
end;
theorem
:: MATRIX_5:25
for
M1
being
Matrix
of
COMPLEX
st
len
M1
>
0
holds
0
*
M1
=
0_Cx
(
(
len
M1
)
,
(
width
M1
)
)
proof
end;
definition
let
s
be
complex-valued
Function
;
let
k
be
set
;
:: original:
.
redefine
func
s
.
k
->
Element
of
COMPLEX
;
coherence
s
.
k
is
Element
of
COMPLEX
proof
end;
end;
theorem
:: MATRIX_5:26
for
i
,
j
being
Element
of
NAT
for
M1
,
M2
being
Matrix
of
COMPLEX
st
len
M2
>
0
holds
ex
s
being
FinSequence
of
COMPLEX
st
(
len
s
=
len
M2
&
s
.
1
=
(
M1
*
(
i
,1)
)
*
(
M2
*
(1,
j
)
)
& ( for
k
being
Element
of
NAT
st 1
<=
k
&
k
<
len
M2
holds
s
.
(
k
+
1
)
=
(
s
.
k
)
+
(
(
M1
*
(
i
,
(
k
+
1
)
)
)
*
(
M2
*
(
(
k
+
1
)
,
j
)
)
)
) )
proof
end;