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

Metamath Proof Explorer

Theorem ablnnncan1

Description: Cancellation law for group subtraction. ( nnncan1 analog.) (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 ablnnncan1 
|- ( ph -> ( ( X .- Y ) .- ( X .- Z ) ) = ( 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 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
8 3 7 syl 
 |-  ( ph -> G e. Grp )
9 1 2 grpsubcl 
 |-  ( ( G e. Grp /\ X e. B /\ Z e. B ) -> ( X .- Z ) e. B )
10 8 4 6 9 syl3anc 
 |-  ( ph -> ( X .- Z ) e. B )
11 1 2 3 4 5 10 ablsub32 
 |-  ( ph -> ( ( X .- Y ) .- ( X .- Z ) ) = ( ( X .- ( X .- Z ) ) .- Y ) )
12 1 2 3 4 6 ablnncan 
 |-  ( ph -> ( X .- ( X .- Z ) ) = Z )
13 12 oveq1d 
 |-  ( ph -> ( ( X .- ( X .- Z ) ) .- Y ) = ( Z .- Y ) )
14 11 13 eqtrd 
 |-  ( ph -> ( ( X .- Y ) .- ( X .- Z ) ) = ( Z .- Y ) )