Metamath Proof Explorer

Theorem ismgmid

Description: Conditions for a class to be the identity element of a magma, if it exists. (Contributed by Mario Carneiro, 27-Dec-2014)

Ref Expression
Hypotheses ismgmid.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
ismgmid.o ⊢ 0 = ( 0g ‘ 𝐺 )
ismgmid.p ⊢ + = ( +g ‘ 𝐺 )
mgmidcl.e ⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
Assertion ismgmid ( 𝜑 → ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑈 ) = 𝑥 ) ) ↔ 0 = 𝑈 ) )

Proof

Step Hyp Ref Expression
1 ismgmid.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ismgmid.o ⊢ 0 = ( 0g ‘ 𝐺 )
3 ismgmid.p ⊢ + = ( +g ‘ 𝐺 )
4 mgmidcl.e ⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
5 id ⊢ ( 𝑈 ∈ 𝐵 → 𝑈 ∈ 𝐵 )
6 mgmidmo ⊢ ∃* 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 )
7 reu5 ⊢ ( ∃! 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ( ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ∧ ∃* 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
8 4 6 7 sylanblrc ⊢ ( 𝜑 → ∃! 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
9 oveq1 ⊢ ( 𝑒 = 𝑈 → ( 𝑒 + 𝑥 ) = ( 𝑈 + 𝑥 ) )
10 9 eqeq1d ⊢ ( 𝑒 = 𝑈 → ( ( 𝑒 + 𝑥 ) = 𝑥 ↔ ( 𝑈 + 𝑥 ) = 𝑥 ) )
11 10 ovanraleqv ⊢ ( 𝑒 = 𝑈 → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑈 ) = 𝑥 ) ) )
12 11 riota2 ⊢ ( ( 𝑈 ∈ 𝐵 ∧ ∃! 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑈 ) = 𝑥 ) ↔ ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 ) )
13 5 8 12 syl2anr ⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑈 ) = 𝑥 ) ↔ ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 ) )
14 13 pm5.32da ⊢ ( 𝜑 → ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑈 ) = 𝑥 ) ) ↔ ( 𝑈 ∈ 𝐵 ∧ ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 ) ) )
15 riotacl ⊢ ( ∃! 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) → ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ∈ 𝐵 )
16 8 15 syl ⊢ ( 𝜑 → ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ∈ 𝐵 )
17 eleq1 ⊢ ( ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 → ( ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ∈ 𝐵 ↔ 𝑈 ∈ 𝐵 ) )
18 16 17 syl5ibcom ⊢ ( 𝜑 → ( ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 → 𝑈 ∈ 𝐵 ) )
19 18 pm4.71rd ⊢ ( 𝜑 → ( ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 ↔ ( 𝑈 ∈ 𝐵 ∧ ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 ) ) )
20 df-riota ⊢ ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = ( ℩ 𝑒 ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
21 1 3 2 grpidval ⊢ 0 = ( ℩ 𝑒 ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
22 20 21 eqtr4i ⊢ ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 0
23 22 eqeq1i ⊢ ( ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 ↔ 0 = 𝑈 )
24 23 a1i ⊢ ( 𝜑 → ( ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 ↔ 0 = 𝑈 ) )
25 14 19 24 3bitr2d ⊢ ( 𝜑 → ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑈 ) = 𝑥 ) ) ↔ 0 = 𝑈 ) )