Metamath Proof Explorer


Theorem lmodslmd

Description: Left semimodules generalize the notion of left modules. (Contributed by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Assertion lmodslmd W LMod W SLMod

Proof

Step Hyp Ref Expression
1 lmodcmn W LMod W CMnd
2 eqid Scalar W = Scalar W
3 2 lmodring W LMod Scalar W Ring
4 ringsrg Scalar W Ring Scalar W SRing
5 3 4 syl W LMod Scalar W SRing
6 eqid Base W = Base W
7 eqid + W = + W
8 eqid W = W
9 eqid Base Scalar W = Base Scalar W
10 eqid + Scalar W = + Scalar W
11 eqid Scalar W = Scalar W
12 eqid 1 Scalar W = 1 Scalar W
13 6 7 8 2 9 10 11 12 islmod W LMod W Grp Scalar W Ring q Base Scalar W r Base Scalar W x Base W w Base W r W w Base W r W w + W x = r W w + W r W x q + Scalar W r W w = q W w + W r W w q Scalar W r W w = q W r W w 1 Scalar W W w = w
14 13 simp3bi W LMod q Base Scalar W r Base Scalar W x Base W w Base W r W w Base W r W w + W x = r W w + W r W x q + Scalar W r W w = q W w + W r W w q Scalar W r W w = q W r W w 1 Scalar W W w = w
15 14 r19.21bi W LMod q Base Scalar W r Base Scalar W x Base W w Base W r W w Base W r W w + W x = r W w + W r W x q + Scalar W r W w = q W w + W r W w q Scalar W r W w = q W r W w 1 Scalar W W w = w
16 15 r19.21bi W LMod q Base Scalar W r Base Scalar W x Base W w Base W r W w Base W r W w + W x = r W w + W r W x q + Scalar W r W w = q W w + W r W w q Scalar W r W w = q W r W w 1 Scalar W W w = w
17 16 r19.21bi W LMod q Base Scalar W r Base Scalar W x Base W w Base W r W w Base W r W w + W x = r W w + W r W x q + Scalar W r W w = q W w + W r W w q Scalar W r W w = q W r W w 1 Scalar W W w = w
18 17 r19.21bi W LMod q Base Scalar W r Base Scalar W x Base W w Base W r W w Base W r W w + W x = r W w + W r W x q + Scalar W r W w = q W w + W r W w q Scalar W r W w = q W r W w 1 Scalar W W w = w
19 18 simpld W LMod q Base Scalar W r Base Scalar W x Base W w Base W r W w Base W r W w + W x = r W w + W r W x q + Scalar W r W w = q W w + W r W w
20 18 simprd W LMod q Base Scalar W r Base Scalar W x Base W w Base W q Scalar W r W w = q W r W w 1 Scalar W W w = w
21 20 simpld W LMod q Base Scalar W r Base Scalar W x Base W w Base W q Scalar W r W w = q W r W w
22 20 simprd W LMod q Base Scalar W r Base Scalar W x Base W w Base W 1 Scalar W W w = w
23 simp-4l W LMod q Base Scalar W r Base Scalar W x Base W w Base W W LMod
24 eqid 0 Scalar W = 0 Scalar W
25 eqid 0 W = 0 W
26 6 2 8 24 25 lmod0vs W LMod w Base W 0 Scalar W W w = 0 W
27 23 26 sylancom W LMod q Base Scalar W r Base Scalar W x Base W w Base W 0 Scalar W W w = 0 W
28 21 22 27 3jca W LMod q Base Scalar W r Base Scalar W x Base W w Base W q Scalar W r W w = q W r W w 1 Scalar W W w = w 0 Scalar W W w = 0 W
29 19 28 jca W LMod q Base Scalar W r Base Scalar W x Base W w Base W r W w Base W r W w + W x = r W w + W r W x q + Scalar W r W w = q W w + W r W w q Scalar W r W w = q W r W w 1 Scalar W W w = w 0 Scalar W W w = 0 W
30 29 ralrimiva W LMod q Base Scalar W r Base Scalar W x Base W w Base W r W w Base W r W w + W x = r W w + W r W x q + Scalar W r W w = q W w + W r W w q Scalar W r W w = q W r W w 1 Scalar W W w = w 0 Scalar W W w = 0 W
31 30 ralrimiva W LMod q Base Scalar W r Base Scalar W x Base W w Base W r W w Base W r W w + W x = r W w + W r W x q + Scalar W r W w = q W w + W r W w q Scalar W r W w = q W r W w 1 Scalar W W w = w 0 Scalar W W w = 0 W
32 31 ralrimiva W LMod q Base Scalar W r Base Scalar W x Base W w Base W r W w Base W r W w + W x = r W w + W r W x q + Scalar W r W w = q W w + W r W w q Scalar W r W w = q W r W w 1 Scalar W W w = w 0 Scalar W W w = 0 W
33 32 ralrimiva W LMod q Base Scalar W r Base Scalar W x Base W w Base W r W w Base W r W w + W x = r W w + W r W x q + Scalar W r W w = q W w + W r W w q Scalar W r W w = q W r W w 1 Scalar W W w = w 0 Scalar W W w = 0 W
34 6 7 8 25 2 9 10 11 12 24 isslmd W SLMod W CMnd Scalar W SRing q Base Scalar W r Base Scalar W x Base W w Base W r W w Base W r W w + W x = r W w + W r W x q + Scalar W r W w = q W w + W r W w q Scalar W r W w = q W r W w 1 Scalar W W w = w 0 Scalar W W w = 0 W
35 1 5 33 34 syl3anbrc W LMod W SLMod