lmodcom

Description: Left module vector sum is commutative. (Contributed by Gérard Lang, 25-Jun-2014)

	Ref	Expression
Hypotheses	lmodcom.v	$⊢ V = {Base}_{W}$
	lmodcom.a	$⊢ \underset{˙}{+} = +_{W}$
Assertion	lmodcom	$⊢ (W \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$

Proof

Step	Hyp	Ref	Expression
1		lmodcom.v	$⊢ V = {Base}_{W}$
2		lmodcom.a	$⊢ \underset{˙}{+} = +_{W}$
3		simp1	$⊢ (W \in LMod \land X \in V \land Y \in V) \to W \in LMod$
4		eqid	$⊢ Scalar (W) = Scalar (W)$
5		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
6		eqid	$⊢ 1_{Scalar (W)} = 1_{Scalar (W)}$
7	4 5 6	lmod1cl	$⊢ W \in LMod \to 1_{Scalar (W)} \in {Base}_{Scalar (W)}$
8	3 7	syl	$⊢ (W \in LMod \land X \in V \land Y \in V) \to 1_{Scalar (W)} \in {Base}_{Scalar (W)}$
9		eqid	$⊢ +_{Scalar (W)} = +_{Scalar (W)}$
10	4 5 9	lmodacl	$⊢ (W \in LMod \land 1_{Scalar (W)} \in {Base}_{Scalar (W)} \land 1_{Scalar (W)} \in {Base}_{Scalar (W)}) \to 1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)} \in {Base}_{Scalar (W)}$
11	3 8 8 10	syl3anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to 1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)} \in {Base}_{Scalar (W)}$
12		simp2	$⊢ (W \in LMod \land X \in V \land Y \in V) \to X \in V$
13		simp3	$⊢ (W \in LMod \land X \in V \land Y \in V) \to Y \in V$
14		eqid	$⊢ \cdot_{W} = \cdot_{W}$
15	1 2 4 14 5	lmodvsdi	$⊢ (W \in LMod \land (1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)} \in {Base}_{Scalar (W)} \land X \in V \land Y \in V)) \to (1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} (X \underset{˙}{+} Y) = ((1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} X) \underset{˙}{+} ((1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} Y)$
16	3 11 12 13 15	syl13anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} (X \underset{˙}{+} Y) = ((1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} X) \underset{˙}{+} ((1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} Y)$
17	1 2	lmodvacl	$⊢ (W \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{+} Y \in V$
18	1 2 4 14 5 9	lmodvsdir	$⊢ (W \in LMod \land (1_{Scalar (W)} \in {Base}_{Scalar (W)} \land 1_{Scalar (W)} \in {Base}_{Scalar (W)} \land X \underset{˙}{+} Y \in V)) \to (1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} (X \underset{˙}{+} Y) = (1_{Scalar (W)} \cdot_{W} (X \underset{˙}{+} Y)) \underset{˙}{+} (1_{Scalar (W)} \cdot_{W} (X \underset{˙}{+} Y))$
19	3 8 8 17 18	syl13anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} (X \underset{˙}{+} Y) = (1_{Scalar (W)} \cdot_{W} (X \underset{˙}{+} Y)) \underset{˙}{+} (1_{Scalar (W)} \cdot_{W} (X \underset{˙}{+} Y))$
20	16 19	eqtr3d	$⊢ (W \in LMod \land X \in V \land Y \in V) \to ((1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} X) \underset{˙}{+} ((1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} Y) = (1_{Scalar (W)} \cdot_{W} (X \underset{˙}{+} Y)) \underset{˙}{+} (1_{Scalar (W)} \cdot_{W} (X \underset{˙}{+} Y))$
21	1 2 4 14 5 9	lmodvsdir	$⊢ (W \in LMod \land (1_{Scalar (W)} \in {Base}_{Scalar (W)} \land 1_{Scalar (W)} \in {Base}_{Scalar (W)} \land X \in V)) \to (1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} X = (1_{Scalar (W)} \cdot_{W} X) \underset{˙}{+} (1_{Scalar (W)} \cdot_{W} X)$
22	3 8 8 12 21	syl13anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} X = (1_{Scalar (W)} \cdot_{W} X) \underset{˙}{+} (1_{Scalar (W)} \cdot_{W} X)$
23	1 4 14 6	lmodvs1	$⊢ (W \in LMod \land X \in V) \to 1_{Scalar (W)} \cdot_{W} X = X$
24	3 12 23	syl2anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to 1_{Scalar (W)} \cdot_{W} X = X$
25	24 24	oveq12d	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (1_{Scalar (W)} \cdot_{W} X) \underset{˙}{+} (1_{Scalar (W)} \cdot_{W} X) = X \underset{˙}{+} X$
26	22 25	eqtrd	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} X = X \underset{˙}{+} X$
27	1 2 4 14 5 9	lmodvsdir	$⊢ (W \in LMod \land (1_{Scalar (W)} \in {Base}_{Scalar (W)} \land 1_{Scalar (W)} \in {Base}_{Scalar (W)} \land Y \in V)) \to (1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} Y = (1_{Scalar (W)} \cdot_{W} Y) \underset{˙}{+} (1_{Scalar (W)} \cdot_{W} Y)$
28	3 8 8 13 27	syl13anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} Y = (1_{Scalar (W)} \cdot_{W} Y) \underset{˙}{+} (1_{Scalar (W)} \cdot_{W} Y)$
29	1 4 14 6	lmodvs1	$⊢ (W \in LMod \land Y \in V) \to 1_{Scalar (W)} \cdot_{W} Y = Y$
30	3 13 29	syl2anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to 1_{Scalar (W)} \cdot_{W} Y = Y$
31	30 30	oveq12d	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (1_{Scalar (W)} \cdot_{W} Y) \underset{˙}{+} (1_{Scalar (W)} \cdot_{W} Y) = Y \underset{˙}{+} Y$
32	28 31	eqtrd	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} Y = Y \underset{˙}{+} Y$
33	26 32	oveq12d	$⊢ (W \in LMod \land X \in V \land Y \in V) \to ((1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} X) \underset{˙}{+} ((1_{Scalar (W)} +_{Scalar (W)} 1_{Scalar (W)}) \cdot_{W} Y) = (X \underset{˙}{+} X) \underset{˙}{+} (Y \underset{˙}{+} Y)$
34	1 4 14 6	lmodvs1	$⊢ (W \in LMod \land X \underset{˙}{+} Y \in V) \to 1_{Scalar (W)} \cdot_{W} (X \underset{˙}{+} Y) = X \underset{˙}{+} Y$
35	3 17 34	syl2anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to 1_{Scalar (W)} \cdot_{W} (X \underset{˙}{+} Y) = X \underset{˙}{+} Y$
36	35 35	oveq12d	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (1_{Scalar (W)} \cdot_{W} (X \underset{˙}{+} Y)) \underset{˙}{+} (1_{Scalar (W)} \cdot_{W} (X \underset{˙}{+} Y)) = (X \underset{˙}{+} Y) \underset{˙}{+} (X \underset{˙}{+} Y)$
37	20 33 36	3eqtr3d	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (X \underset{˙}{+} X) \underset{˙}{+} (Y \underset{˙}{+} Y) = (X \underset{˙}{+} Y) \underset{˙}{+} (X \underset{˙}{+} Y)$
38	1 2	lmodvacl	$⊢ (W \in LMod \land X \in V \land X \in V) \to X \underset{˙}{+} X \in V$
39	3 12 12 38	syl3anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{+} X \in V$
40	1 2	lmodass	$⊢ (W \in LMod \land (X \underset{˙}{+} X \in V \land Y \in V \land Y \in V)) \to ((X \underset{˙}{+} X) \underset{˙}{+} Y) \underset{˙}{+} Y = (X \underset{˙}{+} X) \underset{˙}{+} (Y \underset{˙}{+} Y)$
41	3 39 13 13 40	syl13anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to ((X \underset{˙}{+} X) \underset{˙}{+} Y) \underset{˙}{+} Y = (X \underset{˙}{+} X) \underset{˙}{+} (Y \underset{˙}{+} Y)$
42	1 2	lmodass	$⊢ (W \in LMod \land (X \underset{˙}{+} Y \in V \land X \in V \land Y \in V)) \to ((X \underset{˙}{+} Y) \underset{˙}{+} X) \underset{˙}{+} Y = (X \underset{˙}{+} Y) \underset{˙}{+} (X \underset{˙}{+} Y)$
43	3 17 12 13 42	syl13anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to ((X \underset{˙}{+} Y) \underset{˙}{+} X) \underset{˙}{+} Y = (X \underset{˙}{+} Y) \underset{˙}{+} (X \underset{˙}{+} Y)$
44	37 41 43	3eqtr4d	$⊢ (W \in LMod \land X \in V \land Y \in V) \to ((X \underset{˙}{+} X) \underset{˙}{+} Y) \underset{˙}{+} Y = ((X \underset{˙}{+} Y) \underset{˙}{+} X) \underset{˙}{+} Y$
45		lmodgrp	$⊢ W \in LMod \to W \in Grp$
46	3 45	syl	$⊢ (W \in LMod \land X \in V \land Y \in V) \to W \in Grp$
47	1 2	lmodvacl	$⊢ (W \in LMod \land X \underset{˙}{+} X \in V \land Y \in V) \to (X \underset{˙}{+} X) \underset{˙}{+} Y \in V$
48	3 39 13 47	syl3anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (X \underset{˙}{+} X) \underset{˙}{+} Y \in V$
49	1 2	lmodvacl	$⊢ (W \in LMod \land X \underset{˙}{+} Y \in V \land X \in V) \to (X \underset{˙}{+} Y) \underset{˙}{+} X \in V$
50	3 17 12 49	syl3anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (X \underset{˙}{+} Y) \underset{˙}{+} X \in V$
51	1 2	grprcan	$⊢ (W \in Grp \land ((X \underset{˙}{+} X) \underset{˙}{+} Y \in V \land (X \underset{˙}{+} Y) \underset{˙}{+} X \in V \land Y \in V)) \to (((X \underset{˙}{+} X) \underset{˙}{+} Y) \underset{˙}{+} Y = ((X \underset{˙}{+} Y) \underset{˙}{+} X) \underset{˙}{+} Y \leftrightarrow (X \underset{˙}{+} X) \underset{˙}{+} Y = (X \underset{˙}{+} Y) \underset{˙}{+} X)$
52	46 48 50 13 51	syl13anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (((X \underset{˙}{+} X) \underset{˙}{+} Y) \underset{˙}{+} Y = ((X \underset{˙}{+} Y) \underset{˙}{+} X) \underset{˙}{+} Y \leftrightarrow (X \underset{˙}{+} X) \underset{˙}{+} Y = (X \underset{˙}{+} Y) \underset{˙}{+} X)$
53	44 52	mpbid	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (X \underset{˙}{+} X) \underset{˙}{+} Y = (X \underset{˙}{+} Y) \underset{˙}{+} X$
54	1 2	lmodass	$⊢ (W \in LMod \land (X \in V \land X \in V \land Y \in V)) \to (X \underset{˙}{+} X) \underset{˙}{+} Y = X \underset{˙}{+} (X \underset{˙}{+} Y)$
55	3 12 12 13 54	syl13anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (X \underset{˙}{+} X) \underset{˙}{+} Y = X \underset{˙}{+} (X \underset{˙}{+} Y)$
56	1 2	lmodass	$⊢ (W \in LMod \land (X \in V \land Y \in V \land X \in V)) \to (X \underset{˙}{+} Y) \underset{˙}{+} X = X \underset{˙}{+} (Y \underset{˙}{+} X)$
57	3 12 13 12 56	syl13anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (X \underset{˙}{+} Y) \underset{˙}{+} X = X \underset{˙}{+} (Y \underset{˙}{+} X)$
58	53 55 57	3eqtr3d	$⊢ (W \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{+} (X \underset{˙}{+} Y) = X \underset{˙}{+} (Y \underset{˙}{+} X)$
59	1 2	lmodvacl	$⊢ (W \in LMod \land Y \in V \land X \in V) \to Y \underset{˙}{+} X \in V$
60	59	3com23	$⊢ (W \in LMod \land X \in V \land Y \in V) \to Y \underset{˙}{+} X \in V$
61	1 2	lmodlcan	$⊢ (W \in LMod \land (X \underset{˙}{+} Y \in V \land Y \underset{˙}{+} X \in V \land X \in V)) \to (X \underset{˙}{+} (X \underset{˙}{+} Y) = X \underset{˙}{+} (Y \underset{˙}{+} X) \leftrightarrow X \underset{˙}{+} Y = Y \underset{˙}{+} X)$
62	3 17 60 12 61	syl13anc	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (X \underset{˙}{+} (X \underset{˙}{+} Y) = X \underset{˙}{+} (Y \underset{˙}{+} X) \leftrightarrow X \underset{˙}{+} Y = Y \underset{˙}{+} X)$
63	58 62	mpbid	$⊢ (W \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$

Metamath Proof Explorer

Theorem lmodcom

Proof