Theorem ablpncan3

Description: A cancellation law for Abelian groups. (Contributed by NM, 23-Mar-2015)

	Ref	Expression
Hypotheses	ablsubadd.b	|- B = ( Base ` G )
	ablsubadd.p	|- .+ = ( +g ` G )
	ablsubadd.m	|- .- = ( -g ` G )
Assertion	ablpncan3	|- ( ( 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		simpl	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> G e. Abel )
5		simprl	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> X e. B )
6		ablgrp	|- ( G e. Abel -> G e. Grp )
7	6	adantr	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> G e. Grp )
8		simprr	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> Y e. B )
9	1 3	grpsubcl	|- ( ( G e. Grp /\ Y e. B /\ X e. B ) -> ( Y .- X ) e. B )
10	7 8 5 9	syl3anc	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> ( Y .- X ) e. B )
11	1 2	ablcom	|- ( ( G e. Abel /\ X e. B /\ ( Y .- X ) e. B ) -> ( X .+ ( Y .- X ) ) = ( ( Y .- X ) .+ X ) )
12	4 5 10 11	syl3anc	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> ( X .+ ( Y .- X ) ) = ( ( Y .- X ) .+ X ) )
13	1 2 3	grpnpcan	|- ( ( G e. Grp /\ Y e. B /\ X e. B ) -> ( ( Y .- X ) .+ X ) = Y )
14	7 8 5 13	syl3anc	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> ( ( Y .- X ) .+ X ) = Y )
15	12 14	eqtrd	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> ( X .+ ( Y .- X ) ) = Y )