let X be RealUnitarySpace; :: thesis: NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #) is RealNormSpace
set T = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #);
reconsider T = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #) 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 X ;
thus v + w = v1 + w1
.= w1 + v1
.= w + v ; :: 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 X ;
thus (u + v) + w = (u1 + v1) + w1
.= u1 + (v1 + w1) by RLVECT_1:def 3
.= u + (v + w) ; :: 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 X ;
thus v + (0. T) = v1 + (0. X)
.= 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 X ;
reconsider w1 = - v1 as Element of X ;
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
.= 0. X by RLVECT_1:def 10
.= 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 X ;
thus (a + b) * v = (a + b) * v1
.= (a * v1) + (b * v1) by RLVECT_1:def 6
.= (a * v) + (b * v) ; :: 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 X ;
thus a * (v + w) = a * (v1 + w1)
.= (a * v1) + (a * w1) by RLVECT_1:def 5
.= (a * v) + (a * w) ; :: 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 X ;
thus (a * b) * v = (a * b) * v1
.= a * (b * v1) by RLVECT_1:def 7
.= a * (b * v) ; :: 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 X ;
thus 1 * v = 1 * v1
.= v by RLVECT_1:def 8 ; :: thesis: verum
end;
then A8: T is scalar-unital ;
||.(0. X).|| = 0 by SQUARE_1:17, BHSP_1:1;
then A9: T is reflexive by Def1;
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 X ;
||.v1.|| = 0 by AS, Def1;
then v1 = 0. X by BHSP_1:26;
hence v = 0. T ; :: 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 X ;
thus ||.(a * v).|| = ||.(a * v1).|| by Def1
.= |.a.| * ||.v1.|| by BHSP_1:27
.= |.a.| * ||.v.|| by Def1 ; :: thesis: ||.(v + w).|| <= ||.v.|| + ||.w.||
C3: ||.(v + w).|| = ||.(v1 + w1).|| by Def1;
||.v.|| + ||.w.|| = ||.v1.|| + ((normRU X) . w) by Def1
.= ||.v1.|| + ||.w1.|| by Def1 ;
hence ||.(v + w).|| <= ||.v.|| + ||.w.|| by C3, BHSP_1:30; :: thesis: verum
end;
then T is RealNormSpace-like ;
hence NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #) is RealNormSpace by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10; :: thesis: verum