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 | |
|
lidrideqd.r | |
||
lidrideqd.li | |
||
lidrideqd.ri | |
||
lidrideqd.b | |
||
lidrideqd.p | |
||
lidrididd.o | |
||
Assertion | lidrididd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lidrideqd.l | |
|
2 | lidrideqd.r | |
|
3 | lidrideqd.li | |
|
4 | lidrideqd.ri | |
|
5 | lidrideqd.b | |
|
6 | lidrideqd.p | |
|
7 | lidrididd.o | |
|
8 | oveq2 | |
|
9 | id | |
|
10 | 8 9 | eqeq12d | |
11 | 10 | rspcv | |
12 | 3 11 | mpan9 | |
13 | 1 2 3 4 | lidrideqd | |
14 | oveq1 | |
|
15 | 14 9 | eqeq12d | |
16 | 15 | rspcv | |
17 | oveq2 | |
|
18 | 17 | adantl | |
19 | simpl | |
|
20 | 18 19 | eqtrd | |
21 | 20 | ex | |
22 | 16 21 | syl6com | |
23 | 22 | com23 | |
24 | 4 13 23 | sylc | |
25 | 24 | imp | |
26 | 5 7 6 1 12 25 | ismgmid2 | |