Theorem mgmidsssn0

Description: Property of the set of identities of G . Either G has no identities, and O = (/) , or it has one and this identity is unique and identified by the 0g function. (Contributed by Mario Carneiro, 7-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		mgmidsssn0.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mgmidsssn0.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		mgmidsssn0.p	⊢ + = ( +g ‘ 𝐺 )
4		mgmidsssn0.o	⊢ 𝑂 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) }
5		simpr	⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) ) → ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) )
6		oveq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 + 𝑦 ) = ( 𝑥 + 𝑦 ) )
7	6	eqeq1d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 + 𝑦 ) = 𝑦 ↔ ( 𝑥 + 𝑦 ) = 𝑦 ) )
8	7	ovanraleqv	⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) )
9	8	rspcev	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) → ∃ 𝑧 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) )
10	9	adantl	⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) ) → ∃ 𝑧 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) )
11	1 2 3 10	ismgmid	⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) ) → ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) ↔ 0 = 𝑥 ) )
12	5 11	mpbid	⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) ) → 0 = 𝑥 )
13	12	eqcomd	⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) ) → 𝑥 = 0 )
14		velsn	⊢ ( 𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
15	13 14	sylibr	⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) ) → 𝑥 ∈ { 0 } )
16	15	expr	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) → 𝑥 ∈ { 0 } ) )
17	16	ralrimiva	⊢ ( 𝐺 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) → 𝑥 ∈ { 0 } ) )
18		rabss	⊢ ( { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ⊆ { 0 } ↔ ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) → 𝑥 ∈ { 0 } ) )
19	17 18	sylibr	⊢ ( 𝐺 ∈ 𝑉 → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ⊆ { 0 } )
20	4 19	eqsstrid	⊢ ( 𝐺 ∈ 𝑉 → 𝑂 ⊆ { 0 } )