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

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

A3:
W is right-distributive
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;reconsider x1 = x as Element of V by A1;

x * (1. W) = x1 * (1. V) by A1;

hence x * (1. W) = x ; :: thesis: verum

proof

A4:
for x being Element of W holds x is right_complementable
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;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

proof

A6:
for a, b, x being Element of W holds (a * b) * x = a * (b * x)
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;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

proof

A7:
for v, w being Element of W holds v * w = w * v
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;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

proof

A8:
for x, y, z being VECTOR of W holds (x + y) + z = x + (y + z)
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;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

proof

A9:
for x, y being VECTOR of W holds x + y = y + x
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;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

proof

A10:
W is vector-distributive
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;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

proof

A11:
W is scalar-distributive
let a be Complex; :: according to CLVECT_1:def 2 :: thesis: for b_{1}, b_{2} being Element of the carrier of W holds a * (b_{1} + b_{2}) = (a * b_{1}) + (a * b_{2})

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;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

proof

A12:
W is scalar-associative
let a, b be Complex; :: according to CLVECT_1:def 3 :: thesis: for b_{1} being Element of the carrier of W holds (a + b) * b_{1} = (a * b_{1}) + (b * b_{1})

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;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

proof

A13:
W is vector-associative
let a, b be Complex; :: according to CLVECT_1:def 4 :: thesis: for b_{1} being Element of the carrier of W holds (a * b) * b_{1} = a * (b * b_{1})

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;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

proof

for x being VECTOR of W holds x + (0. W) = x
let x, y be VECTOR of W; :: according to CFUNCDOM:def 9 :: thesis: for b_{1} being object holds b_{1} * (x * y) = (b_{1} * 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;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

proof

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
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;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