set C = CosetSet (V,W);
set aC = addCoset (V,W);
set zC = zeroCoset (V,W);
set lC = lmultCoset (V,W);
set A = VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #);
A1:
VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) is right_zeroed
proof
let A1 be
Element of
VectSpStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #);
RLVECT_1:def 7 A1 + (0. VectSpStr(# (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. VectSpStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #)
= (0. V) + W
by VECTSP_4:60;
hence A1 + (0. VectSpStr(# (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:10
;
verum
end;
A4:
VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) is right_complementable
proof
let A1 be
Element of
VectSpStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #);
ALGSTR_0:def 16 A1 is right_complementable
A5:
0. VectSpStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #)
= (0. V) + W
by VECTSP_4:60;
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
VectSpStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #) ;
take
A2
;
ALGSTR_0:def 11 A1 + A2 = 0. VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #)
thus A1 + A2 =
(a + (- a)) + W
by A6, A7, Def3
.=
0. VectSpStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #)
by A5, RLVECT_1:16
;
verum
end;
A8:
now let x,
y be
Element of
K;
for A1, A2 being Element of VectSpStr(# (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
VectSpStr(#
(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 )A9:
(lmultCoset (V,W)) . (
x,
A1)
= x * A1
by VECTSP_1:def 24;
A1 in CosetSet (
V,
W)
;
then consider aa being
Coset of
W such that A10:
A1 = aa
;
A2 in CosetSet (
V,
W)
;
then consider bb being
Coset of
W such that A11:
A2 = bb
;
consider b being
Vector of
V such that A12:
bb = b + W
by VECTSP_4:def 6;
A13:
(
(lmultCoset (V,W)) . (
x,
A2)
= x * A2 &
(lmultCoset (V,W)) . (
x,
A2)
= (x * b) + W )
by A11, A12, Def5, VECTSP_1:def 24;
A14:
(lmultCoset (V,W)) . (
y,
A1)
= y * A1
by VECTSP_1:def 24;
consider a being
Vector of
V such that A15:
aa = a + W
by VECTSP_4:def 6;
A16:
(addCoset (V,W)) . (
A1,
A2)
= (a + b) + W
by A10, A11, A15, A12, Def3;
A17:
(lmultCoset (V,W)) . (
x,
A1)
= (x * a) + W
by A10, A15, Def5;
thus x * (A1 + A2) =
(lmultCoset (V,W)) . (
x,
( the addF of VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) . (A1,A2)))
by VECTSP_1:def 24
.=
(x * (a + b)) + W
by A16, Def5
.=
((x * a) + (x * b)) + W
by VECTSP_1:def 26
.=
(x * A1) + (x * A2)
by A17, A9, A13, Def3
;
( (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & (1_ K) * A1 = A1 )A18:
(lmultCoset (V,W)) . (
y,
A1)
= (y * a) + W
by A10, A15, Def5;
thus (x + y) * A1 =
the
lmult of
VectSpStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #)
. (
(x + y),
A1)
by VECTSP_1:def 24
.=
((x + y) * a) + W
by A10, A15, Def5
.=
((x * a) + (y * a)) + W
by VECTSP_1:def 27
.=
(x * A1) + (y * A1)
by A17, A9, A18, A14, Def3
;
( (x * y) * A1 = x * (y * A1) & (1_ K) * A1 = A1 )thus (x * y) * A1 =
the
lmult of
VectSpStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #)
. (
(x * y),
A1)
by VECTSP_1:def 24
.=
((x * y) * a) + W
by A10, A15, Def5
.=
(x * (y * a)) + W
by VECTSP_1:def 28
.=
(lmultCoset (V,W)) . (
x,
(y * A1))
by A18, A14, Def5
.=
x * (y * A1)
by VECTSP_1:def 24
;
(1_ K) * A1 = A1thus (1_ K) * A1 =
the
lmult of
VectSpStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #)
. (
(1_ K),
A1)
by VECTSP_1:def 24
.=
((1_ K) * a) + W
by A10, A15, Def5
.=
A1
by A10, A15, VECTSP_1:def 29
;
verum end;
A19:
VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) is Abelian
proof
let A1,
A2 be
Element of
VectSpStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #);
RLVECT_1:def 5 A1 + A2 = A2 + A1
A1 in CosetSet (
V,
W)
;
then consider aa being
Coset of
W such that A20:
A1 = aa
;
consider a being
Vector of
V such that A21:
aa = a + W
by VECTSP_4:def 6;
A2 in CosetSet (
V,
W)
;
then consider bb being
Coset of
W such that A22:
A2 = bb
;
consider b being
Vector of
V such that A23:
bb = b + W
by VECTSP_4:def 6;
thus A1 + A2 =
(a + b) + W
by A20, A22, A21, A23, Def3
.=
A2 + A1
by A20, A22, A21, A23, Def3
;
verum
end;
VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) is add-associative
proof
let A1,
A2,
A3 be
Element of
VectSpStr(#
(CosetSet (V,W)),
(addCoset (V,W)),
(zeroCoset (V,W)),
(lmultCoset (V,W)) #);
RLVECT_1:def 6 (A1 + A2) + A3 = A1 + (A2 + A3)
A1 in CosetSet (
V,
W)
;
then consider aa being
Coset of
W such that A24:
A1 = aa
;
consider a being
Vector of
V such that A25:
aa = a + W
by VECTSP_4:def 6;
A2 in CosetSet (
V,
W)
;
then consider bb being
Coset of
W such that A26:
A2 = bb
;
consider b being
Vector of
V such that A27:
bb = b + W
by VECTSP_4:def 6;
A3 in CosetSet (
V,
W)
;
then consider cc being
Coset of
W such that A28:
A3 = cc
;
consider c being
Vector of
V such that A29:
cc = c + W
by VECTSP_4:def 6;
A30:
(addCoset (V,W)) . (
A2,
A3)
= (b + c) + W
by A26, A28, A27, A29, Def3;
(addCoset (V,W)) . (
A1,
A2)
= (a + b) + W
by A24, A26, A25, A27, Def3;
hence (A1 + A2) + A3 =
((a + b) + c) + W
by A28, A29, Def3
.=
(a + (b + c)) + W
by RLVECT_1:def 6
.=
A1 + (A2 + A3)
by A24, A25, A30, Def3
;
verum
end;
then reconsider A = VectSpStr(# (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 VectSpStr of K by A19, A1, A4, A8, VECTSP_1:def 26, VECTSP_1:def 27, VECTSP_1:def 28, VECTSP_1:def 29;
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