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

let V be LeftMod of K; :: thesis: 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 )

let V be LeftMod of K; :: thesis: 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 )

proof

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

reconsider x = a as Element of V by Th7;

consider b being Element of V such that

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

reconsider b9 = b as Element of (opp V) by Th7;

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

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

end;proof

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

reconsider x = a, y = b as Element of V by Th7;

thus a + b = y + x by A2

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

end;reconsider x = a, y = b as Element of V by Th7;

thus a + b = y + x by A2

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

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

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

reconsider x = a, y = b, z = c as Element of V by Th7;

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 V by Th7;

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 V is right_complementable

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

reconsider x = a as Element of V by Th7;

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

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

end;reconsider x = a as Element of V by Th7;

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

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

reconsider x = a as Element of V by Th7;

consider b being Element of V such that

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

reconsider b9 = b as Element of (opp V) by Th7;

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

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

now :: thesis: 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 )

hence
opp V is strict RightMod of opp K
by A3, VECTSP_2:def 9; :: thesis: verumfor 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); :: thesis: 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; :: thesis: ( (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 ;

:: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: v * (1_ (opp K)) = v

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

.= v by VECTSP_1:def 17 ; :: thesis: verum

end;( (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; :: thesis: ( (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 ;

:: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: v * (1_ (opp K)) = v

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

.= v by VECTSP_1:def 17 ; :: thesis: verum