Theorem ablsub32

Description: Swap the second and third terms in a double group subtraction. (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 )
	ablsub32.z	|- ( ph -> Z e. B )
Assertion	ablsub32	|- ( ph -> ( ( X .- Y ) .- Z ) = ( ( X .- Z ) .- 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		ablsub32.z	|- ( ph -> Z e. B )
7		eqid	|- ( +g ` G ) = ( +g ` G )
8	1 7	ablcom	|- ( ( G e. Abel /\ Y e. B /\ Z e. B ) -> ( Y ( +g ` G ) Z ) = ( Z ( +g ` G ) Y ) )
9	3 5 6 8	syl3anc	|- ( ph -> ( Y ( +g ` G ) Z ) = ( Z ( +g ` G ) Y ) )
10	9	oveq2d	|- ( ph -> ( X .- ( Y ( +g ` G ) Z ) ) = ( X .- ( Z ( +g ` G ) Y ) ) )
11	1 7 2 3 4 5 6	ablsubsub4	|- ( ph -> ( ( X .- Y ) .- Z ) = ( X .- ( Y ( +g ` G ) Z ) ) )
12	1 7 2 3 4 6 5	ablsubsub4	|- ( ph -> ( ( X .- Z ) .- Y ) = ( X .- ( Z ( +g ` G ) Y ) ) )
13	10 11 12	3eqtr4d	|- ( ph -> ( ( X .- Y ) .- Z ) = ( ( X .- Z ) .- Y ) )