:: MATRIX_5 semantic presentation

theorem Th1: :: MATRIX_5:1

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

theorem Th2: :: MATRIX_5:2

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

definition

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

end;

:: deftheorem Def1 defines COMPLEX2Field MATRIX_5:def 1 :

definition

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

end;

:: deftheorem Def2 defines Field2COMPLEX MATRIX_5:def 2 :

theorem Th3: :: MATRIX_5:3

for b₁, b₂ being Matrix of COMPLEX st COMPLEX2Field b₁ = COMPLEX2Field b₂ holds
b₁ = b₂ ;

theorem Th4: :: MATRIX_5:4

for b₁, b₂ being Matrix of F_Complex st Field2COMPLEX b₁ = Field2COMPLEX b₂ holds
b₁ = b₂ ;

theorem Th5: :: MATRIX_5:5

for b₁ being Matrix of COMPLEX holds b₁ = Field2COMPLEX (COMPLEX2Field b₁) ;

theorem Th6: :: MATRIX_5:6

for b₁ being Matrix of F_Complex holds b₁ = COMPLEX2Field (Field2COMPLEX b₁) ;

definition

let c₁, c₂ be Matrix of COMPLEX ;
func c₁ + c₂ -> Matrix of COMPLEX equals :: MATRIX_5:def 3
Field2COMPLEX ((COMPLEX2Field a₁) + (COMPLEX2Field a₂));
coherence ;

end;

:: deftheorem Def3 defines + MATRIX_5:def 3 :

definition

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

end;

:: deftheorem Def4 defines - MATRIX_5:def 4 :

definition

let c₁, c₂ be Matrix of COMPLEX ;
func c₁ - c₂ -> Matrix of COMPLEX equals :: MATRIX_5:def 5
Field2COMPLEX ((COMPLEX2Field a₁) - (COMPLEX2Field a₂));
coherence ;
func c₁ * c₂ -> Matrix of COMPLEX equals :: MATRIX_5:def 6
Field2COMPLEX ((COMPLEX2Field a₁) * (COMPLEX2Field a₂));
coherence ;

end;

:: deftheorem Def5 defines - MATRIX_5:def 5 :

:: deftheorem Def6 defines * MATRIX_5:def 6 :

definition

let c₁ be complex number ;
let c₂ be Matrix of COMPLEX ;
func c₁ * c₂ -> Matrix of COMPLEX means :Def7: :: MATRIX_5:def 7
for b₁ being Element of F_Complex st b₁ = a₁ holds
a₃ = Field2COMPLEX (b₁ * (COMPLEX2Field a₂));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines * MATRIX_5:def 7 :

theorem Th7: :: MATRIX_5:7

for b₁ being Matrix of COMPLEX holds
( len b₁ = len (COMPLEX2Field b₁) & width b₁ = width (COMPLEX2Field b₁) ) ;

theorem Th8: :: MATRIX_5:8

for b₁ being Matrix of F_Complex holds
( len b₁ = len (Field2COMPLEX b₁) & width b₁ = width (Field2COMPLEX b₁) ) ;

theorem Th9: :: MATRIX_5:9

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

theorem Th10: :: MATRIX_5:10

for b₁ being Field
for b₂ being Matrix of b₁ holds (1. b₁) * b₂ = b₂

proof end;

theorem Th11: :: MATRIX_5:11

for b₁ being Matrix of COMPLEX holds 1 * b₁ = b₁

proof end;

theorem Th12: :: MATRIX_5:12

for b₁ being Field
for b₂, b₃ being Element of b₁
for b₄ being Matrix of b₁ holds b₂ * (b₃ * b₄) = (b₂ * b₃) * b₄

proof end;

theorem Th13: :: MATRIX_5:13

for b₁ being Field
for b₂, b₃ being Element of b₁
for b₄ being Matrix of b₁ holds (b₂ + b₃) * b₄ = (b₂ * b₄) + (b₃ * b₄)

proof end;

theorem Th14: :: MATRIX_5:14

for b₁ being Matrix of COMPLEX holds b₁ + b₁ = 2 * b₁

proof end;

theorem Th15: :: MATRIX_5:15

for b₁ being Matrix of COMPLEX holds (b₁ + b₁) + b₁ = 3 * b₁

proof end;

definition

let c₁, c₂ be Nat;
func 0_Cx c₁,c₂ -> Matrix of COMPLEX equals :: MATRIX_5:def 8
Field2COMPLEX (0. F_Complex ,a₁,a₂);
coherence ;

end;

:: deftheorem Def8 defines 0_Cx MATRIX_5:def 8 :

theorem Th16: :: MATRIX_5:16

for b₁, b₂ being Nat holds COMPLEX2Field (0_Cx b₁,b₂) = 0. F_Complex ,b₁,b₂ ;

theorem Th17: :: MATRIX_5:17

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

theorem Th18: :: MATRIX_5:18

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

theorem Th19: :: MATRIX_5:19

for b₁, b₂, b₃ being Matrix of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ & width b₁ = width b₂ & width b₂ = width b₃ & len b₁ > 0 & b₁ + b₃ = b₂ + b₃ holds
b₁ = b₂ by MATRIX_4:4;

theorem Th20: :: MATRIX_5:20

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

theorem Th21: :: MATRIX_5:21

for b₁, b₂ being Matrix of COMPLEX st len b₁ = len b₂ & width b₁ = width b₂ & len b₁ > 0 & b₁ = b₁ + b₂ holds
b₂ = 0_Cx (len b₁),(width b₁)

proof end;

