:: 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

proof end;

registration

ex b_{1} being non empty doubleLoopStr st

( b_{1} is strict & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is unital & b_{1} is distributive )
end;

cluster non empty right_complementable strict unital distributive Abelian add-associative right_zeroed for doubleLoopStr ;

existence ex b

( b

proof 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 ) );

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

ex b_{1} being Ring st

( b_{1} is strict & not b_{1} is degenerated & b_{1} is commutative & b_{1} is almost_left_invertible & b_{1} is domRing-like )
end;

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 b

( b

proof end;

:: 10. AXIOMS OF SKEW-FIELD

registration

coherence

for b_{1} being non empty multLoopStr st b_{1} is commutative & b_{1} is left_unital holds

b_{1} is well-unital

for b_{1} being non empty multLoopStr st b_{1} is commutative & b_{1} is right_unital holds

b_{1} is well-unital

end;
for b

b

proof end;

coherence for b

b

proof 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 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 end;

theorem :: VECTSP_2:2

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 )

for x being Element of R holds

( x = 0. R iff - x = 0. R )

proof 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 )

for x, y being Element of R ex z being Element of R st

( x = y + z & x = z + y )

proof 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;

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

for x being Element of SF st x <> 0. SF holds

ex y being Element of SF st x * y = 1. SF

proof 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

for x, y being Element of SF st y * x = 1. SF holds

x * y = 1. SF

proof 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

for x, y, z being Element of SF st x * y = x * z & x <> 0. SF holds

y = z

proof 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 ;

compatibility

for b_{1} being Element of the carrier of SF holds

( b_{1} = x " iff b_{1} * x = 1. SF )

end;
let x be Element of SF;

assume A1: x <> 0. SF ;

compatibility

for b

( b

proof 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 b_{3} being Element of the carrier of SF holds

( b_{3} = x " iff b_{3} * x = 1. SF );

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 b

( b

definition
end;

:: deftheorem defines / VECTSP_2:def 3 :

for SF being Skew-Field

for x, y being Scalar of SF holds x / y = x * (y ");

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 )

for x being Scalar of SF st x <> 0. SF holds

( x * (x ") = 1. SF & (x ") * x = 1. SF )

proof 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) "

for x, y being Scalar of SF st x <> 0. SF & y <> 0. SF holds

(x ") * (y ") = (y * x) "

proof 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 )

for x, y being Scalar of SF holds

( not x * y = 0. SF or x = 0. SF or y = 0. SF )

proof 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 )

for x being Scalar of SF st x <> 0. SF holds

( (1_ SF) / x = x " & (1_ SF) / (x ") = x )

proof 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 )

for x being Scalar of SF st x <> 0. SF holds

( x * ((1_ SF) / x) = 1_ SF & ((1_ SF) / x) * x = 1_ SF )

proof end;

theorem :: VECTSP_2:17

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)

for y, z, x being Scalar of SF st y <> 0. SF & z <> 0. SF holds

x / y = (x * z) / (y * z)

proof 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) )

for y, x being Scalar of SF st y <> 0. SF holds

( - (x / y) = (- x) / y & x / (- y) = - (x / y) )

proof 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 )

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 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

for y, z, x being Scalar of SF st y <> 0. SF & z <> 0. SF holds

x / (y / z) = (x * z) / y

proof end;

:: 13. LEFT-, RIGHT-, AND BI-MODULE STRUCTURE

definition

let FS be 1-sorted ;

attr c_{2} is strict ;

struct RightModStr over FS -> addLoopStr ;

