:: MATRIX_5 semantic presentation

theorem :: MATRIX_5:1

1 = 1. F_Complex by COMPLEX1:def 7, COMPLFLD:10;

theorem :: MATRIX_5:2

0. F_Complex = 0 by COMPLEX1:def 6, COMPLFLD:9;

definition

let A be Matrix of COMPLEX ;
func COMPLEX2Field A -> Matrix of F_Complex equals :: MATRIX_5:def 1
A;
coherence by COMPLFLD:def 1;

end;

:: deftheorem defines COMPLEX2Field MATRIX_5:def 1 :

definition

let A be Matrix of F_Complex ;
func Field2COMPLEX A -> Matrix of COMPLEX equals :: MATRIX_5:def 2
A;
coherence by COMPLFLD:def 1;

end;

:: deftheorem defines Field2COMPLEX MATRIX_5:def 2 :

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 ;

end;

:: deftheorem defines + MATRIX_5:def 3 :

definition

let A be Matrix of COMPLEX ;
func - A -> Matrix of COMPLEX equals :: MATRIX_5:def 4
Field2COMPLEX (- (COMPLEX2Field A));
coherence ;

end;

:: deftheorem defines - MATRIX_5:def 4 :

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 ;
func A * B -> Matrix of COMPLEX equals :: MATRIX_5:def 6
Field2COMPLEX ((COMPLEX2Field A) * (COMPLEX2Field B));
coherence ;

end;

:: deftheorem defines - MATRIX_5:def 5 :

:: deftheorem defines * MATRIX_5:def 6 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines * MATRIX_5:def 7 :

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 :: MATRIX_5:9

for M being Matrix of COMPLEX st len M > 0 holds
- (- M) = M by MATRIX_4:1;

theorem Th10: :: MATRIX_5:10

for K being Field
for M being Matrix of K holds (1. K) * M = M

proof end;

theorem :: MATRIX_5:11

for M being Matrix of COMPLEX holds 1 * M = M

proof end;

theorem :: 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 * b) * M

proof end;

theorem Th13: :: MATRIX_5:13

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:14

for M being Matrix of COMPLEX holds M + M = 2 * M

proof end;

theorem :: MATRIX_5:15

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 ;

end;

:: deftheorem defines 0_Cx MATRIX_5:def 8 :

theorem :: MATRIX_5:16

for n, m being Nat holds COMPLEX2Field (0_Cx n,m) = 0. F_Complex ,n,m ;

theorem :: MATRIX_5:17

for M being Matrix of COMPLEX st len M > 0 holds
M + (- M) = 0_Cx (len M),(width M) by MATRIX_4:2;

theorem :: MATRIX_5:18

for M being Matrix of COMPLEX st len M > 0 holds
M - M = 0_Cx (len M),(width M) by MATRIX_4:3;

theorem :: MATRIX_5:19

for M1, M2, M3 being Matrix of COMPLEX st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & len M1 > 0 & M1 + M3 = M2 + M3 holds
M1 = M2 by MATRIX_4:4;

theorem :: MATRIX_5:20

for M1, M2 being Matrix of COMPLEX st len M2 > 0 holds
M1 - (- M2) = M1 + M2 by MATRIX_4:1;

theorem :: MATRIX_5:21

for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & len M1 > 0 & M1 = M1 + M2 holds
M2 = 0_Cx (len M1),(width M1)

proof end;

theorem :: MATRIX_5:22

for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & len M1 > 0 & M1 - M2 = 0_Cx (len M1),(width M1) holds
M1 = M2 by MATRIX_4:7;

theorem :: MATRIX_5:23

for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & len M1 > 0 & M1 + M2 = 0_Cx (len M1),(width M1) holds
M2 = - M1

proof end;

theorem :: MATRIX_5:24

for n, m being Nat st n > 0 holds
- (0_Cx n,m) = 0_Cx n,m by MATRIX_4:9;

theorem :: MATRIX_5:25

for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & len M1 > 0 & M2 - M1 = M2 holds
M1 = 0_Cx (len M1),(width M1)

proof end;

theorem :: MATRIX_5:26

for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & len M1 > 0 holds
M1 = M1 - (M2 - M2) by MATRIX_4:11;

theorem :: MATRIX_5:27

for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & len M1 > 0 holds
- (M1 + M2) = (- M1) + (- M2) by MATRIX_4:12;

theorem :: MATRIX_5:28

for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & len M1 > 0 holds
M1 - (M1 - M2) = M2 by MATRIX_4:13;

theorem :: MATRIX_5:29

for M1, M2, M3 being Matrix of COMPLEX st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & len M1 > 0 & M1 - M3 = M2 - M3 holds
M1 = M2 by MATRIX_4:14;

theorem :: MATRIX_5:30

for M1, M2, M3 being Matrix of COMPLEX st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & len M1 > 0 & M3 - M1 = M3 - M2 holds
M1 = M2 by MATRIX_4:15;

theorem :: MATRIX_5:31

for M1, M2, M3 being Matrix of COMPLEX st len M2 = len M3 & width M2 = width M3 & width M1 = len M2 & len M1 > 0 & len M2 > 0 holds
M1 * (M2 + M3) = (M1 * M2) + (M1 * M3) by MATRIX_4:62;

theorem :: MATRIX_5:32

for M1, M2, M3 being Matrix of COMPLEX st len M2 = len M3 & width M2 = width M3 & len M1 = width M2 & len M2 > 0 & len M1 > 0 holds
(M2 + M3) * M1 = (M2 * M1) + (M3 * M1) by MATRIX_4:63;

theorem :: MATRIX_5:33

for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 holds
M1 + M2 = M2 + M1 by MATRIX_3:4;

theorem :: MATRIX_5:34

for M1, M2, M3 being Matrix of COMPLEX st len M1 = len M2 & len M1 = len M3 & width M1 = width M2 & width M1 = width M3 holds
(M1 + M2) + M3 = M1 + (M2 + M3) by MATRIX_3:5;

theorem :: MATRIX_5:35

for M being Matrix of COMPLEX st len M > 0 holds
M + (0_Cx (len M),(width M)) = M

proof end;

theorem Th36: :: MATRIX_5:36

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 & len M1 > 0 holds
b * (M1 + M2) = (b * M1) + (b * M2)

proof end;

theorem :: MATRIX_5:37

for M1, M2 being Matrix of COMPLEX
for a being complex number st len M1 = len M2 & width M1 = width M2 & len M1 > 0 holds
a * (M1 + M2) = (a * M1) + (a * M2)

proof end;

theorem Th38: :: MATRIX_5:38

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:39

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 Th40: :: MATRIX_5:40

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:41

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 FinSequence of COMPLEX ;
let k be set ;
:: original: .
redefine func s . k -> Element of COMPLEX ;
coherence

proof end;

end;

theorem :: MATRIX_5:42

for i, j being Nat
for M1, M2 being Matrix of COMPLEX st len M1 > 0 & len M2 > 0 & width M1 = len M2 & 1 <= i & i <= len M1 & 1 <= j & j <= width M2 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;