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 26
.=
(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 26
.=
(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 26
;
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 VectSp-like VectSpStr of K by A19, A1, A4, A8, VECTSP_1:def 26;
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