Metamath Proof Explorer


Theorem grplidd

Description: The identity element of a group is a left identity. Deduction associated with grplid . (Contributed by SN, 29-Jan-2025)

Ref Expression
Hypotheses grpbn0.b B = Base G
grplid.p + ˙ = + G
grplid.o 0 ˙ = 0 G
grplidd.g φ G Grp
grplidd.1 φ X B
Assertion grplidd φ 0 ˙ + ˙ X = X

Proof

Step Hyp Ref Expression
1 grpbn0.b B = Base G
2 grplid.p + ˙ = + G
3 grplid.o 0 ˙ = 0 G
4 grplidd.g φ G Grp
5 grplidd.1 φ X B
6 1 2 3 grplid G Grp X B 0 ˙ + ˙ X = X
7 4 5 6 syl2anc φ 0 ˙ + ˙ X = X