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
Assertion ablsubsub23 ⊢ G ∈ Abel ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A - ˙ B = C ↔ A - ˙ C = B

Proof

Step Hyp Ref Expression
1 ablsubsub23.v ⊢ V = Base G
2 ablsubsub23.m ⊢ - ˙ = - G
3 simpl ⊢ G ∈ Abel ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → G ∈ Abel
4 simpr3 ⊢ G ∈ Abel ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → C ∈ V
5 simpr2 ⊢ G ∈ Abel ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → B ∈ V
6 eqid ⊢ + G = + G
7 1 6 ablcom ⊢ G ∈ Abel ∧ C ∈ V ∧ B ∈ V → C + G B = B + G C
8 3 4 5 7 syl3anc ⊢ G ∈ Abel ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → C + G B = B + G C
9 8 eqeq1d ⊢ G ∈ Abel ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → C + G B = A ↔ B + G C = A
10 ablgrp ⊢ G ∈ Abel → G ∈ Grp
11 1 6 2 grpsubadd ⊢ G ∈ Grp ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A - ˙ B = C ↔ C + G B = A
12 10 11 sylan ⊢ G ∈ Abel ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A - ˙ B = C ↔ C + G B = A
13 3ancomb ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ↔ A ∈ V ∧ C ∈ V ∧ B ∈ V
14 13 biimpi ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → A ∈ V ∧ C ∈ V ∧ B ∈ V
15 1 6 2 grpsubadd ⊢ G ∈ Grp ∧ A ∈ V ∧ C ∈ V ∧ B ∈ V → A - ˙ C = B ↔ B + G C = A
16 10 14 15 syl2an ⊢ G ∈ Abel ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A - ˙ C = B ↔ B + G C = A
17 9 12 16 3bitr4d ⊢ G ∈ Abel ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A - ˙ B = C ↔ A - ˙ C = B