:: 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;
funcA + 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;
funcA - B ->  Matrix of COMPLEX equals :: MATRIX_5:def 5
 Field2COMPLEX ((COMPLEX2Field A) - (COMPLEX2Field B));
coherence
 Field2COMPLEX ((COMPLEX2Field A) - (COMPLEX2Field B)) is Matrix of COMPLEX ;
funcA * 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;
funcx * 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 b1 being Matrix of COMPLEX st
for ea being Element of F_Complex st ea = x holds
b1 = Field2COMPLEX (ea * (COMPLEX2Field A))
proofend;
uniqueness
 for b1, b2 being Matrix of COMPLEX st ( for ea being Element of F_Complex st ea = x holds
b1 = Field2COMPLEX (ea * (COMPLEX2Field A)) ) & ( for ea being Element of F_Complex st ea = x holds
b2 = Field2COMPLEX (ea * (COMPLEX2Field A)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines * MATRIX_5:def_7_:_
 for x being complex number
for A, b3 being Matrix of COMPLEX holds
( b3 = x * A iff for ea being Element of F_Complex st ea = x holds
b3 = 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
proofend;

theorem :: MATRIX_5:10
for M being Matrix of COMPLEX holds 1 * M = M
proofend;

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

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

theorem :: MATRIX_5:13
for M being Matrix of COMPLEX holds M + M = 2 * M
proofend;

theorem :: MATRIX_5:14
for M being Matrix of COMPLEX holds (M + M) + M = 3 * M
proofend;

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

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

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

theorem :: MATRIX_5:19
for M being Matrix of COMPLEX holds M + (0_Cx ((len M),(width M))) = M
proofend;

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

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

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

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

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

theorem :: MATRIX_5:25
for M1 being Matrix of COMPLEX st len M1 > 0 holds
0 * M1 = 0_Cx ((len M1),(width M1))
proofend;

definition
let s be complex-valued Function;
let k be set ;
:: original:.
redefine funcs . k ->  Element of COMPLEX ;
coherence
 s . k is Element of COMPLEX
proofend;
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 &amp; s . 1 = (M1 * (i,1)) * (M2 * (1,j)) &amp; ( for k being Element of NAT st 1 <= k &amp; k < len M2 holds
s . (k + 1) = (s . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) )
proofend;