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

Theorem lmodfgrp 16883
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 16882 . 2  |-  ( W  e.  LMod  ->  F  e. 
Ring )
3 rnggrp 16588 . 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 1364    e. wcel 1757   ` cfv 5408  Scalarcsca 14226   Grpcgrp 15395   Ringcrg 16579   LModclmod 16874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-nul 4411
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2966  df-sbc 3178  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-nul 3628  df-if 3782  df-sn 3868  df-pr 3870  df-op 3874  df-uni 4082  df-br 4283  df-iota 5371  df-fv 5416  df-ov 6085  df-rng 16582  df-lmod 16876
This theorem is referenced by:  lmodacl  16885  lmodsn0  16887  lmodvneg1  16914  lssvsubcl  16949  lspsnneg  17011  lvecvscan2  17117  lspexch  17134  lspsolvlem  17147  ipsubdir  17915  ipsubdi  17916  ip2eq  17926  ocvlss  17941  lsmcss  17961  islindf4  18111  clmfgrp  20487  ascl0  30630  lincsum  30712  lincsumcl  30714  lincext1  30737  lindslinindsimp1  30740  lindslinindimp2lem1  30741  lindslinindsimp2lem5  30745  ldepsprlem  30755  ldepspr  30756  lincresunit3lem3  30757  lincresunit3lem1  30762  lincresunit3lem2  30763  lincresunit3  30764  lflmul  32326  lkrlss  32353  eqlkr  32357  lkrlsp  32360  lshpkrlem1  32368  ldualvsubval  32415  lcfrlem1  34800  lcdvsubval  34876
  Copyright terms: Public domain W3C validator