Metamath Proof Explorer

Theorem grpsubeq0

Description: If the difference between two group elements is zero, they are equal. ( subeq0 analog.) (Contributed by Jeff Madsen, 6-Jan-2011) (Revised by NM, 31-Mar-2014)

Ref Expression
Hypotheses grpsubid.b ⊢ B = Base G
grpsubid.o ⊢ 0 ˙ = 0 G
grpsubid.m ⊢ - ˙ = - G
Assertion grpsubeq0 ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B → X - ˙ Y = 0 ˙ ↔ X = Y

Proof

Step Hyp Ref Expression
1 grpsubid.b ⊢ B = Base G
2 grpsubid.o ⊢ 0 ˙ = 0 G
3 grpsubid.m ⊢ - ˙ = - G
4 eqid ⊢ + G = + G
5 eqid ⊢ inv g ⁡ G = inv g ⁡ G
6 1 4 5 3 grpsubval ⊢ X ∈ B ∧ Y ∈ B → X - ˙ Y = X + G inv g ⁡ G ⁡ Y
7 6 3adant1 ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B → X - ˙ Y = X + G inv g ⁡ G ⁡ Y
8 7 eqeq1d ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B → X - ˙ Y = 0 ˙ ↔ X + G inv g ⁡ G ⁡ Y = 0 ˙
9 simp1 ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B → G ∈ Grp
10 1 5 grpinvcl ⊢ G ∈ Grp ∧ Y ∈ B → inv g ⁡ G ⁡ Y ∈ B
11 10 3adant2 ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B → inv g ⁡ G ⁡ Y ∈ B
12 simp2 ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B → X ∈ B
13 1 4 2 5 grpinvid2 ⊢ G ∈ Grp ∧ inv g ⁡ G ⁡ Y ∈ B ∧ X ∈ B → inv g ⁡ G ⁡ inv g ⁡ G ⁡ Y = X ↔ X + G inv g ⁡ G ⁡ Y = 0 ˙
14 9 11 12 13 syl3anc ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B → inv g ⁡ G ⁡ inv g ⁡ G ⁡ Y = X ↔ X + G inv g ⁡ G ⁡ Y = 0 ˙
15 1 5 grpinvinv ⊢ G ∈ Grp ∧ Y ∈ B → inv g ⁡ G ⁡ inv g ⁡ G ⁡ Y = Y
16 15 3adant2 ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B → inv g ⁡ G ⁡ inv g ⁡ G ⁡ Y = Y
17 16 eqeq1d ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B → inv g ⁡ G ⁡ inv g ⁡ G ⁡ Y = X ↔ Y = X
18 eqcom ⊢ Y = X ↔ X = Y
19 17 18 bitrdi ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B → inv g ⁡ G ⁡ inv g ⁡ G ⁡ Y = X ↔ X = Y
20 8 14 19 3bitr2d ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B → X - ˙ Y = 0 ˙ ↔ X = Y