![]() |
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 17626 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpidcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grpidcl.o | . . 3 ⊢ 0 = (0g‘𝐺) | |
4 | 2, 3 | mndidcl 17505 | . 2 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
5 | 1, 4 | syl 17 | 1 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1628 ∈ wcel 2135 ‘cfv 6045 Basecbs 16055 0gc0g 16298 Mndcmnd 17491 Grpcgrp 17619 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1867 ax-4 1882 ax-5 1984 ax-6 2050 ax-7 2086 ax-8 2137 ax-9 2144 ax-10 2164 ax-11 2179 ax-12 2192 ax-13 2387 ax-ext 2736 ax-sep 4929 ax-nul 4937 ax-pow 4988 ax-pr 5051 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1631 df-ex 1850 df-nf 1855 df-sb 2043 df-eu 2607 df-mo 2608 df-clab 2743 df-cleq 2749 df-clel 2752 df-nfc 2887 df-ne 2929 df-ral 3051 df-rex 3052 df-reu 3053 df-rmo 3054 df-rab 3055 df-v 3338 df-sbc 3573 df-dif 3714 df-un 3716 df-in 3718 df-ss 3725 df-nul 4055 df-if 4227 df-sn 4318 df-pr 4320 df-op 4324 df-uni 4585 df-br 4801 df-opab 4861 df-mpt 4878 df-id 5170 df-xp 5268 df-rel 5269 df-cnv 5270 df-co 5271 df-dm 5272 df-iota 6008 df-fun 6047 df-fv 6053 df-riota 6770 df-ov 6812 df-0g 16300 df-mgm 17439 df-sgrp 17481 df-mnd 17492 df-grp 17622 |
This theorem is referenced by: grpbn0 17648 grprcan 17652 grpid 17654 isgrpid2 17655 grprinv 17666 grpidinv 17672 grpinvid 17673 grpidrcan 17677 grpidlcan 17678 grpidssd 17688 grpinvval2 17695 grpsubid1 17697 imasgrp 17728 mulgcl 17756 mulgz 17765 subg0 17797 subg0cl 17799 issubg4 17810 0subg 17816 nmzsubg 17832 eqgid 17843 qusgrp 17846 qus0 17849 ghmid 17863 ghmpreima 17879 ghmf1 17886 gafo 17925 gaid 17928 gass 17930 gaorber 17937 gastacl 17938 lactghmga 18020 cayleylem2 18029 symgsssg 18083 symgfisg 18084 od1 18172 gexdvds 18195 sylow1lem2 18210 sylow3lem1 18238 lsmdisj2 18291 0frgp 18388 odadd1 18447 torsubg 18453 oddvdssubg 18454 0cyg 18490 prmcyg 18491 telgsums 18586 dprdfadd 18615 dprdz 18625 pgpfac1lem3a 18671 ring0cl 18765 ringlz 18783 ringrz 18784 kerf1hrm 18941 isdrng2 18955 srng0 19058 lmod0vcl 19090 islmhm2 19236 psr0cl 19592 mplsubglem 19632 evl1gsumd 19919 frgpcyg 20120 ip0l 20179 ocvlss 20214 grpvlinv 20399 matinvgcell 20439 mat0dim0 20471 mdetdiag 20603 mdetuni0 20625 chpdmatlem2 20842 chp0mat 20849 istgp2 22092 cldsubg 22111 tgpconncompeqg 22112 tgpconncomp 22113 snclseqg 22116 tgphaus 22117 tgpt1 22118 qustgphaus 22123 tgptsmscls 22150 nrmmetd 22576 nmfval2 22592 nmval2 22593 nmf2 22594 ngpds3 22609 nmge0 22618 nmeq0 22619 nminv 22622 nmmtri 22623 nmrtri 22625 nm0 22630 tngnm 22652 idnghm 22744 nmcn 22844 clmvz 23107 nmoleub2lem2 23112 nglmle 23296 mdeg0 24025 dchrinv 25181 dchr1re 25183 dchrpt 25187 dchrsum2 25188 dchrhash 25191 rpvmasumlem 25371 rpvmasum2 25396 dchrisum0re 25397 ogrpinvOLD 30020 ogrpinv0lt 30028 ogrpinvlt 30029 isarchi3 30046 archirng 30047 archirngz 30048 archiabllem1b 30051 orngsqr 30109 ornglmulle 30110 orngrmulle 30111 ornglmullt 30112 orngrmullt 30113 orngmullt 30114 ofldchr 30119 isarchiofld 30122 qqh0 30333 sconnpi1 31524 lfl0f 34855 lkrlss 34881 lshpkrlem1 34896 lkrin 34950 dvhgrp 36894 rnglz 42390 zrrnghm 42423 ascl0 42671 evl1at0 42685 |
Copyright terms: Public domain | W3C validator |