![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > grpidcl | Structured version Visualization version GIF version |
Description: The identity element of a group belongs to the group. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
Ref | Expression |
---|---|
grpidcl.b | ⊢ 𝐵 = (Base‘𝐺) |
grpidcl.o | ⊢ 0 = (0g‘𝐺) |
Ref | Expression |
---|---|
grpidcl | ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grpmnd 18826 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpidcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grpidcl.o | . . 3 ⊢ 0 = (0g‘𝐺) | |
4 | 2, 3 | mndidcl 18640 | . 2 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
5 | 1, 4 | syl 17 | 1 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 ‘cfv 6544 Basecbs 17144 0gc0g 17385 Mndcmnd 18625 Grpcgrp 18819 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-iota 6496 df-fun 6546 df-fv 6552 df-riota 7365 df-ov 7412 df-0g 17387 df-mgm 18561 df-sgrp 18610 df-mnd 18626 df-grp 18822 |
This theorem is referenced by: grpbn0 18851 grprcan 18858 grpid 18860 isgrpid2 18861 grprinv 18875 grpidinv 18883 grpinvid 18884 grpidrcan 18888 grpidlcan 18889 grpidssd 18899 grpinvval2 18906 grpsubid1 18908 imasgrp 18939 mulgcl 18971 mulgz 18982 subg0 19012 subg0cl 19014 issubg4 19025 0subgOLD 19032 nmzsubg 19045 eqgid 19060 qusgrp 19065 qus0 19068 ghmid 19098 ghmpreima 19114 ghmf1 19121 gafo 19160 gaid 19163 gass 19165 gaorber 19172 gastacl 19173 lactghmga 19273 cayleylem2 19281 symgsssg 19335 symgfisg 19336 od1 19427 gexdvds 19452 sylow1lem2 19467 sylow3lem1 19495 lsmdisj2 19550 0frgp 19647 odadd1 19716 torsubg 19722 oddvdssubg 19723 0cyg 19761 prmcyg 19762 telgsums 19861 dprdfadd 19890 dprdz 19900 pgpfac1lem3a 19946 ablsimpgprmd 19985 ring0cl 20084 ringlz 20107 ringrz 20108 f1ghm0to0 20279 kerf1ghm 20282 isdrng2 20371 srng0 20468 lmod0vcl 20501 islmhm2 20649 isdomn4 20918 frgpcyg 21129 ip0l 21189 ocvlss 21225 ascl0 21438 psr0cl 21513 mplsubglem 21558 mhp0cl 21689 mhpaddcl 21694 evl1gsumd 21876 grpvlinv 21897 matinvgcell 21937 mat0dim0 21969 mdetdiag 22101 mdetuni0 22123 chpdmatlem2 22341 chp0mat 22348 istgp2 23595 cldsubg 23615 tgpconncompeqg 23616 tgpconncomp 23617 snclseqg 23620 tgphaus 23621 tgpt1 23622 qustgphaus 23627 tgptsmscls 23654 nrmmetd 24083 nmfval2 24100 nmval2 24101 nmf2 24102 ngpds3 24117 nmge0 24126 nmeq0 24127 nminv 24130 nmmtri 24131 nmrtri 24133 nm0 24138 tngnm 24168 idnghm 24260 nmcn 24360 clmvz 24627 nmoleub2lem2 24632 nglmle 24819 mdeg0 25588 dchrinv 26764 dchr1re 26766 dchrpt 26770 dchrsum2 26771 dchrhash 26774 rpvmasumlem 26990 rpvmasum2 27015 dchrisum0re 27016 ogrpinv0lt 32240 ogrpinvlt 32241 isarchi3 32333 archirng 32334 archirngz 32335 archiabllem1b 32338 rmfsupp2 32387 orngsqr 32422 ornglmulle 32423 orngrmulle 32424 ornglmullt 32425 orngrmullt 32426 orngmullt 32427 ofldchr 32432 isarchiofld 32435 qusker 32464 eqg0el 32473 grplsm0l 32513 qus0g 32518 nsgqus0 32521 nsgmgclem 32522 ghmqusker 32532 fedgmullem1 32714 qqh0 32964 sconnpi1 34230 lfl0f 37939 lkrlss 37965 lshpkrlem1 37980 lkrin 38034 dvhgrp 39978 fsuppind 41162 fsuppssind 41165 mhpind 41166 rng0cl 46662 rnglz 46664 rngrz 46665 zrrnghm 46716 rnglidl0 46752 evl1at0 47072 |
Copyright terms: Public domain | W3C validator |