Metamath Proof Explorer


Theorem lidrididd

Description: If there is a left and right identity element for any binary operation (group operation) .+ , the left identity element (and therefore also the right identity element according to lidrideqd ) is equal to the two-sided identity element. (Contributed by AV, 26-Dec-2023)

Ref Expression
Hypotheses lidrideqd.l φLB
lidrideqd.r φRB
lidrideqd.li φxBL+˙x=x
lidrideqd.ri φxBx+˙R=x
lidrideqd.b B=BaseG
lidrideqd.p +˙=+G
lidrididd.o 0˙=0G
Assertion lidrididd φL=0˙

Proof

Step Hyp Ref Expression
1 lidrideqd.l φLB
2 lidrideqd.r φRB
3 lidrideqd.li φxBL+˙x=x
4 lidrideqd.ri φxBx+˙R=x
5 lidrideqd.b B=BaseG
6 lidrideqd.p +˙=+G
7 lidrididd.o 0˙=0G
8 oveq2 x=yL+˙x=L+˙y
9 id x=yx=y
10 8 9 eqeq12d x=yL+˙x=xL+˙y=y
11 10 rspcv yBxBL+˙x=xL+˙y=y
12 3 11 mpan9 φyBL+˙y=y
13 1 2 3 4 lidrideqd φL=R
14 oveq1 x=yx+˙R=y+˙R
15 14 9 eqeq12d x=yx+˙R=xy+˙R=y
16 15 rspcv yBxBx+˙R=xy+˙R=y
17 oveq2 L=Ry+˙L=y+˙R
18 17 adantl y+˙R=yL=Ry+˙L=y+˙R
19 simpl y+˙R=yL=Ry+˙R=y
20 18 19 eqtrd y+˙R=yL=Ry+˙L=y
21 20 ex y+˙R=yL=Ry+˙L=y
22 16 21 syl6com xBx+˙R=xyBL=Ry+˙L=y
23 22 com23 xBx+˙R=xL=RyBy+˙L=y
24 4 13 23 sylc φyBy+˙L=y
25 24 imp φyBy+˙L=y
26 5 7 6 1 12 25 ismgmid2 φL=0˙