![]() |
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 18715 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpbn0.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grplid.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | grplid.o | . . 3 ⊢ 0 = (0g‘𝐺) | |
5 | 2, 3, 4 | mndlid 18536 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) |
6 | 1, 5 | sylan 580 | 1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ‘cfv 6493 (class class class)co 7351 Basecbs 17043 +gcplusg 17093 0gc0g 17281 Mndcmnd 18516 Grpcgrp 18708 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-sep 5254 ax-nul 5261 ax-pr 5382 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-rmo 3351 df-reu 3352 df-rab 3406 df-v 3445 df-sbc 3738 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-mpt 5187 df-id 5529 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-iota 6445 df-fun 6495 df-fv 6501 df-riota 7307 df-ov 7354 df-0g 17283 df-mgm 18457 df-sgrp 18506 df-mnd 18517 df-grp 18711 |
This theorem is referenced by: grprcan 18744 grpid 18746 isgrpid2 18747 grprinv 18760 grpinvid1 18761 grpinvid2 18762 grpidinv2 18765 grpinvid 18767 grplcan 18768 grpasscan1 18769 grpidlcan 18772 grplmulf1o 18780 grpidssd 18782 grpinvadd 18784 grpinvval2 18789 grplactcnv 18809 imasgrp 18822 mulgaddcom 18859 mulgdirlem 18866 subg0 18893 issubg2 18902 issubg4 18906 0subgOLD 18913 isnsg3 18921 nmzsubg 18926 ssnmz 18927 eqger 18939 eqgid 18941 qusgrp 18944 qus0 18947 ghmid 18973 conjghm 18998 conjnmz 19001 subgga 19039 cntzsubg 19076 sylow1lem2 19340 sylow2blem2 19362 sylow2blem3 19363 sylow3lem1 19368 lsmmod 19416 lsmdisj2 19423 pj1rid 19443 abladdsub4 19551 ablpncan2 19553 ablpnpcan 19557 ablnncan 19558 odadd1 19585 odadd2 19586 oddvdssubg 19592 dprdfadd 19758 pgpfac1lem3a 19814 ringlz 19964 ringrz 19965 isabvd 20232 lmod0vlid 20305 lmod0vs 20308 evpmodpmf1o 20953 ocvlss 21029 lsmcss 21049 psr0lid 21316 mplsubglem 21357 mplcoe1 21390 mhpaddcl 21493 mdetunilem6 21918 mdetunilem9 21921 ghmcnp 23418 tgpt0 23422 qustgpopn 23423 mdegaddle 25391 ply1rem 25480 gsumsubg 31714 ogrpinv0le 31749 ogrpaddltrbid 31754 ogrpinv0lt 31756 ogrpinvlt 31757 cyc3genpmlem 31826 isarchi3 31849 archirngz 31851 archiabllem1b 31854 freshmansdream 31893 orngsqr 31925 ornglmulle 31926 orngrmulle 31927 ofldchr 31935 qusker 31967 grplsm0l 32010 quslsm 32012 mxidlprm 32059 dimkerim 32142 matunitlindflem1 36012 lfl0f 37469 lfladd0l 37474 lkrlss 37495 lkrin 37564 dvhgrp 39508 baerlem3lem1 40108 mapdh6bN 40138 hdmap1l6b 40212 hdmapinvlem3 40321 hdmapinvlem4 40322 hdmapglem7b 40329 sn-grplidd 40625 fsuppind 40674 fsuppssind 40677 rnglz 46083 |
Copyright terms: Public domain | W3C validator |