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