![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lmodgrp | Structured version Visualization version GIF version |
Description: A left module is a group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.) |
Ref | Expression |
---|---|
lmodgrp | ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2651 | . . 3 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
2 | eqid 2651 | . . 3 ⊢ (+g‘𝑊) = (+g‘𝑊) | |
3 | eqid 2651 | . . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊) | |
4 | eqid 2651 | . . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊) | |
5 | eqid 2651 | . . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | |
6 | eqid 2651 | . . 3 ⊢ (+g‘(Scalar‘𝑊)) = (+g‘(Scalar‘𝑊)) | |
7 | eqid 2651 | . . 3 ⊢ (.r‘(Scalar‘𝑊)) = (.r‘(Scalar‘𝑊)) | |
8 | eqid 2651 | . . 3 ⊢ (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊)) | |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | islmod 18915 | . 2 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ (Scalar‘𝑊) ∈ Ring ∧ ∀𝑞 ∈ (Base‘(Scalar‘𝑊))∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠 ‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠 ‘𝑊)𝑤) = ((𝑞( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠 ‘𝑊)𝑤) = (𝑞( ·𝑠 ‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤)) ∧ ((1r‘(Scalar‘𝑊))( ·𝑠 ‘𝑊)𝑤) = 𝑤)))) |
10 | 9 | simp1bi 1096 | 1 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1054 = wceq 1523 ∈ wcel 2030 ∀wral 2941 ‘cfv 5926 (class class class)co 6690 Basecbs 15904 +gcplusg 15988 .rcmulr 15989 Scalarcsca 15991 ·𝑠 cvsca 15992 Grpcgrp 17469 1rcur 18547 Ringcrg 18593 LModclmod 18911 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-nul 4822 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-sbc 3469 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-br 4686 df-iota 5889 df-fv 5934 df-ov 6693 df-lmod 18913 |
This theorem is referenced by: lmodbn0 18921 lmodvacl 18925 lmodass 18926 lmodlcan 18927 lmod0vcl 18940 lmod0vlid 18941 lmod0vrid 18942 lmod0vid 18943 lmodvsmmulgdi 18946 lmodfopne 18949 lmodvnegcl 18952 lmodvnegid 18953 lmodvsubcl 18956 lmodcom 18957 lmodabl 18958 lmodvpncan 18964 lmodvnpcan 18965 lmodsubeq0 18970 lmodsubid 18971 lmodvsghm 18972 lmodprop2d 18973 lsssubg 19005 islss3 19007 lssacs 19015 prdslmodd 19017 lspsnneg 19054 lspsnsub 19055 lmodindp1 19062 lmodvsinv2 19085 islmhm2 19086 0lmhm 19088 idlmhm 19089 pwsdiaglmhm 19105 pwssplit3 19109 lspexch 19177 lspsolvlem 19190 mplind 19550 ip0l 20029 ipsubdir 20035 ipsubdi 20036 ip2eq 20046 lsmcss 20084 dsmmlss 20136 frlm0 20146 frlmsubgval 20156 frlmup1 20185 islindf4 20225 matgrp 20284 tlmtgp 22046 clmgrp 22914 ncvspi 23002 cphtchnm 23075 ipcau2 23079 tchcphlem1 23080 tchcph 23082 rrxnm 23225 rrxds 23227 pjthlem2 23255 lclkrlem2m 37125 mapdpglem14 37291 baerlem3lem1 37313 baerlem5amN 37322 baerlem5bmN 37323 baerlem5abmN 37324 mapdh6bN 37343 mapdh6cN 37344 hdmap1l6b 37418 hdmap1l6c 37419 hdmap1neglem1N 37434 hdmap11 37457 kercvrlsm 37970 pwssplit4 37976 pwslnmlem2 37980 mendring 38079 zlmodzxzsub 42463 lmodvsmdi 42488 lincvalsng 42530 lincvalsc0 42535 linc0scn0 42537 linc1 42539 lcoel0 42542 lindslinindimp2lem4 42575 snlindsntor 42585 lincresunit3 42595 |
Copyright terms: Public domain | W3C validator |