theorem Th22: :: MATRIX_5:22

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

theorem Th23: :: MATRIX_5:23

for b₁, b₂ being Matrix of COMPLEX st len b₁ = len b₂ & width b₁ = width b₂ & len b₁ > 0 & b₁ + b₂ = 0_Cx (len b₁),(width b₁) holds
b₂ = - b₁

proof end;

theorem Th24: :: MATRIX_5:24

for b₁, b₂ being Nat st b₁ > 0 holds
- (0_Cx b₁,b₂) = 0_Cx b₁,b₂ by MATRIX_4:9;

theorem Th25: :: MATRIX_5:25

for b₁, b₂ being Matrix of COMPLEX st len b₁ = len b₂ & width b₁ = width b₂ & len b₁ > 0 & b₂ - b₁ = b₂ holds
b₁ = 0_Cx (len b₁),(width b₁)

proof end;

theorem Th26: :: MATRIX_5:26

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

theorem Th27: :: MATRIX_5:27

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

theorem Th28: :: MATRIX_5:28

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

theorem Th29: :: MATRIX_5:29

for b₁, b₂, b₃ being Matrix of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ & width b₁ = width b₂ & width b₂ = width b₃ & len b₁ > 0 & b₁ - b₃ = b₂ - b₃ holds
b₁ = b₂ by MATRIX_4:14;

theorem Th30: :: MATRIX_5:30

for b₁, b₂, b₃ being Matrix of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ & width b₁ = width b₂ & width b₂ = width b₃ & len b₁ > 0 & b₃ - b₁ = b₃ - b₂ holds
b₁ = b₂ by MATRIX_4:15;

theorem Th31: :: MATRIX_5:31

for b₁, b₂, b₃ being Matrix of COMPLEX st len b₂ = len b₃ & width b₂ = width b₃ & width b₁ = len b₂ & len b₁ > 0 & len b₂ > 0 holds
b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃) by MATRIX_4:62;

theorem Th32: :: MATRIX_5:32

for b₁, b₂, b₃ being Matrix of COMPLEX st len b₂ = len b₃ & width b₂ = width b₃ & len b₁ = width b₂ & len b₂ > 0 & len b₁ > 0 holds
(b₂ + b₃) * b₁ = (b₂ * b₁) + (b₃ * b₁) by MATRIX_4:63;

theorem Th33: :: MATRIX_5:33

for b₁, b₂ being Matrix of COMPLEX st len b₁ = len b₂ & width b₁ = width b₂ holds
b₁ + b₂ = b₂ + b₁ by MATRIX_3:4;

theorem Th34: :: MATRIX_5:34

for b₁, b₂, b₃ being Matrix of COMPLEX st len b₁ = len b₂ & len b₁ = len b₃ & width b₁ = width b₂ & width b₁ = width b₃ holds
(b₁ + b₂) + b₃ = b₁ + (b₂ + b₃) by MATRIX_3:5;

theorem Th35: :: MATRIX_5:35

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

proof end;

theorem Th36: :: MATRIX_5:36

for b₁ being Field
for b₂ being Element of b₁
for b₃, b₄ being Matrix of b₁ st len b₃ = len b₄ & width b₃ = width b₄ & len b₃ > 0 holds
b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄)

proof end;

theorem Th37: :: MATRIX_5:37

for b₁, b₂ being Matrix of COMPLEX
for b₃ being complex number st len b₁ = len b₂ & width b₁ = width b₂ & len b₁ > 0 holds
b₃ * (b₁ + b₂) = (b₃ * b₁) + (b₃ * b₂)

proof end;

theorem Th38: :: MATRIX_5:38

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st width b₂ = len b₃ & len b₂ > 0 & len b₃ > 0 holds
(0. b₁,(len b₂),(width b₂)) * b₃ = 0. b₁,(len b₂),(width b₃)

proof end;

theorem Th39: :: MATRIX_5:39

for b₁, b₂ being Matrix of COMPLEX st width b₁ = len b₂ & len b₁ > 0 & len b₂ > 0 holds
(0_Cx (len b₁),(width b₁)) * b₂ = 0_Cx (len b₁),(width b₂)

proof end;

theorem Th40: :: MATRIX_5:40

for b₁ being Field
for b₂ being Matrix of b₁ st len b₂ > 0 holds
(0. b₁) * b₂ = 0. b₁,(len b₂),(width b₂)

proof end;

theorem Th41: :: MATRIX_5:41

for b₁ being Matrix of COMPLEX st len b₁ > 0 holds
0 * b₁ = 0_Cx (len b₁),(width b₁)

proof end;

definition

let c₁ be FinSequence of COMPLEX ;
let c₂ be set ;
redefine func . as c₁ . c₂ -> Element of COMPLEX ;
coherence

proof end;

end;

theorem Th42: :: MATRIX_5:42

for b₁, b₂ being Nat
for b₃, b₄ being Matrix of COMPLEX st len b₃ > 0 & len b₄ > 0 & width b₃ = len b₄ & 1 <= b₁ & b₁ <= len b₃ & 1 <= b₂ & b₂ <= width b₄ holds
ex b₅ being FinSequence of COMPLEX st
( len b₅ = len b₄ & b₅ . 1 = (b₃ * b₁,1) * (b₄ * 1,b₂) & ( for b₆ being Nat st 1 <= b₆ & b₆ < len b₄ holds
b₅ . (b₆ + 1) = (b₅ . b₆) + ((b₃ * b₁,(b₆ + 1)) * (b₄ * (b₆ + 1),b₂)) ) )

proof end;