Theorem ablnncan

Description: Cancellation law for group subtraction. ( nncan 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 )
Assertion	ablnncan	|- ( ph -> ( X .- ( X .- Y ) ) = 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		eqid	|- ( +g ` G ) = ( +g ` G )
7	1 6 2 3 4 4 5	ablsubsub	|- ( ph -> ( X .- ( X .- Y ) ) = ( ( X .- X ) ( +g ` G ) Y ) )
8		ablgrp	|- ( G e. Abel -> G e. Grp )
9	3 8	syl	|- ( ph -> G e. Grp )
10		eqid	|- ( 0g ` G ) = ( 0g ` G )
11	1 10 2	grpsubid	|- ( ( G e. Grp /\ X e. B ) -> ( X .- X ) = ( 0g ` G ) )
12	9 4 11	syl2anc	|- ( ph -> ( X .- X ) = ( 0g ` G ) )
13	12	oveq1d	|- ( ph -> ( ( X .- X ) ( +g ` G ) Y ) = ( ( 0g ` G ) ( +g ` G ) Y ) )
14	1 6 10	grplid	|- ( ( G e. Grp /\ Y e. B ) -> ( ( 0g ` G ) ( +g ` G ) Y ) = Y )
15	9 5 14	syl2anc	|- ( ph -> ( ( 0g ` G ) ( +g ` G ) Y ) = Y )
16	7 13 15	3eqtrd	|- ( ph -> ( X .- ( X .- Y ) ) = Y )