Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lmodfgrp | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
lmodring.1 | ⊢ 𝐹 = (Scalar‘𝑊) |
Ref | Expression |
---|---|
lmodfgrp | ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmodring.1 | . . 3 ⊢ 𝐹 = (Scalar‘𝑊) | |
2 | 1 | lmodring 19571 | . 2 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring) |
3 | ringgrp 19231 | . 2 ⊢ (𝐹 ∈ Ring → 𝐹 ∈ Grp) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 ‘cfv 6348 Scalarcsca 16556 Grpcgrp 18041 Ringcrg 19226 LModclmod 19563 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-nul 5201 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-sbc 3770 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-iota 6307 df-fv 6356 df-ov 7148 df-ring 19228 df-lmod 19565 |
This theorem is referenced by: lmodacl 19574 lmodsn0 19576 lmodvneg1 19606 lssvsubcl 19644 lspsnneg 19707 lvecvscan2 19813 lspexch 19830 lspsolvlem 19843 ascl0 20041 ipsubdir 20714 ipsubdi 20715 ip2eq 20725 ocvlss 20744 lsmcss 20764 islindf4 20910 clmfgrp 23602 lmodvslmhm 30615 lflmul 36084 lkrlss 36111 eqlkr 36115 lkrlsp 36118 lshpkrlem1 36126 ldualvsubval 36173 lcfrlem1 38558 lcdvsubval 38634 lmodvsmdi 44358 lincsum 44412 lincsumcl 44414 lincext1 44437 lindslinindsimp1 44440 lindslinindimp2lem1 44441 lindslinindsimp2lem5 44445 ldepsprlem 44455 ldepspr 44456 lincresunit3lem3 44457 lincresunit3lem1 44462 lincresunit3lem2 44463 lincresunit3 44464 |
Copyright terms: Public domain | W3C validator |