Metamath Proof Explorer


Theorem grpid

Description: Two ways of saying that an element of a group is the identity element. Provides a convenient way to compute the value of the identity element. (Contributed by NM, 24-Aug-2011)

Ref Expression
Hypotheses grpinveu.b 𝐵 = ( Base ‘ 𝐺 )
grpinveu.p + = ( +g𝐺 )
grpinveu.o 0 = ( 0g𝐺 )
Assertion grpid ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( ( 𝑋 + 𝑋 ) = 𝑋0 = 𝑋 ) )

Proof

Step Hyp Ref Expression
1 grpinveu.b 𝐵 = ( Base ‘ 𝐺 )
2 grpinveu.p + = ( +g𝐺 )
3 grpinveu.o 0 = ( 0g𝐺 )
4 eqcom ( 0 = 𝑋𝑋 = 0 )
5 1 3 grpidcl ( 𝐺 ∈ Grp → 0𝐵 )
6 1 2 grprcan ( ( 𝐺 ∈ Grp ∧ ( 𝑋𝐵0𝐵𝑋𝐵 ) ) → ( ( 𝑋 + 𝑋 ) = ( 0 + 𝑋 ) ↔ 𝑋 = 0 ) )
7 6 3exp2 ( 𝐺 ∈ Grp → ( 𝑋𝐵 → ( 0𝐵 → ( 𝑋𝐵 → ( ( 𝑋 + 𝑋 ) = ( 0 + 𝑋 ) ↔ 𝑋 = 0 ) ) ) ) )
8 5 7 mpid ( 𝐺 ∈ Grp → ( 𝑋𝐵 → ( 𝑋𝐵 → ( ( 𝑋 + 𝑋 ) = ( 0 + 𝑋 ) ↔ 𝑋 = 0 ) ) ) )
9 8 pm2.43d ( 𝐺 ∈ Grp → ( 𝑋𝐵 → ( ( 𝑋 + 𝑋 ) = ( 0 + 𝑋 ) ↔ 𝑋 = 0 ) ) )
10 9 imp ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( ( 𝑋 + 𝑋 ) = ( 0 + 𝑋 ) ↔ 𝑋 = 0 ) )
11 1 2 3 grplid ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 0 + 𝑋 ) = 𝑋 )
12 11 eqeq2d ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( ( 𝑋 + 𝑋 ) = ( 0 + 𝑋 ) ↔ ( 𝑋 + 𝑋 ) = 𝑋 ) )
13 10 12 bitr3d ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝑋 = 0 ↔ ( 𝑋 + 𝑋 ) = 𝑋 ) )
14 4 13 bitr2id ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( ( 𝑋 + 𝑋 ) = 𝑋0 = 𝑋 ) )