Theorem lmodabl 20899

Description: A left module is an abelian group (of vectors, under addition). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.)

Assertion

Ref	Expression
lmodabl	⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel)

Proof of Theorem lmodabl

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqidd 2740	. 2 ⊢ (𝑊 ∈ LMod → (Base‘𝑊) = (Base‘𝑊))
2		eqidd 2740	. 2 ⊢ (𝑊 ∈ LMod → (+g‘𝑊) = (+g‘𝑊))
3		lmodgrp 20857	. 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
4		eqid 2739	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
5		eqid 2739	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
6	4, 5	lmodcom 20898	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑥(+g‘𝑊)𝑦) = (𝑦(+g‘𝑊)𝑥))
7	1, 2, 3, 6	isabld 19761	1 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel)

Syntax hints:   → wi 4   ∈ wcel 2119  ‘cfv 6485  Basecbs 17170  +_gcplusg 17211  Abelcabl 19747  LModclmod 20850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-2 12235  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-plusg 17224  df-0g 17395  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-grp 18903  df-minusg 18904  df-cmn 19748  df-abl 19749  df-mgp 20113  df-ur 20154  df-ring 20207  df-lmod 20852

This theorem is referenced by:  lmodcmn  20900  lmodnegadd  20901  lmodvsubadd  20903  lmodvaddsub4  20904  lssvancl1  20935  invlmhm  21032  lmhmplusg  21034  lsmcl  21073  lspprabs  21085  pj1lmhm  21090  pj1lmhm2  21091  lvecindp  21131  lvecindp2  21132  lsmcv  21134  zlmlmod  21497  pjdm2  21686  pjf2  21689  pjfo  21690  ocvpj  21692  frlmsslsp  21771  nlmtlm  24677  ngpocelbl  24687  nmhmplusg  24740  clmabl  25054  cvsi  25115  minveclem2  25411  pjthlem2  25423  ttgcontlem1  28971  quslmod  33441  quslmhm  33442  lindsunlem  33808  qusdimsum  33812  fedgmullem2  33814  bj-modssabl  37640  lcvexchlem3  39528  lcvexchlem4  39529  lcvexchlem5  39530  lsatcvatlem  39541  lsatcvat  39542  lsatcvat3  39544  l1cvat  39547  lshpsmreu  39601  lshpkrlem5  39606  dia2dimlem5  41560  dihjatc3  41805  dihmeetlem9N  41807  dihjatcclem1  41910  dihjat  41915  lclkrlem2b  42000  baerlem3lem1  42199  baerlem5alem1  42200  baerlem5blem1  42201  baerlem3lem2  42202  baerlem5alem2  42203  baerlem5blem2  42204  hdmaprnlem7N  42347  isnumbasgrplem3  43550  gsumlsscl  48871