aggr RightModStr(# carrier, addF, ZeroF, rmult #) -> RightModStr over FS;

sel rmult c_{2} -> Function of [: the carrier of c_{2}, the carrier of FS:], the carrier of c_{2};

end;
attr c

struct RightModStr over FS -> addLoopStr ;

aggr RightModStr(# carrier, addF, ZeroF, rmult #) -> RightModStr over FS;

sel rmult c

registration

let FS be 1-sorted ;

existence

not for b_{1} being RightModStr over FS holds b_{1} is empty

end;
existence

not for b

proof 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;

coherence

not RightModStr(# A,a,Z,r #) is empty ;

end;
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;

coherence

not RightModStr(# A,a,Z,r #) is empty ;

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;
let RMS be non empty RightModStr over FS;

mode Scalar of RMS is Element of FS;

mode Vector of RMS is Element of RMS;

definition

let FS1, FS2 be 1-sorted ;

attr c_{3} is strict ;

struct BiModStr over FS1,FS2 -> VectSpStr over FS1, RightModStr over FS2;

aggr BiModStr(# carrier, addF, ZeroF, lmult, rmult #) -> BiModStr over FS1,FS2;

end;
attr c

struct BiModStr over FS1,FS2 -> VectSpStr over FS1, RightModStr over FS2;

aggr BiModStr(# carrier, addF, ZeroF, lmult, rmult #) -> BiModStr over FS1,FS2;

registration

let FS1, FS2 be 1-sorted ;

existence

not for b_{1} being BiModStr over FS1,FS2 holds b_{1} is empty

end;
existence

not for b

proof 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;

coherence

not BiModStr(# A,a,Z,l,r #) is empty ;

end;
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;

coherence

not BiModStr(# A,a,Z,l,r #) is empty ;

definition

let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;

addLoopStr(# the carrier of R, the addF of R,(0. R) #) is strict AbGroup

end;
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) #);

addLoopStr(# the carrier of R, the addF of R,(0. R) #) is strict AbGroup

proof 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) #);

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 H

Lm4: for R being Ring holds

( H

proof end;

registration

let R be Ring;

ex b_{1} being non empty VectSpStr over R st

( b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is strict )

end;
cluster non empty right_complementable strict Abelian add-associative right_zeroed for VectSpStr over R;

existence ex b

( b

proof end;

definition

let R be Ring;

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;
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 #);

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;

:: 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 #);

for R being Ring holds LeftModule R = VectSpStr(# the carrier of R, the addF of R,(0. R), the multF of R #);

deffunc H

Lm5: for R being Ring holds

( H

proof end;

registration

let R be Ring;

ex b_{1} being non empty RightModStr over R st

( b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is strict )

end;
cluster non empty right_complementable Abelian add-associative right_zeroed strict for RightModStr over R;

existence ex b

( b

proof end;

definition

let R be Ring;

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;
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 #);

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;

:: 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 #);

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;

coherence

the rmult of V . (v,x) is Element of V ;

end;
let V be non empty RightModStr over R;

let x be Element of R;

let v be Element of V;

coherence

the rmult of V . (v,x) is Element of V ;

:: 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);

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 H

Lm6: for R1, R2 being Ring holds

( H

proof end;

registration

let R1, R2 be Ring;

ex b_{1} being non empty BiModStr over R1,R2 st

( b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is strict )

end;
cluster non empty right_complementable Abelian add-associative right_zeroed strict for BiModStr over R1,R2;

existence ex b

( b

proof end;

definition

let R1, R2 be Ring;

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;
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)) #);

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;

:: 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)) #);

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 )

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 end;

registration

let R be Ring;

ex b_{1} being non empty VectSpStr over R st

( b_{1} is vector-distributive & b_{1} is scalar-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is strict )

end;
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 b

( b

proof 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;
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;

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 end;

registration

let R be Ring;

( 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;
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;

:: 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) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )

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 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 ) );

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;

ex b_{1} being non empty RightModStr over R st

( b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is RightMod-like & b_{1} is strict )

end;
cluster non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like for RightModStr over R;

existence ex b

( b

proof 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;
mode RightMod of R is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R;

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

proof end;

registration

let R be Ring;

( 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;
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;

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 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 );

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;

ex b_{1} being non empty BiModStr over R1,R2 st

( b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is RightMod-like & b_{1} is vector-distributive & b_{1} is scalar-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital & b_{1} is BiMod-like & b_{1} is strict )

end;
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 b

( b

proof 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;
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;

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;

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;

registration

let R1, R2 be Ring;

( 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;
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;

theorem :: VECTSP_2:27

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

for a being Element of K holds a * (- (1. K)) = - a

proof 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

for a being Element of K holds (- (1. K)) * a = - a

proof 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 ) )

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 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

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 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 )

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 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)) )

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 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)

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 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)

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 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 ) )

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 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

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 end;