:: Construction of Rings and Left-, Right-, and Bi-Modules over a Ring
:: by Micha{\l} Muzalewski
::
:: Received June 20, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

Lm1:  for L being non empty multLoopStr st L is well-unital holds
1. L = 1_ L
proofend;

registration
cluster non empty right_complementable strict unital distributive Abelian add-associative right_zeroed for doubleLoopStr ;
existence
 ex b1 being non empty doubleLoopStr st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is unital & b1 is distributive )
proofend;
end;

definition
let IT be non empty multLoopStr_0 ;
attrIT is domRing-like  means :Def1: :: VECTSP_2:def 1
 for x, y being Element of IT holds
( not x * y = 0. IT or x = 0. IT or y = 0. IT );
end;

:: deftheorem Def1 defines domRing-like VECTSP_2:def_1_:_
 for IT being non empty multLoopStr_0 holds
( IT is domRing-like iff for x, y being Element of IT holds
( not x * y = 0. IT or x = 0. IT or y = 0. IT ) );

registration
cluster non empty non degenerated right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like for doubleLoopStr ;
existence
 ex b1 being Ring st
( b1 is strict & not b1 is degenerated & b1 is commutative & b1 is almost_left_invertible & b1 is domRing-like )
proofend;
end;

definition
mode comRing is commutative Ring;
end;

definition
mode domRing is non degenerated domRing-like comRing;
end;

theorem :: VECTSP_2:1
for F being Field holds F is domRing
proofend;

definition
mode Skew-Field is non degenerated almost_left_invertible Ring;
end;

:: 10. AXIOMS OF SKEW-FIELD
registration
cluster non empty commutative left_unital  ->  non empty well-unital for multLoopStr ;
coherence
 for b1 being non empty multLoopStr st b1 is commutative & b1 is left_unital holds
b1 is well-unital
proofend;
cluster non empty commutative right_unital  ->  non empty well-unital for multLoopStr ;
coherence
 for b1 being non empty multLoopStr st b1 is commutative & b1 is right_unital holds
b1 is well-unital
proofend;
end;

Lm2:  for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for x, y, z being Scalar of R st x + y = z holds
x = z - y
proofend;

Lm3:  for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for x, z, y being Scalar of R st x = z - y holds
x + y = z
proofend;

theorem :: VECTSP_2:2
for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for x, y, z being Scalar of R holds
( ( x + y = z implies x = z - y ) & ( x = z - y implies x + y = z ) & ( x + y = z implies y = z - x ) & ( y = z - x implies x + y = z ) ) by Lm2, Lm3;

theorem Th3: :: VECTSP_2:3
for R being non empty right_complementable add-associative right_zeroed addLoopStr
for x being Element of R holds
( x = 0. R iff - x = 0. R )
proofend;

theorem :: VECTSP_2:4
for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for x, y being Element of R ex z being Element of R st
( x = y + z & x = z + y )
proofend;

theorem :: VECTSP_2:5
for F being non empty non degenerated right_complementable distributive add-associative right_zeroed doubleLoopStr
for x, y being Element of F st x * y = 1. F holds
( x <> 0. F &amp; y <> 0. F ) by VECTSP_1:6, VECTSP_1:7;

theorem Th6: :: VECTSP_2:6
for SF being non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed doubleLoopStr
for x being Element of SF st x <> 0. SF holds
ex y being Element of SF st x * y = 1. SF
proofend;

theorem Th7: :: VECTSP_2:7
for SF being non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed doubleLoopStr
for x, y being Element of SF st y * x = 1. SF holds
x * y = 1. SF
proofend;

theorem Th8: :: VECTSP_2:8
for SF being non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for x, y, z being Element of SF st x * y = x * z &amp; x <> 0. SF holds
y = z
proofend;

definition
let SF be non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let x be Element of SF;
assume A1: x <> 0. SF ;
redefine func x "  means :Def2: :: VECTSP_2:def 2
it * x = 1. SF;
compatibility
 for b1 being Element of the carrier of SF holds
