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

Metamath Proof Explorer

Theorem ablnncan

Description: Cancellation law for group subtraction. ( nncan analog.) (Contributed by NM, 7-Apr-2015)

Ref Expression
Hypotheses ablnncan.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablnncan.m ⊢ − = ( -g ‘ 𝐺 )
ablnncan.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
ablnncan.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
ablnncan.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion ablnncan ( 𝜑 → ( 𝑋 − ( 𝑋 − 𝑌 ) ) = 𝑌 )

Proof

Step Hyp Ref Expression
1 ablnncan.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ablnncan.m ⊢ − = ( -g ‘ 𝐺 )
3 ablnncan.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
4 ablnncan.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 ablnncan.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
7 1 6 2 3 4 4 5 ablsubsub ⊢ ( 𝜑 → ( 𝑋 − ( 𝑋 − 𝑌 ) ) = ( ( 𝑋 − 𝑋 ) ( +g ‘ 𝐺 ) 𝑌 ) )
8 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
9 3 8 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
10 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
11 1 10 2 grpsubid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 − 𝑋 ) = ( 0g ‘ 𝐺 ) )
12 9 4 11 syl2anc ⊢ ( 𝜑 → ( 𝑋 − 𝑋 ) = ( 0g ‘ 𝐺 ) )
13 12 oveq1d ⊢ ( 𝜑 → ( ( 𝑋 − 𝑋 ) ( +g ‘ 𝐺 ) 𝑌 ) = ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑌 ) )
14 1 6 10 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑌 ) = 𝑌 )
15 9 5 14 syl2anc ⊢ ( 𝜑 → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑌 ) = 𝑌 )
16 7 13 15 3eqtrd ⊢ ( 𝜑 → ( 𝑋 − ( 𝑋 − 𝑌 ) ) = 𝑌 )