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

Theorem lmodfgrp 17719
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 17718 . 2  |-  ( W  e.  LMod  ->  F  e. 
Ring )
3 ringgrp 17401 . 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 1398    e. wcel 1823   ` cfv 5570  Scalarcsca 14790   Grpcgrp 16255   Ringcrg 17396   LModclmod 17710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273  df-ring 17398  df-lmod 17712
This theorem is referenced by:  lmodacl  17721  lmodsn0  17723  lmodvneg1  17751  lssvsubcl  17788  lspsnneg  17850  lvecvscan2  17956  lspexch  17973  lspsolvlem  17986  ipsubdir  18853  ipsubdi  18854  ip2eq  18864  ocvlss  18879  lsmcss  18899  islindf4  19043  clmfgrp  21740  lmodvsmdi  33248  ascl0  33250  lincsum  33303  lincsumcl  33305  lincext1  33328  lindslinindsimp1  33331  lindslinindimp2lem1  33332  lindslinindsimp2lem5  33336  ldepsprlem  33346  ldepspr  33347  lincresunit3lem3  33348  lincresunit3lem1  33353  lincresunit3lem2  33354  lincresunit3  33355  lflmul  35209  lkrlss  35236  eqlkr  35240  lkrlsp  35243  lshpkrlem1  35251  ldualvsubval  35298  lcfrlem1  37685  lcdvsubval  37761
  Copyright terms: Public domain W3C validator