This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )