let X be finite-dimensional RealLinearSpace; :: thesis: for b being OrdBasis of RLSp2RVSp X
for x being Element of X st dim X <> 0 holds
( (sum_norm (X,b)) . x <= (dim X) * ((max_norm (X,b)) . x) & (max_norm (X,b)) . x <= (euclid_norm (X,b)) . x & (euclid_norm (X,b)) . x <= (sum_norm (X,b)) . x )
let b be OrdBasis of RLSp2RVSp X; :: thesis: for x being Element of X st dim X <> 0 holds
( (sum_norm (X,b)) . x <= (dim X) * ((max_norm (X,b)) . x) & (max_norm (X,b)) . x <= (euclid_norm (X,b)) . x & (euclid_norm (X,b)) . x <= (sum_norm (X,b)) . x )
let x be Element of X; :: thesis: ( dim X <> 0 implies ( (sum_norm (X,b)) . x <= (dim X) * ((max_norm (X,b)) . x) & (max_norm (X,b)) . x <= (euclid_norm (X,b)) . x & (euclid_norm (X,b)) . x <= (sum_norm (X,b)) . x ) )
assume A1: dim X <> 0 ; :: thesis: ( (sum_norm (X,b)) . x <= (dim X) * ((max_norm (X,b)) . x) & (max_norm (X,b)) . x <= (euclid_norm (X,b)) . x & (euclid_norm (X,b)) . x <= (sum_norm (X,b)) . x )
consider x1 being Element of (RLSp2RVSp X), z1 being Element of REAL (dim X) such that
A2: ( x = x1 & z1 = x1 |-- b & (max_norm (X,b)) . x = (max_norm (dim X)) . z1 ) by Def3;
consider x2 being Element of (RLSp2RVSp X), z2 being Element of REAL (dim X) such that
A3: ( x = x2 & z2 = x2 |-- b & (sum_norm (X,b)) . x = (sum_norm (dim X)) . z2 ) by Def4;
consider x3 being Element of (RLSp2RVSp X), z3 being Element of REAL (dim X) such that
A4: ( x = x3 & z3 = x3 |-- b & (euclid_norm (X,b)) . x = |.z3.| ) by Def5;
thus ( (sum_norm (X,b)) . x <= (dim X) * ((max_norm (X,b)) . x) & (max_norm (X,b)) . x <= (euclid_norm (X,b)) . x & (euclid_norm (X,b)) . x <= (sum_norm (X,b)) . x ) by A1, A2, A3, A4, Th14; :: thesis: verum