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