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 ⊢BaseW=BaseW
7 eqid ⊢+W=+W
8 eqid ⊢⋅W=⋅W
9 eqid ⊢BaseScalar⁡W=BaseScalar⁡W
10 eqid ⊢+Scalar⁡W=+Scalar⁡W
11 eqid ⊢⋅Scalar⁡W=⋅Scalar⁡W
12 eqid ⊢1Scalar⁡W=1Scalar⁡W
13 6 7 8 2 9 10 11 12 islmod ⊢W∈LMod↔W∈Grp∧Scalar⁡W∈Ring∧∀q∈BaseScalar⁡W∀r∈BaseScalar⁡W∀x∈BaseW∀w∈BaseWr⋅Ww∈BaseW∧r⋅Ww+Wx=r⋅Ww+Wr⋅Wx∧q+Scalar⁡Wr⋅Ww=q⋅Ww+Wr⋅Ww∧q⋅Scalar⁡Wr⋅Ww=q⋅Wr⋅Ww∧1Scalar⁡W⋅Ww=w
14 13 simp3bi ⊢W∈LMod→∀q∈BaseScalar⁡W∀r∈BaseScalar⁡W∀x∈BaseW∀w∈BaseWr⋅Ww∈BaseW∧r⋅Ww+Wx=r⋅Ww+Wr⋅Wx∧q+Scalar⁡Wr⋅Ww=q⋅Ww+Wr⋅Ww∧q⋅Scalar⁡Wr⋅Ww=q⋅Wr⋅Ww∧1Scalar⁡W⋅Ww=w
15 14 r19.21bi ⊢W∈LMod∧q∈BaseScalar⁡W→∀r∈BaseScalar⁡W∀x∈BaseW∀w∈BaseWr⋅Ww∈BaseW∧r⋅Ww+Wx=r⋅Ww+Wr⋅Wx∧q+Scalar⁡Wr⋅Ww=q⋅Ww+Wr⋅Ww∧q⋅Scalar⁡Wr⋅Ww=q⋅Wr⋅Ww∧1Scalar⁡W⋅Ww=w
16 15 r19.21bi ⊢W∈LMod∧q∈BaseScalar⁡W∧r∈BaseScalar⁡W→∀x∈BaseW∀w∈BaseWr⋅Ww∈BaseW∧r⋅Ww+Wx=r⋅Ww+Wr⋅Wx∧q+Scalar⁡Wr⋅Ww=q⋅Ww+Wr⋅Ww∧q⋅Scalar⁡Wr⋅Ww=q⋅Wr⋅Ww∧1Scalar⁡W⋅Ww=w
17 16 r19.21bi ⊢W∈LMod∧q∈BaseScalar⁡W∧r∈BaseScalar⁡W∧x∈BaseW→∀w∈BaseWr⋅Ww∈BaseW∧r⋅Ww+Wx=r⋅Ww+Wr⋅Wx∧q+Scalar⁡Wr⋅Ww=q⋅Ww+Wr⋅Ww∧q⋅Scalar⁡Wr⋅Ww=q⋅Wr⋅Ww∧1Scalar⁡W⋅Ww=w
18 17 r19.21bi ⊢W∈LMod∧q∈BaseScalar⁡W∧r∈BaseScalar⁡W∧x∈BaseW∧w∈BaseW→r⋅Ww∈BaseW∧r⋅Ww+Wx=r⋅Ww+Wr⋅Wx∧q+Scalar⁡Wr⋅Ww=q⋅Ww+Wr⋅Ww∧q⋅Scalar⁡Wr⋅Ww=q⋅Wr⋅Ww∧1Scalar⁡W⋅Ww=w
19 18 simpld ⊢W∈LMod∧q∈BaseScalar⁡W∧r∈BaseScalar⁡W∧x∈BaseW∧w∈BaseW→r⋅Ww∈BaseW∧r⋅Ww+Wx=r⋅Ww+Wr⋅Wx∧q+Scalar⁡Wr⋅Ww=q⋅Ww+Wr⋅Ww
20 18 simprd ⊢W∈LMod∧q∈BaseScalar⁡W∧r∈BaseScalar⁡W∧x∈BaseW∧w∈BaseW→q⋅Scalar⁡Wr⋅Ww=q⋅Wr⋅Ww∧1Scalar⁡W⋅Ww=w
21 20 simpld ⊢W∈LMod∧q∈BaseScalar⁡W∧r∈BaseScalar⁡W∧x∈BaseW∧w∈BaseW→q⋅Scalar⁡Wr⋅Ww=q⋅Wr⋅Ww
22 20 simprd ⊢W∈LMod∧q∈BaseScalar⁡W∧r∈BaseScalar⁡W∧x∈BaseW∧w∈BaseW→1Scalar⁡W⋅Ww=w
23 simp-4l ⊢W∈LMod∧q∈BaseScalar⁡W∧r∈BaseScalar⁡W∧x∈BaseW∧w∈BaseW→W∈LMod
24 eqid ⊢0Scalar⁡W=0Scalar⁡W
25 eqid ⊢0W=0W
26 6 2 8 24 25 lmod0vs ⊢W∈LMod∧w∈BaseW→0Scalar⁡W⋅Ww=0W
27 23 26 sylancom ⊢W∈LMod∧q∈BaseScalar⁡W∧r∈BaseScalar⁡W∧x∈BaseW∧w∈BaseW→0Scalar⁡W⋅Ww=0W
28 21 22 27 3jca ⊢W∈LMod∧q∈BaseScalar⁡W∧r∈BaseScalar⁡W∧x∈BaseW∧w∈BaseW→q⋅Scalar⁡Wr⋅Ww=q⋅Wr⋅Ww∧1Scalar⁡W⋅Ww=w∧0Scalar⁡W⋅Ww=0W
29 19 28 jca ⊢W∈LMod∧q∈BaseScalar⁡W∧r∈BaseScalar⁡W∧x∈BaseW∧w∈BaseW→r⋅Ww∈BaseW∧r⋅Ww+Wx=r⋅Ww+Wr⋅Wx∧q+Scalar⁡Wr⋅Ww=q⋅Ww+Wr⋅Ww∧q⋅Scalar⁡Wr⋅Ww=q⋅Wr⋅Ww∧1Scalar⁡W⋅Ww=w∧0Scalar⁡W⋅Ww=0W
30 29 ralrimiva ⊢W∈LMod∧q∈BaseScalar⁡W∧r∈BaseScalar⁡W∧x∈BaseW→∀w∈BaseWr⋅Ww∈BaseW∧r⋅Ww+Wx=r⋅Ww+Wr⋅Wx∧q+Scalar⁡Wr⋅Ww=q⋅Ww+Wr⋅Ww∧q⋅Scalar⁡Wr⋅Ww=q⋅Wr⋅Ww∧1Scalar⁡W⋅Ww=w∧0Scalar⁡W⋅Ww=0W
31 30 ralrimiva ⊢W∈LMod∧q∈BaseScalar⁡W∧r∈BaseScalar⁡W→∀x∈BaseW∀w∈BaseWr⋅Ww∈BaseW∧r⋅Ww+Wx=r⋅Ww+Wr⋅Wx∧q+Scalar⁡Wr⋅Ww=q⋅Ww+Wr⋅Ww∧q⋅Scalar⁡Wr⋅Ww=q⋅Wr⋅Ww∧1Scalar⁡W⋅Ww=w∧0Scalar⁡W⋅Ww=0W
32 31 ralrimiva ⊢W∈LMod∧q∈BaseScalar⁡W→∀r∈BaseScalar⁡W∀x∈BaseW∀w∈BaseWr⋅Ww∈BaseW∧r⋅Ww+Wx=r⋅Ww+Wr⋅Wx∧q+Scalar⁡Wr⋅Ww=q⋅Ww+Wr⋅Ww∧q⋅Scalar⁡Wr⋅Ww=q⋅Wr⋅Ww∧1Scalar⁡W⋅Ww=w∧0Scalar⁡W⋅Ww=0W
33 32 ralrimiva ⊢W∈LMod→∀q∈BaseScalar⁡W∀r∈BaseScalar⁡W∀x∈BaseW∀w∈BaseWr⋅Ww∈BaseW∧r⋅Ww+Wx=r⋅Ww+Wr⋅Wx∧q+Scalar⁡Wr⋅Ww=q⋅Ww+Wr⋅Ww∧q⋅Scalar⁡Wr⋅Ww=q⋅Wr⋅Ww∧1Scalar⁡W⋅Ww=w∧0Scalar⁡W⋅Ww=0W
34 6 7 8 25 2 9 10 11 12 24 isslmd ⊢W∈SLMod↔W∈CMnd∧Scalar⁡W∈SRing∧∀q∈BaseScalar⁡W∀r∈BaseScalar⁡W∀x∈BaseW∀w∈BaseWr⋅Ww∈BaseW∧r⋅Ww+Wx=r⋅Ww+Wr⋅Wx∧q+Scalar⁡Wr⋅Ww=q⋅Ww+Wr⋅Ww∧q⋅Scalar⁡Wr⋅Ww=q⋅Wr⋅Ww∧1Scalar⁡W⋅Ww=w∧0Scalar⁡W⋅Ww=0W
35 1 5 33 34 syl3anbrc ⊢W∈LMod→W∈SLMod