lmodfgrp - Metamath Proof Explorer

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

Theorem lmodfgrp 20047

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2108 ‘cfv 6418 Scalarcsca 16891 Grpcgrp 18492 Ringcrg 19698 LModclmod 20038

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-nul 5225

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-sbc 3712 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-iota 6376 df-fv 6426 df-ov 7258 df-ring 19700 df-lmod 20040

This theorem is referenced by: lmodacl 20049 lmodsn0 20051 lmodvneg1 20081 lssvsubcl 20120 lspsnneg 20183 lvecvscan2 20289 lspexch 20306 lspsolvlem 20319 ipsubdir 20759 ipsubdi 20760 ip2eq 20770 ocvlss 20789 lsmcss 20809 islindf4 20955 ascl0 20998 clmfgrp 24140 lmodvslmhm 31212 lflmul 37009 lkrlss 37036 eqlkr 37040 lkrlsp 37043 lshpkrlem1 37051 ldualvsubval 37098 lcfrlem1 39483 lcdvsubval 39559 lmodvsmdi 45606 lincsum 45658 lincsumcl 45660 lincext1 45683 lindslinindsimp1 45686 lindslinindimp2lem1 45687 lindslinindsimp2lem5 45691 ldepsprlem 45701 ldepspr 45702 lincresunit3lem3 45703 lincresunit3lem1 45708 lincresunit3lem2 45709 lincresunit3 45710

W3C validator