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=BaseG
grpsubid.o 0˙=0G
grpsubid.m -˙=-G
Assertion grpsubeq0 GGrpXBYBX-˙Y=0˙X=Y

Proof

Step Hyp Ref Expression
1 grpsubid.b B=BaseG
2 grpsubid.o 0˙=0G
3 grpsubid.m -˙=-G
4 eqid +G=+G
5 eqid invgG=invgG
6 1 4 5 3 grpsubval XBYBX-˙Y=X+GinvgGY
7 6 3adant1 GGrpXBYBX-˙Y=X+GinvgGY
8 7 eqeq1d GGrpXBYBX-˙Y=0˙X+GinvgGY=0˙
9 simp1 GGrpXBYBGGrp
10 1 5 grpinvcl GGrpYBinvgGYB
11 10 3adant2 GGrpXBYBinvgGYB
12 simp2 GGrpXBYBXB
13 1 4 2 5 grpinvid2 GGrpinvgGYBXBinvgGinvgGY=XX+GinvgGY=0˙
14 9 11 12 13 syl3anc GGrpXBYBinvgGinvgGY=XX+GinvgGY=0˙
15 1 5 grpinvinv GGrpYBinvgGinvgGY=Y
16 15 3adant2 GGrpXBYBinvgGinvgGY=Y
17 16 eqeq1d GGrpXBYBinvgGinvgGY=XY=X
18 eqcom Y=XX=Y
19 17 18 bitrdi GGrpXBYBinvgGinvgGY=XX=Y
20 8 14 19 3bitr2d GGrpXBYBX-˙Y=0˙X=Y