:: by Michal Muzalewski and Wojciech Skaba

::

:: Received October 22, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let R be Ring;

let V be RightMod of R;

let W1, W2 be Submodule of V;

ex b_{1} being strict Submodule of V st the carrier of b_{1} = { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 ) }

for b_{1}, b_{2} being strict Submodule of V st the carrier of b_{1} = { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 ) } & the carrier of b_{2} = { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 ) } holds

b_{1} = b_{2}
by RMOD_2:29;

end;
let V be RightMod of R;

let W1, W2 be Submodule of V;

func W1 + W2 -> strict Submodule of V means :Def1: :: RMOD_3:def 1

the carrier of it = { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 ) } ;

existence the carrier of it = { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 ) } ;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def1 defines + RMOD_3:def 1 :

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V

for b_{5} being strict Submodule of V holds

( b_{5} = W1 + W2 iff the carrier of b_{5} = { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 ) } );

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V

for b

( b

definition

let R be Ring;

let V be RightMod of R;

let W1, W2 be Submodule of V;

ex b_{1} being strict Submodule of V st the carrier of b_{1} = the carrier of W1 /\ the carrier of W2

for b_{1}, b_{2} being strict Submodule of V st the carrier of b_{1} = the carrier of W1 /\ the carrier of W2 & the carrier of b_{2} = the carrier of W1 /\ the carrier of W2 holds

b_{1} = b_{2}
by RMOD_2:29;

end;
let V be RightMod of R;

let W1, W2 be Submodule of V;

func W1 /\ W2 -> strict Submodule of V means :Def2: :: RMOD_3:def 2

the carrier of it = the carrier of W1 /\ the carrier of W2;

existence the carrier of it = the carrier of W1 /\ the carrier of W2;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def2 defines /\ RMOD_3:def 2 :

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V

for b_{5} being strict Submodule of V holds

( b_{5} = W1 /\ W2 iff the carrier of b_{5} = the carrier of W1 /\ the carrier of W2 );

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V

for b

( b

theorem Th1: :: RMOD_3:1

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V

for x being object holds

( x in W1 + W2 iff ex v1, v2 being Vector of V st

( v1 in W1 & v2 in W2 & x = v1 + v2 ) )

for V being RightMod of R

for W1, W2 being Submodule of V

for x being object holds

( x in W1 + W2 iff ex v1, v2 being Vector of V st

( v1 in W1 & v2 in W2 & x = v1 + v2 ) )

proof end;

theorem :: RMOD_3:2

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V

for v being Vector of V st ( v in W1 or v in W2 ) holds

v in W1 + W2

for V being RightMod of R

for W1, W2 being Submodule of V

for v being Vector of V st ( v in W1 or v in W2 ) holds

v in W1 + W2

proof end;

theorem Th3: :: RMOD_3:3

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V

for x being object holds

( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )

for V being RightMod of R

for W1, W2 being Submodule of V

for x being object holds

( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )

proof end;

Lm1: for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V holds W1 + W2 = W2 + W1

proof end;

Lm2: for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V holds the carrier of W1 c= the carrier of (W1 + W2)

proof end;

Lm3: for R being Ring

for V being RightMod of R

for W1 being Submodule of V

for W2 being strict Submodule of V st the carrier of W1 c= the carrier of W2 holds

W1 + W2 = W2

proof end;

theorem :: RMOD_3:4

theorem :: RMOD_3:5

theorem Th6: :: RMOD_3:6

for R being Ring

for V being RightMod of R

for W1, W2, W3 being Submodule of V holds W1 + (W2 + W3) = (W1 + W2) + W3

for V being RightMod of R

for W1, W2, W3 being Submodule of V holds W1 + (W2 + W3) = (W1 + W2) + W3

proof end;

theorem Th7: :: RMOD_3:7

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V holds

( W1 is Submodule of W1 + W2 & W2 is Submodule of W1 + W2 )

for V being RightMod of R

for W1, W2 being Submodule of V holds

( W1 is Submodule of W1 + W2 & W2 is Submodule of W1 + W2 )

proof end;

theorem Th8: :: RMOD_3:8

for R being Ring

for V being RightMod of R

for W1 being Submodule of V

for W2 being strict Submodule of V holds

( W1 is Submodule of W2 iff W1 + W2 = W2 )

for V being RightMod of R

for W1 being Submodule of V

for W2 being strict Submodule of V holds

( W1 is Submodule of W2 iff W1 + W2 = W2 )

proof end;

theorem Th9: :: RMOD_3:9

for R being Ring

for V being RightMod of R

for W being strict Submodule of V holds

( ((0). V) + W = W & W + ((0). V) = W )

for V being RightMod of R

for W being strict Submodule of V holds

( ((0). V) + W = W & W + ((0). V) = W )

proof end;

Lm4: for R being Ring

for V being RightMod of R

for W, W9, W1 being Submodule of V st the carrier of W = the carrier of W9 holds

( W1 + W = W1 + W9 & W + W1 = W9 + W1 )

proof end;

Lm5: for R being Ring

for V being RightMod of R

for W being Submodule of V holds W is Submodule of (Omega). V

proof end;

theorem :: RMOD_3:10

theorem Th11: :: RMOD_3:11

for R being Ring

for V being RightMod of R

for W being Submodule of V holds

( ((Omega). V) + W = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) & W + ((Omega). V) = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) )

