:: VECTSP_2 semantic presentation

begin

  Lm1:  for L being non empty multLoopStr st L is well-unital holds
1. L = 1_ L
proof
let L be non empty multLoopStr ; ::_thesis: ( L is well-unital implies 1. L = 1_ L )
assume A1: L is well-unital ; ::_thesis: 1. L = 1_ L
then  for h being Element of L holds
( h * (1. L) = h & (1. L) * h = h ) by VECTSP_1:def_6;
hence  1. L = 1_ L by A1, GROUP_1:def_4; ::_thesis: verum
end;

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 )
proof
set F = the strict Field;
 ( the strict Field is unital & the strict Field is distributive ) ;
hence  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 ) ; ::_thesis: verum
end;
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 )
proof
set F = the strict Field;
 for x, y being Scalar of the strict Field holds
( not x * y = 0. the strict Field or x = 0. the strict Field or y = 0. the strict Field ) by VECTSP_1:12;
then A1: the strict Field is domRing-like by Def1;
reconsider F = the strict Field as Ring ;
thus  ex b1 being Ring st
( b1 is strict & not b1 is degenerated & b1 is commutative & b1 is almost_left_invertible & b1 is domRing-like ) by A1; ::_thesis: verum
end;
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
proof
let F be Field; ::_thesis: F is domRing
 for x, y being Scalar of F holds
( not x * y = 0. F or x = 0. F or y = 0. F ) by VECTSP_1:12;
hence  F is domRing by Def1; ::_thesis: verum
end;

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

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
proof
let F be non empty multLoopStr ; ::_thesis: ( F is commutative & F is left_unital implies F is well-unital )
assume A1: ( F is commutative & F is left_unital ) ; ::_thesis: F is well-unital
let x be Scalar of F; :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. F) = x & (1. F) * x = x )
 for F being non empty commutative multMagma
for x, y being Element of F holds x * y = y * x ;
then  x * (1. F) = (1. F) * x by A1;
hence  ( x * (1. F) = x & (1. F) * x = x ) by A1, VECTSP_1:def_8; ::_thesis: verum
end;
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
proof
let F be non empty multLoopStr ; ::_thesis: ( F is commutative & F is right_unital implies F is well-unital )
assume A2: ( F is commutative & F is right_unital ) ; ::_thesis: F is well-unital
let x be Element of F; :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. F) = x & (1. F) * x = x )
 for F being non empty commutative multMagma
for x, y being Element of F holds x * y = y * x ;
then  x * (1. F) = (1. F) * x by A2;
hence  ( x * (1. F) = x & (1. F) * x = x ) by A2, VECTSP_1:def_4; ::_thesis: verum
end;
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
proof
let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for x, y, z being Scalar of R st x + y = z holds
x = z - y
let x, y, z be Scalar of R; ::_thesis: ( x + y = z implies x = z - y )
assume A1: x + y = z ; ::_thesis: x = z - y
thus x = x + (0. R) by RLVECT_1:4
.= x + (y + (- y)) by RLVECT_1:def_10
.= z - y by A1, RLVECT_1:def_3 ; ::_thesis: verum
end;

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
proof
let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for x, z, y being Scalar of R st x = z - y holds
x + y = z
let x, z, y be Scalar of R; ::_thesis: ( x = z - y implies x + y = z )
assume  x = z - y ; ::_thesis: x + y = z
then x + y = z + (y + (- y)) by RLVECT_1:def_3
.= z + (0. R) by RLVECT_1:def_10
.= z by RLVECT_1:4 ;
hence  x + y = z ; ::_thesis: verum
end;

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 )
proof
let R be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for x being Element of R holds
( x = 0. R iff - x = 0. R )
let x be Element of R; ::_thesis: ( x = 0. R iff - x = 0. R )
thus  ( x = 0. R implies - x = 0. R ) by RLVECT_1:12; ::_thesis: ( - x = 0. R implies x = 0. R )
assume  - x = 0. R ; ::_thesis: x = 0. R
then  - (- x) = 0. R by RLVECT_1:12;
hence  x = 0. R by RLVECT_1:17; ::_thesis: verum
end;

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 )
proof
let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for x, y being Element of R ex z being Element of R st
( x = y + z & x = z + y )
let x, y be Element of R; ::_thesis: ex z being Element of R st
( x = y + z & x = z + y )
take z = (- y) + x; ::_thesis: ( x = y + z & x = z + y )
z + y = x + ((- y) + y) by RLVECT_1:def_3
.= x + (0. R) by RLVECT_1:5
.= x by RLVECT_1:4 ;
hence  ( x = y + z & x = z + y ) ; ::_thesis: verum
end;


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 & 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
proof
let SF be non empty non degenerated right_complementable almost_left_invertible associative right_unital well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for x being Element of SF st x <> 0. SF holds
ex y being Element of SF st x * y = 1. SF
let x be Element of SF; ::_thesis: ( x <> 0. SF implies ex y being Element of SF st x * y = 1. SF )
assume  x <> 0. SF ; ::_thesis: ex y being Element of SF st x * y = 1. SF
then consider y being Element of SF such that
A1: y * x = 1. SF by VECTSP_1:def_9;
take  y ; ::_thesis: x * y = 1. SF
 y <> 0. SF by A1, VECTSP_1:7;
then consider z being Element of SF such that
A2: z * y = 1. SF by VECTSP_1:def_9;
z = z * (y * x) by A1, VECTSP_1:def_6
.= (1. SF) * x by A2, GROUP_1:def_3
.= x by VECTSP_1:def_6 ;
hence  x * y = 1. SF by A2; ::_thesis: verum
end;

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
proof
let SF be non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for x, y being Element of SF st y * x = 1. SF holds
x * y = 1. SF
let x, y be Element of SF; ::_thesis: ( y * x = 1. SF implies x * y = 1. SF )
assume A1: y * x = 1. SF ; ::_thesis: x * y = 1. SF
then  x <> 0. SF by VECTSP_1:6;
then consider z being Element of SF such that
A2: x * z = 1_ SF by Th6;
y = y * (x * z) by A2, VECTSP_1:def_4
.= (1_ SF) * z by A1, GROUP_1:def_3
.= z by VECTSP_1:def_8 ;
hence  x * y = 1. SF by A2; ::_thesis: verum
end;

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 & x <> 0. SF holds
y = z
proof
let SF be non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for x, y, z being Element of SF st x * y = x * z & x <> 0. SF holds
y = z
let x, y, z be Element of SF; ::_thesis: ( x * y = x * z & x <> 0. SF implies y = z )
assume that
A1: x * y = x * z and
A2: x <> 0. SF ; ::_thesis: y = z
consider u being Element of SF such that
A3: x * u = 1_ SF by A2, Th6;
A4: u * x = 1_ SF by A3, Th7;
then y = (u * x) * y by VECTSP_1:def_8
.= u * (x * z) by A1, GROUP_1:def_3
.= (1_ SF) * z by A4, GROUP_1:def_3
.= z by VECTSP_1:def_8 ;
hence  y = z ; ::_thesis: verum
end;

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 )
proof
let IT be Element of SF; ::_thesis: ( IT = x " iff IT * x = 1. SF )
A2: x is left_invertible by A1, ALGSTR_0:def_39;
then consider y being Element of SF such that
A3: y * x = 1. SF by ALGSTR_0:def_27;
 x is right_invertible
proof
take  y ; :: according to ALGSTR_0:def_28 ::_thesis: x * y = 1. SF
thus  x * y = 1. SF by A3, Th7; ::_thesis: verum
end;
then consider x1 being Element of SF such that
A4: x * x1 = 1. SF by ALGSTR_0:def_28;
 x is right_mult-cancelable
proof
let y, z be Element of SF; :: according to ALGSTR_0:def_21 ::_thesis: ( not y * x = z * x or y = z )
assume A5: y * x = z * x ; ::_thesis: y = z
thus y = y * (1. SF) by VECTSP_1:def_6
.= (z * x) * x1 by A4, A5, GROUP_1:def_3
.= z * (1. SF) by A4, GROUP_1:def_3
.= z by VECTSP_1:def_6 ; ::_thesis: verum
end;
hence  ( IT = x " iff IT * x = 1. SF ) by A2, ALGSTR_0:def_35; ::_thesis: verum
end;
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 & (x ") * x = 1. SF )
proof
let SF be Skew-Field; ::_thesis: for x being Scalar of SF st x <> 0. SF holds
( x * (x ") = 1. SF & (x ") * x = 1. SF )
let x be Scalar of SF; ::_thesis: ( x <> 0. SF implies ( x * (x ") = 1. SF & (x ") * x = 1. SF ) )
assume  x <> 0. SF ; ::_thesis: ( x * (x ") = 1. SF & (x ") * x = 1. SF )
then  (x ") * x = 1_ SF by Def2;
hence  ( x * (x ") = 1. SF & (x ") * x = 1. SF ) by Th7; ::_thesis: verum
end;

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 " & y = x " )
proof
let SF be Skew-Field; ::_thesis: for y, x being Scalar of SF st y * x = 1_ SF holds
( x = y " & y = x " )
let y, x be Scalar of SF; ::_thesis: ( y * x = 1_ SF implies ( x = y " & y = x " ) )
A1: ( y * x = 1_ SF implies y = x " )
proof
assume A2: y * x = 1_ SF ; ::_thesis: y = x "
then  x <> 0. SF by VECTSP_1:6;
hence  y = x " by A2, Def2; ::_thesis: verum
end;
 ( y * x = 1_ SF implies x = y " )
proof
assume  y * x = 1_ SF ; ::_thesis: x = y "
then  ( y <> 0. SF & x * y = 1_ SF ) by Th7, VECTSP_1:7;
hence  x = y " by Def2; ::_thesis: verum
end;
hence  ( y * x = 1_ SF implies ( x = y " & y = x " ) ) by A1; ::_thesis: verum
end;

theorem Th11: :: VECTSP_2:11
for SF being Skew-Field
for x, y being Scalar of SF st x <> 0. SF & y <> 0. SF holds
(x ") * (y ") = (y * x) "
proof
let SF be Skew-Field; ::_thesis: for x, y being Scalar of SF st x <> 0. SF & y <> 0. SF holds
(x ") * (y ") = (y * x) "
let x, y be Scalar of SF; ::_thesis: ( x <> 0. SF & y <> 0. SF implies (x ") * (y ") = (y * x) " )
assume A1: x <> 0. SF ; ::_thesis: ( not y <> 0. SF or (x ") * (y ") = (y * x) " )
assume A2: y <> 0. SF ; ::_thesis: (x ") * (y ") = (y * x) "
((x ") * (y ")) * (y * x) = (x ") * ((y ") * (y * x)) by GROUP_1:def_3
.= (x ") * (((y ") * y) * x) by GROUP_1:def_3
.= (x ") * ((1_ SF) * x) by A2, Th9
.= (x ") * x by VECTSP_1:def_8
.= 1_ SF by A1, Th9 ;
hence  (x ") * (y ") = (y * x) " by Th10; ::_thesis: verum
end;

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 )
proof
let SF be Skew-Field; ::_thesis: for x, y being Scalar of SF holds
( not x * y = 0. SF or x = 0. SF or y = 0. SF )
let x, y be Scalar of SF; ::_thesis: ( not x * y = 0. SF or x = 0. SF or y = 0. SF )
now__::_thesis:_(_x_*_y_=_0._SF_&_x_<>_0._SF_implies_y_=_0._SF_)
assume that
A1: x * y = 0. SF and
A2: x <> 0. SF ; ::_thesis: y = 0. SF
 x * y = x * (0. SF) by A1, VECTSP_1:6;
hence  y = 0. SF by A2, Th8; ::_thesis: verum
end;
hence  ( not x * y = 0. SF or x = 0. SF or y = 0. SF ) ; ::_thesis: verum
end;

theorem Th13: :: VECTSP_2:13
for SF being Skew-Field
for x being Scalar of SF st x <> 0. SF holds
x " <> 0. SF
proof
let SF be Skew-Field; ::_thesis: for x being Scalar of SF st x <> 0. SF holds
x " <> 0. SF
let x be Scalar of SF; ::_thesis: ( x <> 0. SF implies x " <> 0. SF )
assume A1: x <> 0. SF ; ::_thesis: x " <> 0. SF
assume  x " = 0. SF ; ::_thesis: contradiction
then  x * (x ") = 0. SF by VECTSP_1:6;
then  1. SF = 0. SF by A1, Th9;
hence  contradiction ; ::_thesis: verum
end;

theorem Th14: :: VECTSP_2:14
for SF being Skew-Field
for x being Scalar of SF st x <> 0. SF holds
(x ") " = x
proof
let SF be Skew-Field; ::_thesis: for x being Scalar of SF st x <> 0. SF holds
(x ") " = x
let x be Scalar of SF; ::_thesis: ( x <> 0. SF implies (x ") " = x )
assume A1: x <> 0. SF ; ::_thesis: (x ") " = x
then A2: x " <> 0. SF by Th13;
(x ") " = ((x ") ") * (1_ SF) by VECTSP_1:def_4
.= ((x ") ") * ((x ") * x) by A1, Th9
.= (((x ") ") * (x ")) * x by GROUP_1:def_3 ;
then  (x ") " = (1_ SF) * x by A2, Th9;
hence  (x ") " = x by VECTSP_1:def_8; ::_thesis: verum
end;

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 " & (1_ SF) / (x ") = x )
proof
let SF be Skew-Field; ::_thesis: for x being Scalar of SF st x <> 0. SF holds
( (1_ SF) / x = x " & (1_ SF) / (x ") = x )
let x be Scalar of SF; ::_thesis: ( x <> 0. SF implies ( (1_ SF) / x = x " & (1_ SF) / (x ") = x ) )
 ( x <> 0. SF implies (1_ SF) / (x ") = x )
proof
assume A1: x <> 0. SF ; ::_thesis: (1_ SF) / (x ") = x
(1_ SF) / (x ") = (x ") " by VECTSP_1:def_8
.= x by A1, Th14 ;
hence  (1_ SF) / (x ") = x ; ::_thesis: verum
end;
hence  ( x <> 0. SF implies ( (1_ SF) / x = x " & (1_ SF) / (x ") = x ) ) by VECTSP_1:def_8; ::_thesis: verum
end;

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 & ((1_ SF) / x) * x = 1_ SF )
proof
let SF be Skew-Field; ::_thesis: for x being Scalar of SF st x <> 0. SF holds
( x * ((1_ SF) / x) = 1_ SF & ((1_ SF) / x) * x = 1_ SF )
let x be Scalar of SF; ::_thesis: ( x <> 0. SF implies ( x * ((1_ SF) / x) = 1_ SF & ((1_ SF) / x) * x = 1_ SF ) )
assume A1: x <> 0. SF ; ::_thesis: ( x * ((1_ SF) / x) = 1_ SF & ((1_ SF) / x) * x = 1_ SF )
hence x * ((1_ SF) / x) = x * (x ") by Th15
.= 1_ SF by A1, Th9 ;
::_thesis: ((1_ SF) / x) * x = 1_ SF
thus ((1_ SF) / x) * x = (x ") * x by A1, Th15
.= 1_ SF by A1, Th9 ; ::_thesis: verum
end;

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 & z <> 0. SF holds
x / y = (x * z) / (y * z)
proof
let SF be Skew-Field; ::_thesis: for y, z, x being Scalar of SF st y <> 0. SF & z <> 0. SF holds
x / y = (x * z) / (y * z)
let y, z, x be Scalar of SF; ::_thesis: ( y <> 0. SF & z <> 0. SF implies x / y = (x * z) / (y * z) )
assume A1: y <> 0. SF ; ::_thesis: ( not z <> 0. SF or x / y = (x * z) / (y * z) )
assume A2: z <> 0. SF ; ::_thesis: x / y = (x * z) / (y * z)
thus x / y = (x * (1_ SF)) * (y ") by VECTSP_1:def_4
.= (x * (z * (z "))) * (y ") by A2, Th9
.= ((x * z) * (z ")) * (y ") by GROUP_1:def_3
.= (x * z) * ((z ") * (y ")) by GROUP_1:def_3
.= (x * z) / (y * z) by A1, A2, Th11 ; ::_thesis: verum
end;

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 & x / (- y) = - (x / y) )
proof
let SF be Skew-Field; ::_thesis: for y, x being Scalar of SF st y <> 0. SF holds
( - (x / y) = (- x) / y & x / (- y) = - (x / y) )
let y, x be Scalar of SF; ::_thesis: ( y <> 0. SF implies ( - (x / y) = (- x) / y & x / (- y) = - (x / y) ) )
assume  y <> 0. SF ; ::_thesis: ( - (x / y) = (- x) / y & x / (- y) = - (x / y) )
then A1: - y <> 0. SF by Th3;
thus A2: - (x / y) = (- x) / y by VECTSP_1:9; ::_thesis: x / (- y) = - (x / y)
 - (1. SF) <> 0. SF by Th3;
then  x / (- y) = (x * (- (1_ SF))) / ((- y) * (- (1_ SF))) by A1, Th18;
then x / (- y) = (- (x * (1_ SF))) / ((- y) * (- (1_ SF))) by VECTSP_1:8
.= (- x) / ((- y) * (- (1_ SF))) by VECTSP_1:def_4
.= (- x) / (- ((- y) * (1_ SF))) by VECTSP_1:8
.= (- x) / ((- (- y)) * (1_ SF)) by VECTSP_1:9
.= (- x) / (y * (1_ SF)) by RLVECT_1:17
.= - (x / y) by A2, VECTSP_1:def_4 ;
hence  x / (- y) = - (x / y) ; ::_thesis: verum
end;

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 & (x / z) - (y / z) = (x - y) / z )
proof
let SF be Skew-Field; ::_thesis: for z, x, y being Scalar of SF st z <> 0. SF holds
( (x / z) + (y / z) = (x + y) / z & (x / z) - (y / z) = (x - y) / z )
let z, x, y be Scalar of SF; ::_thesis: ( z <> 0. SF implies ( (x / z) + (y / z) = (x + y) / z & (x / z) - (y / z) = (x - y) / z ) )
 ( z <> 0. SF implies (x / z) - (y / z) = (x - y) / z )
proof
assume  z <> 0. SF ; ::_thesis: (x / z) - (y / z) = (x - y) / z
hence (x / z) - (y / z) = (x / z) + ((- y) / z) by Th19
.= (x - y) / z by VECTSP_1:def_7 ;
::_thesis: verum
end;
hence  ( z <> 0. SF implies ( (x / z) + (y / z) = (x + y) / z & (x / z) - (y / z) = (x - y) / z ) ) by VECTSP_1:def_7; ::_thesis: verum
end;

theorem :: VECTSP_2:21
for SF being Skew-Field
for y, z, x being Scalar of SF st y <> 0. SF & z <> 0. SF holds
x / (y / z) = (x * z) / y
proof
let SF be Skew-Field; ::_thesis: for y, z, x being Scalar of SF st y <> 0. SF & z <> 0. SF holds
x / (y / z) = (x * z) / y
let y, z, x be Scalar of SF; ::_thesis: ( y <> 0. SF & z <> 0. SF implies x / (y / z) = (x * z) / y )
assume A1: y <> 0. SF ; ::_thesis: ( not z <> 0. SF or x / (y / z) = (x * z) / y )
assume A2: z <> 0. SF ; ::_thesis: x / (y / z) = (x * z) / y
then  z " <> 0. SF by Th13;
hence x / (y / z) = x * (((z ") ") * (y ")) by A1, Th11
.= x * (z * (y ")) by A2, Th14
.= (x * z) / y by GROUP_1:def_3 ;
::_thesis: verum
end;

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
proof
let SF be Skew-Field; ::_thesis: for y, x being Scalar of SF st y <> 0. SF holds
(x / y) * y = x
let y, x be Scalar of SF; ::_thesis: ( y <> 0. SF implies (x / y) * y = x )
assume A1: y <> 0. SF ; ::_thesis: (x / y) * y = x
thus (x / y) * y = x * ((y ") * y) by GROUP_1:def_3
.= x * (1_ SF) by A1, Th9
.= x by VECTSP_1:def_4 ; ::_thesis: verum
end;

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
proof
set A = the non empty set ;
set a = the BinOp of the non empty set ;
set Z = the Element of the non empty set ;
set r = the Function of [: the non empty set , the carrier of FS:], the non empty set ;
take  RightModStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the non empty set , the carrier of FS:], the non empty set #) ; ::_thesis: not RightModStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the non empty set , the carrier of FS:], the non empty set #) is empty
thus  not the carrier of RightModStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the non empty set , the carrier of FS:], the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
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
proof
set A = the non empty set ;
set a = the BinOp of the non empty set ;
set Z = the Element of the non empty set ;
set l = the Function of [: the carrier of FS1, the non empty set :], the non empty set ;
set r = the Function of [: the non empty set , the carrier of FS2:], the non empty set ;
take  BiModStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of FS1, the non empty set :], the non empty set , the Function of [: the non empty set , the carrier of FS2:], the non empty set #) ; ::_thesis: not BiModStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of FS1, the non empty set :], the non empty set , the Function of [: the non empty set , the carrier of FS2:], the non empty set #) is empty
thus  not the carrier of BiModStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of FS1, the non empty set :], the non empty set , the Function of [: the non empty set , the carrier of FS2:], the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
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
proof
reconsider IT = addLoopStr(# the carrier of R, the addF of R,(0. R) #) as non empty addLoopStr ;
A1: for x, y, z being Element of IT holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. IT) = x & ex v being Element of IT st x + v = 0. IT )
proof
let x, y, z be Element of IT; ::_thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. IT) = x & ex v being Element of IT st x + v = 0. IT )
reconsider x9 = x, y9 = y, z9 = z as Scalar of R ;
thus x + y = y9 + x9 by RLVECT_1:2
.= y + x ; ::_thesis: ( (x + y) + z = x + (y + z) & x + (0. IT) = x & ex v being Element of IT st x + v = 0. IT )
thus (x + y) + z = (x9 + y9) + z9
.= x9 + (y9 + z9) by RLVECT_1:def_3
.= x + (y + z) ; ::_thesis: ( x + (0. IT) = x & ex v being Element of IT st x + v = 0. IT )
thus x + (0. IT) = x9 + (0. R)
.= x by RLVECT_1:4 ; ::_thesis: ex v being Element of IT st x + v = 0. IT
consider b being Scalar of R such that
A2: x9 + b = 0. R by ALGSTR_0:def_11;
reconsider b9 = b as Element of IT ;
take  b9 ; ::_thesis: x + b9 = 0. IT
thus  x + b9 = 0. IT by A2; ::_thesis: verum
end;
 IT is right_complementable
proof
let x be Element of IT; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x9 = x as Scalar of R ;
consider b being Scalar of R such that
A3: x9 + b = 0. R by ALGSTR_0:def_11;
reconsider b9 = b as Element of IT ;
take  b9 ; :: according to ALGSTR_0:def_11 ::_thesis: x + b9 = 0. IT
thus  x + b9 = 0. IT by A3; ::_thesis: verum
end;
hence  addLoopStr(# the carrier of R, the addF of R,(0. R) #) is strict AbGroup by A1, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4; ::_thesis: verum
end;
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 & H1(R) is add-associative & H1(R) is right_zeroed & H1(R) is right_complementable )
proof
let R be Ring; ::_thesis: ( H1(R) is Abelian & H1(R) is add-associative & H1(R) is right_zeroed & H1(R) is right_complementable )
A1: for x, y, z being Scalar of R
for x9, y9, z9 being Element of H1(R) st x = x9 & y = y9 & z = z9 holds
x + y = x9 + y9 ;
thus  H1(R) is Abelian ::_thesis: ( H1(R) is add-associative & H1(R) is right_zeroed & H1(R) is right_complementable )
proof
let x, y be Element of H1(R); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
reconsider x9 = x, y9 = y as Scalar of R ;
thus x + y = y9 + x9 by A1
.= y + x ; ::_thesis: verum
end;
thus  H1(R) is add-associative ::_thesis: ( H1(R) is right_zeroed & H1(R) is right_complementable )
proof
let x, y, z be Element of H1(R); :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
reconsider x9 = x, y9 = y, z9 = z as Scalar of R ;
thus (x + y) + z = (x9 + y9) + z9
.= x9 + (y9 + z9) by RLVECT_1:def_3
.= x + (y + z) ; ::_thesis: verum
end;
thus  H1(R) is right_zeroed ::_thesis: H1(R) is right_complementable
proof
let x be Element of H1(R); :: according to RLVECT_1:def_4 ::_thesis: x + (0. H1(R)) = x
reconsider x9 = x as Scalar of R ;
thus x + (0. H1(R)) = x9 + (0. R)
.= x by RLVECT_1:4 ; ::_thesis: verum
end;
let x be Element of H1(R); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x9 = x as Scalar of R ;
consider b9 being Scalar of R such that
A2: x9 + b9 = 0. R by ALGSTR_0:def_11;
reconsider b = b9 as Element of H1(R) ;
take  b ; :: according to ALGSTR_0:def_11 ::_thesis: x + b = 0. H1(R)
thus  x + b = 0. H1(R) by A2; ::_thesis: verum
end;

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 & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict )
proof
 ( H1(R) is Abelian & H1(R) is add-associative & H1(R) is right_zeroed & H1(R) is right_complementable ) by Lm4;
hence  ex b1 being non empty VectSpStr over R st
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict ) ; ::_thesis: verum
end;
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 & H2(R) is add-associative & H2(R) is right_zeroed & H2(R) is right_complementable )
proof
let R be Ring; ::_thesis: ( H2(R) is Abelian & H2(R) is add-associative & H2(R) is right_zeroed & H2(R) is right_complementable )
A1: for x, y, z being Scalar of R
for x9, y9, z9 being Element of H2(R) st x = x9 & y = y9 & z = z9 holds
x + y = x9 + y9 ;
thus  H2(R) is Abelian ::_thesis: ( H2(R) is add-associative & H2(R) is right_zeroed & H2(R) is right_complementable )
proof
let x, y be Element of H2(R); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
reconsider x9 = x, y9 = y as Scalar of R ;
thus x + y = y9 + x9 by A1
.= y + x ; ::_thesis: verum
end;
thus  H2(R) is add-associative ::_thesis: ( H2(R) is right_zeroed & H2(R) is right_complementable )
proof
let x, y, z be Element of H2(R); :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
reconsider x9 = x, y9 = y, z9 = z as Scalar of R ;
thus (x + y) + z = (x9 + y9) + z9
.= x9 + (y9 + z9) by RLVECT_1:def_3
.= x + (y + z) ; ::_thesis: verum
end;
thus  H2(R) is right_zeroed ::_thesis: H2(R) is right_complementable
proof
let x be Element of H2(R); :: according to RLVECT_1:def_4 ::_thesis: x + (0. H2(R)) = x
reconsider x9 = x as Scalar of R ;
thus x + (0. H2(R)) = x9 + (0. R)
.= x by RLVECT_1:4 ; ::_thesis: verum
end;
let x be Element of H2(R); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x9 = x as Scalar of R ;
consider b9 being Scalar of R such that
A2: x9 + b9 = 0. R by ALGSTR_0:def_11;
reconsider b = b9 as Element of H2(R) ;
take  b ; :: according to ALGSTR_0:def_11 ::_thesis: x + b = 0. H2(R)
thus  x + b = 0. H2(R) by A2; ::_thesis: verum
end;

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 & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict )
proof
 ( H2(R) is Abelian & H2(R) is add-associative & H2(R) is right_zeroed & H2(R) is right_complementable ) by Lm5;
hence  ex b1 being non empty RightModStr over R st
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict ) ; ::_thesis: verum
end;
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 & H3(R1,R2) is add-associative & H3(R1,R2) is right_zeroed & H3(R1,R2) is right_complementable )
proof
let R1, R2 be Ring; ::_thesis: ( H3(R1,R2) is Abelian & H3(R1,R2) is add-associative & H3(R1,R2) is right_zeroed & H3(R1,R2) is right_complementable )
set G = BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #);
A1: now__::_thesis:_for_x,_y,_z_being_Element_of_BiModStr(#_1,op2,op0,(pr2_(_the_carrier_of_R1,1)),(pr1_(1,_the_carrier_of_R2))_#)_holds_
(_x_+_y_=_y_+_x_&_(x_+_y)_+_z_=_x_+_(y_+_z)_&_x_+_(0._BiModStr(#_1,op2,op0,(pr2_(_the_carrier_of_R1,1)),(pr1_(1,_the_carrier_of_R2))_#))_=_x_&_ex_x9_being_Element_of_BiModStr(#_1,op2,op0,(pr2_(_the_carrier_of_R1,1)),(pr1_(1,_the_carrier_of_R2))_#)_st_x_+_x9_=_0._BiModStr(#_1,op2,op0,(pr2_(_the_carrier_of_R1,1)),(pr1_(1,_the_carrier_of_R2))_#)_)
let x, y, z be Element of BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #); ::_thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #)) = x & ex x9 being Element of BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #) st x + x9 = 0. BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #) )
A2: x + (0. BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #)) = {} by CARD_1:49, TARSKI:def_1;
 ( x + y = {} & (x + y) + z = {} ) by CARD_1:49, TARSKI:def_1;
hence  ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #)) = x & ex x9 being Element of BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #) st x + x9 = 0. BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #) ) by A2, CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;
 BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #) is right_complementable
proof
let x be Element of BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
take  x ; :: according to ALGSTR_0:def_11 ::_thesis: x + x = 0. BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #)
thus  x + x = 0. BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #) by CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;
hence  ( H3(R1,R2) is Abelian & H3(R1,R2) is add-associative & H3(R1,R2) is right_zeroed & H3(R1,R2) is right_complementable ) by A1, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4; ::_thesis: verum
end;

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 & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict )
proof
 ( H3(R1,R2) is Abelian & H3(R1,R2) is add-associative & H3(R1,R2) is right_zeroed & H3(R1,R2) is right_complementable ) by Lm6;
hence  ex b1 being non empty BiModStr over R1,R2 st
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict ) ; ::_thesis: verum
end;
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) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v )
proof
let R be Ring; ::_thesis: for x, y being Scalar of R
for v, w being Vector of (LeftModule R) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v )
set MLT = the multF of R;
set LS = VectSpStr(# the carrier of R, the addF of R,(0. R), the multF of R #);
 for x, y being Scalar of R
for v, w being Vector of VectSpStr(# the carrier of R, the addF of R,(0. R), the multF of R #) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ R) * v = v )
proof
let x, y be Scalar of R; ::_thesis: for v, w being Vector of VectSpStr(# the carrier of R, the addF of R,(0. R), the multF of R #) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ R) * v = v )
let v, w be Vector of VectSpStr(# the carrier of R, the addF of R,(0. R), the multF of R #); ::_thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ R) * v = v )
reconsider v9 = v, w9 = w as Scalar of R ;
thus x * (v + w) = x * (v9 + w9)
.= (x * v9) + (x * w9) by VECTSP_1:def_7
.= (x * v) + (x * w) ; ::_thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ R) * v = v )
thus (x + y) * v = (x + y) * v9
.= (x * v9) + (y * v9) by VECTSP_1:def_7
.= (x * v) + (y * v) ; ::_thesis: ( (x * y) * v = x * (y * v) & (1_ R) * v = v )
thus (x * y) * v = (x * y) * v9
.= x * (y * v9) by GROUP_1:def_3
.= x * (y * v) ; ::_thesis: (1_ R) * v = v
thus (1_ R) * v = (1_ R) * v9
.= v by VECTSP_1:def_8 ; ::_thesis: verum
end;
hence  for x, y being Scalar of R
for v, w being Vector of (LeftModule R) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v ) ; ::_thesis: verum
end;

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 & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict )
proof
take  LeftModule R ; ::_thesis: ( LeftModule R is vector-distributive & LeftModule R is scalar-distributive & LeftModule R is scalar-associative & LeftModule R is scalar-unital & LeftModule R is Abelian & LeftModule R is add-associative & LeftModule R is right_zeroed & LeftModule R is right_complementable & LeftModule R is strict )
thus  for x being Scalar of R
for v, w being Vector of (LeftModule R) holds x * (v + w) = (x * v) + (x * w) by Th23; :: according to VECTSP_1:def_14 ::_thesis: ( LeftModule R is scalar-distributive & LeftModule R is scalar-associative & LeftModule R is scalar-unital & LeftModule R is Abelian & LeftModule R is add-associative & LeftModule R is right_zeroed & LeftModule R is right_complementable & LeftModule R is strict )
thus  for x, y being Scalar of R
for v being Vector of (LeftModule R) holds (x + y) * v = (x * v) + (y * v) by Th23; :: according to VECTSP_1:def_15 ::_thesis: ( LeftModule R is scalar-associative & LeftModule R is scalar-unital & LeftModule R is Abelian & LeftModule R is add-associative & LeftModule R is right_zeroed & LeftModule R is right_complementable & LeftModule R is strict )
thus  for x, y being Scalar of R
for v being Vector of (LeftModule R) holds (x * y) * v = x * (y * v) by Th23; :: according to VECTSP_1:def_16 ::_thesis: ( LeftModule R is scalar-unital & LeftModule R is Abelian & LeftModule R is add-associative & LeftModule R is right_zeroed & LeftModule R is right_complementable & LeftModule R is strict )
thus  for v being Vector of (LeftModule R) holds (1. R) * v = v by Th23; :: according to VECTSP_1:def_17 ::_thesis: ( LeftModule R is Abelian & LeftModule R is add-associative & LeftModule R is right_zeroed & LeftModule R is right_complementable & LeftModule R is strict )
thus  ( LeftModule R is Abelian & LeftModule R is add-associative & LeftModule R is right_zeroed & LeftModule R is right_complementable & LeftModule R is strict ) ; ::_thesis: verum
end;
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 & LeftModule R is scalar-distributive & LeftModule R is scalar-associative & LeftModule R is scalar-unital )
proof
let R be Ring; ::_thesis: ( LeftModule R is vector-distributive & LeftModule R is scalar-distributive & LeftModule R is scalar-associative & LeftModule R is scalar-unital )
thus  for x being Scalar of R
for v, w being Vector of (LeftModule R) holds x * (v + w) = (x * v) + (x * w) by Th23; :: according to VECTSP_1:def_14 ::_thesis: ( LeftModule R is scalar-distributive & LeftModule R is scalar-associative & LeftModule R is scalar-unital )
thus  for x, y being Scalar of R
for v being Vector of (LeftModule R) holds (x + y) * v = (x * v) + (y * v) by Th23; :: according to VECTSP_1:def_15 ::_thesis: ( LeftModule R is scalar-associative & LeftModule R is scalar-unital )
thus  for x, y being Scalar of R
for v being Vector of (LeftModule R) holds (x * y) * v = x * (y * v) by Th23; :: according to VECTSP_1:def_16 ::_thesis: LeftModule R is scalar-unital
thus  for v being Vector of (LeftModule R) holds (1. R) * v = v by Th23; :: according to VECTSP_1:def_17 ::_thesis: verum
end;

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 & LeftModule R is add-associative & LeftModule R is right_zeroed & LeftModule R is right_complementable & LeftModule R is strict & LeftModule R is vector-distributive & LeftModule R is scalar-distributive & LeftModule R is scalar-associative & LeftModule R is scalar-unital ) by Lm7;
end;

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) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
proof
let R be Ring; ::_thesis: for x, y being Scalar of R
for v, w being Vector of (RightModule R) holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
set MLT = the multF of R;
set LS = RightModStr(# the carrier of R, the addF of R,(0. R), the multF of R #);
 for x, y being Scalar of R
for v, w being Vector of RightModStr(# the carrier of R, the addF of R,(0. R), the multF of R #) holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
proof
let x, y be Scalar of R; ::_thesis: for v, w being Vector of RightModStr(# the carrier of R, the addF of R,(0. R), the multF of R #) holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
let v, w be Vector of RightModStr(# the carrier of R, the addF of R,(0. R), the multF of R #); ::_thesis: ( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
reconsider v9 = v, w9 = w as Scalar of R ;
thus (v + w) * x = (v9 + w9) * x
.= (v9 * x) + (w9 * x) by VECTSP_1:def_7
.= (v * x) + (w * x) ; ::_thesis: ( v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
thus v * (x + y) = v9 * (x + y)
.= (v9 * x) + (v9 * y) by VECTSP_1:def_7
.= (v * x) + (v * y) ; ::_thesis: ( v * (y * x) = (v * y) * x & v * (1_ R) = v )
thus v * (y * x) = v9 * (y * x)
.= (v9 * y) * x by GROUP_1:def_3
.= (v * y) * x ; ::_thesis: v * (1_ R) = v
thus v * (1_ R) = v9 * (1_ R)
.= v by VECTSP_1:def_4 ; ::_thesis: verum
end;
hence  for x, y being Scalar of R
for v, w being Vector of (RightModule R) holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v ) ; ::_thesis: verum
end;

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) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & 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) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & 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 & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is RightMod-like & b1 is strict )
proof
take  RightModule R ; ::_thesis: ( RightModule R is Abelian & RightModule R is add-associative & RightModule R is right_zeroed & RightModule R is right_complementable & RightModule R is RightMod-like & RightModule R is strict )
thus  ( RightModule R is Abelian & RightModule R is add-associative & RightModule R is right_zeroed & RightModule R is right_complementable ) ; ::_thesis: ( RightModule R is RightMod-like & RightModule R is strict )
thus  for x, y being Scalar of R
for v, w being Vector of (RightModule R) holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v ) by Th24; :: according to VECTSP_2:def_9 ::_thesis: RightModule R is strict
thus  RightModule R is strict ; ::_thesis: verum
end;
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
proof
let R be Ring; ::_thesis: RightModule R is RightMod-like
let x, y be Scalar of R; :: according to VECTSP_2:def_9 ::_thesis: for v, w being Vector of (RightModule R) holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
let v, w be Vector of (RightModule R); ::_thesis: ( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
thus  ( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v ) by Th24; ::_thesis: verum
end;

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 & RightModule R is add-associative & RightModule R is right_zeroed & RightModule R is right_complementable & 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) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ R1) * v = v & (v + w) * p = (v * p) + (w * p) & v * (p + q) = (v * p) + (v * q) & v * (q * p) = (v * q) * p & v * (1_ R2) = v & x * (v * p) = (x * v) * p )
proof
let R1, R2 be Ring; ::_thesis: 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) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ R1) * v = v & (v + w) * p = (v * p) + (w * p) & v * (p + q) = (v * p) + (v * q) & v * (q * p) = (v * q) * p & v * (1_ R2) = v & x * (v * p) = (x * v) * p )
set a = {} ;
set G = BiModule (R1,R2);
let x, y be Scalar of R1; ::_thesis: for p, q being Scalar of R2
for v, w being Vector of (BiModule (R1,R2)) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ R1) * v = v & (v + w) * p = (v * p) + (w * p) & v * (p + q) = (v * p) + (v * q) & v * (q * p) = (v * q) * p & v * (1_ R2) = v & x * (v * p) = (x * v) * p )
let p, q be Scalar of R2; ::_thesis: for v, w being Vector of (BiModule (R1,R2)) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ R1) * v = v & (v + w) * p = (v * p) + (w * p) & v * (p + q) = (v * p) + (v * q) & v * (q * p) = (v * q) * p & v * (1_ R2) = v & x * (v * p) = (x * v) * p )
let v, w be Vector of (BiModule (R1,R2)); ::_thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ R1) * v = v & (v + w) * p = (v * p) + (w * p) & v * (p + q) = (v * p) + (v * q) & v * (q * p) = (v * q) * p & v * (1_ R2) = v & x * (v * p) = (x * v) * p )
A1: ( (x * y) * v = {} & (1_ R1) * v = {} ) by CARD_1:49, TARSKI:def_1;
 ( x * (v + w) = {} & (x + y) * v = {} ) by CARD_1:49, TARSKI:def_1;
hence  ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ R1) * v = v ) by A1, CARD_1:49, TARSKI:def_1; ::_thesis: ( (v + w) * p = (v * p) + (w * p) & v * (p + q) = (v * p) + (v * q) & v * (q * p) = (v * q) * p & v * (1_ R2) = v & x * (v * p) = (x * v) * p )
A2: ( v * (q * p) = {} & v * (1_ R2) = {} ) by CARD_1:49, TARSKI:def_1;
A3: x * (v * p) = {} by CARD_1:49, TARSKI:def_1;
 ( (v + w) * p = {} & v * (p + q) = {} ) by CARD_1:49, TARSKI:def_1;
hence  ( (v + w) * p = (v * p) + (w * p) & v * (p + q) = (v * p) + (v * q) & v * (q * p) = (v * q) * p & v * (1_ R2) = v & x * (v * p) = (x * v) * p ) by A2, A3, CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;

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 & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is RightMod-like & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is BiMod-like & b1 is strict )
proof
take  BiModule (R1,R2) ; ::_thesis: ( BiModule (R1,R2) is Abelian & BiModule (R1,R2) is add-associative & BiModule (R1,R2) is right_zeroed & BiModule (R1,R2) is right_complementable & BiModule (R1,R2) is RightMod-like & BiModule (R1,R2) is vector-distributive & BiModule (R1,R2) is scalar-distributive & BiModule (R1,R2) is scalar-associative & BiModule (R1,R2) is scalar-unital & BiModule (R1,R2) is BiMod-like & BiModule (R1,R2) is strict )
thus  ( BiModule (R1,R2) is Abelian & BiModule (R1,R2) is add-associative & BiModule (R1,R2) is right_zeroed & BiModule (R1,R2) is right_complementable ) ; ::_thesis: ( BiModule (R1,R2) is RightMod-like & BiModule (R1,R2) is vector-distributive & BiModule (R1,R2) is scalar-distributive & BiModule (R1,R2) is scalar-associative & BiModule (R1,R2) is scalar-unital & BiModule (R1,R2) is BiMod-like & BiModule (R1,R2) is strict )
 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) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ R1) * v = v & (v + w) * p = (v * p) + (w * p) & v * (p + q) = (v * p) + (v * q) & v * (q * p) = (v * q) * p & v * (1_ R2) = v & x * (v * p) = (x * v) * p ) by Lm9;