( b1 = x " iff b1 * x = 1. SF )
proofend;
end;

:: deftheorem Def2 defines " VECTSP_2:def_2_:_
 for SF being non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed doubleLoopStr
for x being Element of SF st x <> 0. SF holds
for b3 being Element of the carrier of SF holds
( b3 = x " iff b3 * x = 1. SF );

definition
let SF be Skew-Field;
let x, y be Scalar of SF;
funcx / y ->  Scalar of SF equals :: VECTSP_2:def 3
x * (y ");
correctness
coherence
x * (y ") is Scalar of SF;
;
end;

:: deftheorem  defines / VECTSP_2:def_3_:_
 for SF being Skew-Field
for x, y being Scalar of SF holds x / y = x * (y ");

theorem Th9: :: VECTSP_2:9
for SF being Skew-Field
for x being Scalar of SF st x <> 0. SF holds
( x * (x ") = 1. SF &amp; (x ") * x = 1. SF )
proofend;

theorem Th10: :: VECTSP_2:10
for SF being Skew-Field
for y, x being Scalar of SF st y * x = 1_ SF holds
( x = y " &amp; y = x " )
proofend;

theorem Th11: :: VECTSP_2:11
for SF being Skew-Field
for x, y being Scalar of SF st x <> 0. SF &amp; y <> 0. SF holds
(x ") * (y ") = (y * x) "
proofend;

theorem :: VECTSP_2:12
for SF being Skew-Field
for x, y being Scalar of SF holds
( not x * y = 0. SF or x = 0. SF or y = 0. SF )
proofend;

theorem Th13: :: VECTSP_2:13
for SF being Skew-Field
for x being Scalar of SF st x <> 0. SF holds
x " <> 0. SF
proofend;

theorem Th14: :: VECTSP_2:14
for SF being Skew-Field
for x being Scalar of SF st x <> 0. SF holds
(x ") " = x
proofend;

theorem Th15: :: VECTSP_2:15
for SF being Skew-Field
for x being Scalar of SF st x <> 0. SF holds
( (1_ SF) / x = x " &amp; (1_ SF) / (x ") = x )
proofend;

theorem :: VECTSP_2:16
for SF being Skew-Field
for x being Scalar of SF st x <> 0. SF holds
( x * ((1_ SF) / x) = 1_ SF &amp; ((1_ SF) / x) * x = 1_ SF )
proofend;

theorem :: VECTSP_2:17
for SF being Skew-Field
for x being Scalar of SF st x <> 0. SF holds
x / x = 1_ SF by Th9;

theorem Th18: :: VECTSP_2:18
for SF being Skew-Field
for y, z, x being Scalar of SF st y <> 0. SF &amp; z <> 0. SF holds
x / y = (x * z) / (y * z)
proofend;

theorem Th19: :: VECTSP_2:19
for SF being Skew-Field
for y, x being Scalar of SF st y <> 0. SF holds
( - (x / y) = (- x) / y &amp; x / (- y) = - (x / y) )
proofend;

theorem :: VECTSP_2:20
for SF being Skew-Field
for z, x, y being Scalar of SF st z <> 0. SF holds
( (x / z) + (y / z) = (x + y) / z &amp; (x / z) - (y / z) = (x - y) / z )
proofend;

theorem :: VECTSP_2:21
for SF being Skew-Field
for y, z, x being Scalar of SF st y <> 0. SF &amp; z <> 0. SF holds
x / (y / z) = (x * z) / y
proofend;

theorem :: VECTSP_2:22
for SF being Skew-Field
for y, x being Scalar of SF st y <> 0. SF holds
(x / y) * y = x
proofend;

:: 13. LEFT-, RIGHT-, AND BI-MODULE STRUCTURE
definition
let FS be 1-sorted ;
attrc2 is strict ;
struct RightModStr over FS ->  addLoopStr ;
aggrRightModStr(# carrier, addF, ZeroF, rmult #) ->  RightModStr over FS;
sel rmult c2 ->  Function of [: the carrier of c2, the carrier of FS:], the carrier of c2;
end;

registration
let FS be 1-sorted ;
cluster non empty for RightModStr over FS;
existence
 not for b1 being RightModStr over FS holds b1 is empty
proofend;
end;

registration
let FS be 1-sorted ;
let A be non empty set ;
let a be BinOp of A;
let Z be Element of A;
let r be Function of [:A, the carrier of FS:],A;
cluster RightModStr(# A,a,Z,r #) ->  non empty ;
coherence
 not RightModStr(# A,a,Z,r #) is empty ;
end;

definition
let FS be non empty doubleLoopStr ;
let RMS be non empty RightModStr over FS;
mode Scalar of RMS is Element of FS;
mode Vector of RMS is Element of RMS;
end;

definition
let FS1, FS2 be 1-sorted ;
attrc3 is strict ;
struct BiModStr over FS1,FS2 ->  VectSpStr over FS1, RightModStr over FS2;
aggrBiModStr(# carrier, addF, ZeroF, lmult, rmult #) ->  BiModStr over FS1,FS2;
end;

registration
let FS1, FS2 be 1-sorted ;
cluster non empty for BiModStr over FS1,FS2;
existence
 not for b1 being BiModStr over FS1,FS2 holds b1 is empty
proofend;
end;

registration
let FS1, FS2 be 1-sorted ;
let A be non empty set ;
let a be BinOp of A;
let Z be Element of A;
let l be Function of [: the carrier of FS1,A:],A;
let r be Function of [:A, the carrier of FS2:],A;
cluster BiModStr(# A,a,Z,l,r #) ->  non empty ;
coherence
 not BiModStr(# A,a,Z,l,r #) is empty ;
end;

definition
let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;
func AbGr R ->  strict AbGroup equals :: VECTSP_2:def 4
 addLoopStr(# the carrier of R, the addF of R,(0. R) #);
coherence
 addLoopStr(# the carrier of R, the addF of R,(0. R) #) is strict AbGroup
proofend;
end;

:: deftheorem  defines AbGr VECTSP_2:def_4_:_
 for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds AbGr R = addLoopStr(# the carrier of R, the addF of R,(0. R) #);

deffunc H1( Ring) ->  VectSpStr over $1 = VectSpStr(# the carrier of $1, the addF of $1,(0. $1), the multF of $1 #);

Lm4:  for R being Ring holds
( H1(R) is Abelian &amp; H1(R) is add-associative &amp; H1(R) is right_zeroed &amp; H1(R) is right_complementable )
proofend;

registration
let R be Ring;
cluster non empty right_complementable strict Abelian add-associative right_zeroed for VectSpStr over R;
existence
 ex b1 being non empty VectSpStr over R st
( b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is strict )
proofend;
end;

definition
let R be Ring;
func LeftModule R ->  non empty right_complementable strict Abelian add-associative right_zeroed VectSpStr over R equals :: VECTSP_2:def 5
 VectSpStr(# the carrier of R, the addF of R,(0. R), the multF of R #);
coherence
 VectSpStr(# the carrier of R, the addF of R,(0. R), the multF of R #) is non empty right_complementable strict Abelian add-associative right_zeroed VectSpStr over R by Lm4;
end;

:: deftheorem  defines LeftModule VECTSP_2:def_5_:_
 for R being Ring holds LeftModule R = VectSpStr(# the carrier of R, the addF of R,(0. R), the multF of R #);

deffunc H2( Ring) ->  RightModStr over $1 = RightModStr(# the carrier of $1, the addF of $1,(0. $1), the multF of $1 #);

Lm5:  for R being Ring holds
( H2(R) is Abelian &amp; H2(R) is add-associative &amp; H2(R) is right_zeroed &amp; H2(R) is right_complementable )
proofend;

registration
let R be Ring;
cluster non empty right_complementable Abelian add-associative right_zeroed strict for RightModStr over R;
existence
 ex b1 being non empty RightModStr over R st
( b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is strict )
proofend;
end;

definition
let R be Ring;
func RightModule R ->  non empty right_complementable Abelian add-associative right_zeroed strict RightModStr over R equals :: VECTSP_2:def 6
 RightModStr(# the carrier of R, the addF of R,(0. R), the multF of R #);
coherence
 RightModStr(# the carrier of R, the addF of R,(0. R), the multF of R #) is non empty right_complementable Abelian add-associative right_zeroed strict RightModStr over R by Lm5;
end;

:: deftheorem  defines RightModule VECTSP_2:def_6_:_
 for R being Ring holds RightModule R = RightModStr(# the carrier of R, the addF of R,(0. R), the multF of R #);

definition
let R be non empty 1-sorted ;
let V be non empty RightModStr over R;
let x be Element of R;
let v be Element of V;
funcv * x ->  Element of V equals :: VECTSP_2:def 7
 the rmult of V . (v,x);
coherence
 the rmult of V . (v,x) is Element of V ;
end;

:: deftheorem  defines * VECTSP_2:def_7_:_
 for R being non empty 1-sorted
for V being non empty RightModStr over R
for x being Element of R
for v being Element of V holds v * x = the rmult of V . (v,x);

deffunc H3( Ring, Ring) ->  BiModStr over $1,$2 = BiModStr(# 1,op2,op0,(pr2 ( the carrier of $1,1)),(pr1 (1, the carrier of $2)) #);

Lm6:  for R1, R2 being Ring holds
( H3(R1,R2) is Abelian &amp; H3(R1,R2) is add-associative &amp; H3(R1,R2) is right_zeroed &amp; H3(R1,R2) is right_complementable )
proofend;

registration
let R1, R2 be Ring;
cluster non empty right_complementable Abelian add-associative right_zeroed strict for BiModStr over R1,R2;
existence
 ex b1 being non empty BiModStr over R1,R2 st
( b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is strict )
proofend;
end;

definition
let R1, R2 be Ring;
func BiModule (R1,R2) ->  non empty right_complementable Abelian add-associative right_zeroed strict BiModStr over R1,R2 equals :: VECTSP_2:def 8
 BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #);
coherence
 BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #) is non empty right_complementable Abelian add-associative right_zeroed strict BiModStr over R1,R2 by Lm6;
end;

:: deftheorem  defines BiModule VECTSP_2:def_8_:_
 for R1, R2 being Ring holds BiModule (R1,R2) = BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #);

theorem Th23: :: VECTSP_2:23
for R being Ring
for x, y being Scalar of R
for v, w being Vector of (LeftModule R) holds
( x * (v + w) = (x * v) + (x * w) &amp; (x + y) * v = (x * v) + (y * v) &amp; (x * y) * v = x * (y * v) &amp; (1. R) * v = v )
proofend;

registration
let R be Ring;
cluster non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed for VectSpStr over R;
existence
 ex b1 being non empty VectSpStr over R st
( b1 is vector-distributive &amp; b1 is scalar-distributive &amp; b1 is scalar-associative &amp; b1 is scalar-unital &amp; b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is strict )
proofend;
end;

definition
let R be Ring;
mode LeftMod of R is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R;
end;

Lm7:  for R being Ring holds
( LeftModule R is vector-distributive &amp; LeftModule R is scalar-distributive &amp; LeftModule R is scalar-associative &amp; LeftModule R is scalar-unital )
proofend;

registration
let R be Ring;
cluster LeftModule R ->  non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ;
coherence
 ( LeftModule R is Abelian &amp; LeftModule R is add-associative &amp; LeftModule R is right_zeroed &amp; LeftModule R is right_complementable &amp; LeftModule R is strict &amp; LeftModule R is vector-distributive &amp; LeftModule R is scalar-distributive &amp; LeftModule R is scalar-associative &amp; LeftModule R is scalar-unital ) by Lm7;
end;

:: 18. AXIOMS OF LEFT MODULE OF RING
theorem Th24: :: VECTSP_2:24
for R being Ring
for x, y being Scalar of R
for v, w being Vector of (RightModule R) holds
( (v + w) * x = (v * x) + (w * x) &amp; v * (x + y) = (v * x) + (v * y) &amp; v * (y * x) = (v * y) * x &amp; v * (1_ R) = v )
proofend;

definition
let R be non empty doubleLoopStr ;
let IT be non empty RightModStr over R;
attrIT is RightMod-like  means :Def9: :: VECTSP_2:def 9
 for x, y being Scalar of R
for v, w being Vector of IT holds
( (v + w) * x = (v * x) + (w * x) &amp; v * (x + y) = (v * x) + (v * y) &amp; v * (y * x) = (v * y) * x &amp; v * (1_ R) = v );
end;

:: deftheorem Def9 defines RightMod-like VECTSP_2:def_9_:_
 for R being non empty doubleLoopStr
for IT being non empty RightModStr over R holds
( IT is RightMod-like iff for x, y being Scalar of R
for v, w being Vector of IT holds
( (v + w) * x = (v * x) + (w * x) &amp; v * (x + y) = (v * x) + (v * y) &amp; v * (y * x) = (v * y) * x &amp; v * (1_ R) = v ) );

registration
let R be Ring;
cluster non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like for RightModStr over R;
existence
 ex b1 being non empty RightModStr over R st
( b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is RightMod-like &amp; b1 is strict )
proofend;
end;

definition
let R be Ring;
mode RightMod of R is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R;
end;

Lm8:  for R being Ring holds RightModule R is RightMod-like
proofend;

registration
let R be Ring;
cluster RightModule R ->  non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like ;
coherence
 ( RightModule R is Abelian &amp; RightModule R is add-associative &amp; RightModule R is right_zeroed &amp; RightModule R is right_complementable &amp; RightModule R is RightMod-like ) by Lm8;
end;

Lm9:  for R1, R2 being Ring
for x, y being Scalar of R1
for p, q being Scalar of R2
for v, w being Vector of (BiModule (R1,R2)) holds
( x * (v + w) = (x * v) + (x * w) &amp; (x + y) * v = (x * v) + (y * v) &amp; (x * y) * v = x * (y * v) &amp; (1_ R1) * v = v &amp; (v + w) * p = (v * p) + (w * p) &amp; v * (p + q) = (v * p) + (v * q) &amp; v * (q * p) = (v * q) * p &amp; v * (1_ R2) = v &amp; x * (v * p) = (x * v) * p )
proofend;

definition
let R1, R2 be Ring;
let IT be non empty BiModStr over R1,R2;
attrIT is BiMod-like  means :Def10: :: VECTSP_2:def 10
 for x being Scalar of R1
for p being Scalar of R2
for v being Vector of IT holds x * (v * p) = (x * v) * p;
end;

:: deftheorem Def10 defines BiMod-like VECTSP_2:def_10_:_
 for R1, R2 being Ring
for IT being non empty BiModStr over R1,R2 holds
( IT is BiMod-like iff for x being Scalar of R1
for p being Scalar of R2
for v being Vector of IT holds x * (v * p) = (x * v) * p );

registration
let R1, R2 be Ring;
cluster non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed strict RightMod-like BiMod-like for BiModStr over R1,R2;
existence
 ex b1 being non empty BiModStr over R1,R2 st
( b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is RightMod-like &amp; b1 is vector-distributive &amp; b1 is scalar-distributive &amp; b1 is scalar-associative &amp; b1 is scalar-unital &amp; b1 is BiMod-like &amp; b1 is strict )
proofend;
end;

definition
let R1, R2 be Ring;
mode BiMod of R1,R2 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed RightMod-like BiMod-like BiModStr over R1,R2;
end;

theorem :: VECTSP_2:25
for R1, R2 being Ring
for V being non empty BiModStr over R1,R2 holds
( ( for x, y being Scalar of R1
for p, q being Scalar of R2
for v, w being Vector of V holds
( x * (v + w) = (x * v) + (x * w) &amp; (x + y) * v = (x * v) + (y * v) &amp; (x * y) * v = x * (y * v) &amp; (1_ R1) * v = v &amp; (v + w) * p = (v * p) + (w * p) &amp; v * (p + q) = (v * p) + (v * q) &amp; v * (q * p) = (v * q) * p &amp; v * (1_ R2) = v &amp; x * (v * p) = (x * v) * p ) ) iff ( V is RightMod-like &amp; V is vector-distributive &amp; V is scalar-distributive &amp; V is scalar-associative &amp; V is scalar-unital &amp; V is BiMod-like ) ) by Def9, Def10, VECTSP_1:def_14, VECTSP_1:def_15, VECTSP_1:def_16, VECTSP_1:def_17;

theorem Th26: :: VECTSP_2:26
for R1, R2 being Ring holds BiModule (R1,R2) is BiMod of R1,R2
proofend;

registration
let R1, R2 be Ring;
cluster BiModule (R1,R2) ->  non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed strict RightMod-like BiMod-like ;
coherence
 ( BiModule (R1,R2) is Abelian &amp; BiModule (R1,R2) is add-associative &amp; BiModule (R1,R2) is right_zeroed &amp; BiModule (R1,R2) is right_complementable &amp; BiModule (R1,R2) is RightMod-like &amp; BiModule (R1,R2) is vector-distributive &amp; BiModule (R1,R2) is scalar-distributive &amp; BiModule (R1,R2) is scalar-associative &amp; BiModule (R1,R2) is scalar-unital &amp; BiModule (R1,R2) is BiMod-like ) by Th26;
end;

theorem :: VECTSP_2:27
for L being non empty multLoopStr st L is well-unital holds
1. L = 1_ L by Lm1;

begin

theorem :: VECTSP_2:28
for K being non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr
for a being Element of K holds a * (- (1. K)) = - a
proofend;

theorem :: VECTSP_2:29
for K being non empty right_complementable left-distributive left_unital add-associative right_zeroed doubleLoopStr
for a being Element of K holds (- (1. K)) * a = - a
proofend;

theorem :: VECTSP_2:30
for F being non degenerated almost_left_invertible Ring
for x being Scalar of F
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed VectSpStr over F
for v being Vector of V holds
( x * v = 0. V iff ( x = 0. F or v = 0. V ) )
proofend;

theorem :: VECTSP_2:31
for F being non degenerated almost_left_invertible Ring
for x being Scalar of F
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed VectSpStr over F
for v being Vector of V st x <> 0. F holds
(x ") * (x * v) = v
proofend;

theorem Th32: :: VECTSP_2:32
for R being non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over R
for x being Scalar of R
for v being Vector of V holds
( v * (0. R) = 0. V &amp; v * (- (1_ R)) = - v &amp; (0. V) * x = 0. V )
proofend;

theorem Th33: :: VECTSP_2:33
for R being non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over R
for x being Scalar of R
for v, w being Vector of V holds
( - (v * x) = v * (- x) &amp; w - (v * x) = w + (v * (- x)) )
proofend;

theorem Th34: :: VECTSP_2:34
for R being non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over R
for x being Scalar of R
for v being Vector of V holds (- v) * x = - (v * x)
proofend;

theorem :: VECTSP_2:35
for R being non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over R
for x being Scalar of R
for v, w being Vector of V holds (v - w) * x = (v * x) - (w * x)
proofend;

theorem :: VECTSP_2:36
for F being non degenerated almost_left_invertible Ring
for x being Scalar of F
for V being non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over F
for v being Vector of V holds
( v * x = 0. V iff ( x = 0. F or v = 0. V ) )
proofend;

theorem :: VECTSP_2:37
for F being non degenerated almost_left_invertible Ring
for x being Scalar of F
for V being non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over F
for v being Vector of V st x <> 0. F holds
(v * x) * (x ") = v
proofend;