![]() |
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 17622 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (( 0 + 𝑋) = 𝑋 ∧ (𝑋 + 0 ) = 𝑋)) |
5 | 4 | simpld 489 | 1 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 ‘cfv 6099 (class class class)co 6876 Basecbs 16181 +gcplusg 16264 0gc0g 16412 Mndcmnd 17606 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 ax-sep 4973 ax-nul 4981 ax-pow 5033 ax-pr 5095 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2590 df-eu 2607 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ne 2970 df-ral 3092 df-rex 3093 df-reu 3094 df-rmo 3095 df-rab 3096 df-v 3385 df-sbc 3632 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-nul 4114 df-if 4276 df-sn 4367 df-pr 4369 df-op 4373 df-uni 4627 df-br 4842 df-opab 4904 df-mpt 4921 df-id 5218 df-xp 5316 df-rel 5317 df-cnv 5318 df-co 5319 df-dm 5320 df-iota 6062 df-fun 6101 df-fv 6107 df-riota 6837 df-ov 6879 df-0g 16414 df-mgm 17554 df-sgrp 17596 df-mnd 17607 |
This theorem is referenced by: issubmnd 17630 ress0g 17631 submnd0 17632 prdsidlem 17634 imasmnd 17640 0mhm 17670 mrcmndind 17678 gsumccat 17690 dfgrp2 17760 grplid 17765 dfgrp3 17827 mhmid 17849 mhmmnd 17850 mulgnn0p1 17865 mulgnn0z 17879 mulgnn0dir 17882 cntzsubm 18077 oppgmnd 18093 odmodnn0 18269 lsmub2x 18372 mulgnn0di 18543 gsumval3 18620 gsumzaddlem 18633 gsumzsplit 18639 srgbinomlem4 18856 dsmmacl 20407 mndvlid 20521 dmatmul 20626 mndifsplit 20765 tsmssplit 22280 omndmul2 30220 omndmul3 30221 slmd0vlid 30283 c0mgm 42696 c0mhm 42697 c0snmgmhm 42701 cznrng 42742 mndpsuppss 42939 |
Copyright terms: Public domain | W3C validator |