Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lmodabl | Structured version Visualization version GIF version |
Description: A left module is an abelian group (of vectors, under addition). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.) |
Ref | Expression |
---|---|
lmodabl | ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqidd 2740 | . 2 ⊢ (𝑊 ∈ LMod → (Base‘𝑊) = (Base‘𝑊)) | |
2 | eqidd 2740 | . 2 ⊢ (𝑊 ∈ LMod → (+g‘𝑊) = (+g‘𝑊)) | |
3 | lmodgrp 19763 | . 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) | |
4 | eqid 2739 | . . 3 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
5 | eqid 2739 | . . 3 ⊢ (+g‘𝑊) = (+g‘𝑊) | |
6 | 4, 5 | lmodcom 19802 | . 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑥(+g‘𝑊)𝑦) = (𝑦(+g‘𝑊)𝑥)) |
7 | 1, 2, 3, 6 | isabld 19041 | 1 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2114 ‘cfv 6340 Basecbs 16589 +gcplusg 16671 Abelcabl 19028 LModclmod 19756 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2711 ax-sep 5168 ax-nul 5175 ax-pow 5233 ax-pr 5297 ax-un 7482 ax-cnex 10674 ax-resscn 10675 ax-1cn 10676 ax-icn 10677 ax-addcl 10678 ax-addrcl 10679 ax-mulcl 10680 ax-mulrcl 10681 ax-mulcom 10682 ax-addass 10683 ax-mulass 10684 ax-distr 10685 ax-i2m1 10686 ax-1ne0 10687 ax-1rid 10688 ax-rnegex 10689 ax-rrecex 10690 ax-cnre 10691 ax-pre-lttri 10692 ax-pre-lttrn 10693 ax-pre-ltadd 10694 ax-pre-mulgt0 10695 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2541 df-eu 2571 df-clab 2718 df-cleq 2731 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rmo 3062 df-rab 3063 df-v 3401 df-sbc 3682 df-csb 3792 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-pss 3863 df-nul 4213 df-if 4416 df-pw 4491 df-sn 4518 df-pr 4520 df-tp 4522 df-op 4524 df-uni 4798 df-iun 4884 df-br 5032 df-opab 5094 df-mpt 5112 df-tr 5138 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5484 df-we 5486 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-rn 5537 df-res 5538 df-ima 5539 df-pred 6130 df-ord 6176 df-on 6177 df-lim 6178 df-suc 6179 df-iota 6298 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-riota 7130 df-ov 7176 df-oprab 7177 df-mpo 7178 df-om 7603 df-wrecs 7979 df-recs 8040 df-rdg 8078 df-er 8323 df-en 8559 df-dom 8560 df-sdom 8561 df-pnf 10758 df-mnf 10759 df-xr 10760 df-ltxr 10761 df-le 10762 df-sub 10953 df-neg 10954 df-nn 11720 df-2 11782 df-ndx 16592 df-slot 16593 df-base 16595 df-sets 16596 df-plusg 16684 df-0g 16821 df-mgm 17971 df-sgrp 18020 df-mnd 18031 df-grp 18225 df-minusg 18226 df-cmn 19029 df-abl 19030 df-mgp 19362 df-ur 19374 df-ring 19421 df-lmod 19758 |
This theorem is referenced by: lmodcmn 19804 lmodnegadd 19805 lmodvsubadd 19807 lmodvaddsub4 19808 lssvancl1 19838 invlmhm 19936 lmhmplusg 19938 lsmcl 19977 lspprabs 19989 pj1lmhm 19994 pj1lmhm2 19995 lvecindp 20032 lvecindp2 20033 lsmcv 20035 zlmlmod 20346 pjdm2 20530 pjf2 20533 pjfo 20534 ocvpj 20536 frlmsslsp 20615 nlmtlm 23450 ngpocelbl 23460 nmhmplusg 23513 clmabl 23824 cvsi 23885 minveclem2 24181 pjthlem2 24193 ttgcontlem1 26834 quslmod 31129 quslmhm 31130 lindsunlem 31280 qusdimsum 31284 fedgmullem2 31286 bj-modssabl 35095 lcvexchlem3 36696 lcvexchlem4 36697 lcvexchlem5 36698 lsatcvatlem 36709 lsatcvat 36710 lsatcvat3 36712 l1cvat 36715 lshpsmreu 36769 lshpkrlem5 36774 dia2dimlem5 38728 dihjatc3 38973 dihmeetlem9N 38975 dihjatcclem1 39078 dihjat 39083 lclkrlem2b 39168 baerlem3lem1 39367 baerlem5alem1 39368 baerlem5blem1 39369 baerlem3lem2 39370 baerlem5alem2 39371 baerlem5blem2 39372 hdmaprnlem7N 39515 isnumbasgrplem3 40525 gsumlsscl 45283 |
Copyright terms: Public domain | W3C validator |