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

Metamath Proof Explorer

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 ‘ 𝐺 ) )