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 holds
( 0 <= (euclid_norm (X,b)) . x & ( (euclid_norm (X,b)) . x = 0 implies x = 0. X ) & ( x = 0. X implies (euclid_norm (X,b)) . x = 0 ) & (euclid_norm (X,b)) . (a * x) = |.a.| * ((euclid_norm (X,b)) . x) & (euclid_norm (X,b)) . (x + y) <= ((euclid_norm (X,b)) . x) + ((euclid_norm (X,b)) . y) )
let b be OrdBasis of RLSp2RVSp X; :: thesis: for x, y being Element of X
for a being Real holds
( 0 <= (euclid_norm (X,b)) . x & ( (euclid_norm (X,b)) . x = 0 implies x = 0. X ) & ( x = 0. X implies (euclid_norm (X,b)) . x = 0 ) & (euclid_norm (X,b)) . (a * x) = |.a.| * ((euclid_norm (X,b)) . x) & (euclid_norm (X,b)) . (x + y) <= ((euclid_norm (X,b)) . x) + ((euclid_norm (X,b)) . y) )
let x, y be Element of X; :: thesis: for a being Real holds
( 0 <= (euclid_norm (X,b)) . x & ( (euclid_norm (X,b)) . x = 0 implies x = 0. X ) & ( x = 0. X implies (euclid_norm (X,b)) . x = 0 ) & (euclid_norm (X,b)) . (a * x) = |.a.| * ((euclid_norm (X,b)) . x) & (euclid_norm (X,b)) . (x + y) <= ((euclid_norm (X,b)) . x) + ((euclid_norm (X,b)) . y) )
let a be Real; :: thesis: ( 0 <= (euclid_norm (X,b)) . x & ( (euclid_norm (X,b)) . x = 0 implies x = 0. X ) & ( x = 0. X implies (euclid_norm (X,b)) . x = 0 ) & (euclid_norm (X,b)) . (a * x) = |.a.| * ((euclid_norm (X,b)) . x) & (euclid_norm (X,b)) . (x + y) <= ((euclid_norm (X,b)) . x) + ((euclid_norm (X,b)) . y) )
set xSUM = (euclid_norm (X,b)) . x;
set ySUM = (euclid_norm (X,b)) . y;
set axSUM = (euclid_norm (X,b)) . (a * x);
set xySUM = (euclid_norm (X,b)) . (x + y);
consider x1 being Element of (RLSp2RVSp X), z1 being Element of REAL (dim X) such that
A1: ( x = x1 & z1 = x1 |-- b & (euclid_norm (X,b)) . x = |.z1.| ) by Def5;
consider x2 being Element of (RLSp2RVSp X), z2 being Element of REAL (dim X) such that
A2: ( y = x2 & z2 = x2 |-- b & (euclid_norm (X,b)) . y = |.z2.| ) by Def5;
consider xy being Element of (RLSp2RVSp X), z3 being Element of REAL (dim X) such that
A3: ( x + y = xy & z3 = xy |-- b & (euclid_norm (X,b)) . (x + y) = |.z3.| ) by Def5;
consider ax being Element of (RLSp2RVSp X), z4 being Element of REAL (dim X) such that
A4: ( a * x = ax & z4 = ax |-- b & (euclid_norm (X,b)) . (a * x) = |.z4.| ) by Def5;
thus 0 <= (euclid_norm (X,b)) . x by A1; :: thesis: ( ( (euclid_norm (X,b)) . x = 0 implies x = 0. X ) & ( x = 0. X implies (euclid_norm (X,b)) . x = 0 ) & (euclid_norm (X,b)) . (a * x) = |.a.| * ((euclid_norm (X,b)) . x) & (euclid_norm (X,b)) . (x + y) <= ((euclid_norm (X,b)) . x) + ((euclid_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 ( (euclid_norm (X,b)) . x = 0 iff x = 0. X ) by A1, EUCLID:7, EUCLID:8, MATRLIN:34; :: thesis: ( (euclid_norm (X,b)) . (a * x) = |.a.| * ((euclid_norm (X,b)) . x) & (euclid_norm (X,b)) . (x + y) <= ((euclid_norm (X,b)) . x) + ((euclid_norm (X,b)) . y) )
reconsider a1 = a as Element of F_Real by XREAL_0:def 1;
ax = a1 * x1 by A1, A4;
then z4 = a1 * (x1 |-- b) by A4, MATRLIN2:18
.= a * z1 by A1 ;
hence (euclid_norm (X,b)) . (a * x) = |.a.| * ((euclid_norm (X,b)) . x) by A1, A4, EUCLID:11; :: thesis: (euclid_norm (X,b)) . (x + y) <= ((euclid_norm (X,b)) . x) + ((euclid_norm (X,b)) . y)
xy = x1 + x2 by A1, A2, A3;
then z3 = (x1 |-- b) + (x2 |-- b) by A3, MATRLIN2:17
.= z1 + z2 by A1, A2 ;
hence (euclid_norm (X,b)) . (x + y) <= ((euclid_norm (X,b)) . x) + ((euclid_norm (X,b)) . y) by A1, A2, A3, EUCLID:12; :: thesis: verum