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 𝐵 = ( Base ‘ 𝐺 )
grpsubid.o 0 = ( 0g𝐺 )
grpsubid.m = ( -g𝐺 )
Assertion grpsubid1 ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝑋 0 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 grpsubid.b 𝐵 = ( Base ‘ 𝐺 )
2 grpsubid.o 0 = ( 0g𝐺 )
3 grpsubid.m = ( -g𝐺 )
4 id ( 𝑋𝐵𝑋𝐵 )
5 1 2 grpidcl ( 𝐺 ∈ Grp → 0𝐵 )
6 eqid ( +g𝐺 ) = ( +g𝐺 )
7 eqid ( invg𝐺 ) = ( invg𝐺 )
8 1 6 7 3 grpsubval ( ( 𝑋𝐵0𝐵 ) → ( 𝑋 0 ) = ( 𝑋 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 0 ) ) )
9 4 5 8 syl2anr ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝑋 0 ) = ( 𝑋 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 0 ) ) )
10 2 7 grpinvid ( 𝐺 ∈ Grp → ( ( invg𝐺 ) ‘ 0 ) = 0 )
11 10 adantr ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( ( invg𝐺 ) ‘ 0 ) = 0 )
12 11 oveq2d ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝑋 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 0 ) ) = ( 𝑋 ( +g𝐺 ) 0 ) )
13 1 6 2 grprid ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝑋 ( +g𝐺 ) 0 ) = 𝑋 )
14 9 12 13 3eqtrd ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝑋 0 ) = 𝑋 )