|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > mndlid | Structured version Visualization version GIF version | ||
| Description: The identity element of a monoid is a left identity. (Contributed by NM, 18-Aug-2011.) | 
| Ref | Expression | 
|---|---|
| mndlrid.b | ⊢ 𝐵 = (Base‘𝐺) | 
| mndlrid.p | ⊢ + = (+g‘𝐺) | 
| mndlrid.o | ⊢ 0 = (0g‘𝐺) | 
| Ref | Expression | 
|---|---|
| mndlid | ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | mndlrid.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
| 2 | mndlrid.p | . . 3 ⊢ + = (+g‘𝐺) | |
| 3 | mndlrid.o | . . 3 ⊢ 0 = (0g‘𝐺) | |
| 4 | 1, 2, 3 | mndlrid 18767 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (( 0 + 𝑋) = 𝑋 ∧ (𝑋 + 0 ) = 𝑋)) | 
| 5 | 4 | simpld 494 | 1 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 ∈ wcel 2107 ‘cfv 6560 (class class class)co 7432 Basecbs 17248 +gcplusg 17298 0gc0g 17485 Mndcmnd 18748 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-sep 5295 ax-nul 5305 ax-pr 5431 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-dif 3953 df-un 3955 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-br 5143 df-opab 5205 df-mpt 5225 df-id 5577 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-iota 6513 df-fun 6562 df-fv 6568 df-riota 7389 df-ov 7435 df-0g 17487 df-mgm 18654 df-sgrp 18733 df-mnd 18749 | 
| This theorem is referenced by: issubmnd 18775 ress0g 18776 submnd0 18777 mndinvmod 18778 mndpsuppss 18779 prdsidlem 18783 imasmnd 18789 xpsmnd0 18792 mndvlid 18813 0subm 18831 0mhm 18833 mndind 18842 gsumccat 18855 dfgrp2 18981 grplid 18986 dfgrp3 19058 mhmid 19082 mhmmnd 19083 mulgnn0p1 19104 mulgnn0z 19120 mulgnn0dir 19123 cntzsubm 19357 oppgmnd 19374 odmodnn0 19559 lsmub2x 19666 mulgnn0di 19844 gsumval3 19926 gsumzaddlem 19940 gsumzsplit 19946 srgbinomlem4 20227 c0mgm 20460 c0mhm 20461 c0snmgmhm 20463 dsmmacl 21762 dmatmul 22504 mndifsplit 22643 tsmssplit 24161 mndlrinv 33030 mndlactf1 33032 mndlactfo 33033 mndlactf1o 33036 mndractf1o 33037 gsumwun 33069 cntzsnid 33073 omndmul2 33090 omndmul3 33091 slmd0vlid 33229 mndmolinv 42097 primrootsunit1 42099 primrootscoprmpow 42101 primrootscoprbij 42104 cznrng 48182 mndtccatid 49239 | 
| Copyright terms: Public domain | W3C validator |