hence  ( BiModule (R1,R2) is RightMod-like & BiModule (R1,R2) is vector-distributive & BiModule (R1,R2) is scalar-distributive & BiModule (R1,R2) is scalar-associative & BiModule (R1,R2) is scalar-unital & BiModule (R1,R2) is BiMod-like & BiModule (R1,R2) is strict ) by Def9, Def10, VECTSP_1:def_14, VECTSP_1:def_15, VECTSP_1:def_16, VECTSP_1:def_17; ::_thesis: verum
end;
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) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ R1) * v = v & (v + w) * p = (v * p) + (w * p) & v * (p + q) = (v * p) + (v * q) & v * (q * p) = (v * q) * p & v * (1_ R2) = v & x * (v * p) = (x * v) * p ) ) iff ( V is RightMod-like & V is vector-distributive & V is scalar-distributive & V is scalar-associative & V is scalar-unital & 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
proof
let R1, R2 be Ring; ::_thesis: BiModule (R1,R2) is BiMod of R1,R2
 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) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ R1) * v = v & (v + w) * p = (v * p) + (w * p) & v * (p + q) = (v * p) + (v * q) & v * (q * p) = (v * q) * p & v * (1_ R2) = v & x * (v * p) = (x * v) * p ) by Lm9;
hence  BiModule (R1,R2) is BiMod of R1,R2 by Def9, Def10, VECTSP_1:def_14, VECTSP_1:def_15, VECTSP_1:def_16, VECTSP_1:def_17; ::_thesis: verum
end;

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 & BiModule (R1,R2) is add-associative & BiModule (R1,R2) is right_zeroed & BiModule (R1,R2) is right_complementable & BiModule (R1,R2) is RightMod-like & BiModule (R1,R2) is vector-distributive & BiModule (R1,R2) is scalar-distributive & BiModule (R1,R2) is scalar-associative & BiModule (R1,R2) is scalar-unital & 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
proof
let K be non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for a being Element of K holds a * (- (1. K)) = - a
let x be Element of K; ::_thesis: x * (- (1. K)) = - x
thus x * (- (1. K)) = x * ((0. K) - (1. K)) by RLVECT_1:14
.= (x * (0. K)) - (x * (1. K)) by VECTSP_1:11
.= (0. K) - (x * (1. K)) by VECTSP_1:6
.= - (x * (1. K)) by RLVECT_1:14
.= - x by VECTSP_1:def_4 ; ::_thesis: verum
end;

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
proof
let K be non empty right_complementable left-distributive left_unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for a being Element of K holds (- (1. K)) * a = - a
let x be Element of K; ::_thesis: (- (1. K)) * x = - x
thus (- (1. K)) * x = ((0. K) - (1. K)) * x by RLVECT_1:14
.= ((0. K) * x) - ((1. K) * x) by VECTSP_1:13
.= (0. K) - ((1. K) * x) by VECTSP_1:7
.= - ((1. K) * x) by RLVECT_1:14
.= - x by VECTSP_1:def_8 ; ::_thesis: verum
end;


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 ) )
proof
let F be non degenerated almost_left_invertible Ring; ::_thesis: 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 ) )
let x be Scalar of F; ::_thesis: 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 ) )
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed VectSpStr over F; ::_thesis: for v being Vector of V holds
( x * v = 0. V iff ( x = 0. F or v = 0. V ) )
let v be Vector of V; ::_thesis: ( x * v = 0. V iff ( x = 0. F or v = 0. V ) )
 ( not x * v = 0. V or x = 0. F or v = 0. V )
