set C = CosetSet (V,W);
set aC = addCoset (V,W);
set zC = zeroCoset (V,W);
set lC = lmultCoset (V,W);
set A = ModuleStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #);
A1:
ModuleStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) is right_zeroed
proof
let A1 be
Element of
ModuleStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #);
RLVECT_1:def 4 A1 + (0. ModuleStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #)) = A1
A1 in CosetSet (
V,
W)
;
then consider aa being
Coset of
W such that A2:
A1 = aa
;
consider a being
Vector of
V such that A3:
aa = a + W
by VECTSP_4:def 6;
0. ModuleStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #)
= (0. V) + W
by VECTSP_4:45;
hence A1 + (0. ModuleStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #)) =
(a + (0. V)) + W
by A2, A3, Def3
.=
A1
by A2, A3, RLVECT_1:4
;
verum
end;
A4:
ModuleStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) is right_complementable
proof
let A1 be
Element of
ModuleStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #);
ALGSTR_0:def 16 A1 is right_complementable
A5:
0. ModuleStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #)
= (0. V) + W
by VECTSP_4:45;
A1 in CosetSet (
V,
W)
;
then consider aa being
Coset of
W such that A6:
A1 = aa
;
consider a being
Vector of
V such that A7:
aa = a + W
by VECTSP_4:def 6;
set A2 =
(- a) + W;
(- a) + W is
Coset of
W
by VECTSP_4:def 6;
then
(- a) + W in CosetSet (
V,
W)
;
then reconsider A2 =
(- a) + W as
Element of
ModuleStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #) ;
take
A2
;
ALGSTR_0:def 11 A1 + A2 = 0. ModuleStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #)
thus A1 + A2 =
(a + (- a)) + W
by A6, A7, Def3
.=
0. ModuleStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #)
by A5, RLVECT_1:5
;
verum
end;
A8:
now for x, y being Element of K
for A1, A2 being Element of ModuleStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) holds
( x * (A1 + A2) = (x * A1) + (x * A2) & (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & (1_ K) * A1 = A1 )let x,
y be
Element of
K;
for A1, A2 being Element of ModuleStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) holds
( x * (A1 + A2) = (x * A1) + (x * A2) & (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & (1_ K) * A1 = A1 )let A1,
A2 be
Element of
ModuleStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #);
( x * (A1 + A2) = (x * A1) + (x * A2) & (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & (1_ K) * A1 = A1 )
A1 in CosetSet (
V,
W)
;
then consider aa being
Coset of
W such that A9:
A1 = aa
;
A2 in CosetSet (
V,
W)
;
then consider bb being
Coset of
W such that A10:
A2 = bb
;
consider b being
Vector of
V such that A11:
bb = b + W
by VECTSP_4:def 6;
A12:
(
(lmultCoset (V,W)) . (
x,
A2)
= x * A2 &
(lmultCoset (V,W)) . (
x,
A2)
= (x * b) + W )
by A10, A11, Def5;
consider a being
Vector of
V such that A13:
aa = a + W
by VECTSP_4:def 6;
A14:
(addCoset (V,W)) . (
A1,
A2)
= (a + b) + W
by A9, A10, A13, A11, Def3;
A15:
(lmultCoset (V,W)) . (
x,
A1)
= (x * a) + W
by A9, A13, Def5;
thus x * (A1 + A2) =
(lmultCoset (V,W)) . (
x,
( the addF of ModuleStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) . (A1,A2)))
.=
(x * (a + b)) + W
by A14, Def5
.=
((x * a) + (x * b)) + W
by VECTSP_1:def 14
.=
(x * A1) + (x * A2)
by A15, A12, Def3
;
( (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & (1_ K) * A1 = A1 )A16:
(lmultCoset (V,W)) . (
y,
A1)
= (y * a) + W
by A9, A13, Def5;
thus (x + y) * A1 =
the
lmult of
ModuleStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #)
. (
(x + y),
A1)
.=
((x + y) * a) + W
by A9, A13, Def5
.=
((x * a) + (y * a)) + W
by VECTSP_1:def 15
.=
(x * A1) + (y * A1)
by A15, A16, Def3
;
( (x * y) * A1 = x * (y * A1) & (1_ K) * A1 = A1 )thus (x * y) * A1 =
the
lmult of
ModuleStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #)
. (
(x * y),
A1)
.=
((x * y) * a) + W
by A9, A13, Def5
.=
(x * (y * a)) + W
by VECTSP_1:def 16
.=
(lmultCoset (V,W)) . (
x,
(y * A1))
by A16, Def5
.=
x * (y * A1)
;
(1_ K) * A1 = A1thus (1_ K) * A1 =
the
lmult of
ModuleStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #)
. (
(1_ K),
A1)
.=
((1_ K) * a) + W
by A9, A13, Def5
.=
A1
by A9, A13, VECTSP_1:def 17
;
verum end;
A17:
ModuleStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) is Abelian
proof
let A1,
A2 be
Element of
ModuleStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #);
RLVECT_1:def 2 A1 + A2 = A2 + A1
A1 in CosetSet (
V,
W)
;
then consider aa being
Coset of
W such that A18:
A1 = aa
;
consider a being
Vector of
V such that A19:
aa = a + W
by VECTSP_4:def 6;
A2 in CosetSet (
V,
W)
;
then consider bb being
Coset of
W such that A20:
A2 = bb
;
consider b being
Vector of
V such that A21:
bb = b + W
by VECTSP_4:def 6;
thus A1 + A2 =
(a + b) + W
by A18, A20, A19, A21, Def3
.=
A2 + A1
by A18, A20, A19, A21, Def3
;
verum
end;
ModuleStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) is add-associative
proof
let A1,
A2,
A3 be
Element of
ModuleStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #);
RLVECT_1:def 3 (A1 + A2) + A3 = A1 + (A2 + A3)
A1 in CosetSet (
V,
W)
;
then consider aa being
Coset of
W such that A22:
A1 = aa
;
consider a being
Vector of
V such that A23:
aa = a + W
by VECTSP_4:def 6;
A2 in CosetSet (
V,
W)
;
then consider bb being
Coset of
W such that A24:
A2 = bb
;
consider b being
Vector of
V such that A25:
bb = b + W
by VECTSP_4:def 6;
A3 in CosetSet (
V,
W)
;
then consider cc being
Coset of
W such that A26:
A3 = cc
;
consider c being
Vector of
V such that A27:
cc = c + W
by VECTSP_4:def 6;
A28:
(addCoset (V,W)) . (
A2,
A3)
= (b + c) + W
by A24, A26, A25, A27, Def3;
(addCoset (V,W)) . (
A1,
A2)
= (a + b) + W
by A22, A24, A23, A25, Def3;
hence (A1 + A2) + A3 =
((a + b) + c) + W
by A26, A27, Def3
.=
(a + (b + c)) + W
by RLVECT_1:def 3
.=
A1 + (A2 + A3)
by A22, A23, A28, Def3
;
verum
end;
then reconsider A = ModuleStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) as non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over K by A17, A1, A4, A8, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17;
take
A
; ( the carrier of A = CosetSet (V,W) & the addF of A = addCoset (V,W) & 0. A = zeroCoset (V,W) & the lmult of A = lmultCoset (V,W) )
thus
( the carrier of A = CosetSet (V,W) & the addF of A = addCoset (V,W) & 0. A = zeroCoset (V,W) & the lmult of A = lmultCoset (V,W) )
; verum