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 𝐵 = ( Base ‘ 𝐺 )
grplid.p + = ( +g𝐺 )
grplid.o 0 = ( 0g𝐺 )
grplidd.g ( 𝜑𝐺 ∈ Grp )
grplidd.1 ( 𝜑𝑋𝐵 )
Assertion grplidd ( 𝜑 → ( 0 + 𝑋 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 grpbn0.b 𝐵 = ( Base ‘ 𝐺 )
2 grplid.p + = ( +g𝐺 )
3 grplid.o 0 = ( 0g𝐺 )
4 grplidd.g ( 𝜑𝐺 ∈ Grp )
5 grplidd.1 ( 𝜑𝑋𝐵 )
6 1 2 3 grplid ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 0 + 𝑋 ) = 𝑋 )
7 4 5 6 syl2anc ( 𝜑 → ( 0 + 𝑋 ) = 𝑋 )