Metamath Proof Explorer


Theorem eqgabl

Description: Value of the subgroup coset equivalence relation on an abelian group. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses eqgabl.x
|- X = ( Base ` G )
eqgabl.n
|- .- = ( -g ` G )
eqgabl.r
|- .~ = ( G ~QG S )
Assertion eqgabl
|- ( ( G e. Abel /\ S C_ X ) -> ( A .~ B <-> ( A e. X /\ B e. X /\ ( B .- A ) e. S ) ) )

Proof

Step Hyp Ref Expression
1 eqgabl.x
 |-  X = ( Base ` G )
2 eqgabl.n
 |-  .- = ( -g ` G )
3 eqgabl.r
 |-  .~ = ( G ~QG S )
4 eqid
 |-  ( invg ` G ) = ( invg ` G )
5 eqid
 |-  ( +g ` G ) = ( +g ` G )
6 1 4 5 3 eqgval
 |-  ( ( G e. Abel /\ S C_ X ) -> ( A .~ B <-> ( A e. X /\ B e. X /\ ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) e. S ) ) )
7 simpll
 |-  ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> G e. Abel )
8 ablgrp
 |-  ( G e. Abel -> G e. Grp )
9 8 ad2antrr
 |-  ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> G e. Grp )
10 simprl
 |-  ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> A e. X )
11 1 4 grpinvcl
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( invg ` G ) ` A ) e. X )
12 9 10 11 syl2anc
 |-  ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( invg ` G ) ` A ) e. X )
13 simprr
 |-  ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> B e. X )
14 1 5 ablcom
 |-  ( ( G e. Abel /\ ( ( invg ` G ) ` A ) e. X /\ B e. X ) -> ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) = ( B ( +g ` G ) ( ( invg ` G ) ` A ) ) )
15 7 12 13 14 syl3anc
 |-  ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) = ( B ( +g ` G ) ( ( invg ` G ) ` A ) ) )
16 1 5 4 2 grpsubval
 |-  ( ( B e. X /\ A e. X ) -> ( B .- A ) = ( B ( +g ` G ) ( ( invg ` G ) ` A ) ) )
17 13 10 16 syl2anc
 |-  ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( B .- A ) = ( B ( +g ` G ) ( ( invg ` G ) ` A ) ) )
18 15 17 eqtr4d
 |-  ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) = ( B .- A ) )
19 18 eleq1d
 |-  ( ( ( G e. Abel /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) e. S <-> ( B .- A ) e. S ) )
20 19 pm5.32da
 |-  ( ( G e. Abel /\ S C_ X ) -> ( ( ( A e. X /\ B e. X ) /\ ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) e. S ) <-> ( ( A e. X /\ B e. X ) /\ ( B .- A ) e. S ) ) )
21 df-3an
 |-  ( ( A e. X /\ B e. X /\ ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) e. S ) <-> ( ( A e. X /\ B e. X ) /\ ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) e. S ) )
22 df-3an
 |-  ( ( A e. X /\ B e. X /\ ( B .- A ) e. S ) <-> ( ( A e. X /\ B e. X ) /\ ( B .- A ) e. S ) )
23 20 21 22 3bitr4g
 |-  ( ( G e. Abel /\ S C_ X ) -> ( ( A e. X /\ B e. X /\ ( ( ( invg ` G ) ` A ) ( +g ` G ) B ) e. S ) <-> ( A e. X /\ B e. X /\ ( B .- A ) e. S ) ) )
24 6 23 bitrd
 |-  ( ( G e. Abel /\ S C_ X ) -> ( A .~ B <-> ( A e. X /\ B e. X /\ ( B .- A ) e. S ) ) )