Theorem ablnnncan

Description: Cancellation law for group subtraction. ( nnncan analog.) (Contributed by NM, 29-Feb-2008) (Revised by AV, 27-Aug-2021)

	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	ablnnncan	|- ( ph -> ( ( X .- ( Y .- Z ) ) .- Z ) = ( X .- 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		ablgrp	|- ( G e. Abel -> G e. Grp )
9	3 8	syl	|- ( ph -> G e. Grp )
10	1 2	grpsubcl	|- ( ( G e. Grp /\ Y e. B /\ Z e. B ) -> ( Y .- Z ) e. B )
11	9 5 6 10	syl3anc	|- ( ph -> ( Y .- Z ) e. B )
12	1 7 2 3 4 11 6	ablsubsub4	|- ( ph -> ( ( X .- ( Y .- Z ) ) .- Z ) = ( X .- ( ( Y .- Z ) ( +g ` G ) Z ) ) )
13	1 7	ablcom	|- ( ( G e. Abel /\ ( Y .- Z ) e. B /\ Z e. B ) -> ( ( Y .- Z ) ( +g ` G ) Z ) = ( Z ( +g ` G ) ( Y .- Z ) ) )
14	3 11 6 13	syl3anc	|- ( ph -> ( ( Y .- Z ) ( +g ` G ) Z ) = ( Z ( +g ` G ) ( Y .- Z ) ) )
15	1 7 2	ablpncan3	|- ( ( G e. Abel /\ ( Z e. B /\ Y e. B ) ) -> ( Z ( +g ` G ) ( Y .- Z ) ) = Y )
16	3 6 5 15	syl12anc	|- ( ph -> ( Z ( +g ` G ) ( Y .- Z ) ) = Y )
17	14 16	eqtrd	|- ( ph -> ( ( Y .- Z ) ( +g ` G ) Z ) = Y )
18	17	oveq2d	|- ( ph -> ( X .- ( ( Y .- Z ) ( +g ` G ) Z ) ) = ( X .- Y ) )
19	12 18	eqtrd	|- ( ph -> ( ( X .- ( Y .- Z ) ) .- Z ) = ( X .- Y ) )