set C = CosetSet (M,k);
set aC = addCoset (M,k);
set lC = lmultCoset (M,k);
set A = Pre-Lp-Space (M,k);
A1:
( the carrier of (Pre-Lp-Space (M,k)) = CosetSet (M,k) & the addF of (Pre-Lp-Space (M,k)) = addCoset (M,k) & 0. (Pre-Lp-Space (M,k)) = zeroCoset (M,k) & the Mult of (Pre-Lp-Space (M,k)) = lmultCoset (M,k) )
by Def11;
thus
Pre-Lp-Space (M,k) is Abelian
( Pre-Lp-Space (M,k) is add-associative & Pre-Lp-Space (M,k) is right_zeroed & Pre-Lp-Space (M,k) is right_complementable & Pre-Lp-Space (M,k) is vector-distributive & Pre-Lp-Space (M,k) is scalar-distributive & Pre-Lp-Space (M,k) is scalar-associative & Pre-Lp-Space (M,k) is scalar-unital )proof
let A1,
A2 be
Element of
(Pre-Lp-Space (M,k));
RLVECT_1:def 2 A1 + A2 = A2 + A1
A1 in CosetSet (
M,
k)
by A1;
then consider a being
PartFunc of
X,
REAL such that A2:
(
A1 = a.e-eq-class_Lp (
a,
M,
k) &
a in Lp_Functions (
M,
k) )
;
A2 in CosetSet (
M,
k)
by A1;
then consider b being
PartFunc of
X,
REAL such that A3:
(
A2 = a.e-eq-class_Lp (
b,
M,
k) &
b in Lp_Functions (
M,
k) )
;
A4:
(
a in A1 &
b in A2 )
by A2, A3, Th38;
then
A1 + A2 = a.e-eq-class_Lp (
(a + b),
M,
k)
by A1, Def8;
hence
A1 + A2 = A2 + A1
by A1, A4, Def8;
verum
end;
thus
Pre-Lp-Space (M,k) is add-associative
( Pre-Lp-Space (M,k) is right_zeroed & Pre-Lp-Space (M,k) is right_complementable & Pre-Lp-Space (M,k) is vector-distributive & Pre-Lp-Space (M,k) is scalar-distributive & Pre-Lp-Space (M,k) is scalar-associative & Pre-Lp-Space (M,k) is scalar-unital )proof
let A1,
A2,
A3 be
Element of
(Pre-Lp-Space (M,k));
RLVECT_1:def 3 (A1 + A2) + A3 = A1 + (A2 + A3)
A1 in CosetSet (
M,
k)
by A1;
then consider a being
PartFunc of
X,
REAL such that A5:
(
A1 = a.e-eq-class_Lp (
a,
M,
k) &
a in Lp_Functions (
M,
k) )
;
A2 in CosetSet (
M,
k)
by A1;
then consider b being
PartFunc of
X,
REAL such that A6:
(
A2 = a.e-eq-class_Lp (
b,
M,
k) &
b in Lp_Functions (
M,
k) )
;
A3 in CosetSet (
M,
k)
by A1;
then consider c being
PartFunc of
X,
REAL such that A7:
(
A3 = a.e-eq-class_Lp (
c,
M,
k) &
c in Lp_Functions (
M,
k) )
;
A8:
(
a in A1 &
b in A2 &
c in A3 )
by A5, A6, A7, Th38;
then
(
(addCoset (M,k)) . (
A1,
A2)
= a.e-eq-class_Lp (
(a + b),
M,
k) &
(addCoset (M,k)) . (
A2,
A3)
= a.e-eq-class_Lp (
(b + c),
M,
k) )
by A1, Def8;
then A9:
(
a + b in A1 + A2 &
b + c in A2 + A3 )
by A1, Th38, Th25, A5, A6, A7;
reconsider a1 =
a,
b1 =
b,
c1 =
c as
VECTOR of
(RLSp_LpFunct (M,k)) by A5, A6, A7;
A10:
(
a + b = a1 + b1 &
b + c = b1 + c1 )
by Th29;
then
a + (b + c) = a1 + (b1 + c1)
by Th29;
then
a + (b + c) = (a1 + b1) + c1
by RLVECT_1:def 3;
then
a + (b + c) = (a + b) + c
by A10, Th29;
then
(A1 + A2) + A3 = a.e-eq-class_Lp (
(a + (b + c)),
M,
k)
by A8, A9, Def8, A1;
hence
(A1 + A2) + A3 = A1 + (A2 + A3)
by A8, A9, Def8, A1;
verum
end;
thus
Pre-Lp-Space (M,k) is right_zeroed
( Pre-Lp-Space (M,k) is right_complementable & Pre-Lp-Space (M,k) is vector-distributive & Pre-Lp-Space (M,k) is scalar-distributive & Pre-Lp-Space (M,k) is scalar-associative & Pre-Lp-Space (M,k) is scalar-unital )proof
let A1 be
Element of
(Pre-Lp-Space (M,k));
RLVECT_1:def 4 A1 + (0. (Pre-Lp-Space (M,k))) = A1
A1 in CosetSet (
M,
k)
by A1;
then consider a being
PartFunc of
X,
REAL such that A11:
(
A1 = a.e-eq-class_Lp (
a,
M,
k) &
a in Lp_Functions (
M,
k) )
;
A12:
a in A1
by A11, Th38;
set z =
X --> 0;
A13:
X --> 0 in 0. (Pre-Lp-Space (M,k))
by A1, Th38, Th23;
reconsider a1 =
a,
z1 =
X --> 0 as
VECTOR of
(RLSp_LpFunct (M,k)) by A11, Th23;
a + (X --> 0) =
a1 + z1
by Th29
.=
a1 + (0. (RLSp_LpFunct (M,k)))
.=
a
by RLVECT_1:def 4
;
hence
A1 + (0. (Pre-Lp-Space (M,k))) = A1
by A1, A11, A12, A13, Def8;
verum
end;
thus
Pre-Lp-Space (M,k) is right_complementable
( Pre-Lp-Space (M,k) is vector-distributive & Pre-Lp-Space (M,k) is scalar-distributive & Pre-Lp-Space (M,k) is scalar-associative & Pre-Lp-Space (M,k) is scalar-unital )proof
let A1 be
Element of
(Pre-Lp-Space (M,k));
ALGSTR_0:def 16 A1 is right_complementable
A1 in CosetSet (
M,
k)
by A1;
then consider a being
PartFunc of
X,
REAL such that A14:
(
A1 = a.e-eq-class_Lp (
a,
M,
k) &
a in Lp_Functions (
M,
k) )
;
A15:
a in A1
by A14, Th38;
reconsider a1 =
a as
VECTOR of
(RLSp_LpFunct (M,k)) by A14;
A16:
(- 1) (#) a in Lp_Functions (
M,
k)
by A14, Th26;
set A2 =
a.e-eq-class_Lp (
((- 1) (#) a),
M,
k);
a.e-eq-class_Lp (
((- 1) (#) a),
M,
k)
in CosetSet (
M,
k)
by A16;
then reconsider A2 =
a.e-eq-class_Lp (
((- 1) (#) a),
M,
k) as
Element of
(Pre-Lp-Space (M,k)) by A1;
take
A2
;
ALGSTR_0:def 11 A1 + A2 = 0. (Pre-Lp-Space (M,k))
A17:
(- 1) (#) a in A2
by Th38, A14, Th26;
consider v,
g being
PartFunc of
X,
REAL such that A18:
(
v in Lp_Functions (
M,
k) &
g in Lp_Functions (
M,
k) &
v = a1 + ((- 1) * a1) &
g = X --> 0 &
v a.e.= g,
M )
by Th31;
(- 1) (#) a = (- 1) * a1
by Th30;
then
a + ((- 1) (#) a) a.e.= g,
M
by Th29, A18;
then
0. (Pre-Lp-Space (M,k)) = a.e-eq-class_Lp (
(a + ((- 1) (#) a)),
M,
k)
by Th42, A18, A1;
hence
A1 + A2 = 0. (Pre-Lp-Space (M,k))
by A15, A17, Def8, A1;
verum
end;
now for x0, y0 being Real
for A1, A2 being Element of (Pre-Lp-Space (M,k)) holds
( x0 * (A1 + A2) = (x0 * A1) + (x0 * A2) & (x0 + y0) * A1 = (x0 * A1) + (y0 * A1) & (x0 * y0) * A1 = x0 * (y0 * A1) & 1 * A1 = A1 )let x0,
y0 be
Real;
for A1, A2 being Element of (Pre-Lp-Space (M,k)) holds
( x0 * (A1 + A2) = (x0 * A1) + (x0 * A2) & (x0 + y0) * A1 = (x0 * A1) + (y0 * A1) & (x0 * y0) * A1 = x0 * (y0 * A1) & 1 * A1 = A1 )let A1,
A2 be
Element of
(Pre-Lp-Space (M,k));
( x0 * (A1 + A2) = (x0 * A1) + (x0 * A2) & (x0 + y0) * A1 = (x0 * A1) + (y0 * A1) & (x0 * y0) * A1 = x0 * (y0 * A1) & 1 * A1 = A1 )reconsider x =
x0,
y =
y0 as
Real ;
A1 in CosetSet (
M,
k)
by A1;
then consider a being
PartFunc of
X,
REAL such that A19:
(
A1 = a.e-eq-class_Lp (
a,
M,
k) &
a in Lp_Functions (
M,
k) )
;
A2 in CosetSet (
M,
k)
by A1;
then consider b being
PartFunc of
X,
REAL such that A20:
(
A2 = a.e-eq-class_Lp (
b,
M,
k) &
b in Lp_Functions (
M,
k) )
;
A21:
(
a in A1 &
b in A2 )
by A19, A20, Th38;
then
(addCoset (M,k)) . (
A1,
A2)
= a.e-eq-class_Lp (
(a + b),
M,
k)
by A1, Def8;
then A22:
a + b in A1 + A2
by Th38, Th25, A19, A20, A1;
reconsider a1 =
a,
b1 =
b as
VECTOR of
(RLSp_LpFunct (M,k)) by A19, A20;
A23:
(
y (#) a = y * a1 &
x (#) a = x * a1 &
x (#) b = x * b1 &
(x + y) (#) a = (x + y) * a1 & 1
(#) a = 1
* a1 )
by Th30;
a + b = a1 + b1
by Th29;
then
x (#) (a + b) = x * (a1 + b1)
by Th30;
then
x (#) (a + b) = (x * a1) + (x * b1)
by RLVECT_1:def 5;
then A24:
x (#) (a + b) = (x (#) a) + (x (#) b)
by A23, Th29;
(x + y) (#) a = (x * a1) + (y * a1)
by A23, RLVECT_1:def 6;
then A25:
(x + y) (#) a = (x (#) a) + (y (#) a)
by A23, Th29;
x (#) (y (#) a) =
x * (y * a1)
by A23, Th30
.=
(x * y) * a1
by RLVECT_1:def 7
;
then A26:
x (#) (y (#) a) = (x * y) (#) a
by Th30;
(
(lmultCoset (M,k)) . (
x,
A1)
= a.e-eq-class_Lp (
(x (#) a),
M,
k) &
(lmultCoset (M,k)) . (
x,
A2)
= a.e-eq-class_Lp (
(x (#) b),
M,
k) &
(lmultCoset (M,k)) . (
y,
A1)
= a.e-eq-class_Lp (
(y (#) a),
M,
k) )
by A1, A21, Def10;
then A27:
(
x (#) a in x * A1 &
x (#) b in x * A2 &
y (#) a in y * A1 )
by A1, Th38, Th26, A19, A20;
x * (A1 + A2) = a.e-eq-class_Lp (
((x (#) a) + (x (#) b)),
M,
k)
by A1, A24, A22, Def10;
hence
x0 * (A1 + A2) = (x0 * A1) + (x0 * A2)
by A1, A27, Def8;
( (x0 + y0) * A1 = (x0 * A1) + (y0 * A1) & (x0 * y0) * A1 = x0 * (y0 * A1) & 1 * A1 = A1 )
(x + y) * A1 = a.e-eq-class_Lp (
((x (#) a) + (y (#) a)),
M,
k)
by A1, A25, A21, Def10;
hence
(x0 + y0) * A1 = (x0 * A1) + (y0 * A1)
by A27, Def8, A1;
( (x0 * y0) * A1 = x0 * (y0 * A1) & 1 * A1 = A1 )
(x0 * y0) * A1 = a.e-eq-class_Lp (
(x (#) (y (#) a)),
M,
k)
by A1, A26, A21, Def10;
hence
(x0 * y0) * A1 = x0 * (y0 * A1)
by A27, Def10, A1;
1 * A1 = A1
1
(#) a = a
by A23, RLVECT_1:def 8;
hence
1
* A1 = A1
by A19, A21, Def10, A1;
verum end;
hence
( Pre-Lp-Space (M,k) is vector-distributive & Pre-Lp-Space (M,k) is scalar-distributive & Pre-Lp-Space (M,k) is scalar-associative & Pre-Lp-Space (M,k) is scalar-unital )
; verum