for V being RightMod of R

for W being Submodule of V holds

( ((Omega). V) + W = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) & W + ((Omega). V) = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) )

proof end;

theorem :: RMOD_3:12

theorem Th14: :: RMOD_3:14

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V holds W1 /\ W2 = W2 /\ W1

for V being RightMod of R

for W1, W2 being Submodule of V holds W1 /\ W2 = W2 /\ W1

proof end;

theorem Th15: :: RMOD_3:15

for R being Ring

for V being RightMod of R

for W1, W2, W3 being Submodule of V holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3

for V being RightMod of R

for W1, W2, W3 being Submodule of V holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3

proof end;

Lm6: for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V holds the carrier of (W1 /\ W2) c= the carrier of W1

proof end;

theorem Th16: :: RMOD_3:16

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V holds

( W1 /\ W2 is Submodule of W1 & W1 /\ W2 is Submodule of W2 )

for V being RightMod of R

for W1, W2 being Submodule of V holds

( W1 /\ W2 is Submodule of W1 & W1 /\ W2 is Submodule of W2 )

proof end;

theorem Th17: :: RMOD_3:17

for R being Ring

for V being RightMod of R

for W2 being Submodule of V holds

( ( for W1 being strict Submodule of V st W1 is Submodule of W2 holds

W1 /\ W2 = W1 ) & ( for W1 being Submodule of V st W1 /\ W2 = W1 holds

W1 is Submodule of W2 ) )

for V being RightMod of R

for W2 being Submodule of V holds

( ( for W1 being strict Submodule of V st W1 is Submodule of W2 holds

W1 /\ W2 = W1 ) & ( for W1 being Submodule of V st W1 /\ W2 = W1 holds

W1 is Submodule of W2 ) )

proof end;

theorem :: RMOD_3:18

for R being Ring

for V being RightMod of R

for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds

W1 /\ W3 is Submodule of W2 /\ W3

for V being RightMod of R

for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds

W1 /\ W3 is Submodule of W2 /\ W3

proof end;

theorem :: RMOD_3:19

for R being Ring

for V being RightMod of R

for W1, W2, W3 being Submodule of V st W1 is Submodule of W3 holds

W1 /\ W2 is Submodule of W3

for V being RightMod of R

for W1, W2, W3 being Submodule of V st W1 is Submodule of W3 holds

W1 /\ W2 is Submodule of W3

proof end;

theorem :: RMOD_3:20

for R being Ring

for V being RightMod of R

for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 & W1 is Submodule of W3 holds

W1 is Submodule of W2 /\ W3

for V being RightMod of R

for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 & W1 is Submodule of W3 holds

W1 is Submodule of W2 /\ W3

proof end;

theorem Th21: :: RMOD_3:21

for R being Ring

for V being RightMod of R

for W being Submodule of V holds

( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )

for V being RightMod of R

for W being Submodule of V holds

( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )

proof end;

theorem Th22: :: RMOD_3:22

for R being Ring

for V being RightMod of R

for W being strict Submodule of V holds

( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )

for V being RightMod of R

for W being strict Submodule of V holds

( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )

proof end;

theorem :: RMOD_3:23

Lm7: for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)

proof end;

theorem :: RMOD_3:24

