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

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

Proof of Theorem lmodfgrp
StepHypRef Expression
1 lmodrng.1 . . 3  |-  F  =  (Scalar `  W )
21lmodrng 15958 . 2  |-  ( W  e.  LMod  ->  F  e. 
Ring )
3 rnggrp 15669 . 2  |-  ( F  e.  Ring  ->  F  e. 
Grp )
42, 3syl 16 1  |-  ( W  e.  LMod  ->  F  e. 
Grp )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725   ` cfv 5454  Scalarcsca 13532   Grpcgrp 14685   Ringcrg 15660   LModclmod 15950
This theorem is referenced by:  lmodacl  15961  lmodsn0  15963  lmodvneg1  15987  lssvsubcl  16020  lspsnneg  16082  lvecvscan2  16184  lspexch  16201  lspsolvlem  16214  ipsubdir  16873  ipsubdi  16874  ip2eq  16884  ocvlss  16899  lsmcss  16919  clmfgrp  19096  islindf4  27285  lflmul  29866  lkrlss  29893  eqlkr  29897  lkrlsp  29900  lshpkrlem1  29908  ldualvsubval  29955  lcfrlem1  32340  lcdvsubval  32416
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-nul 4338
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-sbc 3162  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-iota 5418  df-fv 5462  df-ov 6084  df-rng 15663  df-lmod 15952
  Copyright terms: Public domain W3C validator