:: The Inner Product and Conjugate of Finite Sequences of Complex Numbers
:: by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received April 25, 2005
:: Copyright (c) 2005 Association of Mizar Users
:: deftheorem Def1 defines *' COMPLSP2:def 1 :
Lm1:
for x being FinSequence of COMPLEX
for c being Element of COMPLEX holds c * x = (multcomplex [;] c,(id COMPLEX )) * x
theorem :: COMPLSP2:1
theorem :: COMPLSP2:2
theorem Th3: :: COMPLSP2:3
theorem Th4: :: COMPLSP2:4
theorem Th5: :: COMPLSP2:5
theorem Th6: :: COMPLSP2:6
theorem Th7: :: COMPLSP2:7
theorem :: COMPLSP2:8
theorem :: COMPLSP2:9
theorem :: COMPLSP2:10
theorem :: COMPLSP2:11
theorem :: COMPLSP2:12
theorem Th13: :: COMPLSP2:13
theorem :: COMPLSP2:14
theorem Th15: :: COMPLSP2:15
theorem Th16: :: COMPLSP2:16
theorem Th17: :: COMPLSP2:17
theorem Th18: :: COMPLSP2:18
theorem Th19: :: COMPLSP2:19
theorem Th20: :: COMPLSP2:20
theorem Th21: :: COMPLSP2:21
theorem :: COMPLSP2:22
theorem :: COMPLSP2:23
theorem Th24: :: COMPLSP2:24
theorem Th25: :: COMPLSP2:25
theorem Th26: :: COMPLSP2:26
:: deftheorem defines Re COMPLSP2:def 2 :
theorem Th27: :: COMPLSP2:27
:: deftheorem defines Im COMPLSP2:def 3 :
definition
let x,
y be
FinSequence of
COMPLEX ;
func |(x,y)| -> Element of
COMPLEX equals :: COMPLSP2:def 4
((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))|;
coherence
((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))| is Element of COMPLEX
by XCMPLX_0:def 2;
end;
:: deftheorem defines |( COMPLSP2:def 4 :
theorem Th28: :: COMPLSP2:28
theorem :: COMPLSP2:29
theorem Th30: :: COMPLSP2:30
theorem :: COMPLSP2:31
theorem Th32: :: COMPLSP2:32
theorem Th33: :: COMPLSP2:33
theorem Th34: :: COMPLSP2:34
theorem Th35: :: COMPLSP2:35
theorem Th36: :: COMPLSP2:36
theorem Th37: :: COMPLSP2:37
theorem :: COMPLSP2:38
theorem Th39: :: COMPLSP2:39
theorem Th40: :: COMPLSP2:40
theorem Th41: :: COMPLSP2:41
theorem Th42: :: COMPLSP2:42
theorem Th43: :: COMPLSP2:43
theorem :: COMPLSP2:44
theorem Th45: :: COMPLSP2:45
for
C being
Function of
[:COMPLEX ,COMPLEX :],
COMPLEX for
G being
Function of
[:REAL ,REAL :],
REAL for
x1,
y1 being
FinSequence of
COMPLEX for
x2,
y2 being
FinSequence of
REAL st
x1 = x2 &
y1 = y2 &
len x1 = len y2 & ( for
i being
Element of
NAT st
i in dom x1 holds
C . (x1 . i),
(y1 . i) = G . (x2 . i),
(y2 . i) ) holds
C .: x1,
y1 = G .: x2,
y2
theorem :: COMPLSP2:46
theorem :: COMPLSP2:47
theorem Th48: :: COMPLSP2:48
theorem Th49: :: COMPLSP2:49
theorem :: COMPLSP2:50
theorem :: COMPLSP2:51
theorem Th52: :: COMPLSP2:52
theorem Th53: :: COMPLSP2:53
Lm2:
for x being FinSequence of COMPLEX holds - (0c (len x)) = 0c (len x)
theorem Th54: :: COMPLSP2:54
theorem Th55: :: COMPLSP2:55
theorem :: COMPLSP2:56
theorem :: COMPLSP2:57
theorem Th58: :: COMPLSP2:58
theorem Th59: :: COMPLSP2:59
theorem Th60: :: COMPLSP2:60
theorem :: COMPLSP2:61
theorem :: COMPLSP2:62
theorem Th63: :: COMPLSP2:63
theorem Th64: :: COMPLSP2:64
theorem Th65: :: COMPLSP2:65
theorem Th66: :: COMPLSP2:66
theorem Th67: :: COMPLSP2:67
theorem Th68: :: COMPLSP2:68
theorem :: COMPLSP2:69
theorem Th70: :: COMPLSP2:70
theorem Th71: :: COMPLSP2:71
theorem Th72: :: COMPLSP2:72
theorem Th73: :: COMPLSP2:73
theorem Th74: :: COMPLSP2:74
theorem Th75: :: COMPLSP2:75
theorem :: COMPLSP2:76
theorem :: COMPLSP2:77
theorem Th78: :: COMPLSP2:78
theorem Th79: :: COMPLSP2:79
theorem :: COMPLSP2:80
theorem :: COMPLSP2:81