Theorem ismgmid2

Description: Show that a given element is the identity element of a magma. (Contributed by Mario Carneiro, 27-Dec-2014)

	Ref	Expression
Hypotheses	ismgmid.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	ismgmid.o	⊢ 0 = ( 0g ‘ 𝐺 )
	ismgmid.p	⊢ + = ( +g ‘ 𝐺 )
	ismgmid2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
	ismgmid2.l	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑈 + 𝑥 ) = 𝑥 )
	ismgmid2.r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 𝑈 ) = 𝑥 )
Assertion	ismgmid2	⊢ ( 𝜑 → 𝑈 = 0 )

Proof

Step	Hyp	Ref	Expression
1		ismgmid.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		ismgmid.o	⊢ 0 = ( 0g ‘ 𝐺 )
3		ismgmid.p	⊢ + = ( +g ‘ 𝐺 )
4		ismgmid2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
5		ismgmid2.l	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑈 + 𝑥 ) = 𝑥 )
6		ismgmid2.r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 𝑈 ) = 𝑥 )
7	5 6	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑈 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑈 ) = 𝑥 ) )
8	7	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑈 ) = 𝑥 ) )
9		oveq1	⊢ ( 𝑒 = 𝑈 → ( 𝑒 + 𝑥 ) = ( 𝑈 + 𝑥 ) )
10	9	eqeq1d	⊢ ( 𝑒 = 𝑈 → ( ( 𝑒 + 𝑥 ) = 𝑥 ↔ ( 𝑈 + 𝑥 ) = 𝑥 ) )
11	10	ovanraleqv	⊢ ( 𝑒 = 𝑈 → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑈 ) = 𝑥 ) ) )
12	11	rspcev	⊢ ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑈 ) = 𝑥 ) ) → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
13	4 8 12	syl2anc	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
14	1 2 3 13	ismgmid	⊢ ( 𝜑 → ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑈 ) = 𝑥 ) ) ↔ 0 = 𝑈 ) )
15	4 8 14	mpbi2and	⊢ ( 𝜑 → 0 = 𝑈 )
16	15	eqcomd	⊢ ( 𝜑 → 𝑈 = 0 )