:: MATRIXC1 semantic presentation

definition

let M be Matrix of COMPLEX ;
func M *' -> Matrix of COMPLEX means :Def1: :: MATRIXC1:def 1
( len it = len M & width it = width M & ( for i, j being Nat st [i,j] in Indices M holds
it * i,j = (M * i,j) *' ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th1: :: MATRIXC1:1

for i, j being Nat
for M being Matrix of COMPLEX holds
( [i,j] in Indices M iff ( 1 <= i & i <= len M & 1 <= j & j <= width M ) )

proof end;

theorem Th2: :: MATRIXC1:2

for M being Matrix of COMPLEX holds (M *' ) *' = M

proof end;

theorem Th3: :: MATRIXC1:3

for a being complex number
for M being Matrix of COMPLEX holds
( len (a * M) = len M & width (a * M) = width M )

proof end;

theorem Th4: :: MATRIXC1:4

for i, j being Nat
for a being complex number
for M being Matrix of COMPLEX st len (a * M) = len M & width (a * M) = width M & [i,j] in Indices M holds
(a * M) * i,j = a * (M * i,j)

proof end;

theorem Th5: :: MATRIXC1:5

for a being complex number
for M being Matrix of COMPLEX holds (a * M) *' = (a *' ) * (M *' )

proof end;

theorem Th6: :: MATRIXC1:6

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

proof end;

theorem Th7: :: MATRIXC1:7

for i, j being Nat
for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & [i,j] in Indices M1 holds
(M1 + M2) * i,j = (M1 * i,j) + (M2 * i,j)

proof end;

theorem :: MATRIXC1:8

for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 holds
(M1 + M2) *' = (M1 *' ) + (M2 *' )

proof end;

theorem Th9: :: MATRIXC1:9

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

proof end;

theorem Th10: :: MATRIXC1:10

for i, j being Nat
for M being Matrix of COMPLEX st len (- M) = len M & width (- M) = width M & [i,j] in Indices M holds
(- M) * i,j = - (M * i,j)

proof end;

theorem Th11: :: MATRIXC1:11

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

proof end;

theorem :: MATRIXC1:12

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

proof end;

theorem Th13: :: MATRIXC1:13

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

proof end;

theorem Th14: :: MATRIXC1:14

for i, j being Nat
for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & [i,j] in Indices M1 holds
(M1 - M2) * i,j = (M1 * i,j) - (M2 * i,j)

proof end;

theorem :: MATRIXC1:15

for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 holds
(M1 - M2) *' = (M1 *' ) - (M2 *' )

proof end;

definition

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

end;

:: deftheorem defines @" MATRIXC1:def 2 :

definition

let x be FinSequence of COMPLEX ;
assume A1: len x > 0 ;
func FinSeq2Matrix x -> Matrix of COMPLEX means :: MATRIXC1:def 3
( len it = len x & width it = 1 & ( for j being Nat st j in Seg (len x) holds
it . j = <*(x . j)*> ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines FinSeq2Matrix MATRIXC1:def 3 :

definition

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

end;

:: deftheorem defines Matrix2FinSeq MATRIXC1:def 4 :

definition

let F1, F2 be FinSequence of COMPLEX ;
func mlt F1,F2 -> FinSequence of COMPLEX equals :: MATRIXC1:def 5
multcomplex .: F1,F2;
coherence ;
commutativity

proof end;

end;

:: deftheorem defines mlt MATRIXC1:def 5 :

definition

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

end;

:: deftheorem defines Sum MATRIXC1:def 6 :

definition

let M be Matrix of COMPLEX ;
let F be FinSequence of COMPLEX ;
func M * F -> FinSequence of COMPLEX means :Def7: :: MATRIXC1:def 7
( len it = len M & ( for i being Nat st i in Seg (len M) holds
it . i = Sum (mlt (Line M,i),F) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines * MATRIXC1:def 7 :

Lm1: for a being Element of COMPLEX
for F being FinSequence of COMPLEX holds a * F = (multcomplex [;] a,(id COMPLEX )) * F

proof end;

theorem Th16: :: MATRIXC1:16

for i being Nat
for a being Element of COMPLEX
for R1, R2 being Element of i -tuples_on COMPLEX holds a * (mlt R1,R2) = mlt (a * R1),R2

proof end;

definition

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

end;

:: deftheorem defines * MATRIXC1:def 8 :

theorem :: MATRIXC1:17

for a being Element of COMPLEX
for M being Matrix of COMPLEX holds (M * a) *' = (a *' ) * (M *' ) by Th5;

theorem Th18: :: MATRIXC1:18

for x, y being FinSequence of COMPLEX st len x = len y holds
( len (mlt x,y) = len x & len (mlt x,y) = len y ) by FINSEQ_2:86;

theorem Th19: :: MATRIXC1:19

for F1, F2 being FinSequence of COMPLEX
for i being Nat st i in dom (mlt F1,F2) holds
(mlt F1,F2) . i = (F1 . i) * (F2 . i)

proof end;

definition

let i be Nat;
let R1, R2 be Element of i -tuples_on COMPLEX ;
:: original: mlt
redefine func mlt R1,R2 -> Element of i -tuples_on COMPLEX ;
coherence by FINSEQ_2:140;

end;

theorem Th20: :: MATRIXC1:20

for i, j being Nat
for R1, R2 being Element of i -tuples_on COMPLEX holds (mlt R1,R2) . j = (R1 . j) * (R2 . j)

proof end;

theorem Th21: :: MATRIXC1:21

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

proof end;

theorem Th22: :: MATRIXC1:22

for F being FinSequence of COMPLEX ex G being Function of NAT , COMPLEX st
for n being Nat st 1 <= n & n <= len F holds
G . n = F . n

proof end;

theorem Th23: :: MATRIXC1:23

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

proof end;

theorem Th24: :: MATRIXC1:24

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

proof end;

theorem Th25: :: MATRIXC1:25

for x, y being FinSequence of COMPLEX st len x = len y holds
(mlt x,(y *' )) *' = mlt y,(x *' )

proof end;

theorem Th26: :: MATRIXC1:26

for x, y being FinSequence of COMPLEX
for a being Element of COMPLEX st len x = len y holds
mlt x,(a * y) = a * (mlt x,y)

proof end;

theorem Th27: :: MATRIXC1:27

for x, y being FinSequence of COMPLEX
for a being Element of COMPLEX st len x = len y holds
mlt (a * x),y = a * (mlt x,y)

proof end;

theorem Th28: :: MATRIXC1:28

for x, y being FinSequence of COMPLEX st len x = len y holds
(mlt x,y) *' = mlt (x *' ),(y *' )

proof end;

Lm2: for a, b being Element of COMPLEX holds (multcomplex [;] a,(id COMPLEX )) . b = a * b

proof end;

theorem Th29: :: MATRIXC1:29

for F being FinSequence of COMPLEX
for a being Element of COMPLEX holds Sum (a * F) = a * (Sum F)

proof end;

definition

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

proof end;

end;

:: deftheorem defines FR2FC MATRIXC1:def 9 :

theorem Th30: :: MATRIXC1:30

for R being FinSequence of REAL
for F being FinSequence of COMPLEX st R = F & len R >= 1 holds
addreal $$ R = addcomplex $$ F

proof end;

theorem Th31: :: MATRIXC1:31

for x being FinSequence of REAL
for y being FinSequence of COMPLEX st x = y & len x >= 1 holds
Sum x = Sum y

proof end;

theorem Th32: :: MATRIXC1:32

for F1, F2 being FinSequence of COMPLEX st len F1 = len F2 holds
Sum (F1 - F2) = (Sum F1) - (Sum F2)

proof end;

theorem Th33: :: MATRIXC1:33

for F1, F2 being FinSequence of COMPLEX
for i being Nat st i in dom (F1 + F2) holds
(F1 + F2) . i = (F1 . i) + (F2 . i)

proof end;

theorem Th34: :: MATRIXC1:34

for F1, F2 being FinSequence of COMPLEX
for i being Nat st i in dom (F1 - F2) holds
(F1 - F2) . i = (F1 . i) - (F2 . i)

proof end;

theorem :: MATRIXC1:35

for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
mlt (x - y),z = (mlt x,z) - (mlt y,z)

proof end;

theorem Th36: :: MATRIXC1:36

for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
mlt x,(y - z) = (mlt x,y) - (mlt x,z)

proof end;

theorem :: MATRIXC1:37

for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
mlt x,(y + z) = (mlt x,y) + (mlt x,z)

proof end;

theorem Th38: :: MATRIXC1:38

for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
mlt (x + y),z = (mlt x,z) + (mlt y,z)

proof end;

theorem Th39: :: MATRIXC1:39

for F1, F2 being FinSequence of COMPLEX st len F1 = len F2 holds
Sum (F1 + F2) = (Sum F1) + (Sum F2)

proof end;

theorem Th40: :: MATRIXC1:40

for x1, y1 being FinSequence of COMPLEX
for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds
multcomplex .: x1,y1 = multreal .: x2,y2

proof end;

theorem Th41: :: MATRIXC1:41

for x, y being FinSequence of REAL st len x = len y holds
FR2FC (mlt x,y) = mlt (FR2FC x),(FR2FC y)

proof end;

theorem Th42: :: MATRIXC1:42

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

proof end;

theorem :: MATRIXC1:43

for A, B being Matrix of COMPLEX st len A = len B & width A = width B holds
Indices A = Indices B

proof end;

theorem :: MATRIXC1:44

for i, j being Nat
for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & j in Seg (len M1) holds
Line (M1 + M2),j = (Line M1,j) + (Line M2,j)

proof end;

theorem Th45: :: MATRIXC1:45

for i being Nat
for M being Matrix of COMPLEX st i in Seg (len M) holds
Line M,i = (Line (M *' ),i) *'

proof end;

theorem Th46: :: MATRIXC1:46

for i being Nat
for F being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len F = width M holds
mlt F,((Line (M *' ),i) *' ) = (mlt (Line (M *' ),i),(F *' )) *'

proof end;

theorem Th47: :: MATRIXC1:47

for F being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len F = width M & len F >= 1 holds
(M * F) *' = (M *' ) * (F *' )

proof end;

theorem :: MATRIXC1:48

for F1, F2, F3 being FinSequence of COMPLEX st len F1 = len F2 & len F2 = len F3 holds
mlt F1,(mlt F2,F3) = mlt (mlt F1,F2),F3

proof end;

theorem :: MATRIXC1:49

for F being FinSequence of COMPLEX holds Sum (- F) = - (Sum F)

proof end;

theorem Th50: :: MATRIXC1:50

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

theorem Th51: :: MATRIXC1:51

for F1, F2 being FinSequence of COMPLEX holds Sum (F1 ^ F2) = (Sum F1) + (Sum F2)

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines LineSum MATRIXC1:def 10 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines ColSum MATRIXC1:def 11 :

theorem Th52: :: MATRIXC1:52

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

proof end;

theorem Th53: :: MATRIXC1:53

for f, g being FinSequence of COMPLEX
for n being Nat st len f = n + 1 & g = f | n holds
Sum f = (Sum g) + (f /. (len f))

proof end;

theorem Th54: :: MATRIXC1:54

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

proof end;

definition

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

end;

:: deftheorem defines SumAll MATRIXC1:def 12 :

theorem Th55: :: MATRIXC1:55

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

proof end;

theorem Th56: :: MATRIXC1:56

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

proof end;

definition

let x, y be FinSequence of COMPLEX ;
let M be Matrix of COMPLEX ;
assume A1: ( len x = len M & len y = width M ) ;
func QuadraticForm x,M,y -> Matrix of COMPLEX means :Def13: :: MATRIXC1:def 13
( len it = len x & width it = len y & ( for i, j being Nat st [i,j] in Indices M holds
it * i,j = ((x . i) * (M * i,j)) * ((y . j) *' ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines QuadraticForm MATRIXC1:def 13 :

theorem Th57: :: MATRIXC1:57

for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = len M & len y = width M & len x > 0 & len y > 0 holds
(QuadraticForm x,M,y) @ = (QuadraticForm y,(M @" ),x) *'

proof end;

theorem Th58: :: MATRIXC1:58

for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = len M & len y = width M holds
(QuadraticForm x,M,y) *' = QuadraticForm (x *' ),(M *' ),(y *' )

proof end;

theorem Th59: :: MATRIXC1:59

for x, y being FinSequence of COMPLEX st len x = len y & 0 < len y holds
|(x,y)| = |(y,x)| *'

proof end;

theorem Th60: :: MATRIXC1:60

for x, y being FinSequence of COMPLEX st len x = len y & 0 < len y holds
|(x,y)| *' = |((x *' ),(y *' ))|

proof end;

theorem :: MATRIXC1:61

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

proof end;

theorem Th62: :: MATRIXC1:62

for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = width M & len y = len M & len x > 0 & len y > 0 holds
|(x,((M @" ) * y))| = SumAll (QuadraticForm x,(M @ ),y)

proof end;

theorem Th63: :: MATRIXC1:63

for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len y = len M & len x = width M & len x > 0 & len y > 0 & len M > 0 holds
|((M * x),y)| = SumAll (QuadraticForm x,(M @ ),y)

proof end;

theorem Th64: :: MATRIXC1:64

for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = width M & len y = len M & width M > 0 & len M > 0 holds
|((M * x),y)| = |(x,((M @" ) * y))|

proof end;

theorem :: MATRIXC1:65

for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = len M & len y = width M & width M > 0 & len M > 0 & len x > 0 holds
|(x,(M * y))| = |(((M @" ) * x),y)|

proof end;