let n be non empty Nat; :: thesis: for x, y being Element of REAL n
for a being Real holds
( 0 <= (sum_norm n) . x & ( (sum_norm n) . x = 0 implies x = 0* n ) & ( x = 0* n implies (sum_norm n) . x = 0 ) & (sum_norm n) . (a * x) = |.a.| * ((sum_norm n) . x) & (sum_norm n) . (x + y) <= ((sum_norm n) . x) + ((sum_norm n) . y) )
let x, y be Element of REAL n; :: thesis: for a being Real holds
( 0 <= (sum_norm n) . x & ( (sum_norm n) . x = 0 implies x = 0* n ) & ( x = 0* n implies (sum_norm n) . x = 0 ) & (sum_norm n) . (a * x) = |.a.| * ((sum_norm n) . x) & (sum_norm n) . (x + y) <= ((sum_norm n) . x) + ((sum_norm n) . y) )
let a be Real; :: thesis: ( 0 <= (sum_norm n) . x & ( (sum_norm n) . x = 0 implies x = 0* n ) & ( x = 0* n implies (sum_norm n) . x = 0 ) & (sum_norm n) . (a * x) = |.a.| * ((sum_norm n) . x) & (sum_norm n) . (x + y) <= ((sum_norm n) . x) + ((sum_norm n) . y) )
set xSUM = (sum_norm n) . x;
set ySUM = (sum_norm n) . y;
set axSUM = (sum_norm n) . (a * x);
set xySUM = (sum_norm n) . (x + y);
A2: (sum_norm n) . y = Sum (abs y) by Def2;
0 <= Sum (abs x) by Th9;
hence 0 <= (sum_norm n) . x by Def2; :: thesis: ( ( (sum_norm n) . x = 0 implies x = 0* n ) & ( x = 0* n implies (sum_norm n) . x = 0 ) & (sum_norm n) . (a * x) = |.a.| * ((sum_norm n) . x) & (sum_norm n) . (x + y) <= ((sum_norm n) . x) + ((sum_norm n) . y) )
A3: (sum_norm n) . x = Sum (abs x) by Def2;
thus ( (sum_norm n) . x = 0 iff x = 0* n ) :: thesis: ( (sum_norm n) . (a * x) = |.a.| * ((sum_norm n) . x) & (sum_norm n) . (x + y) <= ((sum_norm n) . x) + ((sum_norm n) . y) )

proof

hereby :: thesis: ( x = 0* n implies (sum_norm n) . x = 0 )

assume (sum_norm n) . x = 0 ; :: thesis: not x <> 0* n
then A5: Sum (abs x) = 0 by Def2;
A6: len x = n by CARD_1:def 7;
A7: len (n |-> 0) = n by CARD_1:def 7;
assume x <> 0* n ; :: thesis: contradiction
then consider j being Nat such that
A8: j in dom x and
A9: x . j <> (n |-> 0) . j by A6, A7, FINSEQ_2:9;
A10: dom x = dom (abs x) by VALUED_1:def 11;
A11: dom x = Seg (len x) by FINSEQ_1:def 3;
0 < |.(x . j).| by A9;
then A12: 0 < (abs x) . j by A8, A10, VALUED_1:def 11;

A13: now :: thesis: for k being Nat st k in dom (abs x) holds
0 <= (abs x) . k

let k be Nat; :: thesis: ( k in dom (abs x) implies 0 <= (abs x) . k )
assume A14: k in dom (abs x) ; :: thesis: 0 <= (abs x) . k
set r = (abs x) . k;
set z = x . k;
0 <= |.(x . k).| ;
hence 0 <= (abs x) . k by A14, VALUED_1:def 11; :: thesis: verum

end;

dom (abs x) = Seg (len (abs x)) by FINSEQ_1:def 3;
then j in dom (abs x) by A8, A11, FINSEQ_2:33;
hence contradiction by A5, A12, A13, RVSUM_1:85; :: thesis: verum

end;

assume x = 0* n ; :: thesis: (sum_norm n) . x = 0
then abs x = n |-> 0 by EUCLID:4;
hence (sum_norm n) . x = 0 by A3, RVSUM_1:81; :: thesis: verum

end;

thus (sum_norm n) . (a * x) = Sum (abs (a * x)) by Def2
.= Sum (|.a.| * (abs x)) by RFUNCT_1:25
.= |.a.| * (Sum (abs x)) by RVSUM_1:87
.= |.a.| * ((sum_norm n) . x) by Def2 ; :: thesis: (sum_norm n) . (x + y) <= ((sum_norm n) . x) + ((sum_norm n) . y)
for j being Nat st j in Seg n holds
(abs (x + y)) . j <= ((abs x) + (abs y)) . j

proof

let j be Nat; :: thesis: ( j in Seg n implies (abs (x + y)) . j <= ((abs x) + (abs y)) . j )
assume A15: j in Seg n ; :: thesis: (abs (x + y)) . j <= ((abs x) + (abs y)) . j
A16: dom x = dom (abs x) by VALUED_1:def 11;
A17: dom x = Seg (len x) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7 ;
A18: dom y = dom (abs y) by VALUED_1:def 11;
A19: dom y = Seg (len y) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7 ;
A20: dom (x + y) = dom (abs (x + y)) by VALUED_1:def 11;
A22: dom ((abs x) + (abs y)) = (dom (abs x)) /\ (dom (abs y)) by VALUED_1:def 1
.= Seg n by A16, A17, A18, A19 ;
A21: dom (x + y) = Seg (len (x + y)) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7 ;
then A23: (abs (x + y)) . j = |.((x + y) . j).| by A15, A20, VALUED_1:def 11
.= |.((x . j) + (y . j)).| by A15, A21, VALUED_1:def 1 ;
|.((x . j) + (y . j)).| <= |.(x . j).| + |.(y . j).| by COMPLEX1:56;
then (abs (x + y)) . j <= ((abs x) . j) + |.(y . j).| by A15, A16, A17, A23, VALUED_1:def 11;
then (abs (x + y)) . j <= ((abs x) . j) + ((abs y) . j) by A15, A18, A19, VALUED_1:def 11;
hence (abs (x + y)) . j <= ((abs x) + (abs y)) . j by A15, A22, VALUED_1:def 1; :: thesis: verum

end;

then Sum (abs (x + y)) <= Sum ((abs x) + (abs y)) by RVSUM_1:82;
then Sum (abs (x + y)) <= (Sum (abs x)) + (Sum (abs y)) by RVSUM_1:89;
hence (sum_norm n) . (x + y) <= ((sum_norm n) . x) + ((sum_norm n) . y) by A2, A3, Def2; :: thesis: verum