Theorem isgrpid2

Description: Properties showing that an element Z is the identity element of a group. (Contributed by NM, 7-Aug-2013)

	Ref	Expression
Hypotheses	grpinveu.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpinveu.p	⊢ + = ( +g ‘ 𝐺 )
	grpinveu.o	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	isgrpid2	⊢ ( 𝐺 ∈ Grp → ( ( 𝑍 ∈ 𝐵 ∧ ( 𝑍 + 𝑍 ) = 𝑍 ) ↔ 0 = 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		grpinveu.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpinveu.p	⊢ + = ( +g ‘ 𝐺 )
3		grpinveu.o	⊢ 0 = ( 0g ‘ 𝐺 )
4	1 2 3	grpid	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑍 + 𝑍 ) = 𝑍 ↔ 0 = 𝑍 ) )
5	4	biimpd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑍 + 𝑍 ) = 𝑍 → 0 = 𝑍 ) )
6	5	expimpd	⊢ ( 𝐺 ∈ Grp → ( ( 𝑍 ∈ 𝐵 ∧ ( 𝑍 + 𝑍 ) = 𝑍 ) → 0 = 𝑍 ) )
7	1 3	grpidcl	⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝐵 )
8	1 2 3	grplid	⊢ ( ( 𝐺 ∈ Grp ∧ 0 ∈ 𝐵 ) → ( 0 + 0 ) = 0 )
9	7 8	mpdan	⊢ ( 𝐺 ∈ Grp → ( 0 + 0 ) = 0 )
10	7 9	jca	⊢ ( 𝐺 ∈ Grp → ( 0 ∈ 𝐵 ∧ ( 0 + 0 ) = 0 ) )
11		eleq1	⊢ ( 0 = 𝑍 → ( 0 ∈ 𝐵 ↔ 𝑍 ∈ 𝐵 ) )
12		id	⊢ ( 0 = 𝑍 → 0 = 𝑍 )
13	12 12	oveq12d	⊢ ( 0 = 𝑍 → ( 0 + 0 ) = ( 𝑍 + 𝑍 ) )
14	13 12	eqeq12d	⊢ ( 0 = 𝑍 → ( ( 0 + 0 ) = 0 ↔ ( 𝑍 + 𝑍 ) = 𝑍 ) )
15	11 14	anbi12d	⊢ ( 0 = 𝑍 → ( ( 0 ∈ 𝐵 ∧ ( 0 + 0 ) = 0 ) ↔ ( 𝑍 ∈ 𝐵 ∧ ( 𝑍 + 𝑍 ) = 𝑍 ) ) )
16	10 15	syl5ibcom	⊢ ( 𝐺 ∈ Grp → ( 0 = 𝑍 → ( 𝑍 ∈ 𝐵 ∧ ( 𝑍 + 𝑍 ) = 𝑍 ) ) )
17	6 16	impbid	⊢ ( 𝐺 ∈ Grp → ( ( 𝑍 ∈ 𝐵 ∧ ( 𝑍 + 𝑍 ) = 𝑍 ) ↔ 0 = 𝑍 ) )