Lm8: for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2

proof end;

theorem :: RMOD_3:25

Lm9: for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1

proof end;

theorem :: RMOD_3:26

Lm10: for R being Ring

for V being RightMod of R

for W1, W2, W3 being Submodule of V holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))

proof end;

theorem :: RMOD_3:27

Lm11: for R being Ring

for V being RightMod of R

for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds

the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))

proof end;

theorem :: RMOD_3:28

Lm12: for R being Ring

for V being RightMod of R

for W1, W2, W3 being Submodule of V holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))

proof end;

theorem :: RMOD_3:29

Lm13: for R being Ring

for V being RightMod of R

for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds

the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))

proof end;

theorem :: RMOD_3:30

theorem Th31: :: RMOD_3:31

for R being Ring

for V being RightMod of R

for W2, W3 being Submodule of V

for W1 being strict Submodule of V st W1 is Submodule of W3 holds

W1 + (W2 /\ W3) = (W1 + W2) /\ W3

for V being RightMod of R

for W2, W3 being Submodule of V

for W1 being strict Submodule of V st W1 is Submodule of W3 holds

W1 + (W2 /\ W3) = (W1 + W2) /\ W3

proof end;

theorem :: RMOD_3:32

for R being Ring

for V being RightMod of R

for W1, W2 being strict Submodule of V holds

( W1 + W2 = W2 iff W1 /\ W2 = W1 )

for V being RightMod of R

for W1, W2 being strict Submodule of V holds

( W1 + W2 = W2 iff W1 /\ W2 = W1 )

proof end;

theorem :: RMOD_3:33

for R being Ring

for V being RightMod of R

for W1 being Submodule of V

for W2, W3 being strict Submodule of V st W1 is Submodule of W2 holds

W1 + W3 is Submodule of W2 + W3

for V being RightMod of R

for W1 being Submodule of V

for W2, W3 being strict Submodule of V st W1 is Submodule of W2 holds

W1 + W3 is Submodule of W2 + W3

proof end;

theorem :: RMOD_3:34

for R being Ring

for V being RightMod of R

for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds

W1 is Submodule of W2 + W3

for V being RightMod of R

for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds

W1 is Submodule of W2 + W3

proof end;

theorem :: RMOD_3:35

for R being Ring

for V being RightMod of R

for W1, W2, W3 being Submodule of V st W1 is Submodule of W3 & W2 is Submodule of W3 holds

W1 + W2 is Submodule of W3

for V being RightMod of R

for W1, W2, W3 being Submodule of V st W1 is Submodule of W3 & W2 is Submodule of W3 holds

W1 + W2 is Submodule of W3

proof end;

theorem :: RMOD_3:36

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V holds

( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) iff ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )

for V being RightMod of R

for W1, W2 being Submodule of V holds

( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) iff ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )

proof end;

definition

let R be Ring;

let V be RightMod of R;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ex W being strict Submodule of V st W = x )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff ex W being strict Submodule of V st W = x ) ) & ( for x being object holds

( x in b_{2} iff ex W being strict Submodule of V st W = x ) ) holds

b_{1} = b_{2}

end;
let V be RightMod of R;

func Submodules V -> set means :Def3: :: RMOD_3:def 3

for x being object holds

( x in it iff ex W being strict Submodule of V st W = x );

existence for x being object holds

( x in it iff ex W being strict Submodule of V st W = x );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def3 defines Submodules RMOD_3:def 3 :

for R being Ring

for V being RightMod of R

for b_{3} being set holds

( b_{3} = Submodules V iff for x being object holds

( x in b_{3} iff ex W being strict Submodule of V st W = x ) );

for R being Ring

for V being RightMod of R

for b

( b

( x in b

registration
end;

definition

let R be Ring;

let V be RightMod of R;

let W1, W2 be Submodule of V;

end;
let V be RightMod of R;

let W1, W2 be Submodule of V;

pred V is_the_direct_sum_of W1,W2 means :: RMOD_3:def 4

( RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) = W1 + W2 & W1 /\ W2 = (0). V );

( RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) = W1 + W2 & W1 /\ W2 = (0). V );

:: deftheorem defines is_the_direct_sum_of RMOD_3:def 4 :

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V holds

