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 ⊢ B = Base G
grpinveu.p ⊢ + ˙ = + G
grpinveu.o ⊢ 0 ˙ = 0 G
Assertion isgrpid2 ⊢ G ∈ Grp → Z ∈ B ∧ Z + ˙ Z = Z ↔ 0 ˙ = Z

Proof

Step Hyp Ref Expression
1 grpinveu.b ⊢ B = Base G
2 grpinveu.p ⊢ + ˙ = + G
3 grpinveu.o ⊢ 0 ˙ = 0 G
4 1 2 3 grpid ⊢ G ∈ Grp ∧ Z ∈ B → Z + ˙ Z = Z ↔ 0 ˙ = Z
5 4 biimpd ⊢ G ∈ Grp ∧ Z ∈ B → Z + ˙ Z = Z → 0 ˙ = Z
6 5 expimpd ⊢ G ∈ Grp → Z ∈ B ∧ Z + ˙ Z = Z → 0 ˙ = Z
7 1 3 grpidcl ⊢ G ∈ Grp → 0 ˙ ∈ B
8 1 2 3 grplid ⊢ G ∈ Grp ∧ 0 ˙ ∈ B → 0 ˙ + ˙ 0 ˙ = 0 ˙
9 7 8 mpdan ⊢ G ∈ Grp → 0 ˙ + ˙ 0 ˙ = 0 ˙
10 7 9 jca ⊢ G ∈ Grp → 0 ˙ ∈ B ∧ 0 ˙ + ˙ 0 ˙ = 0 ˙
11 eleq1 ⊢ 0 ˙ = Z → 0 ˙ ∈ B ↔ Z ∈ B
12 id ⊢ 0 ˙ = Z → 0 ˙ = Z
13 12 12 oveq12d ⊢ 0 ˙ = Z → 0 ˙ + ˙ 0 ˙ = Z + ˙ Z
14 13 12 eqeq12d ⊢ 0 ˙ = Z → 0 ˙ + ˙ 0 ˙ = 0 ˙ ↔ Z + ˙ Z = Z
15 11 14 anbi12d ⊢ 0 ˙ = Z → 0 ˙ ∈ B ∧ 0 ˙ + ˙ 0 ˙ = 0 ˙ ↔ Z ∈ B ∧ Z + ˙ Z = Z
16 10 15 syl5ibcom ⊢ G ∈ Grp → 0 ˙ = Z → Z ∈ B ∧ Z + ˙ Z = Z
17 6 16 impbid ⊢ G ∈ Grp → Z ∈ B ∧ Z + ˙ Z = Z ↔ 0 ˙ = Z