![]() |
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 17753 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (( 0 + 𝑋) = 𝑋 ∧ (𝑋 + 0 ) = 𝑋)) |
5 | 4 | simpld 495 | 1 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1525 ∈ wcel 2083 ‘cfv 6232 (class class class)co 7023 Basecbs 16316 +gcplusg 16398 0gc0g 16546 Mndcmnd 17737 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-ral 3112 df-rex 3113 df-reu 3114 df-rmo 3115 df-rab 3116 df-v 3442 df-sbc 3712 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-br 4969 df-opab 5031 df-mpt 5048 df-id 5355 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-iota 6196 df-fun 6234 df-fv 6240 df-riota 6984 df-ov 7026 df-0g 16548 df-mgm 17685 df-sgrp 17727 df-mnd 17738 |
This theorem is referenced by: issubmnd 17761 ress0g 17762 submnd0 17763 prdsidlem 17765 imasmnd 17771 0mhm 17801 mndind 17809 gsumccat 17821 dfgrp2 17890 grplid 17895 dfgrp3 17959 mhmid 17981 mhmmnd 17982 mulgnn0p1 17998 mulgnn0z 18012 mulgnn0dir 18015 cntzsubm 18211 oppgmnd 18227 odmodnn0 18403 lsmub2x 18506 mulgnn0di 18675 gsumval3 18752 gsumzaddlem 18765 gsumzsplit 18771 srgbinomlem4 18987 dsmmacl 20571 mndvlid 20690 dmatmul 20794 mndifsplit 20933 tsmssplit 22447 omndmul2 30369 omndmul3 30370 slmd0vlid 30484 cntzsnid 30503 c0mgm 43680 c0mhm 43681 c0snmgmhm 43685 cznrng 43726 mndpsuppss 43921 |
Copyright terms: Public domain | W3C validator |