![]() |
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 17892 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpbn0.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grplid.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | grplid.o | . . 3 ⊢ 0 = (0g‘𝐺) | |
5 | 2, 3, 4 | mndlid 17773 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) |
6 | 1, 5 | sylan 572 | 1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 = wceq 1507 ∈ wcel 2048 ‘cfv 6186 (class class class)co 6974 Basecbs 16333 +gcplusg 16415 0gc0g 16563 Mndcmnd 17756 Grpcgrp 17885 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2747 ax-sep 5058 ax-nul 5065 ax-pow 5117 ax-pr 5184 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2756 df-cleq 2768 df-clel 2843 df-nfc 2915 df-ne 2965 df-ral 3090 df-rex 3091 df-reu 3092 df-rmo 3093 df-rab 3094 df-v 3414 df-sbc 3681 df-dif 3831 df-un 3833 df-in 3835 df-ss 3842 df-nul 4178 df-if 4349 df-sn 4440 df-pr 4442 df-op 4446 df-uni 4711 df-br 4928 df-opab 4990 df-mpt 5007 df-id 5309 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-iota 6150 df-fun 6188 df-fv 6194 df-riota 6935 df-ov 6977 df-0g 16565 df-mgm 17704 df-sgrp 17746 df-mnd 17757 df-grp 17888 |
This theorem is referenced by: grprcan 17918 grpid 17920 isgrpid2 17921 grprinv 17934 grpinvid1 17935 grpinvid2 17936 grpidinv2 17939 grpinvid 17941 grplcan 17942 grpasscan1 17943 grpidlcan 17946 grplmulf1o 17954 grpidssd 17956 grpinvadd 17958 grpinvval2 17963 grplactcnv 17983 imasgrp 17996 mulgaddcom 18029 mulgdirlem 18036 subg0 18063 issubg2 18072 issubg4 18076 0subg 18082 isnsg3 18091 nmzsubg 18098 ssnmz 18099 eqger 18107 eqgid 18109 qusgrp 18112 qus0 18115 ghmid 18129 conjghm 18154 conjnmz 18157 subgga 18195 cntzsubg 18232 sylow1lem2 18479 sylow2blem2 18501 sylow2blem3 18502 sylow3lem1 18507 lsmmod 18553 lsmdisj2 18560 pj1rid 18580 abladdsub4 18686 ablpncan2 18688 ablpnpcan 18692 ablnncan 18693 odadd1 18718 odadd2 18719 oddvdssubg 18725 dprdfadd 18886 pgpfac1lem3a 18942 ringlz 19054 ringrz 19055 isabvd 19307 lmod0vlid 19380 lmod0vs 19383 psr0lid 19883 mplsubglem 19922 mplcoe1 19953 mhpaddcl 20038 evpmodpmf1o 20436 ocvlss 20512 lsmcss 20532 mdetunilem6 20924 mdetunilem9 20927 ghmcnp 22420 tgpt0 22424 qustgpopn 22425 mdegaddle 24365 ply1rem 24454 ogrpinvOLD 30425 ogrpinv0le 30426 ogrpaddltrbid 30431 ogrpinv0lt 30433 ogrpinvlt 30434 isarchi3 30473 archirngz 30475 archiabllem1b 30478 gsumsubg 30511 freshmansdream 30529 orngsqr 30547 ornglmulle 30548 orngrmulle 30549 ofldchr 30557 qusker 30588 dimkerim 30643 matunitlindflem1 34307 lfl0f 35628 lfladd0l 35633 lkrlss 35654 lkrin 35723 dvhgrp 37666 baerlem3lem1 38266 mapdh6bN 38296 hdmap1l6b 38370 hdmapinvlem3 38479 hdmapinvlem4 38480 hdmapglem7b 38487 rnglz 43493 |
Copyright terms: Public domain | W3C validator |