Description: The identity element of a group is a right identity. Deduction associated with grprid . (Contributed by SN, 29-Jan-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | grpbn0.b | |- B = ( Base ` G ) |
|
grplid.p | |- .+ = ( +g ` G ) |
||
grplid.o | |- .0. = ( 0g ` G ) |
||
grplidd.g | |- ( ph -> G e. Grp ) |
||
grplidd.1 | |- ( ph -> X e. B ) |
||
Assertion | grpridd | |- ( ph -> ( X .+ .0. ) = X ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grpbn0.b | |- B = ( Base ` G ) |
|
2 | grplid.p | |- .+ = ( +g ` G ) |
|
3 | grplid.o | |- .0. = ( 0g ` G ) |
|
4 | grplidd.g | |- ( ph -> G e. Grp ) |
|
5 | grplidd.1 | |- ( ph -> X e. B ) |
|
6 | 1 2 3 | grprid | |- ( ( G e. Grp /\ X e. B ) -> ( X .+ .0. ) = X ) |
7 | 4 5 6 | syl2anc | |- ( ph -> ( X .+ .0. ) = X ) |