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

Metamath Proof Explorer

Theorem ablsub32

Description: Swap the second and third terms in a double group subtraction. (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 ablsub32 
|- ( ph -> ( ( X .- Y ) .- Z ) = ( ( X .- 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 eqid 
 |-  ( +g ` G ) = ( +g ` G )
8 1 7 ablcom 
 |-  ( ( G e. Abel /\ Y e. B /\ Z e. B ) -> ( Y ( +g ` G ) Z ) = ( Z ( +g ` G ) Y ) )
9 3 5 6 8 syl3anc 
 |-  ( ph -> ( Y ( +g ` G ) Z ) = ( Z ( +g ` G ) Y ) )
10 9 oveq2d 
 |-  ( ph -> ( X .- ( Y ( +g ` G ) Z ) ) = ( X .- ( Z ( +g ` G ) Y ) ) )
11 1 7 2 3 4 5 6 ablsubsub4 
 |-  ( ph -> ( ( X .- Y ) .- Z ) = ( X .- ( Y ( +g ` G ) Z ) ) )
12 1 7 2 3 4 6 5 ablsubsub4 
 |-  ( ph -> ( ( X .- Z ) .- Y ) = ( X .- ( Z ( +g ` G ) Y ) ) )
13 10 11 12 3eqtr4d 
 |-  ( ph -> ( ( X .- Y ) .- Z ) = ( ( X .- Z ) .- Y ) )