set C = CCosetSet M;
set aC = addCCoset M;
set zC = zeroCCoset M;
set lC = lmultCCoset M;
set A = CLSStruct(# (CCosetSet M),(zeroCCoset M),(addCCoset M),(lmultCCoset M) #);
A1:
CLSStruct(# (CCosetSet M),(zeroCCoset M),(addCCoset M),(lmultCCoset M) #) is Abelian
proof
let A1,
A2 be
Element of
CLSStruct(#
(CCosetSet M),
(zeroCCoset M),
(addCCoset M),
(lmultCCoset M) #);
RLVECT_1:def 2 A1 + A2 = A2 + A1
A1 in CCosetSet M
;
then consider a being
PartFunc of
X,
COMPLEX such that A2:
(
A1 = a.e-Ceq-class (
a,
M) &
a in L1_CFunctions M )
;
A2 in CCosetSet M
;
then consider b being
PartFunc of
X,
COMPLEX such that A3:
(
A2 = a.e-Ceq-class (
b,
M) &
b in L1_CFunctions M )
;
A4:
b in A2
by A3, Th31;
A5:
a in A1
by A2, Th31;
then
A1 + A2 = a.e-Ceq-class (
(a + b),
M)
by A4, Def16;
hence
A1 + A2 = A2 + A1
by A5, A4, Def16;
verum
end;
A6:
CLSStruct(# (CCosetSet M),(zeroCCoset M),(addCCoset M),(lmultCCoset M) #) is right_zeroed
proof
set z =
X --> 0c;
A7:
X --> 0c in L1_CFunctions M
by Lm3;
A8:
X --> 0c in 0. CLSStruct(#
(CCosetSet M),
(zeroCCoset M),
(addCCoset M),
(lmultCCoset M) #)
by A7, Th31;
let A1 be
Element of
CLSStruct(#
(CCosetSet M),
(zeroCCoset M),
(addCCoset M),
(lmultCCoset M) #);
RLVECT_1:def 4 A1 + (0. CLSStruct(# (CCosetSet M),(zeroCCoset M),(addCCoset M),(lmultCCoset M) #)) = A1
A1 in CCosetSet M
;
then consider a being
PartFunc of
X,
COMPLEX such that A9:
A1 = a.e-Ceq-class (
a,
M)
and A10:
a in L1_CFunctions M
;
reconsider a1 =
a as
VECTOR of
(CLSp_L1Funct M) by A10;
reconsider a1 =
a,
z1 =
X --> 0c as
VECTOR of
(CLSp_L1Funct M) by A10, A7;
A11:
a + (X --> 0c) =
a1 + z1
by Th19
.=
a1 + (0. (CLSp_L1Funct M))
.=
a
by RLVECT_1:def 4
;
a in A1
by A9, A10, Th31;
hence
A1 + (0. CLSStruct(# (CCosetSet M),(zeroCCoset M),(addCCoset M),(lmultCCoset M) #)) = A1
by A9, A8, A11, Def16;
verum
end;
A12:
now for x, y being Complex
for A1, A2 being Element of CLSStruct(# (CCosetSet M),(zeroCCoset M),(addCCoset M),(lmultCCoset M) #) holds
( x * (A1 + A2) = (x * A1) + (x * A2) & (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & 1r * A1 = A1 )let x,
y be
Complex;
for A1, A2 being Element of CLSStruct(# (CCosetSet M),(zeroCCoset M),(addCCoset M),(lmultCCoset M) #) holds
( x * (A1 + A2) = (x * A1) + (x * A2) & (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & 1r * A1 = A1 )let A1,
A2 be
Element of
CLSStruct(#
(CCosetSet M),
(zeroCCoset M),
(addCCoset M),
(lmultCCoset M) #);
( x * (A1 + A2) = (x * A1) + (x * A2) & (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & 1r * A1 = A1 )reconsider x1 =
x,
y1 =
y as
Element of
COMPLEX by XCMPLX_0:def 2;
A1 in CCosetSet M
;
then consider a being
PartFunc of
X,
COMPLEX such that A13:
A1 = a.e-Ceq-class (
a,
M)
and A14:
a in L1_CFunctions M
;
A15:
a in A1
by A13, A14, Th31;
(lmultCCoset M) . (
x1,
A1)
= a.e-Ceq-class (
(x (#) a),
M)
by A13, A14, Th31, Def18;
then A16:
x (#) a in x * A1
by A14, Th18, Th31;
A2 in CCosetSet M
;
then consider b being
PartFunc of
X,
COMPLEX such that A17:
A2 = a.e-Ceq-class (
b,
M)
and A18:
b in L1_CFunctions M
;
reconsider a1 =
a,
b1 =
b as
VECTOR of
(CLSp_L1Funct M) by A14, A18;
A19:
x (#) a = x1 * a1
by Th20;
A20:
b in A2
by A17, A18, Th31;
(lmultCCoset M) . (
x1,
A2)
= a.e-Ceq-class (
(x (#) b),
M)
by A17, A18, Th31, Def18;
then A21:
x (#) b in x1 * A2
by A18, Th18, Th31;
a + b = a1 + b1
by Th19;
then
x (#) (a + b) = x1 * (a1 + b1)
by Th20;
then A22:
x (#) (a + b) = (x * a1) + (x * b1)
by CLVECT_1:def 2;
A23:
x (#) b = x1 * b1
by Th20;
(addCCoset M) . (
A1,
A2)
= a.e-Ceq-class (
(a + b),
M)
by A15, A20, Def16;
then A24:
a + b in A1 + A2
by A14, A18, Th17, Th31;
x1 * (A1 + A2) =
(lmultCCoset M) . (
x1,
(A1 + A2))
.=
a.e-Ceq-class (
(x (#) (a + b)),
M)
by A24, Def18
.=
a.e-Ceq-class (
((x (#) a) + (x (#) b)),
M)
by A19, A22, A23, Th19
;
hence
x * (A1 + A2) = (x * A1) + (x * A2)
by A16, A21, Def16;
( (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & 1r * A1 = A1 )A25:
y (#) a = y1 * a1
by Th20;
(lmultCCoset M) . (
y1,
A1)
= a.e-Ceq-class (
(y (#) a),
M)
by A13, A14, Th31, Def18;
then A26:
y (#) a in y1 * A1
by A14, Th18, Th31;
A27:
(x + y) (#) a =
(x1 + y1) * a1
by Th20
.=
(x * a1) + (y * a1)
by CLVECT_1:def 3
.=
(x (#) a) + (y (#) a)
by A25, A19, Th19
;
(x1 + y1) * A1 =
(lmultCCoset M) . (
(x1 + y1),
A1)
.=
a.e-Ceq-class (
((x (#) a) + (y (#) a)),
M)
by A27, A13, A14, Th31, Def18
;
hence
(x + y) * A1 = (x * A1) + (y * A1)
by A16, A26, Def16;
( (x * y) * A1 = x * (y * A1) & 1r * A1 = A1 )A28:
x1 (#) (y1 (#) a) =
x1 * (y1 * a1)
by A25, Th20
.=
(x1 * y1) * a1
by CLVECT_1:def 4
.=
(x1 * y1) (#) a
by Th20
;
(x1 * y1) * A1 =
(lmultCCoset M) . (
(x1 * y1),
A1)
.=
a.e-Ceq-class (
(x1 (#) (y1 (#) a)),
M)
by A28, A13, A14, Th31, Def18
.=
(lmultCCoset M) . (
x1,
(y1 * A1))
by A26, Def18
.=
x * (y * A1)
;
hence
(x * y) * A1 = x * (y * A1)
;
1r * A1 = A1A29:
1r (#) a =
1r * a1
by Th20
.=
a
by CLVECT_1:def 5
;
thus 1r * A1 =
(lmultCCoset M) . (
1r,
A1)
.=
A1
by A13, A29, A14, Th31, Def18
;
verum end;
A30:
CLSStruct(# (CCosetSet M),(zeroCCoset M),(addCCoset M),(lmultCCoset M) #) is right_complementable
proof
let A1 be
Element of
CLSStruct(#
(CCosetSet M),
(zeroCCoset M),
(addCCoset M),
(lmultCCoset M) #);
ALGSTR_0:def 16 A1 is right_complementable
A1 in CCosetSet M
;
then consider a being
PartFunc of
X,
COMPLEX such that A31:
A1 = a.e-Ceq-class (
a,
M)
and A32:
a in L1_CFunctions M
;
set A2 =
a.e-Ceq-class (
((- 1r) (#) a),
M);
A33:
(- 1r) (#) a in L1_CFunctions M
by A32, Th18;
then
a.e-Ceq-class (
((- 1r) (#) a),
M)
in CCosetSet M
;
then reconsider A2 =
a.e-Ceq-class (
((- 1r) (#) a),
M) as
Element of
CLSStruct(#
(CCosetSet M),
(zeroCCoset M),
(addCCoset M),
(lmultCCoset M) #) ;
A34:
(
a in A1 &
(- 1r) (#) a in A2 )
by A31, A32, Th18, Th31;
reconsider a1 =
a as
VECTOR of
(CLSp_L1Funct M) by A32;
take
A2
;
ALGSTR_0:def 11 A1 + A2 = 0. CLSStruct(# (CCosetSet M),(zeroCCoset M),(addCCoset M),(lmultCCoset M) #)
consider v,
g being
PartFunc of
X,
COMPLEX such that
v in L1_CFunctions M
and
g in L1_CFunctions M
and A35:
v = a1 + ((- 1r) * a1)
and A36:
g = X --> 0c
and A37:
v a.e.cpfunc= g,
M
by Th21;
A38:
X --> 0c in L1_CFunctions M
by Lm3;
A39:
a + ((- 1r) (#) a) in L1_CFunctions M
by A32, A33, Th17;
(- 1r) (#) a = (- 1r) * a1
by Th20;
then
a + ((- 1r) (#) a) a.e.cpfunc= g,
M
by A35, A37, Th19;
then
0. CLSStruct(#
(CCosetSet M),
(zeroCCoset M),
(addCCoset M),
(lmultCCoset M) #)
= a.e-Ceq-class (
(a + ((- 1r) (#) a)),
M)
by A36, A39, A38, Th32;
hence
A1 + A2 = 0. CLSStruct(#
(CCosetSet M),
(zeroCCoset M),
(addCCoset M),
(lmultCCoset M) #)
by A34, Def16;
verum
end;
CLSStruct(# (CCosetSet M),(zeroCCoset M),(addCCoset M),(lmultCCoset M) #) is add-associative
proof
let A1,
A2,
A3 be
Element of
CLSStruct(#
(CCosetSet M),
(zeroCCoset M),
(addCCoset M),
(lmultCCoset M) #);
RLVECT_1:def 3 (A1 + A2) + A3 = A1 + (A2 + A3)
A1 in CCosetSet M
;
then consider a being
PartFunc of
X,
COMPLEX such that A40:
A1 = a.e-Ceq-class (
a,
M)
and A41:
a in L1_CFunctions M
;
A2 in CCosetSet M
;
then consider b being
PartFunc of
X,
COMPLEX such that A42:
A2 = a.e-Ceq-class (
b,
M)
and A43:
b in L1_CFunctions M
;
A3 in CCosetSet M
;
then consider c being
PartFunc of
X,
COMPLEX such that A44:
A3 = a.e-Ceq-class (
c,
M)
and A45:
c in L1_CFunctions M
;
A46:
c in A3
by A44, A45, Th31;
A47:
b in A2
by A42, A43, Th31;
then
(addCCoset M) . (
A2,
A3)
= a.e-Ceq-class (
(b + c),
M)
by A46, Def16;
then A48:
b + c in A2 + A3
by A43, A45, Th17, Th31;
reconsider a1 =
a,
b1 =
b,
c1 =
c as
VECTOR of
(CLSp_L1Funct M) by A41, A43, A45;
b + c = b1 + c1
by Th19;
then
a + (b + c) = a1 + (b1 + c1)
by Th19;
then A49:
a + (b + c) = (a1 + b1) + c1
by RLVECT_1:def 3;
a + b = a1 + b1
by Th19;
then A50:
a + (b + c) = (a + b) + c
by A49, Th19;
A51:
a in A1
by A40, A41, Th31;
then
(addCCoset M) . (
A1,
A2)
= a.e-Ceq-class (
(a + b),
M)
by A47, Def16;
then
a + b in A1 + A2
by A41, A43, Th17, Th31;
then
(A1 + A2) + A3 = a.e-Ceq-class (
(a + (b + c)),
M)
by A46, A50, Def16;
hence
(A1 + A2) + A3 = A1 + (A2 + A3)
by A51, A48, Def16;
verum
end;
then reconsider A = CLSStruct(# (CCosetSet M),(zeroCCoset M),(addCCoset M),(lmultCCoset M) #) as non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct by A1, A6, A30, A12, CLVECT_1:def 2, CLVECT_1:def 3, CLVECT_1:def 4, CLVECT_1:def 5;
take
A
; ( the carrier of A = CCosetSet M & the addF of A = addCCoset M & 0. A = zeroCCoset M & the Mult of A = lmultCCoset M )
thus
( the carrier of A = CCosetSet M & the addF of A = addCCoset M & 0. A = zeroCCoset M & the Mult of A = lmultCCoset M )
; verum