Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmodcom Unicode version

Theorem lmodcom 15931
 Description: Left module vector sum is commutative. (Contributed by Gérard Lang, 25-Jun-2014.)
Hypotheses
Ref Expression
lmodcom.v
lmodcom.a
Assertion
Ref Expression
lmodcom

Proof of Theorem lmodcom
StepHypRef Expression
1 simp1 957 . . . . . . . 8
2 eqid 2401 . . . . . . . . . . 11 Scalar Scalar
3 eqid 2401 . . . . . . . . . . 11 Scalar Scalar
4 eqid 2401 . . . . . . . . . . 11 Scalar Scalar
52, 3, 4lmod1cl 15918 . . . . . . . . . 10 Scalar Scalar
61, 5syl 16 . . . . . . . . 9 Scalar Scalar
7 eqid 2401 . . . . . . . . . 10 Scalar Scalar
82, 3, 7lmodacl 15902 . . . . . . . . 9 Scalar Scalar Scalar Scalar Scalar ScalarScalar Scalar
91, 6, 6, 8syl3anc 1184 . . . . . . . 8 Scalar ScalarScalar Scalar
10 simp2 958 . . . . . . . 8
11 simp3 959 . . . . . . . 8
12 lmodcom.v . . . . . . . . 9
13 lmodcom.a . . . . . . . . 9
14 eqid 2401 . . . . . . . . 9
1512, 13, 2, 14, 3lmodvsdi 15914 . . . . . . . 8 Scalar ScalarScalar Scalar Scalar ScalarScalar Scalar ScalarScalar Scalar ScalarScalar
161, 9, 10, 11, 15syl13anc 1186 . . . . . . 7 Scalar ScalarScalar Scalar ScalarScalar Scalar ScalarScalar
1712, 13lmodvacl 15905 . . . . . . . 8
1812, 13, 2, 14, 3, 7lmodvsdir 15915 . . . . . . . 8 Scalar Scalar Scalar Scalar Scalar ScalarScalar Scalar Scalar
191, 6, 6, 17, 18syl13anc 1186 . . . . . . 7 Scalar ScalarScalar Scalar Scalar
2016, 19eqtr3d 2435 . . . . . 6 Scalar ScalarScalar Scalar ScalarScalar Scalar Scalar
2112, 13, 2, 14, 3, 7lmodvsdir 15915 . . . . . . . . 9 Scalar Scalar Scalar Scalar Scalar ScalarScalar Scalar Scalar
221, 6, 6, 10, 21syl13anc 1186 . . . . . . . 8 Scalar ScalarScalar Scalar Scalar
2312, 2, 14, 4lmodvs1 15919 . . . . . . . . . 10 Scalar
241, 10, 23syl2anc 643 . . . . . . . . 9 Scalar
2524, 24oveq12d 6052 . . . . . . . 8 Scalar Scalar
2622, 25eqtrd 2433 . . . . . . 7 Scalar ScalarScalar
2712, 13, 2, 14, 3, 7lmodvsdir 15915 . . . . . . . . 9 Scalar Scalar Scalar Scalar Scalar ScalarScalar Scalar Scalar
281, 6, 6, 11, 27syl13anc 1186 . . . . . . . 8 Scalar ScalarScalar Scalar Scalar
2912, 2, 14, 4lmodvs1 15919 . . . . . . . . . 10 Scalar
301, 11, 29syl2anc 643 . . . . . . . . 9 Scalar
3130, 30oveq12d 6052 . . . . . . . 8 Scalar Scalar
3228, 31eqtrd 2433 . . . . . . 7 Scalar ScalarScalar
3326, 32oveq12d 6052 . . . . . 6 Scalar ScalarScalar Scalar ScalarScalar
3412, 2, 14, 4lmodvs1 15919 . . . . . . . 8 Scalar
351, 17, 34syl2anc 643 . . . . . . 7 Scalar
3635, 35oveq12d 6052 . . . . . 6 Scalar Scalar
3720, 33, 363eqtr3d 2441 . . . . 5
3812, 13lmodvacl 15905 . . . . . . 7
391, 10, 10, 38syl3anc 1184 . . . . . 6
4012, 13lmodass 15906 . . . . . 6
411, 39, 11, 11, 40syl13anc 1186 . . . . 5
4212, 13lmodass 15906 . . . . . 6
431, 17, 10, 11, 42syl13anc 1186 . . . . 5
4437, 41, 433eqtr4d 2443 . . . 4
45 lmodgrp 15898 . . . . . 6
461, 45syl 16 . . . . 5
4712, 13lmodvacl 15905 . . . . . 6
481, 39, 11, 47syl3anc 1184 . . . . 5
4912, 13lmodvacl 15905 . . . . . 6
501, 17, 10, 49syl3anc 1184 . . . . 5
5112, 13grprcan 14779 . . . . 5
5246, 48, 50, 11, 51syl13anc 1186 . . . 4
5344, 52mpbid 202 . . 3
5412, 13lmodass 15906 . . . 4
551, 10, 10, 11, 54syl13anc 1186 . . 3
5612, 13lmodass 15906 . . . 4
571, 10, 11, 10, 56syl13anc 1186 . . 3
5853, 55, 573eqtr3d 2441 . 2
5912, 13lmodvacl 15905 . . . 4
60593com23 1159 . . 3
6112, 13lmodlcan 15907 . . 3
621, 17, 60, 10, 61syl13anc 1186 . 2
6358, 62mpbid 202 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   w3a 936   wceq 1649   wcel 1721  cfv 5408  (class class class)co 6034  cbs 13410   cplusg 13470  Scalarcsca 13473  cvsca 13474  cgrp 14626  cur 15603  clmod 15891 This theorem is referenced by:  lmodabl  15932  lssvsubcl  15961  lssvancl2  15963  lspsolv  16156  lflsub  29490  lcfrlem21  31986  lcfrlem42  32007  mapdindp4  32146 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655  ax-cnex 8993  ax-resscn 8994  ax-1cn 8995  ax-icn 8996  ax-addcl 8997  ax-addrcl 8998  ax-mulcl 8999  ax-mulrcl 9000  ax-mulcom 9001  ax-addass 9002  ax-mulass 9003  ax-distr 9004  ax-i2m1 9005  ax-1ne0 9006  ax-1rid 9007  ax-rnegex 9008  ax-rrecex 9009  ax-cnre 9010  ax-pre-lttri 9011  ax-pre-lttrn 9012  ax-pre-ltadd 9013  ax-pre-mulgt0 9014 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-nel 2567  df-ral 2668  df-rex 2669  df-reu 2670  df-rmo 2671  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-iun 4051  df-br 4168  df-opab 4222  df-mpt 4223  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-ov 6037  df-oprab 6038  df-mpt2 6039  df-riota 6499  df-recs 6583  df-rdg 6618  df-er 6855  df-en 7060  df-dom 7061  df-sdom 7062  df-pnf 9069  df-mnf 9070  df-xr 9071  df-ltxr 9072  df-le 9073  df-sub 9239  df-neg 9240  df-nn 9947  df-2 10004  df-ndx 13413  df-slot 13414  df-base 13415  df-sets 13416  df-plusg 13483  df-0g 13668  df-mnd 14631  df-grp 14753  df-minusg 14754  df-mgp 15590  df-rng 15604  df-ur 15606  df-lmod 15893
 Copyright terms: Public domain W3C validator