( V is_the_direct_sum_of W1,W2 iff ( RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) = W1 + W2 & W1 /\ W2 = (0). V ) );

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V holds

( V is_the_direct_sum_of W1,W2 iff ( RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) = W1 + W2 & W1 /\ W2 = (0). V ) );

Lm14: for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V holds

( W1 + W2 = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) iff for v being Vector of V ex v1, v2 being Vector of V st

( v1 in W1 & v2 in W2 & v = v1 + v2 ) )

proof end;

Lm15: for R being Ring

for V being RightMod of R

for v, v1, v2 being Vector of V holds

( v = v1 + v2 iff v1 = v - v2 )

proof end;

theorem Th38: :: RMOD_3:38

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V st V is_the_direct_sum_of W1,W2 holds

V is_the_direct_sum_of W2,W1 by Th14, Lm1;

for V being RightMod of R

for W1, W2 being Submodule of V st V is_the_direct_sum_of W1,W2 holds

V is_the_direct_sum_of W2,W1 by Th14, Lm1;

theorem :: RMOD_3:39

theorem Th40: :: RMOD_3:40

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V

for C1 being Coset of W1

for C2 being Coset of W2 st C1 meets C2 holds

C1 /\ C2 is Coset of W1 /\ W2

for V being RightMod of R

for W1, W2 being Submodule of V

for C1 being Coset of W1

for C2 being Coset of W2 st C1 meets C2 holds

C1 /\ C2 is Coset of W1 /\ W2

proof end;

theorem Th41: :: RMOD_3:41

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V holds

( V is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1

for C2 being Coset of W2 ex v being Vector of V st C1 /\ C2 = {v} )

for V being RightMod of R

for W1, W2 being Submodule of V holds

( V is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1

for C2 being Coset of W2 ex v being Vector of V st C1 /\ C2 = {v} )

proof end;

theorem :: RMOD_3:42

theorem Th43: :: RMOD_3:43

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V

for v, v1, v2, u1, u2 being Vector of V st V is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds

( v1 = u1 & v2 = u2 )

for V being RightMod of R

for W1, W2 being Submodule of V

for v, v1, v2, u1, u2 being Vector of V st V is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds

( v1 = u1 & v2 = u2 )

proof end;

theorem :: RMOD_3:44

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V st V = W1 + W2 & ex v being Vector of V st

for v1, v2, u1, u2 being Vector of V st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds

( v1 = u1 & v2 = u2 ) holds

V is_the_direct_sum_of W1,W2

for V being RightMod of R

for W1, W2 being Submodule of V st V = W1 + W2 & ex v being Vector of V st

for v1, v2, u1, u2 being Vector of V st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds

( v1 = u1 & v2 = u2 ) holds

V is_the_direct_sum_of W1,W2

proof end;

definition

let R be Ring;

let V be RightMod of R;

let v be Vector of V;

let W1, W2 be Submodule of V;

assume A1: V is_the_direct_sum_of W1,W2 ;

ex b_{1} being Element of [: the carrier of V, the carrier of V:] st

( v = (b_{1} `1) + (b_{1} `2) & b_{1} `1 in W1 & b_{1} `2 in W2 )

for b_{1}, b_{2} being Element of [: the carrier of V, the carrier of V:] st v = (b_{1} `1) + (b_{1} `2) & b_{1} `1 in W1 & b_{1} `2 in W2 & v = (b_{2} `1) + (b_{2} `2) & b_{2} `1 in W1 & b_{2} `2 in W2 holds

b_{1} = b_{2}

end;
let V be RightMod of R;

let v be Vector of V;

let W1, W2 be Submodule of V;

assume A1: V is_the_direct_sum_of W1,W2 ;

func v |-- (W1,W2) -> Element of [: the carrier of V, the carrier of V:] means :Def5: :: RMOD_3:def 5

( v = (it `1) + (it `2) & it `1 in W1 & it `2 in W2 );

existence ( v = (it `1) + (it `2) & it `1 in W1 & it `2 in W2 );

ex b

