Theorem grpidd

Description: Deduce the identity element of a magma from its properties. (Contributed by Mario Carneiro, 6-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		grpidd.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
2		grpidd.p	⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
3		grpidd.z	⊢ ( 𝜑 → 0 ∈ 𝐵 )
4		grpidd.i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
5		grpidd.j	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 0 ) = 𝑥 )
6		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
7		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
8		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
9	3 1	eleqtrd	⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝐺 ) )
10	1	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Base ‘ 𝐺 ) ) )
11	10	biimpar	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝑥 ∈ 𝐵 )
12	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → + = ( +g ‘ 𝐺 ) )
13	12	oveqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = ( 0 ( +g ‘ 𝐺 ) 𝑥 ) )
14	13 4	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 )
15	11 14	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 0 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 )
16	12	oveqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 0 ) = ( 𝑥 ( +g ‘ 𝐺 ) 0 ) )
17	16 5	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 0 ) = 𝑥 )
18	11 17	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 0 ) = 𝑥 )
19	6 7 8 9 15 18	ismgmid2	⊢ ( 𝜑 → 0 = ( 0g ‘ 𝐺 ) )