![]() |
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 18102 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpidcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grpidcl.o | . . 3 ⊢ 0 = (0g‘𝐺) | |
4 | 2, 3 | mndidcl 17918 | . 2 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
5 | 1, 4 | syl 17 | 1 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 ∈ wcel 2111 ‘cfv 6324 Basecbs 16475 0gc0g 16705 Mndcmnd 17903 Grpcgrp 18095 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-iota 6283 df-fun 6326 df-fv 6332 df-riota 7093 df-ov 7138 df-0g 16707 df-mgm 17844 df-sgrp 17893 df-mnd 17904 df-grp 18098 |
This theorem is referenced by: grpbn0 18124 grprcan 18129 grpid 18131 isgrpid2 18132 grprinv 18145 grpidinv 18151 grpinvid 18152 grpidrcan 18156 grpidlcan 18157 grpidssd 18167 grpinvval2 18174 grpsubid1 18176 imasgrp 18207 mulgcl 18237 mulgz 18247 subg0 18277 subg0cl 18279 issubg4 18290 0subg 18296 nmzsubg 18309 eqgid 18324 qusgrp 18327 qus0 18330 ghmid 18356 ghmpreima 18372 ghmf1 18379 gafo 18418 gaid 18421 gass 18423 gaorber 18430 gastacl 18431 lactghmga 18525 cayleylem2 18533 symgsssg 18587 symgfisg 18588 od1 18678 gexdvds 18701 sylow1lem2 18716 sylow3lem1 18744 lsmdisj2 18800 0frgp 18897 odadd1 18961 torsubg 18967 oddvdssubg 18968 0cyg 19006 prmcyg 19007 telgsums 19106 dprdfadd 19135 dprdz 19145 pgpfac1lem3a 19191 ablsimpgprmd 19230 ring0cl 19315 ringlz 19333 ringrz 19334 f1ghm0to0 19488 kerf1ghm 19491 isdrng2 19505 srng0 19624 lmod0vcl 19656 islmhm2 19803 frgpcyg 20265 ip0l 20325 ocvlss 20361 ascl0 20570 psr0cl 20632 mplsubglem 20672 mhp0cl 20797 mhpaddcl 20799 evl1gsumd 20981 grpvlinv 21002 matinvgcell 21040 mat0dim0 21072 mdetdiag 21204 mdetuni0 21226 chpdmatlem2 21444 chp0mat 21451 istgp2 22696 cldsubg 22716 tgpconncompeqg 22717 tgpconncomp 22718 snclseqg 22721 tgphaus 22722 tgpt1 22723 qustgphaus 22728 tgptsmscls 22755 nrmmetd 23181 nmfval2 23197 nmval2 23198 nmf2 23199 ngpds3 23214 nmge0 23223 nmeq0 23224 nminv 23227 nmmtri 23228 nmrtri 23230 nm0 23235 tngnm 23257 idnghm 23349 nmcn 23449 clmvz 23716 nmoleub2lem2 23721 nglmle 23906 mdeg0 24671 dchrinv 25845 dchr1re 25847 dchrpt 25851 dchrsum2 25852 dchrhash 25855 rpvmasumlem 26071 rpvmasum2 26096 dchrisum0re 26097 ogrpinv0lt 30773 ogrpinvlt 30774 isarchi3 30866 archirng 30867 archirngz 30868 archiabllem1b 30871 rmfsupp2 30917 orngsqr 30928 ornglmulle 30929 orngrmulle 30930 ornglmullt 30931 orngrmullt 30932 orngmullt 30933 ofldchr 30938 isarchiofld 30941 qusker 30969 eqg0el 30977 fedgmullem1 31113 qqh0 31335 sconnpi1 32599 lfl0f 36365 lkrlss 36391 lshpkrlem1 36406 lkrin 36460 dvhgrp 38403 fsuppind 39456 fsuppssind 39459 rnglz 44508 zrrnghm 44541 evl1at0 44799 |
Copyright terms: Public domain | W3C validator |