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

Theorem lmodfgrp 20331
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 𝐹 = (Scalarβ€˜π‘Š)
Assertion
Ref Expression
lmodfgrp (π‘Š ∈ LMod β†’ 𝐹 ∈ Grp)

Proof of Theorem lmodfgrp
StepHypRef Expression
1 lmodring.1 . . 3 𝐹 = (Scalarβ€˜π‘Š)
21lmodring 20330 . 2 (π‘Š ∈ LMod β†’ 𝐹 ∈ Ring)
3 ringgrp 19969 . 2 (𝐹 ∈ Ring β†’ 𝐹 ∈ Grp)
42, 3syl 17 1 (π‘Š ∈ LMod β†’ 𝐹 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   = wceq 1541   ∈ wcel 2106  β€˜cfv 6496  Scalarcsca 17136  Grpcgrp 18748  Ringcrg 19964  LModclmod 20322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-nul 5263
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-iota 6448  df-fv 6504  df-ov 7360  df-ring 19966  df-lmod 20324
This theorem is referenced by:  lmodacl  20333  lmodsn0  20335  lmodvneg1  20365  lssvsubcl  20404  lspsnneg  20467  lvecvscan2  20573  lspexch  20590  lspsolvlem  20603  ipsubdir  21046  ipsubdi  21047  ip2eq  21057  ocvlss  21076  lsmcss  21096  islindf4  21244  ascl0  21287  clmfgrp  24434  lmodvslmhm  31892  lflmul  37530  lkrlss  37557  eqlkr  37561  lkrlsp  37564  lshpkrlem1  37572  ldualvsubval  37619  lcfrlem1  40005  lcdvsubval  40081  lmodvsmdi  46448  lincsum  46500  lincsumcl  46502  lincext1  46525  lindslinindsimp1  46528  lindslinindimp2lem1  46529  lindslinindsimp2lem5  46533  ldepsprlem  46543  ldepspr  46544  lincresunit3lem3  46545  lincresunit3lem1  46550  lincresunit3lem2  46551  lincresunit3  46552
  Copyright terms: Public domain W3C validator