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 
|- V = ( Base ` W )
lmodcom.a 
|- .+ = ( +g ` W )
Assertion lmodcom 
|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( X .+ Y ) = ( Y .+ X ) )

Proof

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