![]() |
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 18574 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (( 0 + 𝑋) = 𝑋 ∧ (𝑋 + 0 ) = 𝑋)) |
5 | 4 | simpld 495 | 1 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ‘cfv 6496 (class class class)co 7356 Basecbs 17082 +gcplusg 17132 0gc0g 17320 Mndcmnd 18555 |
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 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384 |
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 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-iota 6448 df-fun 6498 df-fv 6504 df-riota 7312 df-ov 7359 df-0g 17322 df-mgm 18496 df-sgrp 18545 df-mnd 18556 |
This theorem is referenced by: issubmnd 18582 ress0g 18583 submnd0 18584 mndinvmod 18585 prdsidlem 18587 imasmnd 18593 0subm 18627 0mhm 18629 mndind 18637 gsumccat 18650 dfgrp2 18774 grplid 18779 dfgrp3 18844 mhmid 18866 mhmmnd 18867 mulgnn0p1 18885 mulgnn0z 18901 mulgnn0dir 18904 cntzsubm 19114 oppgmnd 19133 odmodnn0 19320 lsmub2x 19427 mulgnn0di 19602 gsumval3 19682 gsumzaddlem 19696 gsumzsplit 19702 srgbinomlem4 19958 dsmmacl 21145 mndvlid 21740 dmatmul 21844 mndifsplit 21983 tsmssplit 23501 cntzsnid 31898 omndmul2 31915 omndmul3 31916 slmd0vlid 32052 c0mgm 46179 c0mhm 46180 c0snmgmhm 46184 cznrng 46225 mndpsuppss 46419 mndtccatid 47085 |
Copyright terms: Public domain | W3C validator |