Theorem ablsubsub4

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	ablsubsub4	|- ( 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 3	grpsubcl	|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .- Y ) e. B )
11	9 5 6 10	syl3anc	|- ( ph -> ( X .- Y ) e. B )
12		eqid	|- ( invg ` G ) = ( invg ` G )
13	1 2 12 3	grpsubval	|- ( ( ( X .- Y ) e. B /\ Z e. B ) -> ( ( X .- Y ) .- Z ) = ( ( X .- Y ) .+ ( ( invg ` G ) ` Z ) ) )
14	11 7 13	syl2anc	|- ( ph -> ( ( X .- Y ) .- Z ) = ( ( X .- Y ) .+ ( ( invg ` G ) ` Z ) ) )
15	1 12	grpinvcl	|- ( ( G e. Grp /\ Z e. B ) -> ( ( invg ` G ) ` Z ) e. B )
16	9 7 15	syl2anc	|- ( ph -> ( ( invg ` G ) ` Z ) e. B )
17	1 2 3 4 5 6 16	ablsubsub	|- ( ph -> ( X .- ( Y .- ( ( invg ` G ) ` Z ) ) ) = ( ( X .- Y ) .+ ( ( invg ` G ) ` Z ) ) )
18	1 2 3 12 9 6 7	grpsubinv	|- ( ph -> ( Y .- ( ( invg ` G ) ` Z ) ) = ( Y .+ Z ) )
19	18	oveq2d	|- ( ph -> ( X .- ( Y .- ( ( invg ` G ) ` Z ) ) ) = ( X .- ( Y .+ Z ) ) )
20	14 17 19	3eqtr2d	|- ( ph -> ( ( X .- Y ) .- Z ) = ( X .- ( Y .+ Z ) ) )