set T = NORMSTR(# REAL,(In (0,REAL)),addreal,multreal,absreal #);
reconsider T = NORMSTR(# REAL,(In (0,REAL)),addreal,multreal,absreal #) as non empty NORMSTR ;
now :: thesis: for v, w being Element of T holds v + w = w + v
let v, w be Element of T; :: thesis: v + w = w + v
reconsider v1 = v, w1 = w as Element of REAL ;
thus v + w = v1 + w1 by BINOP_2:def 9
.= w + v by BINOP_2:def 9 ; :: thesis: verum
end;
then A1: T is Abelian ;
now :: thesis: for u, v, w being Element of T holds (u + v) + w = u + (v + w)
let u, v, w be Element of T; :: thesis: (u + v) + w = u + (v + w)
reconsider u1 = u, v1 = v, w1 = w as Element of REAL ;
B1: ( addreal . (u,v) = u1 + v1 & addreal . (v,w) = v1 + w1 ) by BINOP_2:def 9;
thus (u + v) + w = (u1 + v1) + w1 by B1, BINOP_2:def 9
.= u1 + (v1 + w1)
.= u + (v + w) by B1, BINOP_2:def 9 ; :: thesis: verum
end;
then A2: T is add-associative ;
now :: thesis: for v being Element of T holds v + (0. T) = v
let v be Element of T; :: thesis: v + (0. T) = v
reconsider v1 = v as Element of REAL ;
thus v + (0. T) = v1 + 0 by BINOP_2:def 9
.= v ; :: thesis: verum
end;
then A3: T is right_zeroed ;
A4: T is right_complementable
proof
let v be Element of T; :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider v1 = v as Element of REAL ;
reconsider w1 = - v1 as Element of REAL ;
reconsider w = w1 as Element of T ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. T
thus v + w = v1 + w1 by BINOP_2:def 9
.= 0. T ; :: thesis: verum
end;
now :: thesis: for a, b being Real
for v being Element of T holds (a + b) * v = (a * v) + (b * v)
let a, b be Real; :: thesis: for v being Element of T holds (a + b) * v = (a * v) + (b * v)
let v be Element of T; :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider v1 = v as Element of REAL ;
B1: ( multreal . (a,v) = a * v1 & multreal . (b,v) = b * v1 ) by BINOP_2:def 11;
thus (a + b) * v = (a + b) * v1 by BINOP_2:def 11
.= (v1 * a) + (v1 * b)
.= (a * v) + (b * v) by B1, BINOP_2:def 9 ; :: thesis: verum
end;
then A5: T is scalar-distributive ;
now :: thesis: for a being Real
for v, w being Element of T holds a * (v + w) = (a * v) + (a * w)
let a be Real; :: thesis: for v, w being Element of T holds a * (v + w) = (a * v) + (a * w)
let v, w be Element of T; :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider v1 = v, w1 = w as Element of REAL ;
B1: addreal . (v,w) = v1 + w1 by BINOP_2:def 9;
B2: ( multreal . (a,v) = a * v1 & multreal . (a,w) = a * w1 ) by BINOP_2:def 11;
thus a * (v + w) = a * (v1 + w1) by B1, BINOP_2:def 11
.= (a * v1) + (a * w1)
.= (a * v) + (a * w) by B2, BINOP_2:def 9 ; :: thesis: verum
end;
then A6: T is vector-distributive ;
now :: thesis: for a, b being Real
for v being Element of T holds (a * b) * v = a * (b * v)
let a, b be Real; :: thesis: for v being Element of T holds (a * b) * v = a * (b * v)
let v be Element of T; :: thesis: (a * b) * v = a * (b * v)
reconsider v1 = v as Element of REAL ;
B1: multreal . (b,v) = b * v1 by BINOP_2:def 11;
thus (a * b) * v = (a * b) * v1 by BINOP_2:def 11
.= a * (b * v1)
.= a * (b * v) by B1, BINOP_2:def 11 ; :: thesis: verum
end;
then A7: T is scalar-associative ;
now :: thesis: for v being Element of T holds 1 * v = v
let v be Element of T; :: thesis: 1 * v = v
reconsider v1 = v as Element of REAL ;
thus 1 * v = 1 * v1 by BINOP_2:def 11
.= v ; :: thesis: verum
end;
then A8: T is scalar-unital ;
A9: T is reflexive by EUCLID:def 2, COMPLEX1:44;
now :: thesis: for v being Element of T st ||.v.|| = 0 holds
v = 0. T
let v be Element of T; :: thesis: ( ||.v.|| = 0 implies v = 0. T )
assume AS: ||.v.|| = 0 ; :: thesis: v = 0. T
reconsider v1 = v as Element of REAL ;
|.v1.| = 0 by AS, EUCLID:def 2;
hence v = 0. T by COMPLEX1:45; :: thesis: verum
end;
then A10: T is discerning ;
now :: thesis: for a being Real
for v, w being Element of T holds
( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )
let a be Real; :: thesis: for v, w being Element of T holds
( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )
let v, w be Element of T; :: thesis: ( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )
reconsider v1 = v, w1 = w as Element of REAL ;
the normF of T . (a * v) = absreal . (a * v1) by BINOP_2:def 11;
hence ||.(a * v).|| = |.(a * v1).| by EUCLID:def 2
.= |.a.| * |.v1.| by COMPLEX1:65
.= |.a.| * ||.v.|| by EUCLID:def 2 ;
:: thesis: ||.(v + w).|| <= ||.v.|| + ||.w.||
the normF of T . (v + w) = absreal . (v1 + w1) by BINOP_2:def 9;
then C3: ||.(v + w).|| = |.(v1 + w1).| by EUCLID:def 2;
||.v.|| + ||.w.|| = |.v1.| + (absreal . w1) by EUCLID:def 2
.= |.v1.| + |.w1.| by EUCLID:def 2 ;
hence ||.(v + w).|| <= ||.v.|| + ||.w.|| by C3, COMPLEX1:56; :: thesis: verum
end;
then T is RealNormSpace-like ;
hence NORMSTR(# REAL,(In (0,REAL)),addreal,multreal,absreal #) is RealNormSpace by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10; :: thesis: verum