let K be Ring; :: thesis: for W being RightMod of K holds opp W is strict LeftMod of opp K

let W be RightMod of K; :: thesis: opp W is strict LeftMod of opp K

set R = opp K;

reconsider V = opp W as non empty ModuleStr over opp K ;

A1: addLoopStr(# the carrier of (opp W), the addF of (opp W), the ZeroF of (opp W) #) = addLoopStr(# the carrier of W, the addF of W, the ZeroF of W #) by Th9;

then A2: for a, b being Element of (opp W)

for x, y being Element of W st x = a & b = y holds

a + b = x + y ;

A3: ( opp W is Abelian & opp W is add-associative & opp W is right_zeroed & opp W is right_complementable )

let W be RightMod of K; :: thesis: opp W is strict LeftMod of opp K

set R = opp K;

reconsider V = opp W as non empty ModuleStr over opp K ;

A1: addLoopStr(# the carrier of (opp W), the addF of (opp W), the ZeroF of (opp W) #) = addLoopStr(# the carrier of W, the addF of W, the ZeroF of W #) by Th9;

then A2: for a, b being Element of (opp W)

for x, y being Element of W st x = a & b = y holds

a + b = x + y ;

A3: ( opp W is Abelian & opp W is add-associative & opp W is right_zeroed & opp W is right_complementable )

proof

thus
opp W is Abelian
:: thesis: ( opp W is add-associative & opp W is right_zeroed & opp W is right_complementable )

reconsider x = a as Element of W by Th9;

consider b being Element of W such that

A4: x + b = 0. W by ALGSTR_0:def 11;

reconsider b9 = b as Element of (opp W) by Th9;

take b9 ; :: according to ALGSTR_0:def 11 :: thesis: a + b9 = 0. (opp W)

thus a + b9 = 0. (opp W) by A1, A4; :: thesis: verum

end;proof

let a, b be Element of (opp W); :: according to RLVECT_1:def 2 :: thesis: a + b = b + a

reconsider x = a, y = b as Element of W by Th9;

thus a + b = y + x by A2

.= b + a by A1 ; :: thesis: verum

end;reconsider x = a, y = b as Element of W by Th9;

thus a + b = y + x by A2

.= b + a by A1 ; :: thesis: verum

hereby :: according to RLVECT_1:def 3 :: thesis: ( opp W is right_zeroed & opp W is right_complementable )

let a, b, c be Element of (opp W); :: thesis: (a + b) + c = a + (b + c)

reconsider x = a, y = b, z = c as Element of W by Th9;

thus (a + b) + c = (x + y) + z by A1

.= x + (y + z) by RLVECT_1:def 3

.= a + (b + c) by A1 ; :: thesis: verum

end;reconsider x = a, y = b, z = c as Element of W by Th9;

thus (a + b) + c = (x + y) + z by A1

.= x + (y + z) by RLVECT_1:def 3

.= a + (b + c) by A1 ; :: thesis: verum

hereby :: according to RLVECT_1:def 4 :: thesis: opp W is right_complementable

let a be Element of (opp W); :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable let a be Element of (opp W); :: thesis: a + (0. (opp W)) = a

reconsider x = a as Element of W by Th9;

thus a + (0. (opp W)) = x + (0. W) by A1

.= a by RLVECT_1:4 ; :: thesis: verum

end;reconsider x = a as Element of W by Th9;

thus a + (0. (opp W)) = x + (0. W) by A1

.= a by RLVECT_1:4 ; :: thesis: verum

reconsider x = a as Element of W by Th9;

consider b being Element of W such that

A4: x + b = 0. W by ALGSTR_0:def 11;

reconsider b9 = b as Element of (opp W) by Th9;

take b9 ; :: according to ALGSTR_0:def 11 :: thesis: a + b9 = 0. (opp W)

thus a + b9 = 0. (opp W) by A1, A4; :: thesis: verum

now :: thesis: for x, y being Scalar of (opp K)

for v, w being Vector of V holds

( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ (opp K)) * v = v )

hence
opp W is strict LeftMod of opp K
by A3, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17; :: thesis: verumfor v, w being Vector of V holds

( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ (opp K)) * v = v )

let x, y be Scalar of (opp K); :: thesis: for v, w being Vector of V holds

( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ (opp K)) * v = v )

let v, w be Vector of V; :: thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ (opp K)) * v = v )

reconsider p = v, q = w as Vector of W by Th9;

reconsider a = x, b = y as Scalar of K ;

A5: p * b = y * v by Th15;

A6: q * a = x * w by Th15;

A7: p * a = x * v by Th15;

v + w = p + q by Th16;

hence x * (v + w) = (p + q) * a by Th15

.= (p * a) + (q * a) by VECTSP_2:def 9

.= (x * v) + (x * w) by A7, A6, Th16 ;

:: thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ (opp K)) * v = v )

thus (x + y) * v = p * (a + b) by Th15

.= (p * a) + (p * b) by VECTSP_2:def 9

.= (x * v) + (y * v) by A5, A7, Th16 ; :: thesis: ( (x * y) * v = x * (y * v) & (1_ (opp K)) * v = v )

x * y = b * a by Lm3;

hence (x * y) * v = p * (b * a) by Th15

.= (p * b) * a by VECTSP_2:def 9

.= x * (y * v) by A5, Th15 ;

:: thesis: (1_ (opp K)) * v = v

thus (1_ (opp K)) * v = p * (1_ K) by Th15

.= v by VECTSP_2:def 9 ; :: thesis: verum

end;( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ (opp K)) * v = v )

let v, w be Vector of V; :: thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ (opp K)) * v = v )

reconsider p = v, q = w as Vector of W by Th9;

reconsider a = x, b = y as Scalar of K ;

A5: p * b = y * v by Th15;

A6: q * a = x * w by Th15;

A7: p * a = x * v by Th15;

v + w = p + q by Th16;

hence x * (v + w) = (p + q) * a by Th15

.= (p * a) + (q * a) by VECTSP_2:def 9

.= (x * v) + (x * w) by A7, A6, Th16 ;

:: thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ (opp K)) * v = v )

thus (x + y) * v = p * (a + b) by Th15

.= (p * a) + (p * b) by VECTSP_2:def 9

.= (x * v) + (y * v) by A5, A7, Th16 ; :: thesis: ( (x * y) * v = x * (y * v) & (1_ (opp K)) * v = v )

x * y = b * a by Lm3;

hence (x * y) * v = p * (b * a) by Th15

.= (p * b) * a by VECTSP_2:def 9

.= x * (y * v) by A5, Th15 ;

:: thesis: (1_ (opp K)) * v = v

thus (1_ (opp K)) * v = p * (1_ K) by Th15

.= v by VECTSP_2:def 9 ; :: thesis: verum