:: A Theory of Matrices of Complex Elements
:: by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received December 10, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users


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;
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 b1 being Matrix of COMPLEX st
for ea being Element of F_Complex st ea = x holds
b1 = Field2COMPLEX (ea * (COMPLEX2Field A))
proof end;
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
proof end;
end;

:: deftheorem Def7 defines * MATRIX_5:def 7 :
for x being Complex
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
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 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 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 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 Nat st 1 <= k & k < len M2 holds
s . (k + 1) = (s . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) )
proof end;