Metamath Proof Explorer
Description: A monoid's identity element is a two-sided identity. (Contributed by NM, 18-Aug-2011)
|
|
Ref |
Expression |
|
Hypotheses |
mndlrid.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
|
|
mndlrid.p |
⊢ + = ( +g ‘ 𝐺 ) |
|
|
mndlrid.o |
⊢ 0 = ( 0g ‘ 𝐺 ) |
|
Assertion |
mndlrid |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 + 𝑋 ) = 𝑋 ∧ ( 𝑋 + 0 ) = 𝑋 ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
mndlrid.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
mndlrid.p |
⊢ + = ( +g ‘ 𝐺 ) |
3 |
|
mndlrid.o |
⊢ 0 = ( 0g ‘ 𝐺 ) |
4 |
1 2
|
mndid |
⊢ ( 𝐺 ∈ Mnd → ∃ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) ) |
5 |
1 3 2 4
|
mgmlrid |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 + 𝑋 ) = 𝑋 ∧ ( 𝑋 + 0 ) = 𝑋 ) ) |