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 } )