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 B=BaseG
ismgmid.o 0˙=0G
ismgmid.p +˙=+G
mgmidcl.e φeBxBe+˙x=xx+˙e=x
Assertion ismgmid φUBxBU+˙x=xx+˙U=x0˙=U

Proof

Step Hyp Ref Expression
1 ismgmid.b B=BaseG
2 ismgmid.o 0˙=0G
3 ismgmid.p +˙=+G
4 mgmidcl.e φeBxBe+˙x=xx+˙e=x
5 id UBUB
6 mgmidmo *eBxBe+˙x=xx+˙e=x
7 reu5 ∃!eBxBe+˙x=xx+˙e=xeBxBe+˙x=xx+˙e=x*eBxBe+˙x=xx+˙e=x
8 4 6 7 sylanblrc φ∃!eBxBe+˙x=xx+˙e=x
9 oveq1 e=Ue+˙x=U+˙x
10 9 eqeq1d e=Ue+˙x=xU+˙x=x
11 10 ovanraleqv e=UxBe+˙x=xx+˙e=xxBU+˙x=xx+˙U=x
12 11 riota2 UB∃!eBxBe+˙x=xx+˙e=xxBU+˙x=xx+˙U=xιeB|xBe+˙x=xx+˙e=x=U
13 5 8 12 syl2anr φUBxBU+˙x=xx+˙U=xιeB|xBe+˙x=xx+˙e=x=U
14 13 pm5.32da φUBxBU+˙x=xx+˙U=xUBιeB|xBe+˙x=xx+˙e=x=U
15 riotacl ∃!eBxBe+˙x=xx+˙e=xιeB|xBe+˙x=xx+˙e=xB
16 8 15 syl φιeB|xBe+˙x=xx+˙e=xB
17 eleq1 ιeB|xBe+˙x=xx+˙e=x=UιeB|xBe+˙x=xx+˙e=xBUB
18 16 17 syl5ibcom φιeB|xBe+˙x=xx+˙e=x=UUB
19 18 pm4.71rd φιeB|xBe+˙x=xx+˙e=x=UUBιeB|xBe+˙x=xx+˙e=x=U
20 df-riota ιeB|xBe+˙x=xx+˙e=x=ιe|eBxBe+˙x=xx+˙e=x
21 1 3 2 grpidval 0˙=ιe|eBxBe+˙x=xx+˙e=x
22 20 21 eqtr4i ιeB|xBe+˙x=xx+˙e=x=0˙
23 22 eqeq1i ιeB|xBe+˙x=xx+˙e=x=U0˙=U
24 23 a1i φιeB|xBe+˙x=xx+˙e=x=U0˙=U
25 14 19 24 3bitr2d φUBxBU+˙x=xx+˙U=x0˙=U