Metamath Proof Explorer


Theorem ismgmid

Description: The identity element of a magma, if it exists, belongs to the base set. (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 = 𝑈 ) )