:: by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura

::

:: Received December 10, 2004

:: Copyright (c) 2004-2021 Association of Mizar Users

:: deftheorem defines COMPLEX2Field MATRIX_5:def 1 :

for A being Matrix of COMPLEX holds COMPLEX2Field A = A;

for A being Matrix of COMPLEX holds COMPLEX2Field A = A;

:: deftheorem defines Field2COMPLEX MATRIX_5:def 2 :

for A being Matrix of F_Complex holds Field2COMPLEX A = A;

for A being Matrix of F_Complex holds Field2COMPLEX A = A;

theorem :: MATRIX_5:3

theorem :: MATRIX_5:4

definition

let A, B be Matrix of COMPLEX;

Field2COMPLEX ((COMPLEX2Field A) + (COMPLEX2Field B)) is Matrix of COMPLEX ;

end;
func A + B -> Matrix of COMPLEX equals :: MATRIX_5:def 3

Field2COMPLEX ((COMPLEX2Field A) + (COMPLEX2Field B));

coherence Field2COMPLEX ((COMPLEX2Field A) + (COMPLEX2Field B));

Field2COMPLEX ((COMPLEX2Field A) + (COMPLEX2Field B)) is Matrix of COMPLEX ;

:: deftheorem defines + MATRIX_5:def 3 :

for A, B being Matrix of COMPLEX holds A + B = Field2COMPLEX ((COMPLEX2Field A) + (COMPLEX2Field B));

for A, B being Matrix of COMPLEX holds A + B = Field2COMPLEX ((COMPLEX2Field A) + (COMPLEX2Field B));

definition
end;

:: deftheorem defines - MATRIX_5:def 4 :

for A being Matrix of COMPLEX holds - A = Field2COMPLEX (- (COMPLEX2Field A));

for A being Matrix of COMPLEX holds - A = Field2COMPLEX (- (COMPLEX2Field A));

definition

let A, B be Matrix of COMPLEX;

Field2COMPLEX ((COMPLEX2Field A) - (COMPLEX2Field B)) is Matrix of COMPLEX ;

Field2COMPLEX ((COMPLEX2Field A) * (COMPLEX2Field B)) is Matrix of COMPLEX ;

end;
func A - B -> Matrix of COMPLEX equals :: MATRIX_5:def 5

Field2COMPLEX ((COMPLEX2Field A) - (COMPLEX2Field B));

coherence Field2COMPLEX ((COMPLEX2Field A) - (COMPLEX2Field B));

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

Field2COMPLEX ((COMPLEX2Field A) * (COMPLEX2Field B)) is Matrix of COMPLEX ;

:: deftheorem defines - MATRIX_5:def 5 :

for A, B being Matrix of COMPLEX holds A - B = Field2COMPLEX ((COMPLEX2Field A) - (COMPLEX2Field B));

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

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;

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

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}

end;
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 for ea being Element of F_Complex st ea = x holds

it = Field2COMPLEX (ea * (COMPLEX2Field A));

ex b

for ea being Element of F_Complex st ea = x holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def7 defines * MATRIX_5:def 7 :

for x being Complex

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

for x being Complex

for A, b

( b

b

theorem :: MATRIX_5:7

for A being Matrix of COMPLEX holds

( len A = len (COMPLEX2Field A) & width A = width (COMPLEX2Field A) ) ;

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

( len A = len (Field2COMPLEX A) & width A = width (Field2COMPLEX A) ) ;

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

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)

for a, b being Element of K

for M being Matrix of K holds (a + b) * M = (a * M) + (b * M)

proof end;

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

for n, m being Nat holds 0_Cx (n,m) = Field2COMPLEX (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))

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

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

M1 = 0_Cx ((len M1),(width M1))

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)

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)

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

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

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

for M1 being Matrix of K st len M1 > 0 holds

(0. K) * M1 = 0. (K,(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

end;
let k be set ;

:: original: .

redefine func s . k -> Element of COMPLEX ;

coherence

s . k is Element of COMPLEX

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

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;