Theorem lmod4

Description: Commutative/associative law for left module vector sum. (Contributed by NM, 4-Feb-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lmod4.v	$$⊢V={\mathrm{Base}}_W$$
	lmod4.p	$$⊢\underset{\dot{}}{+}={+}_W$$
Assertion	lmod4	$$⊢\left(W\in \mathrm{LMod}\wedge \left(X\in V\wedge Y\in V\right)\wedge \left(Z\in V\wedge U\in V\right)\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}U\right)=\left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}U\right)$$

Proof

Step	Hyp	Ref	Expression
1		lmod4.v	$$⊢V={\mathrm{Base}}_W$$
2		lmod4.p	$$⊢\underset{\dot{}}{+}={+}_W$$
3		lmodcmn	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{CMnd}$$
4	1 2	cmn4	$$⊢\left(W\in \mathrm{CMnd}\wedge \left(X\in V\wedge Y\in V\right)\wedge \left(Z\in V\wedge U\in V\right)\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}U\right)=\left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}U\right)$$
5	3 4	syl3an1	$$⊢\left(W\in \mathrm{LMod}\wedge \left(X\in V\wedge Y\in V\right)\wedge \left(Z\in V\wedge U\in V\right)\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}U\right)=\left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}U\right)$$