now :: thesis: for x being Point of [:G,F:] st x = 0. [:G,F:] holds
||.x.|| = 0
let x be Point of [:G,F:]; :: thesis: ( x = 0. [:G,F:] implies ||.x.|| = 0 )
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
consider v being Element of REAL 2 such that
A2: ( v = <*||.x1.||,||.x2.||*> & (prod_NORM (G,F)) . (x1,x2) = |.v.| ) by Def6;
assume x = 0. [:G,F:] ; :: thesis: ||.x.|| = 0
then ( x1 = 0. G & x2 = 0. F ) by A1, XTUPLE_0:1;
then ( ||.x1.|| = 0 & ||.x2.|| = 0 ) ;
then v = 0* 2 by A2, FINSEQ_2:61;
hence ||.x.|| = 0 by A2, A1, EUCLID:7; :: thesis: verum
end;
then ||.(0. [:G,F:]).|| = 0 ;
hence [:G,F:] is reflexive ; :: thesis: ( [:G,F:] is discerning & [:G,F:] is RealNormSpace-like )
now :: thesis: for x being Point of [:G,F:] st ||.x.|| = 0 holds
x = 0. [:G,F:]
let x be Point of [:G,F:]; :: thesis: ( ||.x.|| = 0 implies x = 0. [:G,F:] )
consider x1 being Point of G, x2 being Point of F such that
A3: x = [x1,x2] by Lm1;
consider v being Element of REAL 2 such that
A4: ( v = <*||.x1.||,||.x2.||*> & (prod_NORM (G,F)) . (x1,x2) = |.v.| ) by Def6;
assume ||.x.|| = 0 ; :: thesis: x = 0. [:G,F:]
then v = 0* 2 by A4, A3, EUCLID:8;
then A5: v = <*0,0*> by FINSEQ_2:61;
( ||.x1.|| = v . 1 & ||.x2.|| = v . 2 ) by A4, FINSEQ_1:44;
then ( ||.x1.|| = 0 & ||.x2.|| = 0 ) by A5, FINSEQ_1:44;
then ( x1 = 0. G & x2 = 0. F ) by NORMSP_0:def 5;
hence x = 0. [:G,F:] by A3; :: thesis: verum
end;
hence [:G,F:] is discerning ; :: thesis: [:G,F:] is RealNormSpace-like
now :: thesis: for x, y being Point of [:G,F:]
for a being Real holds
( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
let x, y be Point of [:G,F:]; :: thesis: for a being Real holds
( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
let a be Real; :: thesis: ( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
consider x1 being Point of G, x2 being Point of F such that
A6: x = [x1,x2] by Lm1;
consider y1 being Point of G, y2 being Point of F such that
A7: y = [y1,y2] by Lm1;
consider v being Element of REAL 2 such that
A8: ( v = <*||.x1.||,||.x2.||*> & (prod_NORM (G,F)) . (x1,x2) = |.v.| ) by Def6;
consider z being Element of REAL 2 such that
A9: ( z = <*||.y1.||,||.y2.||*> & (prod_NORM (G,F)) . (y1,y2) = |.z.| ) by Def6;
thus ||.(a * x).|| = |.a.| * ||.x.|| :: thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||
proof
consider w being Element of REAL 2 such that
A10: ( w = <*||.(a * x1).||,||.(a * x2).||*> & (prod_NORM (G,F)) . ((a * x1),(a * x2)) = |.w.| ) by Def6;
reconsider aa = |.a.|, xx1 = ||.x1.||, xx2 = ||.x2.|| as Real ;
( ||.(a * x1).|| = |.a.| * ||.x1.|| & ||.(a * x2).|| = |.a.| * ||.x2.|| ) by NORMSP_1:def 1;
then w = aa * |[xx1,xx2]| by A10, EUCLID:58
.= |.a.| * v by A8, EUCLID:65 ;
then |.w.| = |.|.a.|.| * |.v.| by EUCLID:11
.= |.a.| * |.v.| ;
hence ||.(a * x).|| = |.a.| * ||.x.|| by A8, A10, A6, Def2; :: thesis: verum
end;
thus ||.(x + y).|| <= ||.x.|| + ||.y.|| :: thesis: verum
proof
consider w being Element of REAL 2 such that
A11: ( w = <*||.(x1 + y1).||,||.(x2 + y2).||*> & (prod_NORM (G,F)) . ((x1 + y1),(x2 + y2)) = |.w.| ) by Def6;
A12: ||.(x + y).|| = |.w.| by A11, A6, A7, Def1;
A13: ( ||.(x1 + y1).|| <= ||.x1.|| + ||.y1.|| & ||.(x2 + y2).|| <= ||.x2.|| + ||.y2.|| ) by NORMSP_1:def 1;
reconsider t1 = ||.x1.|| + ||.y1.||, t2 = ||.x2.|| + ||.y2.|| as Element of REAL by XREAL_0:def 1;
reconsider t = <*t1,t2*> as FinSequence of REAL ;
A14: ( len w = 2 & len t = 2 ) by A11, FINSEQ_1:44;
now :: thesis: for i being Element of NAT st i in Seg (len w) holds
( 0 <= w . i & w . i <= t . i )
let i be Element of NAT ; :: thesis: ( i in Seg (len w) implies ( 0 <= w . b1 & w . b1 <= t . b1 ) )
assume i in Seg (len w) ; :: thesis: ( 0 <= w . b1 & w . b1 <= t . b1 )
then A15: i in Seg 2 by A11, FINSEQ_1:44;
per cases ( i = 1 or i = 2 ) by A15, FINSEQ_1:2, TARSKI:def 2;
suppose A16: i = 1 ; :: thesis: ( 0 <= w . b1 & w . b1 <= t . b1 )
then w . i = ||.(x1 + y1).|| by A11, FINSEQ_1:44;
hence ( 0 <= w . i & w . i <= t . i ) by A13, A16, FINSEQ_1:44, NORMSP_1:4; :: thesis: verum
end;
suppose A17: i = 2 ; :: thesis: ( 0 <= w . b1 & w . b1 <= t . b1 )
then w . i = ||.(x2 + y2).|| by A11, FINSEQ_1:44;
hence ( 0 <= w . i & w . i <= t . i ) by A13, A17, FINSEQ_1:44, NORMSP_1:4; :: thesis: verum
end;
end;
end;
then A18: |.w.| <= |.t.| by A14, PRVECT_2:2;
t = |[||.x1.||,||.x2.||]| + |[||.y1.||,||.y2.||]| by EUCLID:56
.= v + z by A8, A9, EUCLID:64 ;
then |.t.| <= |.v.| + |.z.| by EUCLID:12;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A12, A6, A8, A7, A9, A18, XXREAL_0:2; :: thesis: verum
end;
end;
hence [:G,F:] is RealNormSpace-like by NORMSP_1:def 1; :: thesis: verum