set C = CosetSet M;
set aC = addCoset M;
set zC = zeroCoset M;
set lC = lmultCoset M;
set A = RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #);
A1:
RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) is Abelian
proof
let A1,
A2 be
Element of
RLSStruct(#
(CosetSet M),
(zeroCoset M),
(addCoset M),
(lmultCoset M) #);
RLVECT_1:def 2 A1 + A2 = A2 + A1
A1 in CosetSet M
;
then consider a being
PartFunc of
X,
REAL such that A2:
(
A1 = a.e-eq-class (
a,
M) &
a in L1_Functions M )
;
A2 in CosetSet M
;
then consider b being
PartFunc of
X,
REAL such that A3:
(
A2 = a.e-eq-class (
b,
M) &
b in L1_Functions M )
;
A4:
b in A2
by A3, Th38;
A5:
a in A1
by A2, Th38;
then
A1 + A2 = a.e-eq-class (
(a + b),
M)
by A4, Def15;
hence
A1 + A2 = A2 + A1
by A5, A4, Def15;
verum
end;
A6:
RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) is right_zeroed
proof
consider z being
PartFunc of
X,
REAL such that A7:
z = X --> 0
and A8:
z in L1_Functions M
and A9:
zeroCoset M = a.e-eq-class (
z,
M)
by Def16;
A10:
z in 0. RLSStruct(#
(CosetSet M),
(zeroCoset M),
(addCoset M),
(lmultCoset M) #)
by A8, A9, Th38;
let A1 be
Element of
RLSStruct(#
(CosetSet M),
(zeroCoset M),
(addCoset M),
(lmultCoset M) #);
RLVECT_1:def 4 A1 + (0. RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #)) = A1
A1 in CosetSet M
;
then consider a being
PartFunc of
X,
REAL such that A11:
A1 = a.e-eq-class (
a,
M)
and A12:
a in L1_Functions M
;
reconsider a1 =
a,
z1 =
z as
VECTOR of
(RLSp_L1Funct M) by A12, A8;
A13:
a + z =
a1 + z1
by Th25
.=
a1 + (0. (RLSp_L1Funct M))
by A7
.=
a
by RLVECT_1:def 4
;
a in A1
by A11, A12, Th38;
hence
A1 + (0. RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #)) = A1
by A11, A10, A13, Def15;
verum
end;
A14:
now for x, y being Real
for A1, A2 being Element of RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) holds
( x * (A1 + A2) = (x * A1) + (x * A2) & (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & 1 * A1 = A1 )let x,
y be
Real;
for A1, A2 being Element of RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) holds
( x * (A1 + A2) = (x * A1) + (x * A2) & (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & 1 * A1 = A1 )let A1,
A2 be
Element of
RLSStruct(#
(CosetSet M),
(zeroCoset M),
(addCoset M),
(lmultCoset M) #);
( x * (A1 + A2) = (x * A1) + (x * A2) & (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & 1 * A1 = A1 )reconsider x1 =
x,
y1 =
y as
Real ;
A1 in CosetSet M
;
then consider a being
PartFunc of
X,
REAL such that A15:
A1 = a.e-eq-class (
a,
M)
and A16:
a in L1_Functions M
;
A17:
a in A1
by A15, A16, Th38;
then
(lmultCoset M) . (
x1,
A1)
= a.e-eq-class (
(x (#) a),
M)
by Def17;
then A18:
x (#) a in x * A1
by A16, Th24, Th38;
A2 in CosetSet M
;
then consider b being
PartFunc of
X,
REAL such that A19:
A2 = a.e-eq-class (
b,
M)
and A20:
b in L1_Functions M
;
reconsider a1 =
a,
b1 =
b as
VECTOR of
(RLSp_L1Funct M) by A16, A20;
A21:
x (#) a = x1 * a1
by Th26;
A22:
b in A2
by A19, A20, Th38;
then
(lmultCoset M) . (
x1,
A2)
= a.e-eq-class (
(x (#) b),
M)
by Def17;
then A23:
x (#) b in x1 * A2
by A20, Th24, Th38;
a + b = a1 + b1
by Th25;
then
x (#) (a + b) = x1 * (a1 + b1)
by Th26;
then A24:
x (#) (a + b) = (x * a1) + (x * b1)
by RLVECT_1:def 5;
x (#) b = x1 * b1
by Th26;
then A25:
x (#) (a + b) = (x (#) a) + (x (#) b)
by A21, A24, Th25;
(addCoset M) . (
A1,
A2)
= a.e-eq-class (
(a + b),
M)
by A17, A22, Def15;
then
a + b in A1 + A2
by A16, A20, Th23, Th38;
then
x1 * (A1 + A2) = a.e-eq-class (
((x (#) a) + (x (#) b)),
M)
by A25, Def17;
hence
x * (A1 + A2) = (x * A1) + (x * A2)
by A18, A23, Def15;
( (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & 1 * A1 = A1 )A26:
y (#) a = y1 * a1
by Th26;
(lmultCoset M) . (
y1,
A1)
= a.e-eq-class (
(y (#) a),
M)
by A17, Def17;
then A27:
y (#) a in y1 * A1
by A16, Th24, Th38;
(x + y) (#) a =
(x1 + y1) * a1
by Th26
.=
(x * a1) + (y * a1)
by RLVECT_1:def 6
.=
(x (#) a) + (y (#) a)
by A26, A21, Th25
;
then
(x1 + y1) * A1 = a.e-eq-class (
((x (#) a) + (y (#) a)),
M)
by A17, Def17;
hence
(x + y) * A1 = (x * A1) + (y * A1)
by A18, A27, Def15;
( (x * y) * A1 = x * (y * A1) & 1 * A1 = A1 )x (#) (y (#) a) =
x * (y * a1)
by A26, Th26
.=
(x1 * y1) * a1
by RLVECT_1:def 7
.=
(x * y) (#) a
by Th26
;
then (x1 * y1) * A1 =
a.e-eq-class (
(x1 (#) (y1 (#) a)),
M)
by A17, Def17
.=
x * (y * A1)
by A27, Def17
;
hence
(x * y) * A1 = x * (y * A1)
;
1 * A1 = A11
(#) a =
1
* a1
by Th26
.=
a
by RLVECT_1:def 8
;
hence
1
* A1 = A1
by A15, A17, Def17;
verum end;
A28:
RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) is right_complementable
proof
let A1 be
Element of
RLSStruct(#
(CosetSet M),
(zeroCoset M),
(addCoset M),
(lmultCoset M) #);
ALGSTR_0:def 16 A1 is right_complementable
A1 in CosetSet M
;
then consider a being
PartFunc of
X,
REAL such that A29:
A1 = a.e-eq-class (
a,
M)
and A30:
a in L1_Functions M
;
set A2 =
a.e-eq-class (
((- 1) (#) a),
M);
A31:
(- 1) (#) a in L1_Functions M
by A30, Th24;
then
a.e-eq-class (
((- 1) (#) a),
M)
in CosetSet M
;
then reconsider A2 =
a.e-eq-class (
((- 1) (#) a),
M) as
Element of
RLSStruct(#
(CosetSet M),
(zeroCoset M),
(addCoset M),
(lmultCoset M) #) ;
A32:
(
a in A1 &
(- 1) (#) a in A2 )
by A29, A30, Th24, Th38;
reconsider a1 =
a as
VECTOR of
(RLSp_L1Funct M) by A30;
take
A2
;
ALGSTR_0:def 11 A1 + A2 = 0. RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #)
consider v,
g being
PartFunc of
X,
REAL such that
v in L1_Functions M
and
g in L1_Functions M
and A33:
v = a1 + ((- 1) * a1)
and A34:
g = X --> 0
and A35:
v a.e.= g,
M
by Th27;
A36:
ex
z being
PartFunc of
X,
REAL st
(
z = X --> 0 &
z in L1_Functions M &
zeroCoset M = a.e-eq-class (
z,
M) )
by Def16;
A37:
a + ((- 1) (#) a) in L1_Functions M
by A30, A31, Th23;
(- 1) (#) a = (- 1) * a1
by Th26;
then
a + ((- 1) (#) a) a.e.= g,
M
by A33, A35, Th25;
then
0. RLSStruct(#
(CosetSet M),
(zeroCoset M),
(addCoset M),
(lmultCoset M) #)
= a.e-eq-class (
(a + ((- 1) (#) a)),
M)
by A34, A37, A36, Th39;
hence
A1 + A2 = 0. RLSStruct(#
(CosetSet M),
(zeroCoset M),
(addCoset M),
(lmultCoset M) #)
by A32, Def15;
verum
end;
RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) is add-associative
proof
let A1,
A2,
A3 be
Element of
RLSStruct(#
(CosetSet M),
(zeroCoset M),
(addCoset M),
(lmultCoset M) #);
RLVECT_1:def 3 (A1 + A2) + A3 = A1 + (A2 + A3)
A1 in CosetSet M
;
then consider a being
PartFunc of
X,
REAL such that A38:
A1 = a.e-eq-class (
a,
M)
and A39:
a in L1_Functions M
;
A2 in CosetSet M
;
then consider b being
PartFunc of
X,
REAL such that A40:
A2 = a.e-eq-class (
b,
M)
and A41:
b in L1_Functions M
;
A3 in CosetSet M
;
then consider c being
PartFunc of
X,
REAL such that A42:
A3 = a.e-eq-class (
c,
M)
and A43:
c in L1_Functions M
;
A44:
c in A3
by A42, A43, Th38;
A45:
b in A2
by A40, A41, Th38;
then
(addCoset M) . (
A2,
A3)
= a.e-eq-class (
(b + c),
M)
by A44, Def15;
then A46:
b + c in A2 + A3
by A41, A43, Th23, Th38;
reconsider a1 =
a,
b1 =
b,
c1 =
c as
VECTOR of
(RLSp_L1Funct M) by A39, A41, A43;
b + c = b1 + c1
by Th25;
then
a + (b + c) = a1 + (b1 + c1)
by Th25;
then A47:
a + (b + c) = (a1 + b1) + c1
by RLVECT_1:def 3;
a + b = a1 + b1
by Th25;
then A48:
a + (b + c) = (a + b) + c
by A47, Th25;
A49:
a in A1
by A38, A39, Th38;
then
(addCoset M) . (
A1,
A2)
= a.e-eq-class (
(a + b),
M)
by A45, Def15;
then
a + b in A1 + A2
by A39, A41, Th23, Th38;
then
(A1 + A2) + A3 = a.e-eq-class (
(a + (b + c)),
M)
by A44, A48, Def15;
hence
(A1 + A2) + A3 = A1 + (A2 + A3)
by A49, A46, Def15;
verum
end;
then reconsider A = RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) as non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct by A1, A6, A28, A14, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;
take
A
; ( the carrier of A = CosetSet M & the addF of A = addCoset M & 0. A = zeroCoset M & the Mult of A = lmultCoset M )
thus
( the carrier of A = CosetSet M & the addF of A = addCoset M & 0. A = zeroCoset M & the Mult of A = lmultCoset M )
; verum