This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmodcom

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

Ref Expression
Hypotheses lmodcom.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lmodcom.a ⊢ + = ( +g ‘ 𝑊 )
Assertion lmodcom ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )

Proof

Step Hyp Ref Expression
1 lmodcom.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lmodcom.a ⊢ + = ( +g ‘ 𝑊 )
3 simp1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 𝑊 ∈ LMod )
4 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
5 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
6 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
7 4 5 6 lmod1cl ⊢ ( 𝑊 ∈ LMod → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
8 3 7 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
9 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
10 4 5 9 lmodacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
11 3 8 8 10 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
12 simp2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
13 simp3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ∈ 𝑉 )
14 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
15 1 2 4 14 5 lmodvsdi ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) + ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) )
16 3 11 12 13 15 syl13anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) + ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) )
17 1 2 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
18 1 2 4 14 5 9 lmodvsdir ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 + 𝑌 ) ∈ 𝑉 ) ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) = ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) + ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ) )
19 3 8 8 17 18 syl13anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) = ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) + ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ) )
20 16 19 eqtr3d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) + ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) = ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) + ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ) )
21 1 2 4 14 5 9 lmodvsdir ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) + ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) )
22 3 8 8 12 21 syl13anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) + ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) )
23 1 4 14 6 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = 𝑋 )
24 3 12 23 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = 𝑋 )
25 24 24 oveq12d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) + ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) = ( 𝑋 + 𝑋 ) )
26 22 25 eqtrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = ( 𝑋 + 𝑋 ) )
27 1 2 4 14 5 9 lmodvsdir ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) )
28 3 8 8 13 27 syl13anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) )
29 1 4 14 6 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = 𝑌 )
30 3 13 29 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = 𝑌 )
31 30 30 oveq12d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) = ( 𝑌 + 𝑌 ) )
32 28 31 eqtrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = ( 𝑌 + 𝑌 ) )
33 26 32 oveq12d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) + ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) = ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) )
34 1 4 14 6 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑋 + 𝑌 ) ∈ 𝑉 ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) = ( 𝑋 + 𝑌 ) )
35 3 17 34 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) = ( 𝑋 + 𝑌 ) )
36 35 35 oveq12d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) + ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )
37 20 33 36 3eqtr3d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )
38 1 2 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 + 𝑋 ) ∈ 𝑉 )
39 3 12 12 38 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 + 𝑋 ) ∈ 𝑉 )
40 1 2 lmodass ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑋 + 𝑋 ) ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) )
41 3 39 13 13 40 syl13anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) )
42 1 2 lmodass ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑋 + 𝑌 ) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝑋 + 𝑌 ) + 𝑋 ) + 𝑌 ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )
43 3 17 12 13 42 syl13anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( 𝑋 + 𝑌 ) + 𝑋 ) + 𝑌 ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )
44 37 41 43 3eqtr4d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( ( 𝑋 + 𝑌 ) + 𝑋 ) + 𝑌 ) )
45 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
46 3 45 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 𝑊 ∈ Grp )
47 1 2 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑋 + 𝑋 ) ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) ∈ 𝑉 )
48 3 39 13 47 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) ∈ 𝑉 )
49 1 2 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑋 + 𝑌 ) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑋 + 𝑌 ) + 𝑋 ) ∈ 𝑉 )
50 3 17 12 49 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 + 𝑌 ) + 𝑋 ) ∈ 𝑉 )
51 1 2 grprcan ⊢ ( ( 𝑊 ∈ Grp ∧ ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) ∈ 𝑉 ∧ ( ( 𝑋 + 𝑌 ) + 𝑋 ) ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( ( 𝑋 + 𝑌 ) + 𝑋 ) + 𝑌 ) ↔ ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( ( 𝑋 + 𝑌 ) + 𝑋 ) ) )
52 46 48 50 13 51 syl13anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( ( 𝑋 + 𝑌 ) + 𝑋 ) + 𝑌 ) ↔ ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( ( 𝑋 + 𝑌 ) + 𝑋 ) ) )
53 44 52 mpbid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( ( 𝑋 + 𝑌 ) + 𝑋 ) )
54 1 2 lmodass ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( 𝑋 + ( 𝑋 + 𝑌 ) ) )
55 3 12 12 13 54 syl13anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( 𝑋 + ( 𝑋 + 𝑌 ) ) )
56 1 2 lmodass ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑋 + 𝑌 ) + 𝑋 ) = ( 𝑋 + ( 𝑌 + 𝑋 ) ) )
57 3 12 13 12 56 syl13anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 + 𝑌 ) + 𝑋 ) = ( 𝑋 + ( 𝑌 + 𝑋 ) ) )
58 53 55 57 3eqtr3d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 + ( 𝑋 + 𝑌 ) ) = ( 𝑋 + ( 𝑌 + 𝑋 ) ) )
59 1 2 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑌 + 𝑋 ) ∈ 𝑉 )
60 59 3com23 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑌 + 𝑋 ) ∈ 𝑉 )
61 1 2 lmodlcan ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑋 + 𝑌 ) ∈ 𝑉 ∧ ( 𝑌 + 𝑋 ) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑋 + ( 𝑋 + 𝑌 ) ) = ( 𝑋 + ( 𝑌 + 𝑋 ) ) ↔ ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) )
62 3 17 60 12 61 syl13anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 + ( 𝑋 + 𝑌 ) ) = ( 𝑋 + ( 𝑌 + 𝑋 ) ) ↔ ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) )
63 58 62 mpbid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )