Theorem grpidd2

Description: Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd . (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	grpidd2.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
	grpidd2.p	⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
	grpidd2.z	⊢ ( 𝜑 → 0 ∈ 𝐵 )
	grpidd2.i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
	grpidd2.j	⊢ ( 𝜑 → 𝐺 ∈ Grp )
Assertion	grpidd2	⊢ ( 𝜑 → 0 = ( 0g ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		grpidd2.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
2		grpidd2.p	⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
3		grpidd2.z	⊢ ( 𝜑 → 0 ∈ 𝐵 )
4		grpidd2.i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
5		grpidd2.j	⊢ ( 𝜑 → 𝐺 ∈ Grp )
6	2	oveqd	⊢ ( 𝜑 → ( 0 + 0 ) = ( 0 ( +g ‘ 𝐺 ) 0 ) )
7		oveq2	⊢ ( 𝑥 = 0 → ( 0 + 𝑥 ) = ( 0 + 0 ) )
8		id	⊢ ( 𝑥 = 0 → 𝑥 = 0 )
9	7 8	eqeq12d	⊢ ( 𝑥 = 0 → ( ( 0 + 𝑥 ) = 𝑥 ↔ ( 0 + 0 ) = 0 ) )
10	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 0 + 𝑥 ) = 𝑥 )
11	9 10 3	rspcdva	⊢ ( 𝜑 → ( 0 + 0 ) = 0 )
12	6 11	eqtr3d	⊢ ( 𝜑 → ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 )
13	3 1	eleqtrd	⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝐺 ) )
14		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
15		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
16		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
17	14 15 16	grpid	⊢ ( ( 𝐺 ∈ Grp ∧ 0 ∈ ( Base ‘ 𝐺 ) ) → ( ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 ↔ ( 0g ‘ 𝐺 ) = 0 ) )
18	5 13 17	syl2anc	⊢ ( 𝜑 → ( ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 ↔ ( 0g ‘ 𝐺 ) = 0 ) )
19	12 18	mpbid	⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) = 0 )
20	19	eqcomd	⊢ ( 𝜑 → 0 = ( 0g ‘ 𝐺 ) )