let W be Normed_AlgebraStr ; :: thesis: for V being Algebra st AlgebraStr(# the carrier of W,the multF of W,the addF of W,the Mult of W,the OneF of W,the ZeroF of W #) = V holds
W is Algebra
let V be Algebra; :: thesis: ( AlgebraStr(# the carrier of W,the multF of W,the addF of W,the Mult of W,the OneF of W,the ZeroF of W #) = V implies W is Algebra )
assume A1: AlgebraStr(# the carrier of W,the multF of W,the addF of W,the Mult of W,the OneF of W,the ZeroF of W #) = V ; :: thesis: W is Algebra
reconsider W = W as non empty AlgebraStr by A1;
A2: W is right_unital

proof

let x be Element of W; :: according to VECTSP_1:def 13 :: thesis: x * (1. W) = x
reconsider x1 = x as Element of V by A1;
x * (1. W) = x1 * (1. V) by A1;
hence x * (1. W) = x by VECTSP_1:def 13; :: thesis: verum

end;

A3: W is right-distributive

proof

let x, y, z be Element of W; :: according to VECTSP_1:def 11 :: thesis: x * (y + z) = (x * y) + (x * z)
reconsider x1 = x, y1 = y, z1 = z as Element of V by A1;
x * (y + z) = x1 * (y1 + z1) by A1;
then x * (y + z) = (x1 * y1) + (x1 * z1) by VECTSP_1:def 11;
hence x * (y + z) = (x * y) + (x * z) by A1; :: thesis: verum

end;

A4: for x being Element of W holds x is right_complementable

proof

let x be Element of W; :: thesis: x is right_complementable
reconsider x1 = x as Element of V by A1;
consider v being Element of V such that
A5: x1 + v = 0. V by ALGSTR_0:def 11;
reconsider y = v as Element of W by A1;
x + y = 0. W by A1, A5;
hence x is right_complementable by ALGSTR_0:def 11; :: thesis: verum

end;

A6: for a, b, x being Element of W holds (a * b) * x = a * (b * x)

proof

let a, b, x be Element of W; :: thesis: (a * b) * x = a * (b * x)
reconsider y = x, a1 = a, b1 = b as Element of V by A1;
(a * b) * x = (a1 * b1) * y by A1;
then (a * b) * x = a1 * (b1 * y) by GROUP_1:def 4;
hence (a * b) * x = a * (b * x) by A1; :: thesis: verum

end;

A7: for v, w being Element of W holds v * w = w * v

proof

let v, w be Element of W; :: thesis: v * w = w * v
reconsider v1 = v, w1 = w as Element of V by A1;
v * w = v1 * w1 by A1;
then v * w = w1 * v1 ;
hence v * w = w * v by A1; :: thesis: verum

end;

A8: for x, y, z being VECTOR of W holds (x + y) + z = x + (y + z)

proof

let x, y, z be VECTOR of W; :: thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1;
(x + y) + z = (x1 + y1) + z1 by A1;
then (x + y) + z = x1 + (y1 + z1) by RLVECT_1:def 6;
hence (x + y) + z = x + (y + z) by A1; :: thesis: verum

end;

A9: for x, y being VECTOR of W holds x + y = y + x

proof

let x, y be VECTOR of W; :: thesis: x + y = y + x
reconsider x1 = x, y1 = y as VECTOR of V by A1;
x + y = x1 + y1 by A1;
then x + y = y1 + x1 ;
hence x + y = y + x by A1; :: thesis: verum

end;

A10: W is vector-distributive

proof

let a be real number ; :: according to RLVECT_1:def 8 :: thesis: for b₁, b₂ being Element of the carrier of W holds a * (b₁ + b₂) = (a * b₁) + (a * b₂)
let x, y be Element of W; :: thesis: a * (x + y) = (a * x) + (a * y)
reconsider x1 = x, y1 = y as Element of V by A1;
a * (x + y) = a * (x1 + y1) by A1;
then a * (x + y) = (a * x1) + (a * y1) by RLVECT_1:def 8;
hence a * (x + y) = (a * x) + (a * y) by A1; :: thesis: verum

end;

B10: W is scalar-distributive

proof

let a, b be real number ; :: according to RLVECT_1:def 9 :: thesis: for b₁ being Element of the carrier of W holds (a + b) * b₁ = (a * b₁) + (b * b₁)
let x be Element of W; :: thesis: (a + b) * x = (a * x) + (b * x)
reconsider x1 = x as Element of V by A1;
(a + b) * x = (a + b) * x1 by A1;
then (a + b) * x = (a * x1) + (b * x1) by RLVECT_1:def 9;
hence (a + b) * x = (a * x) + (b * x) by A1; :: thesis: verum
thus verum ; :: thesis: verum

end;

C10: W is scalar-associative

proof

let a, b be real number ; :: according to RLVECT_1:def 10 :: thesis: for b₁ being Element of the carrier of W holds (a * b) * b₁ = a * (b * b₁)
let x be Element of W; :: thesis: (a * b) * x = a * (b * x)
reconsider x1 = x as Element of V by A1;
(a * b) * x = (a * b) * x1 by A1;
then (a * b) * x = a * (b * x1) by RLVECT_1:def 10;
hence (a * b) * x = a * (b * x) by A1; :: thesis: verum

end;

D10: W is vector-associative

proof

let x, y be Element of W; :: according to FUNCSDOM:def 20 :: thesis: for b₁ being Element of REAL holds b₁ * (x * y) = (b₁ * x) * y
reconsider x1 = x, y1 = y as Element of V by A1;
let a be Real; :: thesis: a * (x * y) = (a * x) * y
a * (x * y) = a * (x1 * y1) by A1;
then a * (x * y) = (a * x1) * y1 by FUNCSDOM:def 20;
hence a * (x * y) = (a * x) * y by A1; :: thesis: verum

end;

for x being VECTOR of W holds x + (0. W) = x

proof

let x be VECTOR of W; :: thesis: x + (0. W) = x
reconsider y = x, z = 0. W as VECTOR of V by A1;
x + (0. W) = y + (0. V) by A1;
hence x + (0. W) = x by RLVECT_1:10; :: thesis: verum

end;

hence W is Algebra by A9, A8, A4, A7, A6, A2, A3, A10, B10, C10, D10, ALGSTR_0:def 16, GROUP_1:def 4, GROUP_1:def 16, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7; :: thesis: verum