let x, y, z be Point of Complex_l2_Space; :: thesis: for a being Complex holds
( ( x .|. x = 0 implies x = 0. Complex_l2_Space ) & ( x = 0. Complex_l2_Space implies x .|. x = 0 ) & Re (x .|. x) >= 0 & Im (x .|. x) = 0 & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
let a be Complex; :: thesis: ( ( x .|. x = 0 implies x = 0. Complex_l2_Space ) & ( x = 0. Complex_l2_Space implies x .|. x = 0 ) & Re (x .|. x) >= 0 & Im (x .|. x) = 0 & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
set seqx = seq_id x;
A1: x .|. x = Sum ((seq_id x) (#) ((seq_id x) *')) by CSSPACE:def 17;
A2: (seq_id x) (#) ((seq_id x) *') is absolutely_summable by Lm19;
then Sum ((seq_id x) (#) ((seq_id x) *')) = (Sum (Re ((seq_id x) (#) ((seq_id x) *')))) + ((Sum (Im ((seq_id x) (#) ((seq_id x) *')))) * <i>) by COMSEQ_3:53;
then A3: ( Re (x .|. x) = Sum (Re ((seq_id x) (#) ((seq_id x) *'))) & Im (x .|. x) = Sum (Im ((seq_id x) (#) ((seq_id x) *'))) ) by A1, COMPLEX1:12;
A4: now :: thesis: ( x .|. x = 0 implies x = 0. Complex_l2_Space )
set seq = seq_id x;
A5: x .|. x = Sum ((seq_id x) (#) ((seq_id x) *')) by CSSPACE:def 17;
set rseq = Re ((seq_id x) (#) ((seq_id x) *'));
A6: for n being Nat holds (Re ((seq_id x) (#) ((seq_id x) *'))) . n = ((Re ((seq_id x) . n)) ^2) + ((Im ((seq_id x) . n)) ^2)
proof
let n be Nat; :: thesis: (Re ((seq_id x) (#) ((seq_id x) *'))) . n = ((Re ((seq_id x) . n)) ^2) + ((Im ((seq_id x) . n)) ^2)
A7: n in NAT by ORDINAL1:def 12;
(Re ((seq_id x) (#) ((seq_id x) *'))) . n = (((Re (seq_id x)) (#) (Re ((seq_id x) *'))) - ((Im (seq_id x)) (#) (Im ((seq_id x) *')))) . n by COMSEQ_3:21
.= (((Re (seq_id x)) (#) (Re ((seq_id x) *'))) . n) + ((- ((Im (seq_id x)) (#) (Im ((seq_id x) *')))) . n) by SEQ_1:7
.= (((Re (seq_id x)) (#) (Re ((seq_id x) *'))) . n) + (- (((Im (seq_id x)) (#) (Im ((seq_id x) *'))) . n)) by SEQ_1:10
.= (((Re (seq_id x)) (#) (Re ((seq_id x) *'))) . n) - (((Im (seq_id x)) (#) (Im ((seq_id x) *'))) . n)
.= (((Re (seq_id x)) . n) * ((Re ((seq_id x) *')) . n)) - (((Im (seq_id x)) (#) (Im ((seq_id x) *'))) . n) by SEQ_1:8
.= (((Re (seq_id x)) . n) * ((Re ((seq_id x) *')) . n)) - (((Im (seq_id x)) . n) * ((Im ((seq_id x) *')) . n)) by SEQ_1:8
.= ((Re ((seq_id x) . n)) * ((Re ((seq_id x) *')) . n)) - (((Im (seq_id x)) . n) * ((Im ((seq_id x) *')) . n)) by COMSEQ_3:def 5
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) *') . n))) - (((Im (seq_id x)) . n) * ((Im ((seq_id x) *')) . n)) by COMSEQ_3:def 5
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) *') . n))) - ((Im ((seq_id x) . n)) * ((Im ((seq_id x) *')) . n)) by COMSEQ_3:def 6
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) *') . n))) - ((Im ((seq_id x) . n)) * (Im (((seq_id x) *') . n))) by COMSEQ_3:def 6
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) . n) *'))) - ((Im ((seq_id x) . n)) * (Im (((seq_id x) *') . n))) by COMSEQ_2:def 2, A7
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) . n) *'))) - ((Im ((seq_id x) . n)) * (Im (((seq_id x) . n) *'))) by COMSEQ_2:def 2, A7
.= ((Re ((seq_id x) . n)) * (Re ((seq_id x) . n))) - ((Im ((seq_id x) . n)) * (Im (((seq_id x) . n) *'))) by COMPLEX1:27
.= ((Re ((seq_id x) . n)) * (Re ((seq_id x) . n))) - ((Im ((seq_id x) . n)) * (- (Im ((seq_id x) . n)))) by COMPLEX1:27
.= ((Re ((seq_id x) . n)) ^2) + ((Im ((seq_id x) . n)) * (Im ((seq_id x) . n))) ;
hence (Re ((seq_id x) (#) ((seq_id x) *'))) . n = ((Re ((seq_id x) . n)) ^2) + ((Im ((seq_id x) . n)) ^2) ; :: thesis: verum
end;
A8: for n being Nat holds 0 <= (Re ((seq_id x) (#) ((seq_id x) *'))) . n
proof
let n be Nat; :: thesis: 0 <= (Re ((seq_id x) (#) ((seq_id x) *'))) . n
A9: (Im ((seq_id x) . n)) ^2 >= 0 by XREAL_1:63;
( (Re ((seq_id x) (#) ((seq_id x) *'))) . n = ((Re ((seq_id x) . n)) ^2) + ((Im ((seq_id x) . n)) ^2) & (Re ((seq_id x) . n)) ^2 >= 0 ) by A6, XREAL_1:63;
then (Re ((seq_id x) (#) ((seq_id x) *'))) . n >= 0 + 0 by A9;
hence 0 <= (Re ((seq_id x) (#) ((seq_id x) *'))) . n ; :: thesis: verum
end;
A10: (seq_id x) (#) ((seq_id x) *') is absolutely_summable by Lm19;
assume x .|. x = 0 ; :: thesis: x = 0. Complex_l2_Space
then (Sum (Re ((seq_id x) (#) ((seq_id x) *')))) + ((Sum (Im ((seq_id x) (#) ((seq_id x) *')))) * <i>) = 0 by A5, A10, COMSEQ_3:53;
then A11: Sum (Re ((seq_id x) (#) ((seq_id x) *'))) = 0 by COMPLEX1:4, COMPLEX1:12;
A12: for n being Nat holds (seq_id x) . n = 0
proof
let n be Nat; :: thesis: (seq_id x) . n = 0
(Re ((seq_id x) (#) ((seq_id x) *'))) . n = ((Re ((seq_id x) . n)) ^2) + ((Im ((seq_id x) . n)) ^2) by A6;
then ((Re ((seq_id x) . n)) ^2) + ((Im ((seq_id x) . n)) ^2) = 0 by A10, A11, A8, RSSPACE:17;
hence (seq_id x) . n = 0 by COMPLEX1:5; :: thesis: verum
end;
x is Element of the_set_of_ComplexSequences by CSSPACE:def 11;
hence x = 0. Complex_l2_Space by A12, Lm10, CSSPACE:5; :: thesis: verum
end;
A13: now :: thesis: ( x = 0. Complex_l2_Space implies x .|. x = 0 )
assume A14: x = 0. Complex_l2_Space ; :: thesis: x .|. x = 0
A15: for n being Nat holds ((seq_id x) (#) ((seq_id x) *')) . n = 0
proof
let n be Nat; :: thesis: ((seq_id x) (#) ((seq_id x) *')) . n = 0
thus ((seq_id x) (#) ((seq_id x) *')) . n = ((seq_id x) . n) * (((seq_id x) *') . n) by VALUED_1:5
.= 0c * (((seq_id x) *') . n) by A14, Lm10, CSSPACE:4
.= 0 ; :: thesis: verum
end;
thus x .|. x = Sum ((seq_id x) (#) ((seq_id x) *')) by CSSPACE:def 17
.= 0 by A15, CSSPACE:80 ; :: thesis: verum
end;
set seqy = seq_id y;
A16: for n being Nat holds 0 <= (Re ((seq_id x) (#) ((seq_id x) *'))) . n
proof
let n be Nat; :: thesis: 0 <= (Re ((seq_id x) (#) ((seq_id x) *'))) . n
A17: n in NAT by ORDINAL1:def 12;
A18: ( (Re ((seq_id x) . n)) ^2 >= 0 & (Im ((seq_id x) . n)) ^2 >= 0 ) by XREAL_1:63;
(Re ((seq_id x) (#) ((seq_id x) *'))) . n = Re (((seq_id x) (#) ((seq_id x) *')) . n) by COMSEQ_3:def 5
.= Re (((seq_id x) . n) * (((seq_id x) *') . n)) by VALUED_1:5
.= Re (((seq_id x) . n) * (((seq_id x) . n) *')) by COMSEQ_2:def 2, A17
.= ((Re ((seq_id x) . n)) ^2) + ((Im ((seq_id x) . n)) ^2) by COMPLEX1:40 ;
then (Re ((seq_id x) (#) ((seq_id x) *'))) . n >= 0 + 0 by A18;
hence 0 <= (Re ((seq_id x) (#) ((seq_id x) *'))) . n ; :: thesis: verum
end;
|.(seq_id x).| (#) |.(seq_id y).| is summable by Lm16;
then |.((seq_id x) *').| (#) |.(seq_id y).| is summable by Lm18;
then |.(((seq_id x) *') (#) (seq_id y)).| is summable by COMSEQ_1:46;
then A19: ((seq_id x) *') (#) (seq_id y) is absolutely_summable by COMSEQ_3:def 9;
set seqz = seq_id z;
A20: for n being Nat holds (Im ((seq_id x) (#) ((seq_id x) *'))) . n = 0
proof
let n be Nat; :: thesis: (Im ((seq_id x) (#) ((seq_id x) *'))) . n = 0
A21: n in NAT by ORDINAL1:def 12;
(Im ((seq_id x) (#) ((seq_id x) *'))) . n = Im (((seq_id x) (#) ((seq_id x) *')) . n) by COMSEQ_3:def 6
.= Im (((seq_id x) . n) * (((seq_id x) *') . n)) by VALUED_1:5
.= Im (((seq_id x) . n) * (((seq_id x) . n) *')) by COMSEQ_2:def 2, A21 ;
hence (Im ((seq_id x) (#) ((seq_id x) *'))) . n = 0 by COMPLEX1:40; :: thesis: verum
end;
|.(seq_id x).| (#) |.(seq_id z).| is summable by Lm16;
then |.(seq_id x).| (#) |.((seq_id z) *').| is summable by Lm18;
then |.((seq_id x) (#) ((seq_id z) *')).| is summable by COMSEQ_1:46;
then A22: (seq_id x) (#) ((seq_id z) *') is absolutely_summable by COMSEQ_3:def 9;
|.(seq_id y).| (#) |.(seq_id z).| is summable by Lm16;
then |.(seq_id y).| (#) |.((seq_id z) *').| is summable by Lm18;
then |.((seq_id y) (#) ((seq_id z) *')).| is summable by COMSEQ_1:46;
then A23: (seq_id y) (#) ((seq_id z) *') is absolutely_summable by COMSEQ_3:def 9;
A24: (x + y) .|. z = Sum ((seq_id (x + y)) (#) ((seq_id z) *')) by CSSPACE:def 17
.= Sum ((seq_id ((seq_id x) + (seq_id y))) (#) ((seq_id z) *')) by Lm12
.= Sum (((seq_id x) (#) ((seq_id z) *')) + ((seq_id y) (#) ((seq_id z) *'))) by COMSEQ_1:10
.= (Sum ((seq_id x) (#) ((seq_id z) *'))) + (Sum ((seq_id y) (#) ((seq_id z) *'))) by A22, A23, COMSEQ_3:54
.= ( the scalar of Complex_l2_Space . (x,z)) + (Sum ((seq_id y) (#) ((seq_id z) *'))) by CSSPACE:def 17
.= (x .|. z) + (y .|. z) by CSSPACE:def 17 ;
|.(seq_id x).| (#) |.(seq_id y).| is summable by Lm16;
then |.(seq_id x).| (#) |.((seq_id y) *').| is summable by Lm18;
then |.((seq_id x) (#) ((seq_id y) *')).| is summable by COMSEQ_1:46;
then A25: (seq_id x) (#) ((seq_id y) *') is absolutely_summable by COMSEQ_3:def 9;
A26: (a * x) .|. y = Sum ((seq_id (a * x)) (#) ((seq_id y) *')) by CSSPACE:def 17
.= Sum ((seq_id (a (#) (seq_id x))) (#) ((seq_id y) *')) by Lm13
.= Sum (a (#) ((seq_id x) (#) ((seq_id y) *'))) by COMSEQ_1:12
.= a * (Sum ((seq_id x) (#) ((seq_id y) *'))) by A25, COMSEQ_3:56
.= a * (x .|. y) by CSSPACE:def 17 ;
x .|. y = Sum ((((seq_id x) *') *') (#) ((seq_id y) *')) by CSSPACE:def 17
.= Sum ((((seq_id x) *') (#) (seq_id y)) *') by COMSEQ_2:5
.= (Sum (((seq_id x) *') (#) (seq_id y))) *' by A19, Lm5
.= (y .|. x) *' by CSSPACE:def 17 ;
hence ( ( x .|. x = 0 implies x = 0. Complex_l2_Space ) & ( x = 0. Complex_l2_Space implies x .|. x = 0 ) & Re (x .|. x) >= 0 & Im (x .|. x) = 0 & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) ) by A4, A13, A2, A3, A16, A20, A24, A26, RSSPACE:16, SERIES_1:18; :: thesis: verum