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 17252 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpidcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grpidcl.o | . . 3 ⊢ 0 = (0g‘𝐺) | |
4 | 2, 3 | mndidcl 17131 | . 2 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
5 | 1, 4 | syl 17 | 1 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∈ wcel 1977 ‘cfv 5804 Basecbs 15695 0gc0g 15923 Mndcmnd 17117 Grpcgrp 17245 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-iota 5768 df-fun 5806 df-fv 5812 df-riota 6511 df-ov 6552 df-0g 15925 df-mgm 17065 df-sgrp 17107 df-mnd 17118 df-grp 17248 |
This theorem is referenced by: grpbn0 17274 grprcan 17278 grpid 17280 isgrpid2 17281 grprinv 17292 grpidinv 17298 grpinvid 17299 grpidrcan 17303 grpidlcan 17304 grpidssd 17314 grpinvval2 17321 grpsubid1 17323 imasgrp 17354 mulgcl 17382 mulgz 17391 subg0 17423 subg0cl 17425 issubg4 17436 0subg 17442 nmzsubg 17458 eqgid 17469 qusgrp 17472 qus0 17475 ghmid 17489 ghmpreima 17505 ghmf1 17512 gafo 17552 gaid 17555 gass 17557 gaorber 17564 gastacl 17565 lactghmga 17647 cayleylem2 17656 symgsssg 17710 symgfisg 17711 od1 17799 gexdvds 17822 sylow1lem2 17837 sylow3lem1 17865 lsmdisj2 17918 0frgp 18015 odadd1 18074 torsubg 18080 oddvdssubg 18081 0cyg 18117 prmcyg 18118 telgsums 18213 dprdfadd 18242 dprdz 18252 pgpfac1lem3a 18298 ring0cl 18392 ringlz 18410 ringrz 18411 kerf1hrm 18566 isdrng2 18580 srng0 18683 lmod0vcl 18715 islmhm2 18859 psr0cl 19215 mplsubglem 19255 evl1gsumd 19542 frgpcyg 19741 ip0l 19800 ocvlss 19835 grpvlinv 20020 matinvgcell 20060 mat0dim0 20092 mdetdiag 20224 mdetuni0 20246 chpdmatlem2 20463 chp0mat 20470 istgp2 21705 cldsubg 21724 tgpconcompeqg 21725 tgpconcomp 21726 snclseqg 21729 tgphaus 21730 tgpt1 21731 qustgphaus 21736 tgptsmscls 21763 nrmmetd 22189 nmfval2 22205 nmval2 22206 nmf2 22207 ngpds3 22222 nmge0 22231 nmeq0 22232 nminv 22235 nmmtri 22236 nmrtri 22238 nm0 22243 tngnm 22265 idnghm 22357 nmcn 22455 clmvz 22719 nmoleub2lem2 22724 nglmle 22908 mdeg0 23634 dchrinv 24786 dchr1re 24788 dchrpt 24792 dchrsum2 24793 dchrhash 24796 rpvmasumlem 24976 rpvmasum2 25001 dchrisum0re 25002 ogrpinvOLD 29046 ogrpinv0lt 29054 ogrpinvlt 29055 isarchi3 29072 archirng 29073 archirngz 29074 archiabllem1b 29077 orngsqr 29135 ornglmulle 29136 orngrmulle 29137 ornglmullt 29138 orngrmullt 29139 orngmullt 29140 ofldchr 29145 isarchiofld 29148 qqh0 29356 sconpi1 30475 lfl0f 33374 lkrlss 33400 lshpkrlem1 33415 lkrin 33469 dvhgrp 35414 rnglz 41674 zrrnghm 41707 ascl0 41959 evl1at0 41973 |
Copyright terms: Public domain | W3C validator |