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

Metamath Proof Explorer

Theorem ablnncan

Description: Cancellation law for group subtraction. ( nncan 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 )
Assertion ablnncan 
|- ( ph -> ( X .- ( X .- Y ) ) = 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 eqid 
 |-  ( +g ` G ) = ( +g ` G )
7 1 6 2 3 4 4 5 ablsubsub 
 |-  ( ph -> ( X .- ( X .- Y ) ) = ( ( X .- X ) ( +g ` G ) Y ) )
8 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
9 3 8 syl 
 |-  ( ph -> G e. Grp )
10 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
11 1 10 2 grpsubid 
 |-  ( ( G e. Grp /\ X e. B ) -> ( X .- X ) = ( 0g ` G ) )
12 9 4 11 syl2anc 
 |-  ( ph -> ( X .- X ) = ( 0g ` G ) )
13 12 oveq1d 
 |-  ( ph -> ( ( X .- X ) ( +g ` G ) Y ) = ( ( 0g ` G ) ( +g ` G ) Y ) )
14 1 6 10 grplid 
 |-  ( ( G e. Grp /\ Y e. B ) -> ( ( 0g ` G ) ( +g ` G ) Y ) = Y )
15 9 5 14 syl2anc 
 |-  ( ph -> ( ( 0g ` G ) ( +g ` G ) Y ) = Y )
16 7 13 15 3eqtrd 
 |-  ( ph -> ( X .- ( X .- Y ) ) = Y )