Theorem ablsubsub

Description: Law for double subtraction. (Contributed by NM, 7-Apr-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 )
Assertion	ablsubsub	|- ( ph -> ( X .- ( Y .- Z ) ) = ( ( X .- 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		ablgrp	|- ( G e. Abel -> G e. Grp )
9	4 8	syl	|- ( ph -> G e. Grp )
10	1 2 3	grpsubsub	|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .- ( Y .- Z ) ) = ( X .+ ( Z .- Y ) ) )
11	9 5 6 7 10	syl13anc	|- ( ph -> ( X .- ( Y .- Z ) ) = ( X .+ ( Z .- Y ) ) )
12	1 2 3	grpaddsubass	|- ( ( G e. Grp /\ ( X e. B /\ Z e. B /\ Y e. B ) ) -> ( ( X .+ Z ) .- Y ) = ( X .+ ( Z .- Y ) ) )
13	9 5 7 6 12	syl13anc	|- ( ph -> ( ( X .+ Z ) .- Y ) = ( X .+ ( Z .- Y ) ) )
14	1 2 3	abladdsub	|- ( ( G e. Abel /\ ( X e. B /\ Z e. B /\ Y e. B ) ) -> ( ( X .+ Z ) .- Y ) = ( ( X .- Y ) .+ Z ) )
15	4 5 7 6 14	syl13anc	|- ( ph -> ( ( X .+ Z ) .- Y ) = ( ( X .- Y ) .+ Z ) )
16	11 13 15	3eqtr2d	|- ( ph -> ( X .- ( Y .- Z ) ) = ( ( X .- Y ) .+ Z ) )