This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = 𝑋 ) )