This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsumvallem2

Description: Lemma for properties of the set of identities of G . The set of identities of a monoid is exactly the unique identity element. (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Hypotheses gsumvallem2.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumvallem2.z ⊢ 0 = ( 0g ‘ 𝐺 )
gsumvallem2.p ⊢ + = ( +g ‘ 𝐺 )
gsumvallem2.o ⊢ 𝑂 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) }
Assertion gsumvallem2 ( 𝐺 ∈ Mnd → 𝑂 = { 0 } )

Proof

Step Hyp Ref Expression
1 gsumvallem2.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumvallem2.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsumvallem2.p ⊢ + = ( +g ‘ 𝐺 )
4 gsumvallem2.o ⊢ 𝑂 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) }
5 1 2 3 4 mgmidsssn0 ⊢ ( 𝐺 ∈ Mnd → 𝑂 ⊆ { 0 } )
6 1 2 mndidcl ⊢ ( 𝐺 ∈ Mnd → 0 ∈ 𝐵 )
7 1 3 2 mndlrid ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑦 ∈ 𝐵 ) → ( ( 0 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 0 ) = 𝑦 ) )
8 7 ralrimiva ⊢ ( 𝐺 ∈ Mnd → ∀ 𝑦 ∈ 𝐵 ( ( 0 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 0 ) = 𝑦 ) )
9 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 + 𝑦 ) = ( 0 + 𝑦 ) )
10 9 eqeq1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 + 𝑦 ) = 𝑦 ↔ ( 0 + 𝑦 ) = 𝑦 ) )
11 10 ovanraleqv ⊢ ( 𝑥 = 0 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 0 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 0 ) = 𝑦 ) ) )
12 11 4 elrab2 ⊢ ( 0 ∈ 𝑂 ↔ ( 0 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 0 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 0 ) = 𝑦 ) ) )
13 6 8 12 sylanbrc ⊢ ( 𝐺 ∈ Mnd → 0 ∈ 𝑂 )
14 13 snssd ⊢ ( 𝐺 ∈ Mnd → { 0 } ⊆ 𝑂 )
15 5 14 eqssd ⊢ ( 𝐺 ∈ Mnd → 𝑂 = { 0 } )