Theorem ablpnpcan

Description: Cancellation law for mixed addition and subtraction. ( pnpcan analog.) (Contributed by NM, 29-May-2015)

	Ref	Expression
Hypotheses	ablsubadd.b	|- B = ( Base ` G )
	ablsubadd.p	|- .+ = ( +g ` G )
	ablsubadd.m	|- .- = ( -g ` G )
	ablsubsub.g	|- ( ph -> G e. Abel )
	ablsubsub.x	|- ( ph -> X e. B )
	ablsubsub.y	|- ( ph -> Y e. B )
	ablsubsub.z	|- ( ph -> Z e. B )
	ablpnpcan.g	|- ( ph -> G e. Abel )
	ablpnpcan.x	|- ( ph -> X e. B )
	ablpnpcan.y	|- ( ph -> Y e. B )
	ablpnpcan.z	|- ( ph -> Z e. B )
Assertion	ablpnpcan	|- ( ph -> ( ( X .+ Y ) .- ( X .+ Z ) ) = ( Y .- Z ) )

Proof

Step	Hyp	Ref	Expression
1		ablsubadd.b	|- B = ( Base ` G )
2		ablsubadd.p	|- .+ = ( +g ` G )
3		ablsubadd.m	|- .- = ( -g ` G )
4		ablsubsub.g	|- ( ph -> G e. Abel )
5		ablsubsub.x	|- ( ph -> X e. B )
6		ablsubsub.y	|- ( ph -> Y e. B )
7		ablsubsub.z	|- ( ph -> Z e. B )
8		ablpnpcan.g	|- ( ph -> G e. Abel )
9		ablpnpcan.x	|- ( ph -> X e. B )
10		ablpnpcan.y	|- ( ph -> Y e. B )
11		ablpnpcan.z	|- ( ph -> Z e. B )
12	1 2 3	ablsub4	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( X e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .- ( X .+ Z ) ) = ( ( X .- X ) .+ ( Y .- Z ) ) )
13	4 5 6 5 7 12	syl122anc	|- ( ph -> ( ( X .+ Y ) .- ( X .+ Z ) ) = ( ( X .- X ) .+ ( Y .- Z ) ) )
14		ablgrp	|- ( G e. Abel -> G e. Grp )
15	4 14	syl	|- ( ph -> G e. Grp )
16		eqid	|- ( 0g ` G ) = ( 0g ` G )
17	1 16 3	grpsubid	|- ( ( G e. Grp /\ X e. B ) -> ( X .- X ) = ( 0g ` G ) )
18	15 5 17	syl2anc	|- ( ph -> ( X .- X ) = ( 0g ` G ) )
19	18	oveq1d	|- ( ph -> ( ( X .- X ) .+ ( Y .- Z ) ) = ( ( 0g ` G ) .+ ( Y .- Z ) ) )
20	1 3	grpsubcl	|- ( ( G e. Grp /\ Y e. B /\ Z e. B ) -> ( Y .- Z ) e. B )
21	15 6 7 20	syl3anc	|- ( ph -> ( Y .- Z ) e. B )
22	1 2 16	grplid	|- ( ( G e. Grp /\ ( Y .- Z ) e. B ) -> ( ( 0g ` G ) .+ ( Y .- Z ) ) = ( Y .- Z ) )
23	15 21 22	syl2anc	|- ( ph -> ( ( 0g ` G ) .+ ( Y .- Z ) ) = ( Y .- Z ) )
24	13 19 23	3eqtrd	|- ( ph -> ( ( X .+ Y ) .- ( X .+ Z ) ) = ( Y .- Z ) )