:: MATRIXC1 semantic presentation

definition

let c₁ be Matrix of COMPLEX ;
func c₁ *' -> Matrix of COMPLEX means :Def1: :: MATRIXC1:def 1
( len a₂ = len a₁ & width a₂ = width a₁ & ( for b₁, b₂ being Nat st [b₁,b₂] in Indices a₁ holds
a₂ * b₁,b₂ = (a₁ * b₁,b₂) *' ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines *' MATRIXC1:def 1 :

theorem Th1: :: MATRIXC1:1

for b₁, b₂ being Nat
for b₃ being Matrix of COMPLEX holds
( [b₁,b₂] in Indices b₃ iff ( 1 <= b₁ & b₁ <= len b₃ & 1 <= b₂ & b₂ <= width b₃ ) )

proof end;

theorem Th2: :: MATRIXC1:2

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

proof end;

theorem Th3: :: MATRIXC1:3

for b₁ being complex number
for b₂ being Matrix of COMPLEX holds
( len (b₁ * b₂) = len b₂ & width (b₁ * b₂) = width b₂ )

proof end;

theorem Th4: :: MATRIXC1:4

for b₁, b₂ being Nat
for b₃ being complex number
for b₄ being Matrix of COMPLEX st len (b₃ * b₄) = len b₄ & width (b₃ * b₄) = width b₄ & [b₁,b₂] in Indices b₄ holds
(b₃ * b₄) * b₁,b₂ = b₃ * (b₄ * b₁,b₂)

proof end;

theorem Th5: :: MATRIXC1:5

for b₁ being complex number
for b₂ being Matrix of COMPLEX holds (b₁ * b₂) *' = (b₁ *' ) * (b₂ *' )

proof end;

theorem Th6: :: MATRIXC1:6

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

proof end;

theorem Th7: :: MATRIXC1:7

for b₁, b₂ being Nat
for b₃, b₄ being Matrix of COMPLEX st len b₃ = len b₄ & width b₃ = width b₄ & [b₁,b₂] in Indices b₃ holds
(b₃ + b₄) * b₁,b₂ = (b₃ * b₁,b₂) + (b₄ * b₁,b₂)

proof end;

theorem Th8: :: MATRIXC1:8

for b₁, b₂ being Matrix of COMPLEX st len b₁ = len b₂ & width b₁ = width b₂ holds
(b₁ + b₂) *' = (b₁ *' ) + (b₂ *' )

proof end;

theorem Th9: :: MATRIXC1:9

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

proof end;

theorem Th10: :: MATRIXC1:10

for b₁, b₂ being Nat
for b₃ being Matrix of COMPLEX st len (- b₃) = len b₃ & width (- b₃) = width b₃ & [b₁,b₂] in Indices b₃ holds
(- b₃) * b₁,b₂ = - (b₃ * b₁,b₂)

proof end;

theorem Th11: :: MATRIXC1:11

for b₁ being Matrix of COMPLEX holds (- 1) * b₁ = - b₁

proof end;

theorem Th12: :: MATRIXC1:12

for b₁ being Matrix of COMPLEX holds (- b₁) *' = - (b₁ *' )

proof end;

theorem Th13: :: MATRIXC1:13

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

proof end;

theorem Th14: :: MATRIXC1:14

for b₁, b₂ being Nat
for b₃, b₄ being Matrix of COMPLEX st len b₃ = len b₄ & width b₃ = width b₄ & [b₁,b₂] in Indices b₃ holds
(b₃ - b₄) * b₁,b₂ = (b₃ * b₁,b₂) - (b₄ * b₁,b₂)

proof end;

theorem Th15: :: MATRIXC1:15

for b₁, b₂ being Matrix of COMPLEX st len b₁ = len b₂ & width b₁ = width b₂ holds
(b₁ - b₂) *' = (b₁ *' ) - (b₂ *' )

proof end;

definition

let c₁ be Matrix of COMPLEX ;
func c₁ @" -> Matrix of COMPLEX equals :: MATRIXC1:def 2
(a₁ @ ) *' ;
coherence ;

end;

:: deftheorem Def2 defines @" MATRIXC1:def 2 :

definition

let c₁ be FinSequence of COMPLEX ;
assume E14: len c₁ > 0 ;
func FinSeq2Matrix c₁ -> Matrix of COMPLEX means :: MATRIXC1:def 3
( len a₂ = len a₁ & width a₂ = 1 & ( for b₁ being Nat st b₁ in Seg (len a₁) holds
a₂ . b₁ = <*(a₁ . b₁)*> ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines FinSeq2Matrix MATRIXC1:def 3 :

definition

let c₁ be Matrix of COMPLEX ;
func Matrix2FinSeq c₁ -> FinSequence of COMPLEX equals :: MATRIXC1:def 4
Col a₁,1;
coherence ;

end;

:: deftheorem Def4 defines Matrix2FinSeq MATRIXC1:def 4 :

definition

let c₁, c₂ be FinSequence of COMPLEX ;
func mlt c₁,c₂ -> FinSequence of COMPLEX equals :: MATRIXC1:def 5
multcomplex .: a₁,a₂;
coherence ;
commutativity

proof end;

end;

:: deftheorem Def5 defines mlt MATRIXC1:def 5 :

definition

let c₁ be FinSequence of COMPLEX ;
func Sum c₁ -> Element of COMPLEX equals :: MATRIXC1:def 6
addcomplex $$ a₁;
coherence ;

end;

:: deftheorem Def6 defines Sum MATRIXC1:def 6 :

definition

let c₁ be Matrix of COMPLEX ;
let c₂ be FinSequence of COMPLEX ;
func c₁ * c₂ -> FinSequence of COMPLEX means :Def7: :: MATRIXC1:def 7
( len a₃ = len a₁ & ( for b₁ being Nat st b₁ in Seg (len a₁) holds
a₃ . b₁ = Sum (mlt (Line a₁,b₁),a₂) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines * MATRIXC1:def 7 :

Lemma15: for b₁ being Element of COMPLEX
for b₂ being FinSequence of COMPLEX holds b₁ * b₂ = (multcomplex [;] b₁,(id COMPLEX )) * b₂

proof end;

theorem Th16: :: MATRIXC1:16

for b₁ being Nat
for b₂ being Element of COMPLEX
for b₃, b₄ being Element of b₁ -tuples_on COMPLEX holds b₂ * (mlt b₃,b₄) = mlt (b₂ * b₃),b₄

proof end;

definition

let c₁ be Matrix of COMPLEX ;
let c₂ be complex number ;
func c₁ * c₂ -> Matrix of COMPLEX equals :: MATRIXC1:def 8
a₂ * a₁;
coherence ;

end;

:: deftheorem Def8 defines * MATRIXC1:def 8 :

theorem Th17: :: MATRIXC1:17

for b₁ being Element of COMPLEX
for b₂ being Matrix of COMPLEX holds (b₂ * b₁) *' = (b₁ *' ) * (b₂ *' ) by Th5;

theorem Th18: :: MATRIXC1:18

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
( len (mlt b₁,b₂) = len b₁ & len (mlt b₁,b₂) = len b₂ ) by FINSEQ_2:86;

theorem Th19: :: MATRIXC1:19

for b₁, b₂ being FinSequence of COMPLEX
for b₃ being Nat st b₃ in dom (mlt b₁,b₂) holds
(mlt b₁,b₂) . b₃ = (b₁ . b₃) * (b₂ . b₃)

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of c₁ -tuples_on COMPLEX ;
redefine func mlt as mlt c₂,c₃ -> Element of a₁ -tuples_on COMPLEX ;
coherence by FINSEQ_2:140;

end;

theorem Th20: :: MATRIXC1:20

for b₁, b₂ being Nat
for b₃, b₄ being Element of b₁ -tuples_on COMPLEX holds (mlt b₃,b₄) . b₂ = (b₃ . b₂) * (b₄ . b₂)

proof end;

theorem Th21: :: MATRIXC1:21

for b₁, b₂ being Element of COMPLEX holds (addcomplex . b₁,(b₂ *' )) *' = addcomplex . (b₁ *' ),b₂

proof end;

theorem Th22: :: MATRIXC1:22

for b₁ being FinSequence of COMPLEX ex b₂ being Function of NAT , COMPLEX st
for b₃ being Nat st 1 <= b₃ & b₃ <= len b₁ holds
b₂ . b₃ = b₁ . b₃

proof end;

theorem Th23: :: MATRIXC1:23

for b₁ being FinSequence of COMPLEX st len (b₁ *' ) >= 1 holds
addcomplex $$ (b₁ *' ) = (addcomplex $$ b₁) *'

proof end;

theorem Th24: :: MATRIXC1:24

for b₁ being FinSequence of COMPLEX st len b₁ >= 1 holds
Sum (b₁ *' ) = (Sum b₁) *'

proof end;

theorem Th25: :: MATRIXC1:25

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
(mlt b₁,(b₂ *' )) *' = mlt b₂,(b₁ *' )

proof end;

theorem Th26: :: MATRIXC1:26

for b₁, b₂ being FinSequence of COMPLEX
for b₃ being Element of COMPLEX st len b₁ = len b₂ holds
mlt b₁,(b₃ * b₂) = b₃ * (mlt b₁,b₂)

proof end;

theorem Th27: :: MATRIXC1:27

for b₁, b₂ being FinSequence of COMPLEX
for b₃ being Element of COMPLEX st len b₁ = len b₂ holds
mlt (b₃ * b₁),b₂ = b₃ * (mlt b₁,b₂)

proof end;

theorem Th28: :: MATRIXC1:28

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
(mlt b₁,b₂) *' = mlt (b₁ *' ),(b₂ *' )

proof end;

Lemma28: for b₁, b₂ being Element of COMPLEX holds (multcomplex [;] b₁,(id COMPLEX )) . b₂ = b₁ * b₂

proof end;

theorem Th29: :: MATRIXC1:29

for b₁ being FinSequence of COMPLEX
for b₂ being Element of COMPLEX holds Sum (b₂ * b₁) = b₂ * (Sum b₁)

proof end;

definition

let c₁ be FinSequence of REAL ;
func FR2FC c₁ -> FinSequence of COMPLEX equals :: MATRIXC1:def 9
a₁;
coherence

proof end;

end;

:: deftheorem Def9 defines FR2FC MATRIXC1:def 9 :

theorem Th30: :: MATRIXC1:30

for b₁ being FinSequence of REAL
for b₂ being FinSequence of COMPLEX st b₁ = b₂ & len b₁ >= 1 holds
addreal $$ b₁ = addcomplex $$ b₂

proof end;

theorem Th31: :: MATRIXC1:31

for b₁ being FinSequence of REAL
for b₂ being FinSequence of COMPLEX st b₁ = b₂ & len b₁ >= 1 holds
Sum b₁ = Sum b₂

proof end;

theorem Th32: :: MATRIXC1:32

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
Sum (b₁ - b₂) = (Sum b₁) - (Sum b₂)

proof end;

theorem Th33: :: MATRIXC1:33

for b₁, b₂ being FinSequence of COMPLEX
for b₃ being Nat st b₃ in dom (b₁ + b₂) holds
(b₁ + b₂) . b₃ = (b₁ . b₃) + (b₂ . b₃)

proof end;

theorem Th34: :: MATRIXC1:34

for b₁, b₂ being FinSequence of COMPLEX
for b₃ being Nat st b₃ in dom (b₁ - b₂) holds
(b₁ - b₂) . b₃ = (b₁ . b₃) - (b₂ . b₃)

proof end;

theorem Th35: :: MATRIXC1:35

for b₁, b₂, b₃ being FinSequence of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ holds
mlt (b₁ - b₂),b₃ = (mlt b₁,b₃) - (mlt b₂,b₃)

proof end;

theorem Th36: :: MATRIXC1:36

for b₁, b₂, b₃ being FinSequence of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ holds
mlt b₁,(b₂ - b₃) = (mlt b₁,b₂) - (mlt b₁,b₃)

proof end;

theorem Th37: :: MATRIXC1:37

for b₁, b₂, b₃ being FinSequence of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ holds
mlt b₁,(b₂ + b₃) = (mlt b₁,b₂) + (mlt b₁,b₃)

proof end;

theorem Th38: :: MATRIXC1:38

for b₁, b₂, b₃ being FinSequence of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ holds
mlt (b₁ + b₂),b₃ = (mlt b₁,b₃) + (mlt b₂,b₃)

proof end;

theorem Th39: :: MATRIXC1:39

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
Sum (b₁ + b₂) = (Sum b₁) + (Sum b₂)

proof end;

theorem Th40: :: MATRIXC1:40

for b₁, b₂ being FinSequence of COMPLEX
for b₃, b₄ being FinSequence of REAL st b₁ = b₃ & b₂ = b₄ & len b₁ = len b₄ holds
multcomplex .: b₁,b₂ = multreal .: b₃,b₄

proof end;

theorem Th41: :: MATRIXC1:41

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ holds
FR2FC (mlt b₁,b₂) = mlt (FR2FC b₁),(FR2FC b₂)

proof end;

theorem Th42: :: MATRIXC1:42

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ & len b₁ > 0 holds
|(b₁,b₂)| = Sum (mlt b₁,(b₂ *' ))

proof end;

theorem Th43: :: MATRIXC1:43

for b₁, b₂ being Matrix of COMPLEX st len b₁ = len b₂ & width b₁ = width b₂ holds
Indices b₁ = Indices b₂

proof end;

theorem Th44: :: MATRIXC1:44

for b₁, b₂ being Nat
for b₃, b₄ being Matrix of COMPLEX st len b₃ = len b₄ & width b₃ = width b₄ & b₂ in Seg (len b₃) holds
Line (b₃ + b₄),b₂ = (Line b₃,b₂) + (Line b₄,b₂)

proof end;

theorem Th45: :: MATRIXC1:45

for b₁ being Nat
for b₂ being Matrix of COMPLEX st b₁ in Seg (len b₂) holds
Line b₂,b₁ = (Line (b₂ *' ),b₁) *'

proof end;

theorem Th46: :: MATRIXC1:46

for b₁ being Nat
for b₂ being FinSequence of COMPLEX
for b₃ being Matrix of COMPLEX st len b₂ = width b₃ holds
mlt b₂,((Line (b₃ *' ),b₁) *' ) = (mlt (Line (b₃ *' ),b₁),(b₂ *' )) *'

proof end;

theorem Th47: :: MATRIXC1:47

for b₁ being FinSequence of COMPLEX
for b₂ being Matrix of COMPLEX st len b₁ = width b₂ & len b₁ >= 1 holds
(b₂ * b₁) *' = (b₂ *' ) * (b₁ *' )

proof end;

theorem Th48: :: MATRIXC1:48

for b₁, b₂, b₃ being FinSequence of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ holds
mlt b₁,(mlt b₂,b₃) = mlt (mlt b₁,b₂),b₃

proof end;

theorem Th49: :: MATRIXC1:49

for b₁ being FinSequence of COMPLEX holds Sum (- b₁) = - (Sum b₁)

proof end;

theorem Th50: :: MATRIXC1:50

for b₁ being Element of COMPLEX holds Sum <*b₁*> = b₁ by FINSOP_1:12;

theorem Th51: :: MATRIXC1:51

for b₁, b₂ being FinSequence of COMPLEX holds Sum (b₁ ^ b₂) = (Sum b₁) + (Sum b₂)

proof end;

definition

let c₁ be Matrix of COMPLEX ;
func LineSum c₁ -> FinSequence of COMPLEX means :Def10: :: MATRIXC1:def 10
( len a₂ = len a₁ & ( for b₁ being Nat st b₁ in Seg (len a₁) holds
a₂ . b₁ = Sum (Line a₁,b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines LineSum MATRIXC1:def 10 :

definition

let c₁ be Matrix of COMPLEX ;
func ColSum c₁ -> FinSequence of COMPLEX means :Def11: :: MATRIXC1:def 11
( len a₂ = width a₁ & ( for b₁ being Nat st b₁ in Seg (width a₁) holds
a₂ . b₁ = Sum (Col a₁,b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines ColSum MATRIXC1:def 11 :

theorem Th52: :: MATRIXC1:52

for b₁ being FinSequence of COMPLEX st len b₁ = 1 holds
Sum b₁ = b₁ . 1

proof end;

theorem Th53: :: MATRIXC1:53

for b₁, b₂ being FinSequence of COMPLEX
for b₃ being Nat st len b₁ = b₃ + 1 & b₂ = b₁ | b₃ holds
Sum b₁ = (Sum b₂) + (b₁ /. (len b₁))

proof end;

theorem Th54: :: MATRIXC1:54

for b₁ being Matrix of COMPLEX st len b₁ > 0 holds
Sum (LineSum b₁) = Sum (ColSum b₁)

proof end;

definition

let c₁ be Matrix of COMPLEX ;
func SumAll c₁ -> Element of COMPLEX equals :: MATRIXC1:def 12
Sum (LineSum a₁);
coherence ;

end;

:: deftheorem Def12 defines SumAll MATRIXC1:def 12 :

theorem Th55: :: MATRIXC1:55

for b₁ being Matrix of COMPLEX holds ColSum b₁ = LineSum (b₁ @ )

proof end;

theorem Th56: :: MATRIXC1:56

for b₁ being Matrix of COMPLEX st len b₁ > 0 holds
SumAll b₁ = SumAll (b₁ @ )

proof end;

definition

let c₁, c₂ be FinSequence of COMPLEX ;
let c₃ be Matrix of COMPLEX ;
assume E53: ( len c₁ = len c₃ & len c₂ = width c₃ ) ;
func QuadraticForm c₁,c₃,c₂ -> Matrix of COMPLEX means :Def13: :: MATRIXC1:def 13
( len a₄ = len a₁ & width a₄ = len a₂ & ( for b₁, b₂ being Nat st [b₁,b₂] in Indices a₃ holds
a₄ * b₁,b₂ = ((a₁ . b₁) * (a₃ * b₁,b₂)) * ((a₂ . b₂) *' ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines QuadraticForm MATRIXC1:def 13 :

theorem Th57: :: MATRIXC1:57

for b₁, b₂ being FinSequence of COMPLEX
for b₃ being Matrix of COMPLEX st len b₁ = len b₃ & len b₂ = width b₃ & len b₁ > 0 & len b₂ > 0 holds
(QuadraticForm b₁,b₃,b₂) @ = (QuadraticForm b₂,(b₃ @" ),b₁) *'

proof end;

theorem Th58: :: MATRIXC1:58

for b₁, b₂ being FinSequence of COMPLEX
for b₃ being Matrix of COMPLEX st len b₁ = len b₃ & len b₂ = width b₃ holds
(QuadraticForm b₁,b₃,b₂) *' = QuadraticForm (b₁ *' ),(b₃ *' ),(b₂ *' )

proof end;

theorem Th59: :: MATRIXC1:59

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ & 0 < len b₂ holds
|(b₁,b₂)| = |(b₂,b₁)| *'

proof end;

theorem Th60: :: MATRIXC1:60

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ & 0 < len b₂ holds
|(b₁,b₂)| *' = |((b₁ *' ),(b₂ *' ))|

proof end;

theorem Th61: :: MATRIXC1:61

for b₁ being Matrix of COMPLEX st width b₁ > 0 holds
(b₁ @ ) *' = (b₁ *' ) @

proof end;

theorem Th62: :: MATRIXC1:62

for b₁, b₂ being FinSequence of COMPLEX
for b₃ being Matrix of COMPLEX st len b₁ = width b₃ & len b₂ = len b₃ & len b₁ > 0 & len b₂ > 0 holds
|(b₁,((b₃ @" ) * b₂))| = SumAll (QuadraticForm b₁,(b₃ @ ),b₂)

proof end;

theorem Th63: :: MATRIXC1:63

for b₁, b₂ being FinSequence of COMPLEX
for b₃ being Matrix of COMPLEX st len b₂ = len b₃ & len b₁ = width b₃ & len b₁ > 0 & len b₂ > 0 & len b₃ > 0 holds
|((b₃ * b₁),b₂)| = SumAll (QuadraticForm b₁,(b₃ @ ),b₂)

proof end;

theorem Th64: :: MATRIXC1:64

for b₁, b₂ being FinSequence of COMPLEX
for b₃ being Matrix of COMPLEX st len b₁ = width b₃ & len b₂ = len b₃ & width b₃ > 0 & len b₃ > 0 holds
|((b₃ * b₁),b₂)| = |(b₁,((b₃ @" ) * b₂))|

proof end;

theorem Th65: :: MATRIXC1:65

for b₁, b₂ being FinSequence of COMPLEX
for b₃ being Matrix of COMPLEX st len b₁ = len b₃ & len b₂ = width b₃ & width b₃ > 0 & len b₃ > 0 & len b₁ > 0 holds
|(b₁,(b₃ * b₂))| = |(((b₃ @" ) * b₁),b₂)|

proof end;