Metamath Proof Explorer


Theorem grpsubid1

Description: Subtraction of the identity from a group element. (Contributed by Mario Carneiro, 14-Jan-2015)

Ref Expression
Hypotheses grpsubid.b B = Base G
grpsubid.o 0 ˙ = 0 G
grpsubid.m - ˙ = - G
Assertion grpsubid1 G Grp X B X - ˙ 0 ˙ = X

Proof

Step Hyp Ref Expression
1 grpsubid.b B = Base G
2 grpsubid.o 0 ˙ = 0 G
3 grpsubid.m - ˙ = - G
4 id X B X B
5 1 2 grpidcl G Grp 0 ˙ B
6 eqid + G = + G
7 eqid inv g G = inv g G
8 1 6 7 3 grpsubval X B 0 ˙ B X - ˙ 0 ˙ = X + G inv g G 0 ˙
9 4 5 8 syl2anr G Grp X B X - ˙ 0 ˙ = X + G inv g G 0 ˙
10 2 7 grpinvid G Grp inv g G 0 ˙ = 0 ˙
11 10 adantr G Grp X B inv g G 0 ˙ = 0 ˙
12 11 oveq2d G Grp X B X + G inv g G 0 ˙ = X + G 0 ˙
13 1 6 2 grprid G Grp X B X + G 0 ˙ = X
14 9 12 13 3eqtrd G Grp X B X - ˙ 0 ˙ = X