![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > grplid | Structured version Visualization version GIF version |
Description: The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.) |
Ref | Expression |
---|---|
grpbn0.b | ⊢ 𝐵 = (Base‘𝐺) |
grplid.p | ⊢ + = (+g‘𝐺) |
grplid.o | ⊢ 0 = (0g‘𝐺) |
Ref | Expression |
---|---|
grplid | ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grpmnd 18928 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpbn0.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grplid.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | grplid.o | . . 3 ⊢ 0 = (0g‘𝐺) | |
5 | 2, 3, 4 | mndlid 18740 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) |
6 | 1, 5 | sylan 578 | 1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1534 ∈ wcel 2099 ‘cfv 6544 (class class class)co 7414 Basecbs 17206 +gcplusg 17259 0gc0g 17447 Mndcmnd 18720 Grpcgrp 18921 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5295 ax-nul 5302 ax-pr 5424 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-ral 3052 df-rex 3061 df-rmo 3365 df-reu 3366 df-rab 3421 df-v 3465 df-sbc 3777 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4324 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4907 df-br 5145 df-opab 5207 df-mpt 5228 df-id 5571 df-xp 5679 df-rel 5680 df-cnv 5681 df-co 5682 df-dm 5683 df-iota 6496 df-fun 6546 df-fv 6552 df-riota 7370 df-ov 7417 df-0g 17449 df-mgm 18626 df-sgrp 18705 df-mnd 18721 df-grp 18924 |
This theorem is referenced by: grplidd 18957 grprcan 18961 grpid 18963 isgrpid2 18964 grprinv 18978 grpinvid1 18979 grpinvid2 18980 grpidinv2 18985 grpinvid 18987 grplcan 18988 grpasscan1 18989 grpidlcan 18992 grplmulf1o 19001 grpidssd 19004 grpinvadd 19006 grpinvval2 19011 grplactcnv 19031 imasgrp 19044 mulgaddcom 19086 mulgdirlem 19093 subg0 19120 issubg2 19129 issubg4 19133 0subgOLD 19140 isnsg3 19148 nmzsubg 19153 ssnmz 19154 eqgid 19168 qusgrp 19174 qus0 19177 ghmid 19210 conjghm 19237 subgga 19288 cntzsubg 19327 sylow1lem2 19591 sylow2blem2 19613 sylow2blem3 19614 sylow3lem1 19619 lsmmod 19667 lsmdisj2 19674 pj1rid 19694 abladdsub4 19803 ablpncan2 19807 ablpnpcan 19811 ablnncan 19812 odadd1 19840 odadd2 19841 oddvdssubg 19847 dprdfadd 20014 pgpfac1lem3a 20070 rnglz 20142 rngrz 20143 isabvd 20785 lmod0vlid 20862 lmod0vs 20865 freshmansdream 21566 evpmodpmf1o 21586 ocvlss 21662 lsmcss 21682 psr0lid 21956 mplsubglem 22002 mplcoe1 22038 mhpaddcl 22139 mdetunilem6 22605 mdetunilem9 22608 ghmcnp 24105 tgpt0 24109 qustgpopn 24110 mdegaddle 26096 ply1rem 26188 gsumsubg 32916 ogrpinv0le 32952 ogrpaddltrbid 32957 ogrpinv0lt 32959 ogrpinvlt 32960 cyc3genpmlem 33031 isarchi3 33054 archirngz 33056 archiabllem1b 33059 orngsqr 33185 ornglmulle 33186 orngrmulle 33187 qusker 33228 grplsm0l 33282 quslsm 33284 mxidlprm 33349 matunitlindflem1 37328 lfl0f 38778 lfladd0l 38783 lkrlss 38804 lkrin 38873 dvhgrp 40817 baerlem3lem1 41417 mapdh6bN 41447 hdmap1l6b 41521 hdmapinvlem3 41630 hdmapinvlem4 41631 hdmapglem7b 41638 fsuppind 42278 fsuppssind 42281 |
Copyright terms: Public domain | W3C validator |