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

Metamath Proof Explorer

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 = 𝑍 ) )