| 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 18958 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
| 2 | grpidcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
| 3 | grpidcl.o | . . 3 ⊢ 0 = (0g‘𝐺) | |
| 4 | 2, 3 | mndidcl 18762 | . 2 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
| 5 | 1, 4 | syl 17 | 1 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 ‘cfv 6561 Basecbs 17247 0gc0g 17484 Mndcmnd 18747 Grpcgrp 18951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-iota 6514 df-fun 6563 df-fv 6569 df-riota 7388 df-ov 7434 df-0g 17486 df-mgm 18653 df-sgrp 18732 df-mnd 18748 df-grp 18954 |
| This theorem is referenced by: grpbn0 18984 grprcan 18991 grpid 18993 isgrpid2 18994 grprinv 19008 grpidinv 19016 grpinvid 19017 grpidrcan 19021 grpidlcan 19022 grpidssd 19034 grpinvval2 19041 grpsubid1 19043 imasgrp 19074 mulgcl 19109 mulgz 19120 subg0 19150 subg0cl 19152 issubg4 19163 0subgOLD 19170 nmzsubg 19183 eqgid 19198 eqg0el 19201 qusgrp 19204 qus0 19207 ghmid 19240 ghmpreima 19256 f1ghm0to0 19263 kerf1ghm 19265 ghmqusker 19305 gafo 19314 gaid 19317 gass 19319 gaorber 19326 gastacl 19327 lactghmga 19423 cayleylem2 19431 symgsssg 19485 symgfisg 19486 od1 19577 gexdvds 19602 sylow1lem2 19617 sylow3lem1 19645 lsmdisj2 19700 0frgp 19797 odadd1 19866 torsubg 19872 oddvdssubg 19873 0cyg 19911 prmcyg 19912 telgsums 20011 dprdfadd 20040 dprdz 20050 pgpfac1lem3a 20096 ablsimpgprmd 20135 rng0cl 20160 rnglz 20162 rngrz 20163 ring0cl 20264 zrrnghm 20536 isdomn4 20716 isdrng2 20743 srng0 20855 lmod0vcl 20889 islmhm2 21037 rnglidl0 21239 frgpcyg 21592 ip0l 21654 ocvlss 21690 ascl0 21904 psr0cl 21972 mplsubglem 22019 mhp0cl 22150 mhpaddcl 22155 evl1gsumd 22361 grpvlinv 22402 matinvgcell 22441 mat0dim0 22473 mdetdiag 22605 mdetuni0 22627 chpdmatlem2 22845 chp0mat 22852 istgp2 24099 cldsubg 24119 tgpconncompeqg 24120 tgpconncomp 24121 snclseqg 24124 tgphaus 24125 tgpt1 24126 qustgphaus 24131 tgptsmscls 24158 nrmmetd 24587 nmfval2 24604 nmval2 24605 nmf2 24606 ngpds3 24621 nmge0 24630 nmeq0 24631 nminv 24634 nmmtri 24635 nmrtri 24637 nm0 24642 tngnm 24672 idnghm 24764 nmcn 24866 clmvz 25144 nmoleub2lem2 25149 nglmle 25336 mdeg0 26109 dchrinv 27305 dchr1re 27307 dchrpt 27311 dchrsum2 27312 dchrhash 27315 rpvmasumlem 27531 rpvmasum2 27556 dchrisum0re 27557 ogrpinv0lt 33099 ogrpinvlt 33100 isarchi3 33194 archirng 33195 archirngz 33196 archiabllem1b 33199 rmfsupp2 33242 erler 33269 rlocaddval 33272 rlocmulval 33273 rloc0g 33275 fracfld 33310 orngsqr 33334 ornglmulle 33335 orngrmulle 33336 ornglmullt 33337 orngrmullt 33338 orngmullt 33339 ofldchr 33344 isarchiofld 33347 qusker 33377 grplsm0l 33431 qus0g 33435 nsgqus0 33438 nsgmgclem 33439 fedgmullem1 33680 irredminply 33757 rtelextdg2lem 33767 qqh0 33985 sconnpi1 35244 lfl0f 39070 lkrlss 39096 lshpkrlem1 39111 lkrin 39165 dvhgrp 41109 primrootscoprmpow 42100 aks5lem7 42201 fsuppind 42600 fsuppssind 42603 mhpind 42604 evl1at0 48308 |
| Copyright terms: Public domain | W3C validator |