Metamath Proof Explorer


Theorem grpsubeq0

Description: If the difference between two group elements is zero, they are equal. ( subeq0 analog.) (Contributed 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