Theorem lmodfgrp 21174

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  ‘cfv 6558  Scalarcsca 17460  Grpcgrp 19173  Ringcrg 20489  LModclmod 21165

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446  df-ring 20491  df-lmod 21167

This theorem is used by:  lmodacl  21177  lmodsn0  21179  lmodvneg1  21210  lssvsubcl  21249  lspsnneg  21311  lvecvscan2  21420  lspexch  21437  lspsolvlem  21450  ipsubdir  21978  ipsubdi  21979  ip2eq  21989  ocvlss  22008  lsmcss  22028  islindf4  22174  ascl0  22222  clmfgrp  25422  lmodvslmhm  33681  lflmul  40317  lkrlss  40344  eqlkr  40348  lkrlsp  40351  lshpkrlem1  40359  ldualvsubval  40406  lcfrlem1  42791  lcdvsubval  42867  lmodvsmdi  49696  lincsum  49746  lincsumcl  49748  lincext1  49771  lindslinindsimp1  49774  lindslinindimp2lem1  49775  lindslinindsimp2lem5  49779  ldepsprlem  49789  ldepspr  49790  lincresunit3lem3  49791  lincresunit3lem1  49796  lincresunit3lem2  49797  lincresunit3  49798