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	⊢ 𝑉 = ( Base ‘ 𝐺 )
	ablsubsub23.m	⊢ − = ( -g ‘ 𝐺 )
Assertion	ablsubsub23	⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) = 𝐶 ↔ ( 𝐴 − 𝐶 ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ablsubsub23.v	⊢ 𝑉 = ( Base ‘ 𝐺 )
2		ablsubsub23.m	⊢ − = ( -g ‘ 𝐺 )
3		simpl	⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐺 ∈ Abel )
4		simpr3	⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 )
5		simpr2	⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
6		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
7	1 6	ablcom	⊢ ( ( 𝐺 ∈ Abel ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐶 ( +g ‘ 𝐺 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝐺 ) 𝐶 ) )
8	3 4 5 7	syl3anc	⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐶 ( +g ‘ 𝐺 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝐺 ) 𝐶 ) )
9	8	eqeq1d	⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐶 ( +g ‘ 𝐺 ) 𝐵 ) = 𝐴 ↔ ( 𝐵 ( +g ‘ 𝐺 ) 𝐶 ) = 𝐴 ) )
10		ablgrp	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
11	1 6 2	grpsubadd	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) = 𝐶 ↔ ( 𝐶 ( +g ‘ 𝐺 ) 𝐵 ) = 𝐴 ) )
12	10 11	sylan	⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) = 𝐶 ↔ ( 𝐶 ( +g ‘ 𝐺 ) 𝐵 ) = 𝐴 ) )
13		3ancomb	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ↔ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
14	13	biimpi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
15	1 6 2	grpsubadd	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐶 ) = 𝐵 ↔ ( 𝐵 ( +g ‘ 𝐺 ) 𝐶 ) = 𝐴 ) )
16	10 14 15	syl2an	⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐶 ) = 𝐵 ↔ ( 𝐵 ( +g ‘ 𝐺 ) 𝐶 ) = 𝐴 ) )
17	9 12 16	3bitr4d	⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) = 𝐶 ↔ ( 𝐴 − 𝐶 ) = 𝐵 ) )