Theorem ablnnncan1

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

	Ref	Expression
Hypotheses	ablnncan.b	|- B = ( Base ` G )
	ablnncan.m	|- .- = ( -g ` G )
	ablnncan.g	|- ( ph -> G e. Abel )
	ablnncan.x	|- ( ph -> X e. B )
	ablnncan.y	|- ( ph -> Y e. B )
	ablsub32.z	|- ( ph -> Z e. B )
Assertion	ablnnncan1	|- ( ph -> ( ( X .- Y ) .- ( X .- Z ) ) = ( Z .- Y ) )

Proof

Step	Hyp	Ref	Expression
1		ablnncan.b	|- B = ( Base ` G )
2		ablnncan.m	|- .- = ( -g ` G )
3		ablnncan.g	|- ( ph -> G e. Abel )
4		ablnncan.x	|- ( ph -> X e. B )
5		ablnncan.y	|- ( ph -> Y e. B )
6		ablsub32.z	|- ( ph -> Z e. B )
7		ablgrp	|- ( G e. Abel -> G e. Grp )
8	3 7	syl	|- ( ph -> G e. Grp )
9	1 2	grpsubcl	|- ( ( G e. Grp /\ X e. B /\ Z e. B ) -> ( X .- Z ) e. B )
10	8 4 6 9	syl3anc	|- ( ph -> ( X .- Z ) e. B )
11	1 2 3 4 5 10	ablsub32	|- ( ph -> ( ( X .- Y ) .- ( X .- Z ) ) = ( ( X .- ( X .- Z ) ) .- Y ) )
12	1 2 3 4 6	ablnncan	|- ( ph -> ( X .- ( X .- Z ) ) = Z )
13	12	oveq1d	|- ( ph -> ( ( X .- ( X .- Z ) ) .- Y ) = ( Z .- Y ) )
14	11 13	eqtrd	|- ( ph -> ( ( X .- Y ) .- ( X .- Z ) ) = ( Z .- Y ) )