let R be Ring; for V being LeftMod of R
for W being Subspace of V
for Ws being strict Subspace of V st Ws = (Omega). W holds
addCoset (V,W) = addCoset (V,Ws)
let V be LeftMod of R; for W being Subspace of V
for Ws being strict Subspace of V st Ws = (Omega). W holds
addCoset (V,W) = addCoset (V,Ws)
let W be Subspace of V; for Ws being strict Subspace of V st Ws = (Omega). W holds
addCoset (V,W) = addCoset (V,Ws)
let Ws be strict Subspace of V; ( Ws = (Omega). W implies addCoset (V,W) = addCoset (V,Ws) )
assume AS:
Ws = (Omega). W
; addCoset (V,W) = addCoset (V,Ws)
set f1 = addCoset (V,W);
set f2 = addCoset (V,Ws);
set C = CosetSet (V,W);
set Cs = CosetSet (V,Ws);
A14:
CosetSet (V,W) = CosetSet (V,Ws)
by AS, LmStrict1;
now for A, B being Element of CosetSet (V,W) holds (addCoset (V,W)) . (A,B) = (addCoset (V,Ws)) . (A,B)let A,
B be
Element of
CosetSet (
V,
W);
(addCoset (V,W)) . (A,B) = (addCoset (V,Ws)) . (A,B)
A in CosetSet (
V,
W)
;
then consider A1 being
Coset of
W such that A17:
A1 = A
;
consider a being
Vector of
V such that A18:
A1 = a + W
by VECTSP_4:def 6;
B in CosetSet (
V,
W)
;
then consider B1 being
Coset of
W such that A19:
B1 = B
;
consider b being
Vector of
V such that A20:
B1 = b + W
by VECTSP_4:def 6;
reconsider As =
A as
Element of
CosetSet (
V,
Ws)
by AS, LmStrict1;
A21:
As = a + Ws
by AS, A17, A18, LmStrict11a;
reconsider Bs =
B as
Element of
CosetSet (
V,
Ws)
by AS, LmStrict1;
A22:
Bs = b + Ws
by AS, A19, A20, LmStrict11a;
thus (addCoset (V,W)) . (
A,
B) =
(a + b) + W
by A17, A19, A18, A20, VECTSP10:def 3
.=
(a + b) + Ws
by LmStrict11a, AS
.=
(addCoset (V,Ws)) . (
A,
B)
by A21, A22, VECTSP10:def 3
;
verum end;
hence
addCoset (V,W) = addCoset (V,Ws)
by A14, BINOP_1:2; verum