This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) = 𝑋 )