slmdcmn

Description: A semimodule is a commutative monoid. (Contributed by Thierry Arnoux, 1-Apr-2018)

		Ref	Expression
	Assertion	slmdcmn	$⊢ W \in SLMod \to W \in CMnd$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{W} = {Base}_{W}$
2		eqid	$⊢ +_{W} = +_{W}$
3		eqid	$⊢ \cdot_{W} = \cdot_{W}$
4		eqid	$⊢ 0_{W} = 0_{W}$
5		eqid	$⊢ Scalar (W) = Scalar (W)$
6		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
7		eqid	$⊢ +_{Scalar (W)} = +_{Scalar (W)}$
8		eqid	$⊢ \cdot_{Scalar (W)} = \cdot_{Scalar (W)}$
9		eqid	$⊢ 1_{Scalar (W)} = 1_{Scalar (W)}$
10		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
11	1 2 3 4 5 6 7 8 9 10	isslmd	$⊢ W \in SLMod \leftrightarrow (W \in CMnd \land Scalar (W) \in SRing \land \forall w \in {Base}_{Scalar (W)} \forall z \in {Base}_{Scalar (W)} \forall x \in {Base}_{W} \forall y \in {Base}_{W} ((z \cdot_{W} y \in {Base}_{W} \land z \cdot_{W} (y +_{W} x) = (z \cdot_{W} y) +_{W} (z \cdot_{W} x) \land (w +_{Scalar (W)} z) \cdot_{W} y = (w \cdot_{W} y) +_{W} (z \cdot_{W} y)) \land ((w \cdot_{Scalar (W)} z) \cdot_{W} y = w \cdot_{W} (z \cdot_{W} y) \land 1_{Scalar (W)} \cdot_{W} y = y \land 0_{Scalar (W)} \cdot_{W} y = 0_{W})))$
12	11	simp1bi	$⊢ W \in SLMod \to W \in CMnd$

Metamath Proof Explorer