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=BaseG
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=BaseG
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+GB=B+GC
8 3 4 5 7 syl3anc ⊢G∈Abel∧A∈V∧B∈V∧C∈V→C+GB=B+GC
9 8 eqeq1d ⊢G∈Abel∧A∈V∧B∈V∧C∈V→C+GB=A↔B+GC=A
10 ablgrp ⊢G∈Abel→G∈Grp
11 1 6 2 grpsubadd ⊢G∈Grp∧A∈V∧B∈V∧C∈V→A-˙B=C↔C+GB=A
12 10 11 sylan ⊢G∈Abel∧A∈V∧B∈V∧C∈V→A-˙B=C↔C+GB=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+GC=A
16 10 14 15 syl2an ⊢G∈Abel∧A∈V∧B∈V∧C∈V→A-˙C=B↔B+GC=A
17 9 12 16 3bitr4d ⊢G∈Abel∧A∈V∧B∈V∧C∈V→A-˙B=C↔A-˙C=B