Theorem lmodfgrp 19045

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

Step	Hyp	Ref	Expression
1		lmodring.1	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
2	1	lmodring 19044	. 2 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)
3		ringgrp 18723	. 2 ⊢ (𝐹 ∈ Ring → 𝐹 ∈ Grp)
4	2, 3	syl 17	1 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp)

Syntax hints:   → wi 4   = wceq 1620   ∈ wcel 2127  ‘cfv 6037  Scalarcsca 16117  Grpcgrp 17594  Ringcrg 18718  LModclmod 19036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-nul 4929

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-iota 6000  df-fv 6045  df-ov 6804  df-ring 18720  df-lmod 19038

This theorem is referenced by:  lmodacl  19047  lmodsn0  19049  lmodvneg1  19079  lssvsubcl  19117  lspsnneg  19179  lvecvscan2  19285  lspexch  19302  lspsolvlem  19315  ipsubdir  20160  ipsubdi  20161  ip2eq  20171  ocvlss  20189  lsmcss  20209  islindf4  20350  clmfgrp  23042  lflmul  34827  lkrlss  34854  eqlkr  34858  lkrlsp  34861  lshpkrlem1  34869  ldualvsubval  34916  lcfrlem1  37302  lcdvsubval  37378  lmodvsmdi  42642  ascl0  42644  lincsum  42697  lincsumcl  42699  lincext1  42722  lindslinindsimp1  42725  lindslinindimp2lem1  42726  lindslinindsimp2lem5  42730  ldepsprlem  42740  ldepspr  42741  lincresunit3lem3  42742  lincresunit3lem1  42747  lincresunit3lem2  42748  lincresunit3  42749