Metamath Proof Explorer


Theorem mgmidsssn0

Description: Property of the set of identities of G . Either G has no identities, and O = (/) , or it has one and this identity is unique and identified by the 0g function. (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Hypotheses mgmidsssn0.b B=BaseG
mgmidsssn0.z 0˙=0G
mgmidsssn0.p +˙=+G
mgmidsssn0.o O=xB|yBx+˙y=yy+˙x=y
Assertion mgmidsssn0 GVO0˙

Proof

Step Hyp Ref Expression
1 mgmidsssn0.b B=BaseG
2 mgmidsssn0.z 0˙=0G
3 mgmidsssn0.p +˙=+G
4 mgmidsssn0.o O=xB|yBx+˙y=yy+˙x=y
5 simpr GVxByBx+˙y=yy+˙x=yxByBx+˙y=yy+˙x=y
6 oveq1 z=xz+˙y=x+˙y
7 6 eqeq1d z=xz+˙y=yx+˙y=y
8 7 ovanraleqv z=xyBz+˙y=yy+˙z=yyBx+˙y=yy+˙x=y
9 8 rspcev xByBx+˙y=yy+˙x=yzByBz+˙y=yy+˙z=y
10 9 adantl GVxByBx+˙y=yy+˙x=yzByBz+˙y=yy+˙z=y
11 1 2 3 10 ismgmid GVxByBx+˙y=yy+˙x=yxByBx+˙y=yy+˙x=y0˙=x
12 5 11 mpbid GVxByBx+˙y=yy+˙x=y0˙=x
13 12 eqcomd GVxByBx+˙y=yy+˙x=yx=0˙
14 velsn x0˙x=0˙
15 13 14 sylibr GVxByBx+˙y=yy+˙x=yx0˙
16 15 expr GVxByBx+˙y=yy+˙x=yx0˙
17 16 ralrimiva GVxByBx+˙y=yy+˙x=yx0˙
18 rabss xB|yBx+˙y=yy+˙x=y0˙xByBx+˙y=yy+˙x=yx0˙
19 17 18 sylibr GVxB|yBx+˙y=yy+˙x=y0˙
20 4 19 eqsstrid GVO0˙