let X be non empty set ; :: thesis: for V being ComplexAlgebra

for V1 being non empty Subset of V

for d1, d2 being Element of X

for A being BinOp of X

for M being Function of [:X,X:],X

for MR being Function of [:COMPLEX,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:COMPLEX,V1:] & V1 is having-inverse holds

ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V

let V be ComplexAlgebra; :: thesis: for V1 being non empty Subset of V

for d1, d2 being Element of X

for A being BinOp of X

for M being Function of [:X,X:],X

for MR being Function of [:COMPLEX,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:COMPLEX,V1:] & V1 is having-inverse holds

ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V

let V1 be non empty Subset of V; :: thesis: for d1, d2 being Element of X

for A being BinOp of X

for M being Function of [:X,X:],X

for MR being Function of [:COMPLEX,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:COMPLEX,V1:] & V1 is having-inverse holds

ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V

let d1, d2 be Element of X; :: thesis: for A being BinOp of X

for M being Function of [:X,X:],X

for MR being Function of [:COMPLEX,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:COMPLEX,V1:] & V1 is having-inverse holds

ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V

let A be BinOp of X; :: thesis: for M being Function of [:X,X:],X

for MR being Function of [:COMPLEX,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:COMPLEX,V1:] & V1 is having-inverse holds

ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V

let M be Function of [:X,X:],X; :: thesis: for MR being Function of [:COMPLEX,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:COMPLEX,V1:] & V1 is having-inverse holds

ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V

let MR be Function of [:COMPLEX,X:],X; :: thesis: ( V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:COMPLEX,V1:] & V1 is having-inverse implies ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V )

assume that

A1: V1 = X and

A2: d1 = 0. V and

A3: d2 = 1. V and

A4: A = the addF of V || V1 and

A5: M = the multF of V || V1 and

A6: MR = the Mult of V | [:COMPLEX,V1:] and

A7: for v being Element of V st v in V1 holds

- v in V1 ; :: according to C0SP1:def 1 :: thesis: ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V

reconsider W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) as non empty ComplexAlgebraStr ;

hence ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V by A1, A4, A5, A6, A10, Def1; :: thesis: verum

for V1 being non empty Subset of V

for d1, d2 being Element of X

for A being BinOp of X

for M being Function of [:X,X:],X

for MR being Function of [:COMPLEX,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:COMPLEX,V1:] & V1 is having-inverse holds

ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V

let V be ComplexAlgebra; :: thesis: for V1 being non empty Subset of V

for d1, d2 being Element of X

for A being BinOp of X

for M being Function of [:X,X:],X

for MR being Function of [:COMPLEX,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:COMPLEX,V1:] & V1 is having-inverse holds

ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V

let V1 be non empty Subset of V; :: thesis: for d1, d2 being Element of X

for A being BinOp of X

for M being Function of [:X,X:],X

for MR being Function of [:COMPLEX,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:COMPLEX,V1:] & V1 is having-inverse holds

ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V

let d1, d2 be Element of X; :: thesis: for A being BinOp of X

for M being Function of [:X,X:],X

for MR being Function of [:COMPLEX,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:COMPLEX,V1:] & V1 is having-inverse holds

ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V

let A be BinOp of X; :: thesis: for M being Function of [:X,X:],X

for MR being Function of [:COMPLEX,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:COMPLEX,V1:] & V1 is having-inverse holds

ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V

let M be Function of [:X,X:],X; :: thesis: for MR being Function of [:COMPLEX,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:COMPLEX,V1:] & V1 is having-inverse holds

ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V

let MR be Function of [:COMPLEX,X:],X; :: thesis: ( V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:COMPLEX,V1:] & V1 is having-inverse implies ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V )

assume that

A1: V1 = X and

A2: d1 = 0. V and

A3: d2 = 1. V and

A4: A = the addF of V || V1 and

A5: M = the multF of V || V1 and

A6: MR = the Mult of V | [:COMPLEX,V1:] and

A7: for v being Element of V st v in V1 holds

- v in V1 ; :: according to C0SP1:def 1 :: thesis: ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V

reconsider W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) as non empty ComplexAlgebraStr ;

A8: now :: thesis: for x, y being Element of W holds x + y = the addF of V . (x,y)

let x, y be Element of W; :: thesis: x + y = the addF of V . (x,y)

reconsider x1 = x, y1 = y as Element of V by A1, TARSKI:def 3;

x + y = the addF of V . [x,y] by A1, A4, FUNCT_1:49;

