let X be finite-dimensional RealLinearSpace; :: thesis: for b being OrdBasis of RLSp2RVSp X
for x, y being Element of X
for a being Real st dim X <> 0 holds
( 0 <= (sum_norm (X,b)) . x & ( (sum_norm (X,b)) . x = 0 implies x = 0. X ) & ( x = 0. X implies (sum_norm (X,b)) . x = 0 ) & (sum_norm (X,b)) . (a * x) = |.a.| * ((sum_norm (X,b)) . x) & (sum_norm (X,b)) . (x + y) <= ((sum_norm (X,b)) . x) + ((sum_norm (X,b)) . y) )
let b be OrdBasis of RLSp2RVSp X; :: thesis: for x, y being Element of X
for a being Real st dim X <> 0 holds
( 0 <= (sum_norm (X,b)) . x & ( (sum_norm (X,b)) . x = 0 implies x = 0. X ) & ( x = 0. X implies (sum_norm (X,b)) . x = 0 ) & (sum_norm (X,b)) . (a * x) = |.a.| * ((sum_norm (X,b)) . x) & (sum_norm (X,b)) . (x + y) <= ((sum_norm (X,b)) . x) + ((sum_norm (X,b)) . y) )
let x, y be Element of X; :: thesis: for a being Real st dim X <> 0 holds
( 0 <= (sum_norm (X,b)) . x & ( (sum_norm (X,b)) . x = 0 implies x = 0. X ) & ( x = 0. X implies (sum_norm (X,b)) . x = 0 ) & (sum_norm (X,b)) . (a * x) = |.a.| * ((sum_norm (X,b)) . x) & (sum_norm (X,b)) . (x + y) <= ((sum_norm (X,b)) . x) + ((sum_norm (X,b)) . y) )
let a be Real; :: thesis: ( dim X <> 0 implies ( 0 <= (sum_norm (X,b)) . x & ( (sum_norm (X,b)) . x = 0 implies x = 0. X ) & ( x = 0. X implies (sum_norm (X,b)) . x = 0 ) & (sum_norm (X,b)) . (a * x) = |.a.| * ((sum_norm (X,b)) . x) & (sum_norm (X,b)) . (x + y) <= ((sum_norm (X,b)) . x) + ((sum_norm (X,b)) . y) ) )
assume A1: dim X <> 0 ; :: thesis: ( 0 <= (sum_norm (X,b)) . x & ( (sum_norm (X,b)) . x = 0 implies x = 0. X ) & ( x = 0. X implies (sum_norm (X,b)) . x = 0 ) & (sum_norm (X,b)) . (a * x) = |.a.| * ((sum_norm (X,b)) . x) & (sum_norm (X,b)) . (x + y) <= ((sum_norm (X,b)) . x) + ((sum_norm (X,b)) . y) )
set xSUM = (sum_norm (X,b)) . x;
set ySUM = (sum_norm (X,b)) . y;
set axSUM = (sum_norm (X,b)) . (a * x);
set xySUM = (sum_norm (X,b)) . (x + y);
consider x1 being Element of (RLSp2RVSp X), z1 being Element of REAL (dim X) such that
A2: ( x = x1 & z1 = x1 |-- b & (sum_norm (X,b)) . x = (sum_norm (dim X)) . z1 ) by Def4;
consider x2 being Element of (RLSp2RVSp X), z2 being Element of REAL (dim X) such that
A3: ( y = x2 & z2 = x2 |-- b & (sum_norm (X,b)) . y = (sum_norm (dim X)) . z2 ) by Def4;
consider xy being Element of (RLSp2RVSp X), z3 being Element of REAL (dim X) such that
A4: ( x + y = xy & z3 = xy |-- b & (sum_norm (X,b)) . (x + y) = (sum_norm (dim X)) . z3 ) by Def4;
consider ax being Element of (RLSp2RVSp X), z4 being Element of REAL (dim X) such that
A5: ( a * x = ax & z4 = ax |-- b & (sum_norm (X,b)) . (a * x) = (sum_norm (dim X)) . z4 ) by Def4;
thus 0 <= (sum_norm (X,b)) . x by A2, Th13, A1; :: thesis: ( ( (sum_norm (X,b)) . x = 0 implies x = 0. X ) & ( x = 0. X implies (sum_norm (X,b)) . x = 0 ) & (sum_norm (X,b)) . (a * x) = |.a.| * ((sum_norm (X,b)) . x) & (sum_norm (X,b)) . (x + y) <= ((sum_norm (X,b)) . x) + ((sum_norm (X,b)) . y) )
0* (dim X) = (dim (RLSp2RVSp X)) |-> (0. F_Real) by REAL_NS2:81
.= (len b) |-> (0. F_Real) by MATRLIN2:21
.= (0. (RLSp2RVSp X)) |-- b by MATRLIN2:20 ;
hence ( (sum_norm (X,b)) . x = 0 iff x = 0. X ) by A1, A2, Th13, MATRLIN:34; :: thesis: ( (sum_norm (X,b)) . (a * x) = |.a.| * ((sum_norm (X,b)) . x) & (sum_norm (X,b)) . (x + y) <= ((sum_norm (X,b)) . x) + ((sum_norm (X,b)) . y) )
reconsider a1 = a as Element of F_Real by XREAL_0:def 1;
ax = a1 * x1 by A2, A5;
then z4 = a1 * (x1 |-- b) by A5, MATRLIN2:18
.= a * z1 by A2 ;
hence (sum_norm (X,b)) . (a * x) = |.a.| * ((sum_norm (X,b)) . x) by A1, A2, A5, Th13; :: thesis: (sum_norm (X,b)) . (x + y) <= ((sum_norm (X,b)) . x) + ((sum_norm (X,b)) . y)
xy = x1 + x2 by A2, A3, A4;
then z3 = (x1 |-- b) + (x2 |-- b) by A4, MATRLIN2:17
.= z1 + z2 by A2, A3 ;
hence (sum_norm (X,b)) . (x + y) <= ((sum_norm (X,b)) . x) + ((sum_norm (X,b)) . y) by A1, A2, A3, A4, Th13; :: thesis: verum