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 18104 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpbn0.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grplid.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | grplid.o | . . 3 ⊢ 0 = (0g‘𝐺) | |
5 | 2, 3, 4 | mndlid 17925 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) |
6 | 1, 5 | sylan 582 | 1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1533 ∈ wcel 2110 ‘cfv 6349 (class class class)co 7150 Basecbs 16477 +gcplusg 16559 0gc0g 16707 Mndcmnd 17905 Grpcgrp 18097 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4561 df-pr 4563 df-op 4567 df-uni 4832 df-br 5059 df-opab 5121 df-mpt 5139 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-iota 6308 df-fun 6351 df-fv 6357 df-riota 7108 df-ov 7153 df-0g 16709 df-mgm 17846 df-sgrp 17895 df-mnd 17906 df-grp 18100 |
This theorem is referenced by: grprcan 18131 grpid 18133 isgrpid2 18134 grprinv 18147 grpinvid1 18148 grpinvid2 18149 grpidinv2 18152 grpinvid 18154 grplcan 18155 grpasscan1 18156 grpidlcan 18159 grplmulf1o 18167 grpidssd 18169 grpinvadd 18171 grpinvval2 18176 grplactcnv 18196 imasgrp 18209 mulgaddcom 18245 mulgdirlem 18252 subg0 18279 issubg2 18288 issubg4 18292 0subg 18298 isnsg3 18306 nmzsubg 18311 ssnmz 18312 eqger 18324 eqgid 18326 qusgrp 18329 qus0 18332 ghmid 18358 conjghm 18383 conjnmz 18386 subgga 18424 cntzsubg 18461 sylow1lem2 18718 sylow2blem2 18740 sylow2blem3 18741 sylow3lem1 18746 lsmmod 18795 lsmdisj2 18802 pj1rid 18822 abladdsub4 18928 ablpncan2 18930 ablpnpcan 18934 ablnncan 18935 odadd1 18962 odadd2 18963 oddvdssubg 18969 dprdfadd 19136 pgpfac1lem3a 19192 ringlz 19331 ringrz 19332 isabvd 19585 lmod0vlid 19658 lmod0vs 19661 psr0lid 20169 mplsubglem 20208 mplcoe1 20240 mhpaddcl 20332 evpmodpmf1o 20734 ocvlss 20810 lsmcss 20830 mdetunilem6 21220 mdetunilem9 21223 ghmcnp 22717 tgpt0 22721 qustgpopn 22722 mdegaddle 24662 ply1rem 24751 gsumsubg 30679 ogrpinv0le 30711 ogrpaddltrbid 30716 ogrpinv0lt 30718 ogrpinvlt 30719 cyc3genpmlem 30788 isarchi3 30811 archirngz 30813 archiabllem1b 30816 freshmansdream 30854 orngsqr 30872 ornglmulle 30873 orngrmulle 30874 ofldchr 30882 qusker 30913 mxidlprm 30972 dimkerim 31018 matunitlindflem1 34882 lfl0f 36199 lfladd0l 36204 lkrlss 36225 lkrin 36294 dvhgrp 38237 baerlem3lem1 38837 mapdh6bN 38867 hdmap1l6b 38941 hdmapinvlem3 39050 hdmapinvlem4 39051 hdmapglem7b 39058 rnglz 44149 |
Copyright terms: Public domain | W3C validator |