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

Metamath Proof Explorer

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