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

Metamath Proof Explorer

Theorem ablsubsub23

Description: Swap subtrahend and result of group subtraction. (Contributed by NM, 14-Dec-2007) (Revised by AV, 7-Oct-2021)

Ref Expression
Hypotheses ablsubsub23.v 
|- V = ( Base ` G )
ablsubsub23.m 
|- .- = ( -g ` G )
Assertion ablsubsub23 
|- ( ( G e. Abel /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .- B ) = C <-> ( A .- C ) = B ) )

Proof

Step Hyp Ref Expression
1 ablsubsub23.v 
 |-  V = ( Base ` G )
2 ablsubsub23.m 
 |-  .- = ( -g ` G )
3 simpl 
 |-  ( ( G e. Abel /\ ( A e. V /\ B e. V /\ C e. V ) ) -> G e. Abel )
4 simpr3 
 |-  ( ( G e. Abel /\ ( A e. V /\ B e. V /\ C e. V ) ) -> C e. V )
5 simpr2 
 |-  ( ( G e. Abel /\ ( A e. V /\ B e. V /\ C e. V ) ) -> B e. V )
6 eqid 
 |-  ( +g ` G ) = ( +g ` G )
7 1 6 ablcom 
 |-  ( ( G e. Abel /\ C e. V /\ B e. V ) -> ( C ( +g ` G ) B ) = ( B ( +g ` G ) C ) )
8 3 4 5 7 syl3anc 
 |-  ( ( G e. Abel /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( C ( +g ` G ) B ) = ( B ( +g ` G ) C ) )
9 8 eqeq1d 
 |-  ( ( G e. Abel /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( C ( +g ` G ) B ) = A <-> ( B ( +g ` G ) C ) = A ) )
10 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
11 1 6 2 grpsubadd 
 |-  ( ( G e. Grp /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .- B ) = C <-> ( C ( +g ` G ) B ) = A ) )
12 10 11 sylan 
 |-  ( ( G e. Abel /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .- B ) = C <-> ( C ( +g ` G ) B ) = A ) )
13 3ancomb 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) <-> ( A e. V /\ C e. V /\ B e. V ) )
14 13 biimpi 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( A e. V /\ C e. V /\ B e. V ) )
15 1 6 2 grpsubadd 
 |-  ( ( G e. Grp /\ ( A e. V /\ C e. V /\ B e. V ) ) -> ( ( A .- C ) = B <-> ( B ( +g ` G ) C ) = A ) )
16 10 14 15 syl2an 
 |-  ( ( G e. Abel /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .- C ) = B <-> ( B ( +g ` G ) C ) = A ) )
17 9 12 16 3bitr4d 
 |-  ( ( G e. Abel /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .- B ) = C <-> ( A .- C ) = B ) )