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