Theorem ablpncan2

Description: Cancellation law for subtraction. (Contributed by NM, 2-Oct-2014)

	Ref	Expression
Hypotheses	ablsubadd.b	|- B = ( Base ` G )
	ablsubadd.p	|- .+ = ( +g ` G )
	ablsubadd.m	|- .- = ( -g ` G )
Assertion	ablpncan2	|- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( ( X .+ Y ) .- X ) = Y )

Proof

Step	Hyp	Ref	Expression
1		ablsubadd.b	|- B = ( Base ` G )
2		ablsubadd.p	|- .+ = ( +g ` G )
3		ablsubadd.m	|- .- = ( -g ` G )
4		simp1	|- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> G e. Abel )
5		simp2	|- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> X e. B )
6		simp3	|- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> Y e. B )
7	1 2 3	abladdsub	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ X e. B ) ) -> ( ( X .+ Y ) .- X ) = ( ( X .- X ) .+ Y ) )
8	4 5 6 5 7	syl13anc	|- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( ( X .+ Y ) .- X ) = ( ( X .- X ) .+ Y ) )
9		ablgrp	|- ( G e. Abel -> G e. Grp )
10	4 9	syl	|- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> G e. Grp )
11		eqid	|- ( 0g ` G ) = ( 0g ` G )
12	1 11 3	grpsubid	|- ( ( G e. Grp /\ X e. B ) -> ( X .- X ) = ( 0g ` G ) )
13	10 5 12	syl2anc	|- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( X .- X ) = ( 0g ` G ) )
14	13	oveq1d	|- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( ( X .- X ) .+ Y ) = ( ( 0g ` G ) .+ Y ) )
15	1 2 11	grplid	|- ( ( G e. Grp /\ Y e. B ) -> ( ( 0g ` G ) .+ Y ) = Y )
16	10 6 15	syl2anc	|- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( ( 0g ` G ) .+ Y ) = Y )
17	8 14 16	3eqtrd	|- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( ( X .+ Y ) .- X ) = Y )