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

Theorem lmodfgrp 17369
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
lmodring.1  |-  F  =  (Scalar `  W )
Assertion
Ref Expression
lmodfgrp  |-  ( W  e.  LMod  ->  F  e. 
Grp )

Proof of Theorem lmodfgrp
StepHypRef Expression
1 lmodring.1 . . 3  |-  F  =  (Scalar `  W )
21lmodring 17368 . 2  |-  ( W  e.  LMod  ->  F  e. 
Ring )
3 ringgrp 17052 . 2  |-  ( F  e.  Ring  ->  F  e. 
Grp )
42, 3syl 16 1  |-  ( W  e.  LMod  ->  F  e. 
Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767   ` cfv 5593  Scalarcsca 14570   Grpcgrp 15902   Ringcrg 17047   LModclmod 17360
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4581
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4251  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6297  df-ring 17049  df-lmod 17362
This theorem is referenced by:  lmodacl  17371  lmodsn0  17373  lmodvneg1  17401  lssvsubcl  17438  lspsnneg  17500  lvecvscan2  17606  lspexch  17623  lspsolvlem  17636  ipsubdir  18523  ipsubdi  18524  ip2eq  18534  ocvlss  18549  lsmcss  18569  islindf4  18719  clmfgrp  21416  lmodvsmdi  32349  ascl0  32351  lincsum  32404  lincsumcl  32406  lincext1  32429  lindslinindsimp1  32432  lindslinindimp2lem1  32433  lindslinindsimp2lem5  32437  ldepsprlem  32447  ldepspr  32448  lincresunit3lem3  32449  lincresunit3lem1  32454  lincresunit3lem2  32455  lincresunit3  32456  lflmul  34158  lkrlss  34185  eqlkr  34189  lkrlsp  34192  lshpkrlem1  34200  ldualvsubval  34247  lcfrlem1  36632  lcdvsubval  36708
  Copyright terms: Public domain W3C validator