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 18048 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpidcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grpidcl.o | . . 3 ⊢ 0 = (0g‘𝐺) | |
4 | 2, 3 | mndidcl 17914 | . 2 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
5 | 1, 4 | syl 17 | 1 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 ‘cfv 6348 Basecbs 16471 0gc0g 16701 Mndcmnd 17899 Grpcgrp 18041 |
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-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 |
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-ne 3014 df-ral 3140 df-rex 3141 df-reu 3142 df-rmo 3143 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-opab 5120 df-mpt 5138 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-iota 6307 df-fun 6350 df-fv 6356 df-riota 7103 df-ov 7148 df-0g 16703 df-mgm 17840 df-sgrp 17889 df-mnd 17900 df-grp 18044 |
This theorem is referenced by: grpbn0 18070 grprcan 18075 grpid 18077 isgrpid2 18078 grprinv 18091 grpidinv 18097 grpinvid 18098 grpidrcan 18102 grpidlcan 18103 grpidssd 18113 grpinvval2 18120 grpsubid1 18122 imasgrp 18153 mulgcl 18183 mulgz 18193 subg0 18223 subg0cl 18225 issubg4 18236 0subg 18242 nmzsubg 18255 eqgid 18270 qusgrp 18273 qus0 18276 ghmid 18302 ghmpreima 18318 ghmf1 18325 gafo 18364 gaid 18367 gass 18369 gaorber 18376 gastacl 18377 lactghmga 18462 cayleylem2 18470 symgsssg 18524 symgfisg 18525 od1 18615 gexdvds 18638 sylow1lem2 18653 sylow3lem1 18681 lsmdisj2 18737 0frgp 18834 odadd1 18897 torsubg 18903 oddvdssubg 18904 0cyg 18942 prmcyg 18943 telgsums 19042 dprdfadd 19071 dprdz 19081 pgpfac1lem3a 19127 ablsimpgprmd 19166 ring0cl 19248 ringlz 19266 ringrz 19267 f1ghm0to0 19421 kerf1ghm 19426 kerf1hrmOLD 19427 isdrng2 19441 srng0 19560 lmod0vcl 19592 islmhm2 19739 ascl0 20041 psr0cl 20102 mplsubglem 20142 mhp0cl 20265 mhpaddcl 20266 mhpinvcl 20267 evl1gsumd 20448 frgpcyg 20648 ip0l 20708 ocvlss 20744 grpvlinv 20934 matinvgcell 20972 mat0dim0 21004 mdetdiag 21136 mdetuni0 21158 chpdmatlem2 21375 chp0mat 21382 istgp2 22627 cldsubg 22646 tgpconncompeqg 22647 tgpconncomp 22648 snclseqg 22651 tgphaus 22652 tgpt1 22653 qustgphaus 22658 tgptsmscls 22685 nrmmetd 23111 nmfval2 23127 nmval2 23128 nmf2 23129 ngpds3 23144 nmge0 23153 nmeq0 23154 nminv 23157 nmmtri 23158 nmrtri 23160 nm0 23165 tngnm 23187 idnghm 23279 nmcn 23379 clmvz 23642 nmoleub2lem2 23647 nglmle 23832 mdeg0 24591 dchrinv 25764 dchr1re 25766 dchrpt 25770 dchrsum2 25771 dchrhash 25774 rpvmasumlem 25990 rpvmasum2 26015 dchrisum0re 26016 ogrpinv0lt 30650 ogrpinvlt 30651 isarchi3 30743 archirng 30744 archirngz 30745 archiabllem1b 30748 rmfsupp2 30793 orngsqr 30804 ornglmulle 30805 orngrmulle 30806 ornglmullt 30807 orngrmullt 30808 orngmullt 30809 ofldchr 30814 isarchiofld 30817 qusker 30845 eqg0el 30853 fedgmullem1 30924 qqh0 31124 sconnpi1 32383 lfl0f 36085 lkrlss 36111 lshpkrlem1 36126 lkrin 36180 dvhgrp 38123 symgsubmefmndALT 43996 rnglz 44083 zrrnghm 44116 evl1at0 44373 |
Copyright terms: Public domain | W3C validator |