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	⊢ ( 𝜑 → ( 𝑋 − ( 𝑋 − 𝑌 ) ) = 𝑌 )