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

Theorem lmodfgrp 17133
Description: The scalar component of a left module is an additive group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
Hypothesis
Ref Expression
lmodrng.1
Assertion
Ref Expression
lmodfgrp

Proof of Theorem lmodfgrp
StepHypRef Expression
1 lmodrng.1 . . 3
21lmodrng 17132 . 2
3 rnggrp 16826 . 2
42, 3syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1370  e.wcel 1758  `cfv 5537   csca 14400   cgrp 15569   crg 16821   clmod 17124
This theorem is referenced by:  lmodacl  17135  lmodsn0  17137  lmodvneg1  17164  lssvsubcl  17201  lspsnneg  17263  lvecvscan2  17369  lspexch  17386  lspsolvlem  17399  ipsubdir  18264  ipsubdi  18265  ip2eq  18275  ocvlss  18290  lsmcss  18310  islindf4  18460  clmfgrp  21042  lmodvsmdi  31671  ascl0  31674  lincsum  31735  lincsumcl  31737  lincext1  31760  lindslinindsimp1  31763  lindslinindimp2lem1  31764  lindslinindsimp2lem5  31768  ldepsprlem  31778  ldepspr  31779  lincresunit3lem3  31780  lincresunit3lem1  31785  lincresunit3lem2  31786  lincresunit3  31787  lflmul  33564  lkrlss  33591  eqlkr  33595  lkrlsp  33598  lshpkrlem1  33606  ldualvsubval  33653  lcfrlem1  36038  lcdvsubval  36114
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-nul 4538
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3083  df-sbc 3298  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4209  df-br 4410  df-iota 5500  df-fv 5545  df-ov 6225  df-rng 16823  df-lmod 17126
  Copyright terms: Public domain W3C validator