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

Metamath Proof Explorer

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 )