Theorem lmodfgrp 20916

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 20915	. 2 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)
3		ringgrp 20267	. 2 ⊢ (𝐹 ∈ Ring → 𝐹 ∈ Grp)
4	2, 3	syl 17	1 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp)

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  ‘cfv 6517  Scalarcsca 17272  Grpcgrp 18958  Ringcrg 20262  LModclmod 20907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5255

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rab 3414  df-v 3455  df-sbc 3745  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395  df-ring 20264  df-lmod 20909

This theorem is referenced by:  lmodacl  20919  lmodsn0  20921  lmodvneg1  20952  lssvsubcl  20991  lspsnneg  21053  lvecvscan2  21162  lspexch  21179  lspsolvlem  21192  ipsubdir  21674  ipsubdi  21675  ip2eq  21685  ocvlss  21704  lsmcss  21724  islindf4  21870  ascl0  21916  clmfgrp  25113  lmodvslmhm  33191  lflmul  39656  lkrlss  39683  eqlkr  39687  lkrlsp  39690  lshpkrlem1  39698  ldualvsubval  39745  lcfrlem1  42130  lcdvsubval  42206  lmodvsmdi  48965  lincsum  49015  lincsumcl  49017  lincext1  49040  lindslinindsimp1  49043  lindslinindimp2lem1  49044  lindslinindsimp2lem5  49048  ldepsprlem  49058  ldepspr  49059  lincresunit3lem3  49060  lincresunit3lem1  49065  lincresunit3lem2  49066  lincresunit3  49067