proof
assume  x * v = 0. V ; ::_thesis: ( x = 0. F or v = 0. V )
then A1: ((x ") * x) * v = (x ") * (0. V) by VECTSP_1:def_16
.= 0. V by VECTSP_1:14 ;
assume  x <> 0. F ; ::_thesis: v = 0. V
then  0. V = (1_ F) * v by A1, Th9;
hence  v = 0. V by VECTSP_1:def_17; ::_thesis: verum
end;
hence  ( x * v = 0. V iff ( x = 0. F or v = 0. V ) ) by VECTSP_1:14; ::_thesis: verum
end;

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
proof
let F be non degenerated almost_left_invertible Ring; ::_thesis: 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
let x be Scalar of F; ::_thesis: 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
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed VectSpStr over F; ::_thesis: for v being Vector of V st x <> 0. F holds
(x ") * (x * v) = v
let v be Vector of V; ::_thesis: ( x <> 0. F implies (x ") * (x * v) = v )
assume A1: x <> 0. F ; ::_thesis: (x ") * (x * v) = v
(x ") * (x * v) = ((x ") * x) * v by VECTSP_1:def_16
.= (1_ F) * v by A1, Th9
.= v by VECTSP_1:def_17 ;
hence  (x ") * (x * v) = v ; ::_thesis: verum
end;


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 & v * (- (1_ R)) = - v & (0. V) * x = 0. V )
proof
let R be non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & v * (- (1_ R)) = - v & (0. V) * x = 0. V )
let V be non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over R; ::_thesis: for x being Scalar of R
for v being Vector of V holds
( v * (0. R) = 0. V & v * (- (1_ R)) = - v & (0. V) * x = 0. V )
let x be Scalar of R; ::_thesis: for v being Vector of V holds
( v * (0. R) = 0. V & v * (- (1_ R)) = - v & (0. V) * x = 0. V )
let v be Vector of V; ::_thesis: ( v * (0. R) = 0. V & v * (- (1_ R)) = - v & (0. V) * x = 0. V )
v + (v * (0. R)) = (v * (1_ R)) + (v * (0. R)) by Def9
.= v * ((1_ R) + (0. R)) by Def9
.= v * (1_ R) by RLVECT_1:4
.= v by Def9
.= v + (0. V) by RLVECT_1:4 ;
hence A1: v * (0. R) = 0. V by RLVECT_1:8; ::_thesis: ( v * (- (1_ R)) = - v & (0. V) * x = 0. V )
(v * (- (1_ R))) + v = (v * (- (1_ R))) + (v * (1_ R)) by Def9
.= v * ((- (1_ R)) + (1_ R)) by Def9
.= 0. V by A1, RLVECT_1:5 ;
then  (v * (- (1_ R))) + (v + (- v)) = (0. V) + (- v) by RLVECT_1:def_3;
then (0. V) + (- v) = (v * (- (1_ R))) + (0. V) by RLVECT_1:5
.= v * (- (1_ R)) by RLVECT_1:4 ;
hence  v * (- (1_ R)) = - v by RLVECT_1:4; ::_thesis: (0. V) * x = 0. V
(0. V) * x = v * ((0. R) * x) by A1, Def9
.= 0. V by A1, VECTSP_1:7 ;
hence  (0. V) * x = 0. V ; ::_thesis: verum
end;

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) & w - (v * x) = w + (v * (- x)) )
proof
let R be non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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) & w - (v * x) = w + (v * (- x)) )
let V be non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over R; ::_thesis: for x being Scalar of R
for v, w being Vector of V holds
( - (v * x) = v * (- x) & w - (v * x) = w + (v * (- x)) )
let x be Scalar of R; ::_thesis: for v, w being Vector of V holds
( - (v * x) = v * (- x) & w - (v * x) = w + (v * (- x)) )
let v, w be Vector of V; ::_thesis: ( - (v * x) = v * (- x) & w - (v * x) = w + (v * (- x)) )
A1: - (v * x) = (v * x) * (- (1_ R)) by Th32
.= v * (x * (- (1_ R))) by Def9
.= v * (- (x * (1_ R))) by VECTSP_1:8 ;
hence  - (v * x) = v * (- x) by VECTSP_1:def_4; ::_thesis: w - (v * x) = w + (v * (- x))
thus  w - (v * x) = w + (v * (- x)) by A1, VECTSP_1:def_4; ::_thesis: verum
end;

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)
proof
let R be non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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)
let V be non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over R; ::_thesis: for x being Scalar of R
for v being Vector of V holds (- v) * x = - (v * x)
let x be Scalar of R; ::_thesis: for v being Vector of V holds (- v) * x = - (v * x)
let v be Vector of V; ::_thesis: (- v) * x = - (v * x)
(- v) * x = (v * (- (1_ R))) * x by Th32
.= v * ((- (1_ R)) * x) by Def9
.= v * (- ((1_ R) * x)) by VECTSP_1:9
.= v * (- x) by VECTSP_1:def_8 ;
hence  (- v) * x = - (v * x) by Th33; ::_thesis: verum
end;

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)
proof
let R be non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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)
let V be non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over R; ::_thesis: for x being Scalar of R
for v, w being Vector of V holds (v - w) * x = (v * x) - (w * x)
let x be Scalar of R; ::_thesis: for v, w being Vector of V holds (v - w) * x = (v * x) - (w * x)
let v, w be Vector of V; ::_thesis: (v - w) * x = (v * x) - (w * x)
(v - w) * x = (v + (- w)) * x
.= (v * x) + ((- w) * x) by Def9
.= (v * x) + (- (w * x)) by Th34 ;
hence  (v - w) * x = (v * x) - (w * x) ; ::_thesis: verum
end;


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 ) )
proof
let F be non degenerated almost_left_invertible Ring; ::_thesis: 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 ) )
let x be Scalar of F; ::_thesis: 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 ) )
let V be non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over F; ::_thesis: for v being Vector of V holds
( v * x = 0. V iff ( x = 0. F or v = 0. V ) )
let v be Vector of V; ::_thesis: ( v * x = 0. V iff ( x = 0. F or v = 0. V ) )
 ( not v * x = 0. V or x = 0. F or v = 0. V )
proof
assume  v * x = 0. V ; ::_thesis: ( x = 0. F or v = 0. V )
then A1: v * (x * (x ")) = (0. V) * (x ") by Def9
.= 0. V by Th32 ;
assume  x <> 0. F ; ::_thesis: v = 0. V
then  0. V = v * (1_ F) by A1, Th9;
hence  v = 0. V by Def9; ::_thesis: verum
end;
hence  ( v * x = 0. V iff ( x = 0. F or v = 0. V ) ) by Th32; ::_thesis: verum
end;

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
proof
let F be non degenerated almost_left_invertible Ring; ::_thesis: 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
let x be Scalar of F; ::_thesis: 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
let V be non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over F; ::_thesis: for v being Vector of V st x <> 0. F holds
(v * x) * (x ") = v
let v be Vector of V; ::_thesis: ( x <> 0. F implies (v * x) * (x ") = v )
assume A1: x <> 0. F ; ::_thesis: (v * x) * (x ") = v
(v * x) * (x ") = v * (x * (x ")) by Def9
.= v * (1_ F) by A1, Th9
.= v by Def9 ;
hence  (v * x) * (x ") = v ; ::_thesis: verum
end;