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