( v = (b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines |-- RMOD_3:def 5 :

for R being Ring

for V being RightMod of R

for v being Vector of V

for W1, W2 being Submodule of V st V is_the_direct_sum_of W1,W2 holds

for b_{6} being Element of [: the carrier of V, the carrier of V:] holds

( b_{6} = v |-- (W1,W2) iff ( v = (b_{6} `1) + (b_{6} `2) & b_{6} `1 in W1 & b_{6} `2 in W2 ) );

for R being Ring

for V being RightMod of R

for v being Vector of V

for W1, W2 being Submodule of V st V is_the_direct_sum_of W1,W2 holds

for b

( b

theorem :: RMOD_3:45

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V

for v being Vector of V st V is_the_direct_sum_of W1,W2 holds

(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2

for V being RightMod of R

for W1, W2 being Submodule of V

for v being Vector of V st V is_the_direct_sum_of W1,W2 holds

(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2

proof end;

theorem :: RMOD_3:46

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V

for v being Vector of V st V is_the_direct_sum_of W1,W2 holds

(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1

for V being RightMod of R

for W1, W2 being Submodule of V

for v being Vector of V st V is_the_direct_sum_of W1,W2 holds

(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1

proof end;

definition

let R be Ring;

let V be RightMod of R;

ex b_{1} being BinOp of (Submodules V) st

for A1, A2 being Element of Submodules V

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

b_{1} . (A1,A2) = W1 + W2

for b_{1}, b_{2} being BinOp of (Submodules V) st ( for A1, A2 being Element of Submodules V

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

b_{1} . (A1,A2) = W1 + W2 ) & ( for A1, A2 being Element of Submodules V

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

b_{2} . (A1,A2) = W1 + W2 ) holds

b_{1} = b_{2}

end;
let V be RightMod of R;

func SubJoin V -> BinOp of (Submodules V) means :Def6: :: RMOD_3:def 6

for A1, A2 being Element of Submodules V

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

it . (A1,A2) = W1 + W2;

existence for A1, A2 being Element of Submodules V

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

it . (A1,A2) = W1 + W2;

ex b

for A1, A2 being Element of Submodules V

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

b

proof end;

uniqueness for b

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

b

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

b

b

proof end;

:: deftheorem Def6 defines SubJoin RMOD_3:def 6 :

for R being Ring

for V being RightMod of R

for b_{3} being BinOp of (Submodules V) holds

( b_{3} = SubJoin V iff for A1, A2 being Element of Submodules V

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

b_{3} . (A1,A2) = W1 + W2 );

for R being Ring

for V being RightMod of R

for b

( b

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

b

definition

let R be Ring;

let V be RightMod of R;

ex b_{1} being BinOp of (Submodules V) st

for A1, A2 being Element of Submodules V

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

b_{1} . (A1,A2) = W1 /\ W2

for b_{1}, b_{2} being BinOp of (Submodules V) st ( for A1, A2 being Element of Submodules V

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

b_{1} . (A1,A2) = W1 /\ W2 ) & ( for A1, A2 being Element of Submodules V

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

b_{2} . (A1,A2) = W1 /\ W2 ) holds

b_{1} = b_{2}

end;
let V be RightMod of R;

func SubMeet V -> BinOp of (Submodules V) means :Def7: :: RMOD_3:def 7

for A1, A2 being Element of Submodules V

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

it . (A1,A2) = W1 /\ W2;

existence for A1, A2 being Element of Submodules V

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

it . (A1,A2) = W1 /\ W2;

ex b

for A1, A2 being Element of Submodules V

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

b

proof end;

uniqueness for b

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

b

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

b

b

proof end;

:: deftheorem Def7 defines SubMeet RMOD_3:def 7 :

for R being Ring

for V being RightMod of R

for b_{3} being BinOp of (Submodules V) holds

( b_{3} = SubMeet V iff for A1, A2 being Element of Submodules V

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

b_{3} . (A1,A2) = W1 /\ W2 );

for R being Ring

for V being RightMod of R

for b

( b

for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds

b

theorem Th47: :: RMOD_3:47

for R being Ring

for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is Lattice

for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is Lattice

proof end;

theorem Th48: :: RMOD_3:48

for R being Ring

for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 0_Lattice

for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 0_Lattice

proof end;

theorem Th49: :: RMOD_3:49

for R being Ring

for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 1_Lattice

for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 1_Lattice

proof end;

theorem :: RMOD_3:50

for R being Ring

for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 01_Lattice

for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 01_Lattice

proof end;

theorem :: RMOD_3:51

for R being Ring

for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is M_Lattice

for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is M_Lattice

proof end;