let W be Normed_Complex_AlgebraStr ; :: thesis: for V being ComplexAlgebra st ComplexAlgebraStr(# 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 ComplexAlgebra
let V be ComplexAlgebra; :: thesis: ( ComplexAlgebraStr(# 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 ComplexAlgebra )
assume A1: ComplexAlgebraStr(# 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 ComplexAlgebra
reconsider W = W as non empty ComplexAlgebraStr by A1;
A2: W is right_unital

proof

let x be Element of W; :: according to VECTSP_1:def 4 :: 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 ; :: thesis: verum

end;

A3: W is right-distributive

proof

let x, y, z be Element of W; :: according to VECTSP_1:def 2 :: 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 2;
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 ; :: 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 3;
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 3;
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 Complex; :: according to CLVECT_1:def 2 :: thesis: for b₁, b₂ being Element of the carrier of W holds a * (b₁ + b₂) = (a * b₁) + (a * b₂)
let x, y be VECTOR 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 CLVECT_1:def 2;
hence a * (x + y) = (a * x) + (a * y) by A1; :: thesis: verum

end;

A11: W is scalar-distributive

proof

let a, b be Complex; :: according to CLVECT_1:def 3 :: thesis: for b₁ being Element of the carrier of W holds (a + b) * b₁ = (a * b₁) + (b * b₁)
let x be VECTOR 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 CLVECT_1:def 3;
hence (a + b) * x = (a * x) + (b * x) by A1; :: thesis: verum

end;

A12: W is scalar-associative

proof

let a, b be Complex; :: according to CLVECT_1:def 4 :: thesis: for b₁ being Element of the carrier of W holds (a * b) * b₁ = a * (b * b₁)
let x be VECTOR 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 CLVECT_1:def 4;
hence (a * b) * x = a * (b * x) by A1; :: thesis: verum

end;

A13: W is vector-associative

proof

let x, y be VECTOR of W; :: according to CFUNCDOM:def 9 :: thesis: for b₁ being object holds b₁ * (x * y) = (b₁ * x) * y
reconsider x1 = x, y1 = y as Element of V by A1;
let a be Complex; :: thesis: a * (x * y) = (a * x) * y
a * (x * y) = a * (x1 * y1) by A1;
then a * (x * y) = (a * x1) * y1 by CFUNCDOM:def 9;
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:4; :: thesis: verum

end;

hence W is ComplexAlgebra by A9, A8, A4, A7, A6, A2, A3, A10, A11, A12, A13, ALGSTR_0:def 16, GROUP_1:def 3, GROUP_1:def 12, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; :: thesis: verum