:: 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-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, NUMBERS, FINSEQ_1, FINSEQ_2, ARYTM_3, NAT_1, XXREAL_0,
FUNCT_1, RELAT_1, TARSKI, BINOP_2, FUNCOP_1, ARYTM_1, XCMPLX_0, CARD_1,
COMPLEX1, RVSUM_1, REAL_1, ZFMISC_1, VALUED_0, VALUED_1;
notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1,
RELAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, PARTFUN1, BINOP_1, FUNCOP_1,
FINSEQ_1, FINSEQOP, VALUED_0, VALUED_1, SEQ_4, COMPLEX1, RVSUM_1,
FINSEQ_2, BINOP_2, MATRIX_5, XXREAL_0, COMSEQ_2;
constructors SETWISEO, REAL_1, BINOP_2, FINSEQOP, SEQ_4, MATRIX_5, BINOP_1,
RVSUM_1, RELSET_1, COMSEQ_2;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0,
BINOP_2, MEMBERED, FINSEQ_2, VALUED_0, VALUED_1, XREAL_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities VALUED_1, ORDINAL1;
expansions FINSEQ_1;
theorems FUNCT_1, FUNCT_2, FINSEQ_1, FUNCOP_1, FINSEQ_2, FINSEQOP, RELAT_1,
BINOP_2, COMPLEX1, XCMPLX_0, FINSEQ_3, RVSUM_1, ORDINAL1, VALUED_0,
VALUED_1, SEQ_4, CARD_1, XREAL_0, COMSEQ_2;
begin :: Preliminaries
reserve i,j for Element of NAT,
x,y,z for FinSequence of COMPLEX,
c for Element of COMPLEX,
R,R1,R2 for Element of i-tuples_on COMPLEX;
definition let z be FinSequence of COMPLEX;
redefine func z*' -> FinSequence of COMPLEX means :Def1: :: redefines *' (COMSEQ_2, definition)
len it = len z & for i being Nat st 1<=i & i<=len z holds it.i = (z.i)*';
coherence
proof
set f = z*';
A1: dom f = dom z by COMSEQ_2:def 1;
ex n being Nat st dom z = Seg n by FINSEQ_1:def 2;
then
A2: f is FinSequence by A1,FINSEQ_1:def 2;
rng f c= COMPLEX
proof
let y be object;
thus thesis by XCMPLX_0:def 2;
end;
hence thesis by A2, FINSEQ_1:def 4;
end;
compatibility
proof
let IT be FinSequence of COMPLEX;
thus IT = z*' implies
len IT = len z & for i being Nat st 1<=i & i<=len z holds IT.i = (z.i)*'
proof
assume
A3: IT = z*';
then dom IT = dom z by COMSEQ_2:def 1;
hence thesis by A3,COMSEQ_2:def 1,FINSEQ_3:25,29;
end;
assume that
A4: len IT = len z and
A5: for i being Nat st 1<=i & i<=len z holds IT.i = (z.i)*';
A6: dom IT = dom z by A4,FINSEQ_3:29;
now
let i be set;
assume
A7: i in dom IT;
then reconsider j = i as Nat;
1 <= j & j <= len z by A4,A7,FINSEQ_3:25;
hence IT.i = (z.i)*' by A5;
end;
hence IT = z*' by A6,COMSEQ_2:def 1;
end;
end;
Lm1: c*x = (multcomplex[;](c,id COMPLEX))*x
proof
c multcomplex = multcomplex[;](c,id COMPLEX) by SEQ_4:def 4;
hence thesis by SEQ_4:def 9;
end;
theorem
i in dom (x+y) implies (x+y).i = x.i + y.i by VALUED_1:def 1;
theorem
i in dom (x-y) implies (x-y).i = x.i - y.i by VALUED_1:13;
definition let i,R1,R2;
redefine func R1 - R2 -> Element of i-tuples_on COMPLEX; :: redefines - (VALUED_1, definition)
coherence
proof
R1 - R2 = diffcomplex.:(R1,R2) by SEQ_4:def 7;
hence thesis by FINSEQ_2:120;
end;
end;
definition let i,R1,R2;
redefine func R1 + R2 -> Element of i-tuples_on COMPLEX; :: redefines + (VALUED_1, definition)
coherence
proof
R1 + R2 = addcomplex.:(R1,R2) by SEQ_4:def 6;
hence thesis by FINSEQ_2:120;
end;
end;
definition let i, R;
let r be Complex;
redefine func r*R -> Element of i-tuples_on COMPLEX; :: redefines * (SEQ_4, synonym) → (#) (VALUED_1, definition)
coherence
proof
reconsider q = r as Element of COMPLEX by XCMPLX_0:def 2;
q*R = (multcomplex[;](q,id COMPLEX))*R by Lm1;
hence thesis by FINSEQ_2:113;
end;
end;
Lm2: for F being complex-valued FinSequence holds F is FinSequence of COMPLEX
proof
let F be complex-valued FinSequence;
rng F c= COMPLEX by VALUED_0:def 1;
hence thesis by FINSEQ_1:def 4;
end;
theorem Th3:
for a being Complex, x being complex-valued FinSequence holds
len (a(#)x) = len x
proof
let a be Complex, x be complex-valued FinSequence;
set n=len x;
x is FinSequence of COMPLEX by Lm2; then
reconsider z=x as Element of n-tuples_on COMPLEX by FINSEQ_2:92;
reconsider a9 = a as Element of COMPLEX by XCMPLX_0:def 2;
len (a9*z)=n by CARD_1:def 7;
hence thesis;
end;
theorem
for x being complex-valued FinSequence holds dom x = dom -x by VALUED_1:8;
theorem Th5:
for x being complex-valued FinSequence holds len (-x)=len x
proof
let x be complex-valued FinSequence;
dom (-x)=dom x by VALUED_1:8;
hence thesis by FINSEQ_3:29;
end;
theorem Th6:
for x1,x2 being complex-valued FinSequence st len x1=len x2 holds
len (x1+x2)=len x1
proof
let x1,x2 be complex-valued FinSequence;
set n=len x1;
A1: x2 is FinSequence of COMPLEX by Lm2;
x1 is FinSequence of COMPLEX by Lm2; then
reconsider z1=x1 as Element of (len x1)-tuples_on COMPLEX by FINSEQ_2:92;
assume len x1=len x2; then
reconsider z2=x2 as Element of n-tuples_on COMPLEX by A1,FINSEQ_2:92;
dom (z1+z2)=Seg n by FINSEQ_2:124;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th7:
for x1,x2 being complex-valued FinSequence st len x1=len x2 holds
len (x1-x2)=len x1
proof
let x1,x2 be complex-valued FinSequence;
set n=len x1;
A1: x2 is FinSequence of COMPLEX by Lm2;
x1 is FinSequence of COMPLEX by Lm2; then
reconsider z1=x1 as Element of (len x1)-tuples_on COMPLEX by FINSEQ_2:92;
assume len x1=len x2; then
reconsider z2=x2 as Element of n-tuples_on COMPLEX by A1,FINSEQ_2:92;
dom (z1-z2)=Seg n by FINSEQ_2:124;
hence thesis by FINSEQ_1:def 3;
end;
theorem
for f being complex-valued FinSequence holds f is Element of COMPLEX len f
proof
let f be complex-valued FinSequence;
f is FinSequence of COMPLEX by Lm2; then
f is Element of COMPLEX* by FINSEQ_1:def 11;
then f in { s where s is Element of COMPLEX*: len s = len f };
then f in ((len f)-tuples_on COMPLEX) by FINSEQ_2:def 4;
hence thesis by SEQ_4:def 11;
end;
::$CT 4
theorem Th9:
for x being FinSequence of COMPLEX holds (-x).i = -x.i
proof
let x be FinSequence of COMPLEX;
per cases;
suppose
A1: not i in dom -x; then
A2: not i in dom x by VALUED_1:8;
thus (-x).i = -0 by A1,FUNCT_1:def 2
.= -x.i by A2,FUNCT_1:def 2;
end;
suppose
A3: i in dom -x;
set r = x.i;
-x = compcomplex*x by SEQ_4:def 8;
then (-x).i = compcomplex.r by A3,FUNCT_1:12;
hence thesis by BINOP_2:def 1;
end;
end;
definition let i,R;
redefine func -R -> Element of i-tuples_on COMPLEX; :: redefines - (VALUED_1, definition)
coherence
proof
-R = compcomplex*R by SEQ_4:def 8;
hence thesis by FINSEQ_2:113;
end;
end;
theorem
c = R.j implies (-R).j = -c by Th9;
theorem Th11:
for a being Complex holds dom(a*x) = dom x
proof
let a be Complex;
dom(a multcomplex) = COMPLEX by FUNCT_2:def 1;
then rng x c= dom(a multcomplex) by FINSEQ_1:def 4;
hence dom x = dom((a multcomplex)*x) by RELAT_1:27
.= dom(a*x) by SEQ_4:def 9;
end;
theorem Th12:
for i being Nat, a being Complex holds (a*x).i = a*(x.i)
proof
let i be Nat, a be Complex;
reconsider aa = a as Element of COMPLEX by XCMPLX_0:def 2;
per cases;
suppose
A1: not i in dom (a*x); then
A2: not i in dom x by Th11;
thus (a*x).i = a*0 by A1,FUNCT_1:def 2
.= a*(x.i) by A2,FUNCT_1:def 2;
end;
suppose
A3: i in dom (a*x);
set a9 = x.i;
A4: a*x = (multcomplex[;](aa,id COMPLEX))*x by Lm1; then
A5: a9 in dom(multcomplex[;](aa,id COMPLEX)) by A3,FUNCT_1:11;
thus (a*x).i = (multcomplex[;](aa,id COMPLEX)).a9 by A3,A4,FUNCT_1:12
.= multcomplex.(a,(id COMPLEX).a9) by A5,FUNCOP_1:32
.= a*(x.i) by BINOP_2:def 5;
end;
end;
theorem Th13:
for a being Complex holds (a*x)*' = a*'*(x*')
proof
let a be Complex;
reconsider aa = a as Element of COMPLEX by XCMPLX_0:def 2;
len (a*'*(x*')) = len (x*') by Th3; then
A1: len (a*'*(x*')) = len x by Def1;
A2: len (a*x) = len x by Th3;
A3: now
let i be Nat;
assume that
A4: 1 <= i and
A5: i <= len ((a*x)*');
A6: i <= len (a*x) by A5,Def1;
hence (a*x)*'.i = (((a*x).i)*') by A4,Def1
.= (aa*(x.i))*' by Th12
.= aa*'*(x.i)*' by COMPLEX1:35
.= a*'*((x*').i) by A2,A4,A6,Def1
.= (a*'*(x*')).i by Th12;
end;
len ((a*x)*') = len (a*x) by Def1;
hence thesis by A1,A3,Th3;
end;
theorem Th14:
(R1+R2).j = R1.j + R2.j
proof
per cases;
suppose
A1: not j in Seg i; then
A2: not j in dom R2 by FINSEQ_2:124;
A3: not j in dom R1 by A1,FINSEQ_2:124;
not j in dom(R1+R2) by A1,FINSEQ_2:124;
hence (R1+R2).j = 0+0 by FUNCT_1:def 2
.= R1.j + 0 by A3,FUNCT_1:def 2
.= R1.j + R2.j by A2,FUNCT_1:def 2;
end;
suppose j in Seg i;
then j in dom (R1 + R2) by FINSEQ_2:124;
hence thesis by VALUED_1:def 1;
end;
end;
theorem Th15:
for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds
(x1 + x2)*' = x1*' + x2*'
proof
let x1,x2 be FinSequence of COMPLEX;
reconsider x9=x1 as Element of (len x1)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9=x2 as Element of (len x2)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider x3=x1*' as Element of (len (x1*'))-tuples_on COMPLEX by
FINSEQ_2:92;
reconsider x4=x2*' as Element of (len (x2*'))-tuples_on COMPLEX by
FINSEQ_2:92;
assume
A1: len x1=len x2; then
A2: len (x1 + x2) = len x1 by Th6;
A3: len x1=len (x1*') & len x2=len (x2*') by Def1;
A4: now
let i be Nat;
A5: i in NAT by ORDINAL1:def 12;
assume that
A6: 1 <= i and
A7: i <= len ((x1 + x2)*');
A8: i <= len (x1 + x2) by A7,Def1;
hence (x1 + x2)*'.i = (((x1 + x2).i)*') by A6,Def1
.= (x9.i + y9.i)*' by A1,A5,Th14
.= (x1.i)*'+(x2.i)*' by COMPLEX1:32
.= ((x1*').i)+(x2.i)*' by A2,A6,A8,Def1
.= ((x1*').i)+((x2*').i) by A1,A2,A6,A8,Def1
.= (x3+x4).i by A1,A3,A5,Th14;
end;
len (x1*' + x2*') = len x1 by A1,A3,Th6;
hence thesis by A4,A2,Def1;
end;
theorem Th16:
(R1-R2).j = R1.j - R2.j
proof
per cases;
suppose
A1: not j in Seg i; then
A2: not j in dom R2 by FINSEQ_2:124;
A3: not j in dom R1 by A1,FINSEQ_2:124;
not j in dom(R1-R2) by A1,FINSEQ_2:124;
hence (R1-R2).j = 0-0 by FUNCT_1:def 2
.= R1.j - 0 by A3,FUNCT_1:def 2
.= R1.j - R2.j by A2,FUNCT_1:def 2;
end;
suppose
j in Seg i;
then j in dom (R1 - R2) by FINSEQ_2:124;
hence thesis by VALUED_1:13;
end;
end;
theorem Th17:
for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds
(x1 - x2)*' = x1*' - x2*'
proof
let x1,x2 be FinSequence of COMPLEX;
reconsider x9=x1 as Element of (len x1)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9=x2 as Element of (len x2)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider x3=x1*' as Element of (len (x1*'))-tuples_on COMPLEX by
FINSEQ_2:92;
reconsider x4=x2*' as Element of (len (x2*'))-tuples_on COMPLEX by
FINSEQ_2:92;
assume
A1: len x1=len x2; then
A2: len (x1 - x2) = len x1 by Th7;
A3: len x1=len (x1*') & len x2=len (x2*') by Def1;
A4: now
let i be Nat;
A5: i in NAT by ORDINAL1:def 12;
assume that
A6: 1 <= i and
A7: i <= len ((x1 - x2)*');
A8: i <= len (x1 - x2) by A7,Def1;
hence (x1 - x2)*'.i = (((x1 - x2).i)*') by A6,Def1
.= (x9.i - y9.i)*' by A1,A5,Th16
.= (x1.i)*'-(x2.i)*' by COMPLEX1:34
.= ((x1*').i)-(x2.i)*' by A2,A6,A8,Def1
.= ((x1*').i)-((x2*').i) by A1,A2,A6,A8,Def1
.= (x3-x4).i by A1,A3,A5,Th16;
end;
len (x1*' - x2*') = len x1 by A1,A3,Th7;
hence thesis by A4,A2,Def1;
end;
theorem
for z being FinSequence of COMPLEX holds (z*')*' = z;
theorem
for z being FinSequence of COMPLEX holds (-z)*' = -(z*')
proof
let z be FinSequence of COMPLEX;
thus (-z)*'= ((-1r)*')*(z*') by Th13,COMPLEX1:def 4
.= -z*' by COMPLEX1:30,33,def 4;
end;
theorem Th20:
for z being Complex holds z+z*' = 2*(Re z)
proof
let z be Complex;
z+z*'=Re z + Re (z*')+(Im z + Im (z*'))*<i> by COMPLEX1:81
.=Re z + Re (z*')+(Im z + -Im z)*<i> by COMPLEX1:27
.=Re z + Re z by COMPLEX1:27
.=2*(Re z);
hence thesis;
end;
theorem Th21:
for x,y being complex-valued FinSequence st len x=len y holds
(x-y).i = x.i - y.i
proof
let x,y be complex-valued FinSequence;
A1:x is FinSequence of COMPLEX & y is FinSequence of COMPLEX by Lm2; then
reconsider x2=x as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider y2=y as Element of (len y)-tuples_on COMPLEX by A1,FINSEQ_2:92;
reconsider y29=(x2 - y2) as Element of (len (x2 - y2))-tuples_on COMPLEX by
FINSEQ_2:92;
assume
A2: len x=len y; then
A3: len (x - y) = len x by Th7;
per cases;
suppose
A4: not i in Seg (len x); then
A5: not i in dom x2 by FINSEQ_2:124;
A6: not i in dom y2 by A2,A4,FINSEQ_2:124;
not i in dom(y29) by A3,A4,FINSEQ_2:124;
then (x2-y2).i = 0-0 by FUNCT_1:def 2
.= x2.i - 0 by A5,FUNCT_1:def 2
.= x2.i - y2.i by A6,FUNCT_1:def 2;
hence thesis;
end;
suppose i in Seg (len x);
then i in dom (y29) by A3,FINSEQ_2:124;
hence thesis by VALUED_1:13;
end;
end;
theorem Th22:
for x,y being complex-valued FinSequence st len x=len y holds
(x+y).i = x.i + y.i
proof
let x,y be complex-valued FinSequence;
A1:x is FinSequence of COMPLEX & y is FinSequence of COMPLEX by Lm2; then
reconsider x2=x as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider y2=y as Element of (len y)-tuples_on COMPLEX by A1,FINSEQ_2:92;
reconsider y29=(x2 + y2) as Element of (len (x2 + y2))-tuples_on COMPLEX by
FINSEQ_2:92;
assume
A2: len x=len y; then
A3: len (x + y) = len x by Th6;
per cases;
suppose
A4: not i in Seg len x; then
A5: not i in dom x2 by FINSEQ_2:124;
A6: not i in dom y2 by A2,A4,FINSEQ_2:124;
not i in dom(y29) by A3,A4,FINSEQ_2:124;
then (x2+y2).i = 0+0 by FUNCT_1:def 2
.= x2.i + 0 by A5,FUNCT_1:def 2
.= x2.i + y2.i by A6,FUNCT_1:def 2;
hence thesis;
end;
suppose i in Seg len x;
then i in dom y29 by A3,FINSEQ_2:124;
hence thesis by VALUED_1:def 1;
end;
end;
definition let z be FinSequence of COMPLEX;
func Re z -> FinSequence of REAL equals
1/2*(z+z*');
coherence
proof
A1: len z = len (z*') by Def1;
A2: len (1/2*(z+z*')) = len (z+z*') by Th3
.= len z by A1,Th6;
rng (1/2*(z+z*')) c= REAL
proof
let w be object;
assume w in rng (1/2*(z+z*'));
then consider x being object such that
A3: x in dom (1/2*(z+z*')) and
A4: w=(1/2*(z+z*')).x by FUNCT_1:def 3;
reconsider i=x as Element of NAT by A3;
x in Seg len (1/2*(z+z*')) by A3,FINSEQ_1:def 3; then
A5: 1<=i & i<=len z by A2,FINSEQ_1:1;
(1/2*(z+z*')).i = 1/2*((z+z*').i) by Th12
.=1/2*((z.i)+(z*').i) by A1,Th22
.=1/2*((z.i)+(z.i)*') by A5,Def1
.=(1/2)*(2*(Re (z.i))) by Th20;
hence thesis by A4;
end;
hence thesis by FINSEQ_1:def 4;
end;
end;
theorem Th23:
for z being Complex holds z-z*' = 2*(Im z) * <i>
proof
let z be Complex;
z-z*'= Re z - Re (z*') + (Im z - Im (z*'))*<i> by COMPLEX1:84
.= Re z - Re (z*')+(Im z - -Im z)*<i> by COMPLEX1:27
.= Re z - Re z + (Im z - -Im z)*<i> by COMPLEX1:27
.= 2*(Im z)*<i>;
hence thesis;
end;
definition
let z be FinSequence of COMPLEX;
func Im z -> FinSequence of REAL equals
(-1/2*<i>)*(z-z*');
coherence
proof
A1: len z = len (z*') by Def1;
A2: len ((-1/2*<i>)*(z-z*')) = len (z-z*') by Th3
.= len z by A1,Th7;
rng ((-1/2*<i>)*(z-z*')) c= REAL
proof
let w be object;
assume w in rng ((-1/2*<i>)*(z-z*'));
then consider x being object such that
A3: x in dom ((-1/2*<i>)*(z-z*')) and
A4: w=((-1/2*<i>)*(z-z*')).x by FUNCT_1:def 3;
reconsider i=x as Element of NAT by A3;
x in Seg len ((-1/2*<i>)*(z-z*')) by A3,FINSEQ_1:def 3; then
A5: 1<=i & i<=len z by A2,FINSEQ_1:1;
((-1/2*<i>)*(z-z*')).i =(-1/2*<i>)*((z-z*').i) by Th12
.=(-1/2*<i>)*((z.i)-(z*').i) by A1,Th21
.=(-1/2*<i>)*((z.i)-(z.i)*') by A5,Def1
.=(-1/2*<i>)*((2*(Im (z.i))) * <i>) by Th23;
hence thesis by A4;
end;
hence thesis by FINSEQ_1:def 4;
end;
end;
definition
let x,y be FinSequence of COMPLEX;
func |( x,y )| -> Element of COMPLEX equals
|(Re x,Re y)| - <i>*(|(Re x,Im y)|) + <i>*(|(Im x,Re y)|) + |(Im x,Im y)|;
coherence by XCMPLX_0:def 2;
end;
theorem Th24:
for x,y,z being complex-valued FinSequence st len x=len y & len y=len z
holds x + (y + z) = x + y + z
proof
let x,y,z be complex-valued FinSequence;
reconsider x1=x, y1 = y, z1 = z as FinSequence of COMPLEX by Lm2;
assume
A1: len x=len y & len y=len z;
reconsider z9=z1 as Element of (len z)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9=y1 as Element of (len y)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider x9=x1 as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
x + (y + z) = addcomplex.:(x1,y1+z1) by SEQ_4:def 6
.= addcomplex.:(x1,addcomplex.:(y1,z1)) by SEQ_4:def 6
.= addcomplex.:(addcomplex.:(x9,y9),z9) by A1,FINSEQOP:28
.= addcomplex.:(x1+y1,z1) by SEQ_4:def 6
.= x + y + z by SEQ_4:def 6;
hence thesis;
end;
::$CT
theorem Th25:
for c being Complex, x,y being FinSequence of COMPLEX st
len x=len y holds c*(x+y) = c*x + c*y
proof
let c be Complex, x,y be FinSequence of COMPLEX;
assume
A1: len x=len y;
set cM = c multcomplex;
reconsider y9=y as Element of (len y)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider x9=x as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
A2: c is Element of COMPLEX by XCMPLX_0:def 2;
c*(x+y) = cM*(x + y) by SEQ_4:def 9
.= cM*(addcomplex.:(x,y)) by SEQ_4:def 6
.= addcomplex.:(cM*x9,cM*y9) by A1,A2,FINSEQOP:51,SEQ_4:56
.= cM*x + cM*y by SEQ_4:def 6
.= c*x + cM*y by SEQ_4:def 9
.= c*x + c*y by SEQ_4:def 9;
hence thesis;
end;
::$CT
theorem Th26:
for x,y being complex-valued FinSequence st len x=len y & x + y = 0c
(len x) holds x = -y & y = -x
proof
let x,y be complex-valued FinSequence;
assume that
A1: len x=len y and
A2: x + y = 0c (len x);
reconsider x1=x, y1 = y as FinSequence of COMPLEX by Lm2;
reconsider x9=x1 as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9=y1 as Element of (len y)-tuples_on COMPLEX by FINSEQ_2:92;
A3: x + y = addcomplex.:(x1,y1) & -y = compcomplex*y1 by SEQ_4:def 6,def 8;
x + y = (len x) |-> 0c by A2,SEQ_4:def 12;
then x9 = -y9 by A1,A3,BINOP_2:1,FINSEQOP:74,SEQ_4:51,52;
hence thesis;
end;
theorem Th27:
for x being complex-valued FinSequence holds x + 0c (len x) = x
proof
let x be complex-valued FinSequence;
A1:x is FinSequence of COMPLEX by Lm2; then
reconsider x9=x as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
x + 0c (len x) = x+(len x) |-> 0c by SEQ_4:def 12
.= addcomplex.:(x,(len x) |-> 0c) by A1,SEQ_4:def 6
.= x9 by BINOP_2:1,FINSEQOP:56;
hence thesis;
end;
theorem Th28:
for x being complex-valued FinSequence holds x + -x = 0c (len x)
proof
let x be complex-valued FinSequence;
A1:x is FinSequence of COMPLEX & -x is FinSequence of COMPLEX by Lm2; then
reconsider x9=x as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
x + -x = addcomplex.:(x,-x) by A1,SEQ_4:def 6
.= addcomplex.:(x,compcomplex*x) by A1,SEQ_4:def 8
.= (len x9) |-> 0c by BINOP_2:1,FINSEQOP:73,SEQ_4:51,52
.= 0c (len x9) by SEQ_4:def 12;
hence thesis;
end;
theorem Th29:
for x,y being complex-valued FinSequence st len x=len y holds
-(x + y) = -x + -y
proof
let x,y be complex-valued FinSequence;
assume
A1: len x=len y;
A2: len (-y) = len y by Th5; then
A3: len (-x + -y) = len (-x) by A1,Th5,Th6;
A4: len (-x) = len x by Th5;
A5: len (x + y) = len x by A1,Th6;
then (x + y) + (-x + -y) = y + x + -x + -y by A1,A2,A4,Th24
.= y + (x + -x) + -y by A1,A4,Th24
.= y + 0c (len x) + -y by Th28
.= y + -y by A1,Th27
.= 0c (len y) by Th28;
hence thesis by A1,A4,A5,A3,Th26;
end;
theorem Th30:
for x,y,z being complex-valued FinSequence st len x=len y & len y=len z
holds x - y - z = x - (y + z)
proof
let x,y,z be complex-valued FinSequence;
assume that
A1: len x=len y and
A2: len y=len z;
len (-y) = len y & len (-z) = len z by Th5;
then x - y - z = x + (- y + - z) by A1,A2,Th24
.= x - (y + z) by A2,Th29;
hence thesis;
end;
theorem Th31:
for x,y,z being complex-valued FinSequence st len x=len y & len y=len z
holds x + (y - z) = x + y - z
proof
let x,y,z be complex-valued FinSequence;
assume
A1: len x=len y & len y=len z;
len (-z) = len z by Th5;
hence thesis by A1,Th24;
end;
::$CT
theorem Th32:
for x,y being complex-valued FinSequence st len x=len y holds
-(x - y) = -x + y
proof
let x,y be complex-valued FinSequence;
assume
A1: len x=len y;
len (-y) = len y by Th5;
then -(x - y) = -x +--y by A1,Th29
.= -x + y;
hence thesis;
end;
theorem Th33:
for x,y,z being complex-valued FinSequence st
len x=len y & len y=len z holds x - (y - z) = x - y + z
proof
let x,y,z be complex-valued FinSequence;
assume that
A1: len x=len y and
A2: len y=len z;
A3: len (-y) = len y by Th5;
x - (y - z) = x + (- y + z) by A2,Th32
.= x - y + z by A1,A2,A3,Th24;
hence thesis;
end;
theorem Th34:
for c being Complex holds c*(0c (len x)) = 0c (len x)
proof
let c be Complex;
reconsider cc = c as Element of COMPLEX by XCMPLX_0:def 2;
A1: rng (0c (len x)) c= COMPLEX by FINSEQ_1:def 4;
c*(0c (len x)) = multcomplex[;](cc,id COMPLEX)*(0c (len x)) by Lm1
.= multcomplex[;](cc,(id COMPLEX)*(0c (len x))) by FUNCOP_1:34
.= multcomplex[;](cc,(0c (len x))) by A1,RELAT_1:53
.= multcomplex[;](cc,(len x |-> 0c)) by SEQ_4:def 12
.= (len x) |->(multcomplex.(cc,0c)) by FINSEQOP:18
.= (len x) |->(cc*0c) by BINOP_2:def 5
.= (0c (len x)) by SEQ_4:def 12;
hence thesis;
end;
theorem Th35:
for c being Complex holds -c*x = c*(-x)
proof
let c be Complex;
A1: len (c*(-x))=len (-x) & len (c*x)=len x by Th3;
A2: len x=len (-x) by Th5;
then c*(-x) + c*x = c*(x+-x) by Th25
.= c*(0c (len x)) by Th28
.= 0c (len x) by Th34;
hence thesis by A2,A1,Th26;
end;
theorem Th36:
for c being Complex, x,y being FinSequence of COMPLEX st
len x=len y holds c*(x-y) = c*x - c*y
proof
let c be Complex, x,y be FinSequence of COMPLEX;
assume
A1: len x=len y;
reconsider cc = c as Element of COMPLEX by XCMPLX_0:def 2;
reconsider y9=y as Element of (len y)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider x9=x as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
set cM = cc multcomplex;
c*(x-y) = cM*(x +(- y)) by SEQ_4:def 9
.= cM*(addcomplex.:(x,(-y))) by SEQ_4:def 6
.= addcomplex.:(cM*x9,cM*(-y9)) by A1,FINSEQOP:51,SEQ_4:56
.= cM*x + cM*(-y) by SEQ_4:def 6
.= c*x + cM*(-y) by SEQ_4:def 9
.= c*x + c*(-y) by SEQ_4:def 9
.= c*x - c*y by Th35;
hence thesis;
end;
theorem
for x1,y1 being Element of COMPLEX
for x2,y2 being Real st x1 = x2 &
y1 = y2 holds addcomplex.(x1,y1) = addreal.(x2,y2)
proof
let x1,y1 be Element of COMPLEX;
let x2,y2 be Real;
A1: addcomplex.(x1,y1)= x1+y1 by BINOP_2:def 3;
assume x1 = x2 & y1 = y2;
hence thesis by A1,BINOP_2:def 9;
end;
reserve C for Function of [:COMPLEX,COMPLEX:],COMPLEX;
reserve G for Function of [:REAL,REAL:],REAL;
theorem Th38:
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 st i in dom
x1 holds C.(x1.i,y1.i)=G.(x2.i,y2.i)) holds C.:(x1,y1)=G.:(x2,y2)
proof
let x1,y1 be FinSequence of COMPLEX;
let x2,y2 be FinSequence of REAL;
assume that
A1: x1 = x2 and
A2: y1 = y2 and
A3: len x1=len y2 and
A4: for i st i in dom x1 holds C.(x1.i,y1.i)=G.(x2.i,y2.i);
A5: len (G.:(x2,y2)) = len x1 by A1,A3,FINSEQ_2:72;
now
let i be Nat;
assume that
A6: 1 <= i and
A7: i <= len (C.:(x1,y1));
A8: i <= len x1 by A2,A3,A7,FINSEQ_2:72; then
A9: i in dom x1 by A6,FINSEQ_3:25;
A10: i in dom (G.:(x2,y2)) by A5,A6,A8,FINSEQ_3:25;
i in dom (C.:(x1,y1)) by A6,A7,FINSEQ_3:25;
hence (C.:(x1,y1)).i = C.(x1.i,y1.i) by FUNCOP_1:22
.= G.(x2.i,y2.i) by A4,A9
.= (G.:(x2,y2)).i by A10,FUNCOP_1:22;
end;
hence thesis by A5,A2,A3,FINSEQ_2:72;
end;
theorem
for x1,y1 being FinSequence of COMPLEX for x2,y2 being FinSequence of
REAL st x1 = x2 & y1 = y2 & len x1=len y2 holds addcomplex.:(x1,y1) = addreal.:
(x2,y2)
proof
let x1,y1 be FinSequence of COMPLEX;
let x2,y2 be FinSequence of REAL;
assume that
A1: x1 = x2 & y1 = y2 and
A2: len x1=len y2;
for i st i in dom x1 holds addcomplex.(x1.i,y1.i)=addreal.(x2.i,y2.i)
proof
let i;
x1.i + y1.i = addcomplex.(x1.i,y1.i) by BINOP_2:def 3;
hence thesis by A1,BINOP_2:def 9;
end;
hence thesis by A1,A2,Th38;
end;
::$CT
theorem Th40:
for x being FinSequence of COMPLEX holds len (Re x)=len x & len (Im x)=len x
proof
let x be FinSequence of COMPLEX;
A1: len x=len (x*') by Def1;
A2: len (Im x) =len (x-x*') by Th3
.=len x by A1,Th7;
len (Re x) =len (x+x*') by Th3
.=len x by A1,Th6;
hence thesis by A2;
end;
theorem Th41:
for x,y being FinSequence of COMPLEX st len x=len y holds Re (x+
y) = Re x + Re y & Im(x + y) = Im x + Im y
proof
let x,y be FinSequence of COMPLEX;
A1: len (-x*')=len (x*') by Th5;
assume
A2: len x=len y;
then
A3: len (x+y)=len x by Th6;
A4: len y=len (y*') by Def1;
then
A5: len (y+(y*'))=len y by Th6;
A6: len x=len (x*') by Def1;
then
A7: len (x+(x*'))=len x by Th6;
A8: len (x-(x*'))=len x by A6,Th7;
A9: len (y-(y*'))=len y by A4,Th7;
thus Re (x+y)=1/2*((x+y)+(x*'+y*')) by A2,Th15
.=1/2*((x+y+x*')+y*') by A2,A4,A6,A3,Th24
.=1/2*((x+x*'+y)+y*') by A2,A6,Th24
.=1/2*((x+x*')+(y+y*')) by A2,A4,A7,Th24
.= Re x + Re y by A2,A7,A5,Th25;
thus Im (x+y)=(-1/2*<i>)*((x+y)-(x*'+y*')) by A2,Th15
.=(-1/2*<i>)*((x+y)-x*'-y*') by A2,A4,A6,A3,Th30
.=(-1/2*<i>)*(x+-x*'+y-y*') by A2,A6,A1,Th24
.=(-1/2*<i>)*((x-x*')+(y-y*')) by A2,A4,A8,Th31
.=Im x + Im y by A2,A8,A9,Th25;
end;
theorem
for x1,y1 being FinSequence of COMPLEX for x2,y2 being FinSequence of
REAL st x1 = x2 & y1 = y2 & len x1=len y2 holds diffcomplex.:(x1,y1) = diffreal
.:(x2,y2)
proof
let x1,y1 be FinSequence of COMPLEX, x2,y2 be FinSequence of REAL;
assume that
A1: x1 = x2 & y1 = y2 and
A2: len x1=len y2;
for i st i in dom x1 holds diffcomplex.(x1.i,y1.i)=diffreal.(x2.i,y2.i)
proof
let i;
x1.i - y1.i = diffcomplex.(x1.i,y1.i) by BINOP_2:def 4;
hence thesis by A1,BINOP_2:def 10;
end;
hence thesis by A1,A2,Th38;
end;
::$CT
theorem Th43:
for x,y being FinSequence of COMPLEX st len x=len y holds
Re(x - y) = Re x - Re y & Im(x - y) = Im x - Im y
proof
let x,y be FinSequence of COMPLEX;
assume
A1: len x=len y;
then
A2: len (x-y)=len x by Th7;
A3: len x=len (x*') by Def1;
then
A4: len (x+(x*'))=len x by Th6;
A5: len y=len (y*') by Def1;
then
A6: len (y+(y*'))=len y by Th6;
thus Re (x-y)=(1/2)*((x-y)+(x*'-y*')) by A1,Th17
.=(1/2)*(x*'+(x-y)-y*') by A1,A5,A3,A2,Th31
.=(1/2)*(x*'+((x-y)-y*')) by A1,A5,A3,A2,Th31
.=(1/2)*(x*'+(x-(y+y*'))) by A1,A5,Th30
.=(1/2)*(x+x*'-(y+y*')) by A1,A3,A6,Th31
.= Re x - Re y by A1,A4,A6,Th36;
A7: len (x-(x*'))=len x by A3,Th7;
A8: len (y-(y*'))=len y by A5,Th7;
thus Im (x-y)=(-1/2*<i>)*((x-y)-(x*'-y*')) by A1,Th17
.=(-1/2*<i>)*((x-y)-x*'+y*') by A1,A5,A3,A2,Th33
.=(-1/2*<i>)*(x-(x*'+y)+y*') by A1,A3,Th30
.=(-1/2*<i>)*(x-x*'-y+y*') by A1,A3,Th30
.=(-1/2*<i>)*((x-x*')-(y-y*')) by A1,A5,A7,Th33
.=Im x - Im y by A1,A7,A8,Th36;
end;
theorem Th44:
for a, b being Complex holds a*(b*z) = (a*b)*z
proof
let a, b be Complex;
reconsider aa = a, bb = b, ab=a*b as Element of COMPLEX by XCMPLX_0:def 2;
thus (a*b)*z = (multcomplex[;](ab,id COMPLEX))*z by Lm1
.= multcomplex[;](multcomplex.(aa,bb),id COMPLEX)*z by BINOP_2:def 5
.= multcomplex[;](aa,multcomplex[;](bb,id COMPLEX))*z by FUNCOP_1:62
.= (multcomplex[;](aa,id COMPLEX)*multcomplex[;](bb,id COMPLEX))*z by
FUNCOP_1:55
.= (multcomplex[;](aa,id COMPLEX))*(multcomplex[;](bb,id COMPLEX)*z) by
RELAT_1:36
.= (multcomplex[;](aa,id COMPLEX))*(b*z) by Lm1
.= a*(b*z) by Lm1;
end;
Lm3: -(0c (len x)) = 0c (len x)
proof
-(0c (len x)) = -((len x) |-> 0c) by SEQ_4:def 12
.= compcomplex*((len x) |-> 0c) by SEQ_4:def 8
.= len x |->(compcomplex.0c) by FINSEQOP:16
.= (len x) |-> -0c by BINOP_2:def 1
.= (0c (len x)) by SEQ_4:def 12;
hence thesis;
end;
theorem Th45:
for c being Complex holds (-c)*x = -(c*x)
proof
let c be Complex;
A1: len ((-c)*x)=len x by Th3;
A2: len (c*x)=len x by Th3;
(-c)*x + c*x = (-1)*c*x + c*x .= -(c*x)+ c*x by Th44
.= -(c*x - c*x) by A2,Th32
.= -(0c (len x)) by A2,Th28
.= 0c (len x) by Lm3;
hence thesis by A1,A2,Th26;
end;
reserve h for Function of COMPLEX,COMPLEX,
g for Function of REAL,REAL;
theorem Th46:
for y1 being FinSequence of COMPLEX for y2 being FinSequence of
REAL st len y1=len y2 & (for i st i in dom y1 holds h.(y1.i)=g.(y2.i)) holds h*
y1 = g*y2
proof
let y1 be FinSequence of COMPLEX;
let y2 be FinSequence of REAL;
assume that
A1: len y1=len y2 and
A2: for i st i in dom y1 holds h.(y1.i)=g.(y2.i);
A3: len (g*y2) = len y1 by A1,FINSEQ_2:33;
now
let i be Nat;
assume that
A4: 1 <= i and
A5: i <= len (h*y1);
A6: i <= len y1 by A5,FINSEQ_2:33;
then
A7: i in dom y1 by A4,FINSEQ_3:25;
A8: i in dom (g*y2) by A3,A4,A6,FINSEQ_3:25;
i in dom (h*y1) by A4,A5,FINSEQ_3:25;
hence (h*y1).i = h.(y1.i) by FUNCT_1:12
.= g.(y2.i) by A2,A7
.= (g*y2).i by A8,FUNCT_1:12;
end;
hence thesis by A3,FINSEQ_2:33;
end;
theorem
for y1 being FinSequence of COMPLEX for y2 being FinSequence of REAL
st y1 = y2 & len y1=len y2 holds compcomplex*y1 = compreal*y2
proof
let y1 be FinSequence of COMPLEX;
let y2 be FinSequence of REAL;
assume that
A1: y1 = y2 and
A2: len y1=len y2;
for i st i in dom y1 holds compcomplex.(y1.i)=compreal.(y2.i)
proof
let i;
assume i in dom y1;
- y1.i = compcomplex.(y1.i) by BINOP_2:def 1;
hence thesis by A1,BINOP_2:def 7;
end;
hence thesis by A2,Th46;
end;
::$CT
theorem Th48:
for x being FinSequence of COMPLEX holds Re (<i>*x) = -(Im x) &
Im (<i>*x) = Re x
proof
let x be FinSequence of COMPLEX;
A1: len (x*') = len x by Def1;
A2: Im (<i>*x) =(((-1/2)*<i>))*(<i>*x-((-<i>)*(x*'))) by Th13,COMPLEX1:31
.=(((-1/2)*<i>))*(<i>*x+-(-(<i>*x*'))) by Th45
.=(((-1/2)*<i>))*(<i>*(x+x*')) by A1,Th25
.=(((-1/2)*<i>)*<i>)*(x+x*') by Th44
.=Re x;
Re (<i>*x) =(1/2)*(<i>*x+((-<i>)*(x*'))) by Th13,COMPLEX1:31
.=(1/2)*(<i>*x-(<i>*((x*')))) by Th45
.=(1/2)*(<i>*(x-(x*'))) by A1,Th36
.=(1/2*<i>)*(x-x*') by Th44
.=((-1)*((-1/2)*<i>))*(x-x*')
.=-(Im x) by Th44;
hence thesis by A2;
end;
theorem Th49:
for x,y being FinSequence of COMPLEX st len x=len y holds
|(<i>*x,y)| = <i>*(|(x,y)|)
proof
let x,y be FinSequence of COMPLEX;
assume
A1: len x=len y;
A2: len (Im y) = len y by Th40;
A3: len (Re y) = len y by Th40;
A4: len (Im x) = len x by Th40;
|(<i>*x,y)| =|(-(Im x),Re y)| - <i>*(|(Re (<i>*x),Im y)|) + <i>*(|(Im (
<i>*x),Re y)|) + |(Im (<i>*x),Im y)| by Th48
.=|(-(Im x),Re y)| - <i>*(|(-(Im x),Im y)|) + <i>*(|(Im (<i>*x),Re y)|)
+ |(Im (<i>*x),Im y)| by Th48
.=|(-(Im x),Re y)| - <i>*(|(-(Im x),Im y)|) + <i>*(|(Re x,Re y)|) + |(Im
(<i>*x),Im y)| by Th48
.=|(-(Im x),Re y)| - <i>*(|(-(Im x),Im y)|) + <i>*(|(Re x,Re y)|) + |(Re
x,Im y)| by Th48
.=-|((Im x),Re y)| - <i>*(|(-(Im x),Im y)|) + <i>*(|(Re x,Re y)|) + |(Re
x,Im y)| by A1,A3,A4,RVSUM_1:122
.=-|((Im x),Re y)| - <i>*(-|((Im x),Im y)|) + <i>*(|(Re x,Re y)|) + |(Re
x,Im y)| by A1,A4,A2,RVSUM_1:122
.=<i>*(|(x,y)|);
hence thesis;
end;
theorem Th50:
for x,y being FinSequence of COMPLEX st len x=len y holds |(x,
<i>*y)| = -<i>*(|(x,y)|)
proof
let x,y be FinSequence of COMPLEX;
assume
A1: len x=len y;
A2: len (Im x) = len x by Th40;
A3: len (Re x) = len x by Th40;
A4: len (Im y) = len y by Th40;
|(x,<i>*y)| =|(Re x,-(Im y))| - <i>*(|(Re x,Im (<i>*y))|) + <i>*(|(Im x,
Re (<i>*y))|) + |(Im x,Im (<i>*y))| by Th48
.=|(Re x,-(Im y))| - <i>*(|(Re x,Re y)|) + <i>*(|(Im x,Re (<i>*y))|) +
|(Im x,Im (<i>*y))| by Th48
.=|(Re x,-(Im y))| - <i>*(|(Re x,Re y)|) + <i>*(|(Im x,-Im y)|) + |(Im x
,Im (<i>*y))| by Th48
.=|(Re x,-(Im y))| - <i>*(|(Re x,Re y)|) + <i>*(|(Im x,-Im y)|) + |(Im x
,Re y)| by Th48
.=-|(Re x,Im y)| - <i>*(|(Re x,Re y)|) + <i>*(|(Im x,-Im y)|) + |(Im x,
Re y)| by A1,A3,A4,RVSUM_1:122
.=-|(Re x,Im y)| - <i>*(|(Re x,Re y)|) + <i>*(-(|(Im x,Im y)|)) + |(Im x
,Re y)| by A1,A2,A4,RVSUM_1:122
.=-<i>*(|(x,y)|);
hence thesis;
end;
theorem
for a1 being Element of COMPLEX,y1 being FinSequence of COMPLEX for a2
being Element of REAL,y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len
y1=len y2 holds (a1 multcomplex)*y1 = (a2 multreal)*y2
proof
let a1 be Element of COMPLEX,y1 be FinSequence of COMPLEX;
let a2 be Element of REAL,y2 be FinSequence of REAL;
assume that
A1: a1=a2 & y1 = y2 and
A2: len y1=len y2;
for i st i in dom y1 holds (a1 multcomplex).(y1.i)=(a2 multreal).(y2.i)
proof
let i;
reconsider y2i = y2.i as Element of REAL by XREAL_0:def 1;
assume i in dom y1;
A3: (a2*y2).i = a2*(y2.i) by RVSUM_1:44
.= multreal.(a2,(id REAL).(y2i)) by BINOP_2:def 11
.= (multreal[;](a2,id REAL)).(y2i) by FUNCOP_1:53
.= (a2 multreal).(y2.i) by RVSUM_1:def 3;
(a1*y1).i = a1*(y1.i) by Th12
.= multcomplex.(a1,(id COMPLEX).(y1.i)) by BINOP_2:def 5
.= (multcomplex[;](a1,id COMPLEX)).(y1.i) by FUNCOP_1:53
.= (a1 multcomplex).(y1.i) by SEQ_4:def 4;
hence thesis by A1,A3;
end;
hence thesis by A2,Th46;
end;
::$CT
theorem Th52:
for a, b being Complex holds (a+b)*z = a*z + b*z
proof
let a, b be Complex;
reconsider aa = a, bb = b, ab=a+b as Element of COMPLEX by XCMPLX_0:def 2;
set c1M = multcomplex[;](aa,id COMPLEX), c2M = multcomplex[;](bb,id COMPLEX);
thus (a + b)*z = (multcomplex[;](ab,id COMPLEX))*z by Lm1
.= multcomplex[;](addcomplex.(aa,bb),id COMPLEX)*z by BINOP_2:def 3
.= addcomplex.:(c1M,c2M)*z by FINSEQOP:35,SEQ_4:54
.= addcomplex.:(c1M*z,c2M*z) by FUNCOP_1:25
.= c1M*z + c2M*z by SEQ_4:def 6
.= a*z + c2M*z by Lm1
.= a*z + b*z by Lm1;
end;
theorem Th53:
for a, b being Complex holds (a-b)*z = a*z - b*z
proof
let a, b be Complex;
reconsider aa = a, bb = b as Element of COMPLEX by XCMPLX_0:def 2;
(a - b)*z=(a+(-b))*z .= aa*z +(-bb)*z by Th52
.= a*z - b*z by Th45;
hence thesis;
end;
theorem Th54:
for a being Element of COMPLEX,x being FinSequence of COMPLEX
holds Re (a*x) = Re a * Re x - Im a * Im x & Im (a*x) = Im a * Re x + Re a * Im
x
proof
let a be Element of COMPLEX, x be FinSequence of COMPLEX;
reconsider z5=Re a, z6=Im a as Element of COMPLEX by XCMPLX_0:def 2;
A1: len (x*') = len x by Def1;
len (1/2*z5*x) = len x by Th3;
then
A2: len ((1/2*<i>)*z6*x+1/2*z5*x) =len ((1/2*<i>)*z6*x) by Th3,Th6;
A3: len (1/2*z5*x) = len x by Th3;
A4: len (z5*x) = len x & len ((<i>*z6)*x) = len x by Th3;
A5: Re a * Re x =(z5 * (1/2))*(x+x*') by Th44
.=(z5*1/2)*x+(z5*1/2)*(x*') by A1,Th25;
A6: len Re x = len x & len (Re a * Re x)=len (Re x) by Th40,RVSUM_1:117;
A7: len ((z5-z6*<i>)*x*') = len (x*') & len ((z5 + <i>*z6)*x) = len x by Th3;
A8: len (((-1/2*<i>)*z6)*(x*')) = len (x*') by Th3;
A9: Im a * Im x =(z6 * (-1/2*<i>))*(x-x*') by Th44
.=((-1/2*<i>)*z6)*x -((-1/2*<i>)*z6)*(x*') by A1,Th36;
A10: len (((-1/2*<i>)*z6)*x) = len x by Th3;
A11: len (z5*(x*')) = len (x*') & len ((z6*<i>)*(x*')) = len (x*') by Th3;
A12: len (1/2*z5*(x*')) = len (x*') & len (((1/2*<i>)*z6)*x) = len x by Th3;
A13: Re (a*x) = (1/2)*((a*'*x*')+a*x) by Th13
.= (1/2)*((a*'*x*')+((z5) + <i>*z6)*x) by COMPLEX1:13
.= (1/2)*(((z5-z6*<i>)*x*')+(z5 + <i>*z6)*x) by COMPLEX1:def 11
.= (1/2)*((z5-z6*<i>)*x*')+(1/2)*((z5 + <i>*z6)*x) by A7,Th25,Def1
.= (1/2)*((z5-z6*<i>)*x*')+(1/2)*(z5*x + (<i>*z6)*x) by Th52
.= (1/2)*(z5*(x*')-(z6*<i>)*(x*'))+(1/2)*(z5*x + (<i>*z6)*x) by Th53
.= 1/2*(z5*(x*')-(z6*<i>)*(x*')) +(1/2*(z5*x) + 1/2*((<i>*z6)*x)) by A4
,Th25
.= ((1/2*(z5*(x*'))-1/2*((z6*<i>)*(x*')))) +(1/2*(z5*x) + 1/2*((<i>*z6)*
x)) by A11,Th36
.= 1/2*(z5*(x*'))-1/2*((<i>*z6)*(x*')) +(1/2*(z5*x) + 1/2*(<i>*z6)*x) by
Th44
.= (1/2*(z5*(x*'))+(-(1/2*<i>)*z6*(x*'))) +((1/2*(z5*x) + (1/2*<i>)*z6*x
)) by Th44
.= (1/2*(z5*(x*'))+((-1/2*<i>*z6)*(x*'))) +((1/2*(z5*x) + (1/2*<i>)*z6*x
)) by Th45
.= ((1/2*z5)*(x*')+((-1/2*<i>)*z6)*(x*')) +((1/2*(z5*x) + (1/2*<i>)*z6*x
)) by Th44
.= (1/2*z5*x + (1/2*<i>)*z6*x) + (1/2*z5*(x*') + (-1/2*<i>)*z6*(x*')) by
Th44
.= ((1/2*<i>)*z6*x+1/2*z5*x) + 1/2*z5*(x*') + (-1/2*<i>)*z6*(x*') by A1,A8
,A12,A2,Th24
.= (1/2*z5*x+1/2*z5*(x*')) +((-(-1/2*<i>)*z6)*x) +((-1/2*<i>)*z6*(x*'))
by A1,A3,A12,Th24
.= (1/2*z5*x+1/2*z5*(x*')) -((-1/2*<i>)*z6*x) +((-1/2*<i>)*z6*(x*')) by
Th45
.= Re a * Re x - Im a * Im x by A1,A5,A9,A6,A10,A8,Th33;
A14: len (((1/2*<i>)*z5)*(x*'))=len (x*') by Th3;
A15: Im a * Re x = (z6 * (1/2))*(x+x*') by Th44
.= (1/2*z6)*x+(1/2*z6)*(x*') by A1,Th25;
A16: len ((<i>*z6)*(x*')) = len (x*') & len ((-z5)*(x*')) = len (x*') by Th3;
A17: len ((1/2)*(z6*x)) = len (z6*x) by Th3;
A18: len (z6*(x*')) = len (x*') & len ((1/2)*(z6*(x*')))=len (z6*(x*')) by Th3;
then
A19: len ((1/2)*(z6*x)+(1/2)*(z6*(x*'))) = len ((1/2)*(z6*x)) by A1,A17,Th3,Th6
;
A20: len (((-1/2*<i>)*z5)*x) = len x by Th3;
then
A21: len ((1/2)*(z6*x)+((-1/2*<i>)*z5)*x) = len ((1/2)*(z6*x)) by A17,Th3,Th6;
A22: Re a * Im x = (z5 * (-1/2*<i>))*(x-x*') by Th44
.= ((-1/2*<i>)*z5)*x-((-1/2*<i>)*z5)*(x*') by A1,Th36;
A23: len (z6*x)=len x by Th3;
len ((a*x)*') = len (a*x) & len (-(a*x)*') = len ((a*x)*') by Def1,Th5;
then Im (a*x) = (-1/2*<i>)*((-((a*x)*')))+(-1/2*<i>)*(a*x) by Th25
.= (-1/2*<i>)*(-((a*')*(x*')))+(-1/2*<i>)*(a*x) by Th13
.= (-1/2*<i>)*(-((a*')*(x*'))) +(-1/2*<i>)*((z5 + <i>*z6)*x) by COMPLEX1:13
.= (-1/2*<i>)*(-((z5-z6*<i>)*x*')) +(-1/2*<i>)*((z5 + <i>*z6)*x) by
COMPLEX1:def 11
.= (-1/2*<i>)*((-(z5-z6*<i>))*x*') +(-1/2*<i>)*((z5 + <i>*z6)*x) by Th45
.= (-1/2*<i>)*((-z5+z6*<i>)*(x*')) +(-1/2*<i>)*((z5 + <i>*z6)*x)
.= (-1/2*<i>)*((-z5)*(x*')+(<i>*z6)*(x*')) +(-1/2*<i>)*((z5 + <i>*z6)*x)
by Th52
.= (-1/2*<i>)*((-z5)*(x*')+(<i>*z6)*(x*')) +(-1/2*<i>)*(z5*x + (<i>*z6)*
x) by Th52
.= (-1/2*<i>)*((-z5)*(x*')+(<i>*z6)*(x*')) +((-1/2*<i>)*(z5*x) + (-1/2*
<i>)*((<i>*z6)*x)) by A4,Th25
.= (-1/2*<i>)*((-z5)*(x*'))+(-1/2*<i>)*((<i>*z6)*(x*')) +((-1/2*<i>)*(z5
*x) + (-1/2*<i>)*((<i>*z6)*x)) by A16,Th25
.= ((-1/2*<i>)*(-z5))*(x*')+(-1/2*<i>)*((<i>*z6)*(x*')) +((-1/2*<i>)*(z5
*x) + (-1/2*<i>)*((<i>*z6)*x)) by Th44
.= ((-1/2*<i>)*(-z5))*(x*')+(-1/2*<i>)*(<i>*(z6*(x*'))) +((-1/2*<i>)*(z5
*x) + (-1/2*<i>)*((<i>*z6)*x)) by Th44
.= ((-1/2*<i>)*(-z5))*(x*')+((-1/2*<i>)*<i>)*(z6*(x*')) +((-1/2*<i>)*(z5
*x) + (-1/2*<i>)*((<i>*z6)*x)) by Th44
.= ((-1/2*<i>)*(-z5))*(x*')+((-1/2*<i>)*<i>)*(z6*(x*')) +(((-1/2*<i>)*z5
)*x + (-1/2*<i>)*((<i>*z6)*x)) by Th44
.= ((-1/2*<i>)*(-z5))*(x*')+((-1/2*<i>)*<i>)*(z6*(x*')) +(((-1/2*<i>)*z5
)*x + (-1/2*<i>)*(<i>*(z6*x))) by Th44
.= (1/2)*(z6*x)+((-1/2*<i>)*z5)*x +((1/2)*(z6*(x*'))+((1/2*<i>)*z5)*(x*'
)) by Th44
.= (1/2)*(z6*x)+(((-1/2*<i>)*z5)*x) +(1/2)*(z6*(x*'))+((1/2*<i>)*z5)*(x
*') by A1,A23,A17,A18,A14,A21,Th24
.= (1/2)*(z6*x)+(1/2)*(z6*(x*')) + (((-1/2*<i>)*z5)*x)+((1/2*<i>)*z5)*(x
*') by A1,A23,A17,A20,A18,Th24
.= (1/2*(z6*x)+(1/2)*(z6*(x*')))+((((-1/2*<i>)*z5)*x)+((1/2*<i>)*z5)*(x
*')) by A1,A23,A17,A20,A14,A19,Th24
.= (1/2*z6)*x+(1/2)*(z6*(x*')) +((((-1/2*<i>)*z5)*x)+((1/2*<i>)*z5)*(x*'
)) by Th44
.= (1/2*z6)*x+(1/2*z6)*(x*') +(((-1/2*<i>)*z5)*x+((-((-1/2*<i>)*z5))*(x
*'))) by Th44
.= Im a * Re x + Re a * Im x by A15,A22,Th45;
hence thesis by A13;
end;
begin :: The Inner Product and Conjugate of Finite Sequences
theorem Th55:
for x1,x2,y being FinSequence of COMPLEX st len x1=len x2 & len
x2=len y holds |((x1+x2),y)| = |(x1,y)| + |(x2,y)|
proof
let x1,x2,y be FinSequence of COMPLEX;
assume that
A1: len x1=len x2 and
A2: len x2=len y;
A3: len (Re x1) = len x1 & len (Re x2) = len x2 by Th40;
A4: len (Im y) = len y by Th40;
A5: len (Im x1) = len x1 & len (Im x2) = len x2 by Th40;
A6: len (Re y) = len y by Th40;
|((x1+x2),y)| = |((Re x1+ Re x2),Re y)| - <i>*(|(Re (x1+x2),Im y)|) +
<i>*(|(Im (x1+x2),Re y)|) + |(Im (x1+x2),Im y)| by A1,Th41
.= |((Re x1+ Re x2),Re y)| - <i>*(|((Re x1+Re x2),Im y)|) + <i>*(|(Im (
x1+x2),Re y)|) + |(Im (x1+x2),Im y)| by A1,Th41
.= |((Re x1+ Re x2),Re y)| - <i>*(|((Re x1+Re x2),Im y)|) + <i>*(|((Im
x1+ Im x2),Re y)|) + |(Im (x1+x2),Im y)| by A1,Th41
.= |((Re x1+ Re x2),Re y)| - <i>*(|((Re x1+Re x2),Im y)|) + <i>*(|((Im
x1+ Im x2),Re y)|) + |((Im x1+ Im x2),Im y)| by A1,Th41
.= |(Re x1,Re y)|+ |(Re x2,Re y)| - <i>*(|((Re x1+Re x2),Im y)|) + <i>*(
|((Im x1+ Im x2),Re y)|) + |((Im x1+ Im x2),Im y)| by A1,A2,A3,A6,RVSUM_1:120
.= |(Re x1,Re y)|+ |(Re x2,Re y)| - <i>*(|(Re x1,Im y)| + |(Re x2,Im y)|
) + <i>*(|((Im x1+ Im x2),Re y)|) + |((Im x1+ Im x2),Im y)| by A1,A2,A3,A4,
RVSUM_1:120
.= |(Re x1,Re y)|+ |(Re x2,Re y)| - <i>*(|(Re x1,Im y)| + |(Re x2,Im y)|
) + <i>*(|(Im x1,Re y)|+ |(Im x2,Re y)|) + |((Im x1+ Im x2),Im y)| by A1,A2,A6
,A5,RVSUM_1:120
.= |(Re x1,Re y)| + |(Re x2,Re y)| - <i>*(|(Re x1,Im y)| + |(Re x2,Im y
)|) + <i>*(|(Im x1,Re y)| + |(Im x2,Re y)|) + (|(Im x1,Im y)|+ |(Im x2,Im y)|)
by A1,A2,A5,A4,RVSUM_1:120
.= |(x1,y)| + |(x2,y)|;
hence thesis;
end;
theorem Th56:
for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds
|(-x1, x2)| = -|(x1, x2)|
proof
let x1,x2 be FinSequence of COMPLEX;
assume
A1: len x1=len x2;
A2: len (<i>*x1)=len x1 by Th3;
|(-x1, x2)| = |(<i>*<i>*x1, x2)| .= |(<i>*(<i>*x1), x2)| by Th44
.= <i>*(|(<i>*x1, x2)|) by A1,A2,Th49
.= <i>*(<i>*(|(x1, x2)|)) by A1,Th49
.= (-1)*|(x1, x2)|;
hence thesis;
end;
theorem Th57:
for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds
|(x1, -x2)| = -|(x1, x2)|
proof
let x1,x2 be FinSequence of COMPLEX;
assume
A1: len x1=len x2;
A2: len (<i>*x2)=len x2 by Th3;
|(x1, -x2)| = |(x1, <i>*<i>*x2)| .= |(x1, <i>*(<i>*x2))| by Th44
.= -<i>*(|(x1, <i>*x2)|) by A1,A2,Th50
.= -<i>*(-<i>*(|(x1, x2)|)) by A1,Th50
.= -(|(x1, x2)|);
hence thesis;
end;
theorem
for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds
|(-x1, -x2)| = |(x1, x2)|
proof
let x1,x2 be FinSequence of COMPLEX;
assume
A1: len x1=len x2;
then len (-x2)=len x1 by Th5;
then |(-x1, -x2)| = -|(x1, -x2)| by Th56
.= --|(x1, x2)| by A1,Th57;
hence thesis;
end;
theorem Th59:
for x1,x2,x3 being FinSequence of COMPLEX st
len x1=len x2 & len x2=len x3 holds
|(x1-x2, x3)| = |(x1, x3)| - |(x2, x3)|
proof
let x1,x2,x3 be FinSequence of COMPLEX;
assume that
A1: len x1=len x2 and
A2: len x2=len x3;
len (-x2)=len x2 by Th5;
then |(x1 - x2, x3)| = |(x1, x3)| + |(-x2, x3)| by A1,A2,Th55
.= |(x1, x3)| + - |(x2, x3)| by A2,Th56;
hence thesis;
end;
theorem Th60:
for x,y1,y2 being FinSequence of COMPLEX st
len x=len y1 & len y1=len y2 holds |(x, y1+y2)| = |(x, y1)| + |(x, y2)|
proof
let x,y1,y2 be FinSequence of COMPLEX;
assume that
A1: len x=len y1 and
A2: len y1=len y2;
A3: len (Re y1) = len y1 & len (Re y2) = len y2 by Th40;
A4: len (Im x) = len x by Th40;
A5: len (Im y1) = len y1 & len (Im y2) = len y2 by Th40;
A6: len (Re x) = len x by Th40;
|(x,(y1+y2))| = |(Re x,(Re y1+ Re y2))| - <i>*(|(Re x,Im (y1+y2))|) +
<i>*(|(Im x,Re (y1+y2))|) + |(Im x,Im (y1+y2))| by A2,Th41
.= |(Re x,(Re y1+ Re y2))| - <i>*(|(Re x,Im (y1+y2))|) + <i>*(|(Im x,Re
(y1+y2))|) + |(Im x,(Im y1+Im y2))| by A2,Th41
.= |(Re x,(Re y1+ Re y2))| - <i>*(|(Re x,(Im y1+Im y2))|) + <i>*(|(Im x,
Re (y1+y2))|) + |(Im x,(Im y1+Im y2))| by A2,Th41
.= |(Re x,(Re y1+ Re y2))| - <i>*(|(Re x,(Im y1+Im y2))|) + <i>*(|(Im x,
(Re y1+Re y2))|) + |(Im x,(Im y1+Im y2))| by A2,Th41
.= |(Re x,Re y1)|+ |(Re x,Re y2)| - <i>*(|(Re x,(Im y1+Im y2))|) + <i>*(
|(Im x,(Re y1+Re y2))|) + |(Im x,(Im y1+Im y2))| by A1,A2,A3,A6,RVSUM_1:120
.= |(Re x,Re y1)|+ |(Re x,Re y2)| - <i>*(|(Re x,(Im y1+Im y2))|) + <i>*(
|(Im x,(Re y1+Re y2))|) + (|(Im x,Im y1)|+|(Im x,Im y2)|) by A1,A2,A5,A4,
RVSUM_1:120
.= |(Re x,Re y1)|+ |(Re x,Re y2)| - <i>*(|(Re x,Im y1)|+|(Re x,Im y2)|)
+ <i>*(|(Im x,(Re y1+Re y2))|) + (|(Im x,Im y1)|+|(Im x,Im y2)|) by A1,A2,A6,A5
,RVSUM_1:120
.= |(Re x,Re y1)|+ |(Re x,Re y2)| - <i>*(|(Re x,Im y1)|+|(Re x,Im y2)|)
+ <i>*(|(Im x,Re y1)|+|(Im x,Re y2)|) + (|(Im x,Im y1)|+|(Im x,Im y2)|) by A1
,A2,A3,A4,RVSUM_1:120
.= |(x,y1)| + |(x,y2)|;
hence thesis;
end;
theorem Th61:
for x,y1,y2 being FinSequence of COMPLEX st len x=len y1 & len y1=len y2
holds |(x, y1-y2)| = |(x, y1)| - |(x, y2)|
proof
let x,y1,y2 be FinSequence of COMPLEX;
assume that
A1: len x=len y1 and
A2: len y1=len y2;
A3: len (Re y1) = len y1 & len (Re y2) = len y2 by Th40;
A4: len (Im x) = len x by Th40;
A5: len (Im y1) = len y1 & len (Im y2) = len y2 by Th40;
A6: len (Re x) = len x by Th40;
|(x,(y1-y2))| = |(Re x,(Re y1- Re y2))| - <i>*(|(Re x,Im (y1-y2))|) +
<i>*(|(Im x,Re (y1-y2))|) + |(Im x,Im (y1-y2))| by A2,Th43
.= |(Re x,(Re y1- Re y2))| - <i>*(|(Re x,Im (y1-y2))|) + <i>*(|(Im x,Re
(y1-y2))|) + |(Im x,(Im y1-Im y2))| by A2,Th43
.= |(Re x,(Re y1- Re y2))| - <i>*(|(Re x,(Im y1-Im y2))|) + <i>*(|(Im x,
Re (y1-y2))|) + |(Im x,(Im y1-Im y2))| by A2,Th43
.= |(Re x,(Re y1- Re y2))| - <i>*(|(Re x,(Im y1-Im y2))|) + <i>*(|(Im x,
(Re y1-Re y2))|) + |(Im x,(Im y1-Im y2))| by A2,Th43
.= |(Re x,Re y1)|- |(Re x,Re y2)| - <i>*(|(Re x,(Im y1-Im y2))|) + <i>*(
|(Im x,(Re y1-Re y2))|) + |(Im x,(Im y1-Im y2))| by A1,A2,A3,A6,RVSUM_1:124
.= |(Re x,Re y1)|- |(Re x,Re y2)| - <i>*(|(Re x,(Im y1-Im y2))|) + <i>*(
|(Im x,(Re y1-Re y2))|) + (|(Im x,Im y1)|-|(Im x,Im y2)|) by A1,A2,A5,A4,
RVSUM_1:124
.= |(Re x,Re y1)|- |(Re x,Re y2)| - <i>*(|(Re x,Im y1)|-|(Re x,Im y2)|)
+ <i>*(|(Im x,(Re y1-Re y2))|) + (|(Im x,Im y1)|-|(Im x,Im y2)|) by A1,A2,A6,A5
,RVSUM_1:124
.= |(Re x,Re y1)|- |(Re x,Re y2)| - <i>*(|(Re x,Im y1)|-|(Re x,Im y2)|)
+ <i>*(|(Im x,Re y1)|-|(Im x,Re y2)|) + (|(Im x,Im y1)|-|(Im x,Im y2)|) by A1
,A2,A3,A4,RVSUM_1:124
.= |(x,y1)| - |(x,y2)|;
hence thesis;
end;
theorem Th62:
for x1,x2,y1,y2 being FinSequence of COMPLEX st len x1=len x2 &
len x2=len y1 & len y1=len y2 holds
|(x1+x2, y1+y2)| = |(x1, y1)| + |(x1, y2)| + |(x2, y1)| + |(x2, y2)|
proof
let x1,x2,y1,y2 be FinSequence of COMPLEX;
assume that
A1: len x1=len x2 and
A2: len x2=len y1 and
A3: len y1=len y2;
|(x1+x2, y2)| = |(x1, y2)| + |(x2, y2)| by A1,A2,A3,Th55;
then
A4: |(x1+x2, y1)| + |(x1+x2, y2)| = (|(x1, y1)|+|(x2, y1)|) + (|(x1, y2)| +
|(x2, y2)|) by A1,A2,Th55;
len (x1+x2)=len x1 by A1,Th6;
hence thesis by A1,A2,A3,A4,Th60;
end;
theorem Th63:
for x1,x2,y1,y2 being FinSequence of COMPLEX st
len x1=len x2 & len x2=len y1 & len y1=len y2 holds
|(x1-x2, y1-y2)| = |(x1, y1)| - |(x1, y2)| - |(x2, y1)| + |(x2, y2)|
proof
let x1,x2,y1,y2 be FinSequence of COMPLEX;
assume that
A1: len x1=len x2 and
A2: len x2=len y1 and
A3: len y1=len y2;
|(x1,y1-y2)| = |(x1,y1)| - |(x1,y2)| by A1,A2,A3,Th61; then
A4: |(x1,y1-y2)| - |(x2,y1-y2)| = (|(x1,y1)|-|(x1,y2)|)-(|(x2,y1)|-|(x2,y2)|
) by A2,A3,Th61;
len (y1 - y2)=len y1 by A3,Th7;
hence thesis by A1,A2,A4,Th59;
end;
theorem Th64:
for x,y being FinSequence of COMPLEX holds |(x,y)| = (|(y,x)|)*'
proof
let x,y be FinSequence of COMPLEX;
set x1=|(Re y,Re x)|,x2=|(Re y,Im x)|,y1=|(Im y,Re x)|, y2=|(Im y,Im x)|;
reconsider x19=x1, x29=x2, y19=y1, y29=y2 as Element of REAL
by XREAL_0:def 1;
A1: Im x19=0 by COMPLEX1:def 2;
A2: Im x29=0 by COMPLEX1:def 2;
A3: Im y29=0 by COMPLEX1:def 2;
A4: Im y19=0 by COMPLEX1:def 2;
reconsider x19=x1, x29=x2, y19=y1, y29=y2 as Element of COMPLEX by
XCMPLX_0:def 2;
(|(y,x)|)*' =(x19 + y29 + <i>*((y19) - (x29)))*'
.=(x19 + y29)*' + (<i>*((y19) - (x29)))*' by COMPLEX1:32
.=(x19)*' + (y29)*' + (<i>*((y19) - (x29)))*' by COMPLEX1:32
.=x19 + (y29)*' + (<i>*((y19) - (x29)))*' by A1,COMPLEX1:38
.=x19 + y29 + (<i>*((y19) - (x29)))*' by A3,COMPLEX1:38
.=x19 + y29 + (-<i>)*((y19) - (x29))*' by COMPLEX1:31,35
.=x19 + y29 + (-<i>)*((y19)*' - (x29)*') by COMPLEX1:34
.=x19 + y29 + (-<i>)*((y19) - (x29)*') by A4,COMPLEX1:38
.=x19 + y29 + (-<i>)*((y19) - (x29)) by A2,COMPLEX1:38
.=|(x, y)|;
hence thesis;
end;
theorem
for x,y being FinSequence of COMPLEX st len x=len y holds
|(x+y,x+y)| = |(x,x)| + 2*Re(|(x,y)|) + |(y,y)|
proof
let x,y be FinSequence of COMPLEX;
set z=|(x, y)|;
assume len x=len y;
then |(x+y, x+y)| =|(x, x)| + |(x, y)| + |(y, x)| + |(y, y)| by Th62
.=|(x, x)| + |(x, y)| + (|(x, y)|)*' + |(y, y)| by Th64
.=|(x, x)| + (z+z*') + |(y, y)|
.=|(x, x)| + 2*Re(|(x, y)|) + |(y, y)| by Th20;
hence thesis;
end;
theorem
for x,y being FinSequence of COMPLEX st len x=len y holds
|(x-y, x-y)| = |(x, x)| - 2*Re(|(x, y)|) + |(y, y)|
proof
let x,y be FinSequence of COMPLEX;
set z=|(x, y)|;
assume len x=len y;
then |(x-y, x-y)| =|(x, x)| - |(x, y)| - |(y, x)| + |(y, y)| by Th63
.=|(x, x)| - |(x, y)| - (|(x, y)|)*' + |(y, y)| by Th64
.=|(x, x)| - (z + z*') + |(y, y)|
.=|(x, x)| - 2*Re(|(x, y)|) + |(y, y)| by Th20;
hence thesis;
end;
theorem Th67:
for a being Element of COMPLEX, x,y being FinSequence of COMPLEX
st len x=len y holds |(a*x,y)| = a*(|(x,y)|)
proof
let a be Element of COMPLEX, x,y be FinSequence of COMPLEX;
assume
A1: len x=len y;
A2: len (Re a * Im x) = len (Im x) & len (Im a * Re x) = len (Re x) by
RVSUM_1:117;
A3: len (Re a * Re x) = len (Re x) & len (Im a * Im x) = len (Im x) by
RVSUM_1:117;
A4: len (Re x) = len x by Th40;
A5: len (Im y) = len y by Th40;
A6: len (Re y) = len y by Th40;
A7: len (Im x) = len x by Th40;
|(a*x,y)| = |((Re a * Re x - Im a * Im x),Re y)| - <i>*(|(Re (a*x),Im y
)|) + <i>*(|(Im (a*x),Re y)|) + |(Im (a*x),Im y)| by Th54
.= |((Re a * Re x - Im a * Im x),Re y)| - <i>*(|((Re a * Re x - Im a *
Im x),Im y)|) + <i>*(|(Im (a*x),Re y)|) + |(Im (a*x),Im y)| by Th54
.= |((Re a * Re x - Im a * Im x),Re y)| - <i>*(|((Re a * Re x - Im a *
Im x),Im y)|) + <i>*(|((Im a * Re x + Re a * Im x),Re y)|) + |(Im (a*x),Im y)|
by Th54
.= |((Re a * Re x - Im a * Im x),Re y)| - <i>*(|((Re a * Re x - Im a *
Im x),Im y)|) + <i>*(|((Im a * Re x + Re a * Im x),Re y)|) + (|((Im a * Re x +
Re a * Im x),Im y)|) by Th54
.= |(Re a * Re x,Re y)|-|(Im a * Im x,Re y)| - <i>*(|((Re a * Re x - Im
a * Im x),Im y)|) + <i>*(|((Im a * Re x + Re a * Im x),Re y)|) + (|((Im a * Re
x + Re a * Im x),Im y)|) by A1,A4,A6,A7,A3,RVSUM_1:124
.= |(Re a * Re x,Re y)|-|(Im a * Im x,Re y)| - <i>*((|(Re a * Re x,Im y
)|)-(|(Im a * Im x,Im y)|)) + <i>*(|((Im a * Re x + Re a * Im x),Re y)|) + (|((
Im a * Re x + Re a * Im x),Im y)|) by A1,A4,A7,A5,A3,RVSUM_1:124
.= |(Re a * Re x,Re y)|-|(Im a * Im x,Re y)| - <i>*((|(Re a * Re x,Im y
)|)-(|(Im a * Im x,Im y)|)) + <i>*((|(Im a * Re x,Re y)|)+(|(Re a * Im x,Re y)|
)) + (|((Im a * Re x + Re a * Im x),Im y)|) by A1,A4,A6,A7,A2,RVSUM_1:120
.= |(Re a * Re x,Re y)|-|(Im a * Im x,Re y)| - <i>*((|(Re a * Re x,Im y
)|)-(|(Im a * Im x,Im y)|)) + <i>*((|(Im a * Re x,Re y)|)+(|(Re a * Im x,Re y)|
)) + ((|(Im a * Re x,Im y)|)+(|(Re a * Im x,Im y)|)) by A1,A4,A7,A5,A2,
RVSUM_1:120
.= |(Re a * Re x,Re y)|-|(Im a * Im x,Re y)| - <i>*((Re a * (|(Re x,Im y
)|))-(|(Im a * Im x,Im y)|)) + <i>*((|(Im a * Re x,Re y)|)+(|(Re a * Im x,Re y
)|)) + ((|(Im a * Re x,Im y)|)+(|(Re a * Im x,Im y)|)) by A1,A4,A5,RVSUM_1:121
.= |(Re a * Re x,Re y)|-|(Im a * Im x,Re y)| - <i>*((Re a * (|(Re x,Im y
)|))-Im a * (|(Im x,Im y)|)) + <i>*((|(Im a * Re x,Re y)|)+(|(Re a * Im x,Re y
)|)) + ((|(Im a * Re x,Im y)|)+(|(Re a * Im x,Im y)|)) by A1,A7,A5,RVSUM_1:121
.= Re a * (|(Re x,Re y)|)-|(Im a * Im x,Re y)| - <i>*((Re a * (|(Re x,Im
y)|))-Im a * (|(Im x,Im y)|)) + <i>*((|(Im a * Re x,Re y)|)+(|(Re a * Im x,Re y
)|)) + ((|(Im a * Re x,Im y)|)+(|(Re a * Im x,Im y)|)) by A1,A4,A6,RVSUM_1:121
.= Re a * (|(Re x,Re y)|)-Im a * (|(Im x,Re y)|) - <i>*((Re a * (|(Re x,
Im y)|))-Im a * (|(Im x,Im y)|)) + <i>*((|(Im a * Re x,Re y)|)+(|(Re a * Im x,
Re y)|)) + ((|(Im a * Re x,Im y)|)+(|(Re a * Im x,Im y)|)) by A1,A6,A7,
RVSUM_1:121
.= Re a * (|(Re x,Re y)|)-Im a * (|(Im x,Re y)|) - <i>*((Re a * (|(Re x,
Im y)|))-Im a * (|(Im x,Im y)|)) + <i>*(Im a * (|(Re x,Re y)|)+(|(Re a * Im x,
Re y)|)) + ((|(Im a * Re x,Im y)|)+(|(Re a * Im x,Im y)|)) by A1,A4,A6,
RVSUM_1:121
.= Re a * (|(Re x,Re y)|)-Im a * (|(Im x,Re y)|) - <i>*((Re a * (|(Re x,
Im y)|))-Im a * (|(Im x,Im y)|)) + <i>*(Im a * (|(Re x,Re y)|)+Re a * (|(Im x,
Re y)|)) + ((|(Im a * Re x,Im y)|)+(|(Re a * Im x,Im y)|)) by A1,A6,A7,
RVSUM_1:121
.= Re a * (|(Re x,Re y)|)-Im a * (|(Im x,Re y)|) - <i>*((Re a * (|(Re x,
Im y)|))-Im a * (|(Im x,Im y)|)) + <i>*(Im a * (|(Re x,Re y)|)+Re a * (|(Im x,
Re y)|)) + (Im a * (|(Re x,Im y)|)+(|(Re a * Im x,Im y)|)) by A1,A4,A5,
RVSUM_1:121
.= Re a * (|(Re x,Re y)|)-Im a * (|(Im x,Re y)|) - <i>*((Re a * (|(Re x,
Im y)|))-Im a * (|(Im x,Im y)|)) + <i>*(Im a * (|(Re x,Re y)|)+Re a * (|(Im x,
Re y)|)) + (Im a * (|(Re x,Im y)|)+Re a * (|(Im x,Im y)|)) by A1,A7,A5,
RVSUM_1:121
.= Re a*(|(Re x,Re y)|) + <i>*(Im a)*(|(Re x,Re y)|) - Re a*<i>*(|(Re x,
Im y)|) + (Im a)*(|(Re x,Im y)|) + (Re a*(<i>*(|(Im x,Re y)|)) - (Im a)*(|(Im x
,Re y)|)) + (Re a + <i>*(Im a))*(|(Im x,Im y)|)
.= Re a*(|(Re x,Re y)|) + <i>*(Im a)*(|(Re x,Re y)|) - Re a*<i>*(|(Re x,
Im y)|) + (Im a)*(|(Re x,Im y)|) + (Re a + <i>*(Im a))*(<i>*(|(Im x,Re y)|)) +
a*(|(Im x,Im y)|) by COMPLEX1:13
.= Re a*(|(Re x,Re y)|) + <i>*(Im a)*(|(Re x,Re y)|) - (Re a + <i>*(Im a
))*(<i>*(|(Re x,Im y)|)) + a*(<i>*(|(Im x,Re y)|)) + a*(|(Im x,Im y)|) by
COMPLEX1:13
.= (Re a + <i>*(Im a))*(|(Re x,Re y)|) - a*(<i>*(|(Re x,Im y)|)) + a*(
<i>*(|(Im x,Re y)|)) + a*(|(Im x,Im y)|) by COMPLEX1:13
.= a*(|(Re x,Re y)|) - a*(<i>*(|(Re x,Im y)|)) + a*(<i>*(|(Im x,Re y)|))
+ a*(|(Im x,Im y)|) by COMPLEX1:13
.= a*(|(x,y)|);
hence thesis;
end;
theorem Th68:
for a being Element of COMPLEX, x,y being FinSequence of COMPLEX
st len x=len y holds |(x,a*y)| = (a*')*(|(x,y)|)
proof
let a be Element of COMPLEX, x,y be FinSequence of COMPLEX;
assume
A1: len x=len y;
|(x,a*y)|=(|(a*y,x)|)*' by Th64
.=(a*|(y,x)|)*' by A1,Th67
.=(a*')*(|(y,x)|)*' by COMPLEX1:35
.=(a*')*(|(x,y)|) by Th64;
hence thesis;
end;
theorem
for a,b being Element of COMPLEX,x,y,z being FinSequence of COMPLEX st
len x=len y & len y=len z holds |((a*x+b*y), z)| = a*|(x,z)| + b*|(y,z)|
proof
let a,b be Element of COMPLEX,x,y,z be FinSequence of COMPLEX;
assume that
A1: len x=len y and
A2: len y=len z;
len (a*x)=len x & len (b*y)=len y by Th3;
then |(a*x + b*y, z)| = |(a*x, z)| + |(b*y, z)| by A1,A2,Th55
.= a*|(x,z)| + |(b*y,z)| by A1,A2,Th67
.= a*|(x,z)| + b*|(y,z)| by A2,Th67;
hence thesis;
end;
theorem
for a,b being Element of COMPLEX,x,y,z being FinSequence of COMPLEX st
len x=len y & len y=len z holds |(x,a*y+b*z)| = (a*')*|(x,y)| + (b*')*|(x,z)|
proof
let a,b be Element of COMPLEX,x,y,z be FinSequence of COMPLEX;
assume that
A1: len x=len y and
A2: len y=len z;
len (a*y)=len y & len (b*z)=len z by Th3;
then |(x,a*y+b*z)| = |(x, a*y)| + |(x, b*z)| by A1,A2,Th60
.= (a*')*|(x,y)| + |(x,b*z)| by A1,Th68
.= (a*')*|(x,y)| + (b*')*|(x,z)| by A1,A2,Th68;
hence thesis;
end;