Theorem ablnnncan1

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

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

Proof

Step	Hyp	Ref	Expression
1		ablnncan.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		ablnncan.m	⊢ − = ( -g ‘ 𝐺 )
3		ablnncan.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
4		ablnncan.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		ablnncan.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		ablsub32.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
7		ablgrp	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
8	3 7	syl	⊢ ( 𝜑 → 𝐺 ∈ Grp )
9	1 2	grpsubcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 − 𝑍 ) ∈ 𝐵 )
10	8 4 6 9	syl3anc	⊢ ( 𝜑 → ( 𝑋 − 𝑍 ) ∈ 𝐵 )
11	1 2 3 4 5 10	ablsub32	⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) − ( 𝑋 − 𝑍 ) ) = ( ( 𝑋 − ( 𝑋 − 𝑍 ) ) − 𝑌 ) )
12	1 2 3 4 6	ablnncan	⊢ ( 𝜑 → ( 𝑋 − ( 𝑋 − 𝑍 ) ) = 𝑍 )
13	12	oveq1d	⊢ ( 𝜑 → ( ( 𝑋 − ( 𝑋 − 𝑍 ) ) − 𝑌 ) = ( 𝑍 − 𝑌 ) )
14	11 13	eqtrd	⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) − ( 𝑋 − 𝑍 ) ) = ( 𝑍 − 𝑌 ) )