hence x + y = the addF of V . (x,y) ; :: thesis: verum

end;reconsider x1 = x, y1 = y as Element of V by A1, TARSKI:def 3;

x + y = the addF of V . [x,y] by A1, A4, FUNCT_1:49;

hence x + y = the addF of V . (x,y) ; :: thesis: verum

A9: now :: thesis: for a, x being VECTOR of W holds a * x = the multF of V . (a,x)

A10:
( W is Abelian & W is add-associative & W is right_zeroed & W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
let a, x be VECTOR of W; :: thesis: a * x = the multF of V . (a,x)

a * x = the multF of V . [a,x] by A1, A5, FUNCT_1:49;

hence a * x = the multF of V . (a,x) ; :: thesis: verum

end;a * x = the multF of V . [a,x] by A1, A5, FUNCT_1:49;

hence a * x = the multF of V . (a,x) ; :: thesis: verum

proof

( 0. W = 0. V & 1. W = 1. V )
by A2, A3;
set Mv = the multF of V;

set MV = the Mult of V;

set Av = the addF of V;

for x, y being VECTOR of W holds a * (x + y) = (a * x) + (a * y) :: according to CLVECT_1:def 2 :: thesis: ( W is scalar-distributive & W is scalar-associative & W is vector-associative )

for v being VECTOR of W holds (a + b) * v = (a * v) + (b * v) :: according to CLVECT_1:def 3 :: thesis: ( W is scalar-associative & W is vector-associative )

for v being VECTOR of W holds (a * b) * v = a * (b * v) :: according to CLVECT_1:def 4 :: thesis: W is vector-associative

for a being Complex holds a * (x * y) = (a * x) * y :: according to CFUNCDOM:def 9 :: thesis: verum

end;set MV = the Mult of V;

set Av = the addF of V;

hereby :: according to RLVECT_1:def 2 :: thesis: ( W is add-associative & W is right_zeroed & W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )

let x, y be VECTOR of W; :: thesis: x + y = y + x

reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def 3;

( x + y = x1 + y1 & y + x = y1 + x1 ) by A8;

hence x + y = y + x ; :: thesis: verum

end;reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def 3;

( x + y = x1 + y1 & y + x = y1 + x1 ) by A8;

hence x + y = y + x ; :: thesis: verum

hereby :: according to RLVECT_1:def 3 :: thesis: ( W is right_zeroed & W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )

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, TARSKI:def 3;

x + (y + z) = the addF of V . (x1,(y + z)) by A8;

then A11: x + (y + z) = x1 + (y1 + z1) by A8;

(x + y) + z = the addF of V . ((x + y),z1) by A8;

then (x + y) + z = (x1 + y1) + z1 by A8;

hence (x + y) + z = x + (y + z) by A11, RLVECT_1:def 3; :: thesis: verum

end;reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1, TARSKI:def 3;

x + (y + z) = the addF of V . (x1,(y + z)) by A8;

then A11: x + (y + z) = x1 + (y1 + z1) by A8;

(x + y) + z = the addF of V . ((x + y),z1) by A8;

then (x + y) + z = (x1 + y1) + z1 by A8;

hence (x + y) + z = x + (y + z) by A11, RLVECT_1:def 3; :: thesis: verum

hereby :: according to RLVECT_1:def 4 :: thesis: ( W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )

thus
W is right_complementable
:: thesis: ( W is commutative & W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )let x be VECTOR of W; :: thesis: x + (0. W) = x

reconsider y = x, z = 0. W as VECTOR of V by A1, TARSKI:def 3;

thus x + (0. W) = y + (0. V) by A2, A8

.= x by RLVECT_1:4 ; :: thesis: verum

end;reconsider y = x, z = 0. W as VECTOR of V by A1, TARSKI:def 3;

thus x + (0. W) = y + (0. V) by A2, A8

.= x by RLVECT_1:4 ; :: thesis: verum

proof

let x be Element of W; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable

reconsider x1 = x as Element of V by A1, TARSKI:def 3;

consider v being Element of V such that

A12: x1 + v = 0. V by ALGSTR_0:def 11;

v = - x1 by A12, VECTSP_1:16;

then reconsider y = v as Element of W by A1, A7;

take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. W

thus x + y = 0. W by A2, A8, A12; :: thesis: verum

end;reconsider x1 = x as Element of V by A1, TARSKI:def 3;

consider v being Element of V such that

A12: x1 + v = 0. V by ALGSTR_0:def 11;

v = - x1 by A12, VECTSP_1:16;

then reconsider y = v as Element of W by A1, A7;

take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. W

thus x + y = 0. W by A2, A8, A12; :: thesis: verum

hereby :: according to GROUP_1:def 12 :: thesis: ( W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )

let v, w be Element of W; :: thesis: v * w = w * v

reconsider v1 = v, w1 = w as Element of V by A1, TARSKI:def 3;

( v * w = v1 * w1 & w * v = w1 * v1 ) by A9;

hence v * w = w * v ; :: thesis: verum

end;reconsider v1 = v, w1 = w as Element of V by A1, TARSKI:def 3;

( v * w = v1 * w1 & w * v = w1 * v1 ) by A9;

hence v * w = w * v ; :: thesis: verum

hereby :: according to GROUP_1:def 3 :: thesis: ( W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )

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, TARSKI:def 3;

a * (b * x) = the multF of V . (a,(b * x)) by A9;

then A13: a * (b * x) = a1 * (b1 * y) by A9;

a * b = a1 * b1 by A9;

then (a * b) * x = (a1 * b1) * y by A9;

hence (a * b) * x = a * (b * x) by A13, GROUP_1:def 3; :: thesis: verum

end;reconsider y = x, a1 = a, b1 = b as Element of V by A1, TARSKI:def 3;

a * (b * x) = the multF of V . (a,(b * x)) by A9;

then A13: a * (b * x) = a1 * (b1 * y) by A9;

a * b = a1 * b1 by A9;

then (a * b) * x = (a1 * b1) * y by A9;

hence (a * b) * x = a * (b * x) by A13, GROUP_1:def 3; :: thesis: verum

hereby :: according to VECTSP_1:def 4 :: thesis: ( W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )

let v be Element of W; :: thesis: v * (1. W) = v

reconsider v1 = v as Element of V by A1, TARSKI:def 3;

v * (1. W) = v1 * (1. V) by A3, A9;

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

end;reconsider v1 = v as Element of V by A1, TARSKI:def 3;

v * (1. W) = v1 * (1. V) by A3, A9;

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

hereby :: according to VECTSP_1:def 2 :: thesis: ( W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )

thus
for a being Complexlet x, y, z be Element of W; :: thesis: x * (y + z) = (x * y) + (x * z)

reconsider x1 = x, y1 = y, z1 = z as Element of V by A1, TARSKI:def 3;

y + z = y1 + z1 by A8;

then x * (y + z) = x1 * (y1 + z1) by A9;

then A14: x * (y + z) = (x1 * y1) + (x1 * z1) by VECTSP_1:def 2;

( x * y = x1 * y1 & x * z = x1 * z1 ) by A9;

hence x * (y + z) = (x * y) + (x * z) by A8, A14; :: thesis: verum

end;reconsider x1 = x, y1 = y, z1 = z as Element of V by A1, TARSKI:def 3;

y + z = y1 + z1 by A8;

then x * (y + z) = x1 * (y1 + z1) by A9;

then A14: x * (y + z) = (x1 * y1) + (x1 * z1) by VECTSP_1:def 2;

( x * y = x1 * y1 & x * z = x1 * z1 ) by A9;

hence x * (y + z) = (x * y) + (x * z) by A8, A14; :: thesis: verum

for x, y being VECTOR of W holds a * (x + y) = (a * x) + (a * y) :: according to CLVECT_1:def 2 :: thesis: ( W is scalar-distributive & W is scalar-associative & W is vector-associative )

proof

thus
for a, b being Complex
let a be Complex; :: thesis: for x, y being VECTOR of W holds a * (x + y) = (a * x) + (a * y)

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, TARSKI:def 3;

A15: a * x = a * x1 by A1, A6, Lm1;

A16: a * y = a * y1 by A1, A6, Lm1;

x + y = x1 + y1 by A8;

then a * (x + y) = a * (x1 + y1) by A1, A6, Lm1;

then a * (x + y) = (a * x1) + (a * y1) by CLVECT_1:def 2;

hence a * (x + y) = (a * x) + (a * y) by A8, A15, A16; :: 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, TARSKI:def 3;

A15: a * x = a * x1 by A1, A6, Lm1;

A16: a * y = a * y1 by A1, A6, Lm1;

x + y = x1 + y1 by A8;

then a * (x + y) = a * (x1 + y1) by A1, A6, Lm1;

then a * (x + y) = (a * x1) + (a * y1) by CLVECT_1:def 2;

hence a * (x + y) = (a * x) + (a * y) by A8, A15, A16; :: thesis: verum

for v being VECTOR of W holds (a + b) * v = (a * v) + (b * v) :: according to CLVECT_1:def 3 :: thesis: ( W is scalar-associative & W is vector-associative )

proof

thus
for a, b being Complex
let a, b be Complex; :: thesis: for v being VECTOR of W holds (a + b) * v = (a * v) + (b * v)

let x be Element of W; :: thesis: (a + b) * x = (a * x) + (b * x)

reconsider x1 = x as Element of V by A1, TARSKI:def 3;

A17: a * x = a * x1 by A1, A6, Lm1;

A18: b * x = b * x1 by A1, A6, Lm1;

(a + b) * x = (a + b) * x1 by A1, A6, Lm1;

then (a + b) * x = (a * x1) + (b * x1) by CLVECT_1:def 3;

hence (a + b) * x = (a * x) + (b * x) by A8, A17, A18; :: thesis: verum

end;let x be Element of W; :: thesis: (a + b) * x = (a * x) + (b * x)

reconsider x1 = x as Element of V by A1, TARSKI:def 3;

A17: a * x = a * x1 by A1, A6, Lm1;

A18: b * x = b * x1 by A1, A6, Lm1;

(a + b) * x = (a + b) * x1 by A1, A6, Lm1;

then (a + b) * x = (a * x1) + (b * x1) by CLVECT_1:def 3;

hence (a + b) * x = (a * x) + (b * x) by A8, A17, A18; :: thesis: verum

for v being VECTOR of W holds (a * b) * v = a * (b * v) :: according to CLVECT_1:def 4 :: thesis: W is vector-associative

proof

thus
for x, y being Element of W
let a, b be Complex; :: thesis: for v being VECTOR of W holds (a * b) * v = a * (b * v)

let x be Element of W; :: thesis: (a * b) * x = a * (b * x)

reconsider x1 = x as Element of V by A1, TARSKI:def 3;

reconsider y = b * x as Element of W ;

reconsider y1 = b * x1 as Element of V ;

A19: b * x = b * x1 by A1, A6, Lm1;

A20: a * (b * x) = a * (b * x1) by A1, A6, A19, Lm1;

(a * b) * x = (a * b) * x1 by A1, A6, Lm1;

hence (a * b) * x = a * (b * x) by A20, CLVECT_1:def 4; :: thesis: verum

end;let x be Element of W; :: thesis: (a * b) * x = a * (b * x)

reconsider x1 = x as Element of V by A1, TARSKI:def 3;

reconsider y = b * x as Element of W ;

reconsider y1 = b * x1 as Element of V ;

A19: b * x = b * x1 by A1, A6, Lm1;

A20: a * (b * x) = a * (b * x1) by A1, A6, A19, Lm1;

(a * b) * x = (a * b) * x1 by A1, A6, Lm1;

hence (a * b) * x = a * (b * x) by A20, CLVECT_1:def 4; :: thesis: verum

for a being Complex holds a * (x * y) = (a * x) * y :: according to CFUNCDOM:def 9 :: thesis: verum

proof

thus
verum
; :: thesis: verum
let x, y be Element of W; :: thesis: for a being Complex holds a * (x * y) = (a * x) * y

let a be Complex; :: thesis: a * (x * y) = (a * x) * y

reconsider x1 = x, y1 = y as Element of V by A1, TARSKI:def 3;

A21: a * x = a * x1 by A1, A6, Lm1;

A22: a * (x * y) = a * (x1 * y1) by A1, A6, Lm1, A9;

a * (x1 * y1) = (a * x1) * y1 by CFUNCDOM:def 9;

hence a * (x * y) = (a * x) * y by A9, A21, A22; :: thesis: verum

end;let a be Complex; :: thesis: a * (x * y) = (a * x) * y

reconsider x1 = x, y1 = y as Element of V by A1, TARSKI:def 3;

A21: a * x = a * x1 by A1, A6, Lm1;

A22: a * (x * y) = a * (x1 * y1) by A1, A6, Lm1, A9;

a * (x1 * y1) = (a * x1) * y1 by CFUNCDOM:def 9;

hence a * (x * y) = (a * x) * y by A9, A21, A22; :: thesis: verum

hence ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V by A1, A4, A5, A6, A10, Def1; :: thesis: verum