let K be Ring; for V being LeftMod of K holds opp V is strict RightMod of opp K
let V be LeftMod of K; opp V is strict RightMod of opp K
set R = opp K;
reconsider W = opp V as non empty RightModStr over opp K ;
A1:
addLoopStr(# the carrier of (opp V), the addF of (opp V), the ZeroF of (opp V) #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #)
by Th7;
then A2:
for a, b being Element of (opp V)
for x, y being Element of V st x = a & b = y holds
a + b = x + y
;
A3:
( opp V is Abelian & opp V is add-associative & opp V is right_zeroed & opp V is right_complementable )
now for x, y being Scalar of (opp K)
for v, w being Vector of W holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ (opp K)) = v )let x,
y be
Scalar of
(opp K);
for v, w being Vector of W holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ (opp K)) = v )let v,
w be
Vector of
W;
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ (opp K)) = v )reconsider p =
v,
q =
w as
Vector of
V by Th7;
reconsider a =
x,
b =
y as
Scalar of
K ;
A5:
b * p = v * y
by Th12;
A6:
a * q = w * x
by Th12;
A7:
a * p = v * x
by Th12;
v + w = p + q
by Th13;
hence (v + w) * x =
a * (p + q)
by Th12
.=
(a * p) + (a * q)
by VECTSP_1:def 14
.=
(v * x) + (w * x)
by A7, A6, Th13
;
( v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ (opp K)) = v )thus v * (x + y) =
(a + b) * p
by Th12
.=
(a * p) + (b * p)
by VECTSP_1:def 15
.=
(v * x) + (v * y)
by A5, A7, Th13
;
( v * (y * x) = (v * y) * x & v * (1_ (opp K)) = v )thus v * (y * x) =
(a * b) * p
by Lm3, Th12
.=
a * (b * p)
by VECTSP_1:def 16
.=
(v * y) * x
by A5, Th12
;
v * (1_ (opp K)) = vthus v * (1_ (opp K)) =
(1_ K) * p
by Th12
.=
v
by VECTSP_1:def 17
;
verum end;
hence
opp V is strict RightMod of opp K
by A3, VECTSP_2:def 9; verum