Theorem grpnnncan2

Description: Cancellation law for group subtraction. ( nnncan2 analog.) (Contributed by NM, 15-Feb-2008) (Revised by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	grpnnncan2.b	|- B = ( Base ` G )
	grpnnncan2.m	|- .- = ( -g ` G )
Assertion	grpnnncan2	|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Z ) .- ( Y .- Z ) ) = ( X .- Y ) )

Proof

Step	Hyp	Ref	Expression
1		grpnnncan2.b	|- B = ( Base ` G )
2		grpnnncan2.m	|- .- = ( -g ` G )
3		simpl	|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> G e. Grp )
4		simpr1	|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B )
5		simpr3	|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. B )
6	1 2	grpsubcl	|- ( ( G e. Grp /\ Y e. B /\ Z e. B ) -> ( Y .- Z ) e. B )
7	6	3adant3r1	|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y .- Z ) e. B )
8		eqid	|- ( +g ` G ) = ( +g ` G )
9	1 8 2	grpsubsub4	|- ( ( G e. Grp /\ ( X e. B /\ Z e. B /\ ( Y .- Z ) e. B ) ) -> ( ( X .- Z ) .- ( Y .- Z ) ) = ( X .- ( ( Y .- Z ) ( +g ` G ) Z ) ) )
10	3 4 5 7 9	syl13anc	|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Z ) .- ( Y .- Z ) ) = ( X .- ( ( Y .- Z ) ( +g ` G ) Z ) ) )
11	1 8 2	grpnpcan	|- ( ( G e. Grp /\ Y e. B /\ Z e. B ) -> ( ( Y .- Z ) ( +g ` G ) Z ) = Y )
12	11	3adant3r1	|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Y .- Z ) ( +g ` G ) Z ) = Y )
13	12	oveq2d	|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .- ( ( Y .- Z ) ( +g ` G ) Z ) ) = ( X .- Y ) )
14	10 13	eqtrd	|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Z ) .- ( Y .- Z ) ) = ( X .- Y ) )