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 𝑋 = ( Base ‘ 𝐺 )
eqgabl.n = ( -g𝐺 )
eqgabl.r = ( 𝐺 ~QG 𝑆 )
Assertion eqgabl ( ( 𝐺 ∈ Abel ∧ 𝑆𝑋 ) → ( 𝐴 𝐵 ↔ ( 𝐴𝑋𝐵𝑋 ∧ ( 𝐵 𝐴 ) ∈ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 eqgabl.x 𝑋 = ( Base ‘ 𝐺 )
2 eqgabl.n = ( -g𝐺 )
3 eqgabl.r = ( 𝐺 ~QG 𝑆 )
4 eqid ( invg𝐺 ) = ( invg𝐺 )
5 eqid ( +g𝐺 ) = ( +g𝐺 )
6 1 4 5 3 eqgval ( ( 𝐺 ∈ Abel ∧ 𝑆𝑋 ) → ( 𝐴 𝐵 ↔ ( 𝐴𝑋𝐵𝑋 ∧ ( ( ( invg𝐺 ) ‘ 𝐴 ) ( +g𝐺 ) 𝐵 ) ∈ 𝑆 ) ) )
7 simpll ( ( ( 𝐺 ∈ Abel ∧ 𝑆𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → 𝐺 ∈ Abel )
8 ablgrp ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
9 8 ad2antrr ( ( ( 𝐺 ∈ Abel ∧ 𝑆𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → 𝐺 ∈ Grp )
10 simprl ( ( ( 𝐺 ∈ Abel ∧ 𝑆𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → 𝐴𝑋 )
11 1 4 grpinvcl ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) → ( ( invg𝐺 ) ‘ 𝐴 ) ∈ 𝑋 )
12 9 10 11 syl2anc ( ( ( 𝐺 ∈ Abel ∧ 𝑆𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( ( invg𝐺 ) ‘ 𝐴 ) ∈ 𝑋 )
13 simprr ( ( ( 𝐺 ∈ Abel ∧ 𝑆𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → 𝐵𝑋 )
14 1 5 ablcom ( ( 𝐺 ∈ Abel ∧ ( ( invg𝐺 ) ‘ 𝐴 ) ∈ 𝑋𝐵𝑋 ) → ( ( ( invg𝐺 ) ‘ 𝐴 ) ( +g𝐺 ) 𝐵 ) = ( 𝐵 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 𝐴 ) ) )
15 7 12 13 14 syl3anc ( ( ( 𝐺 ∈ Abel ∧ 𝑆𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( ( ( invg𝐺 ) ‘ 𝐴 ) ( +g𝐺 ) 𝐵 ) = ( 𝐵 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 𝐴 ) ) )
16 1 5 4 2 grpsubval ( ( 𝐵𝑋𝐴𝑋 ) → ( 𝐵 𝐴 ) = ( 𝐵 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 𝐴 ) ) )
17 13 10 16 syl2anc ( ( ( 𝐺 ∈ Abel ∧ 𝑆𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( 𝐵 𝐴 ) = ( 𝐵 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 𝐴 ) ) )
18 15 17 eqtr4d ( ( ( 𝐺 ∈ Abel ∧ 𝑆𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( ( ( invg𝐺 ) ‘ 𝐴 ) ( +g𝐺 ) 𝐵 ) = ( 𝐵 𝐴 ) )
19 18 eleq1d ( ( ( 𝐺 ∈ Abel ∧ 𝑆𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( ( ( ( invg𝐺 ) ‘ 𝐴 ) ( +g𝐺 ) 𝐵 ) ∈ 𝑆 ↔ ( 𝐵 𝐴 ) ∈ 𝑆 ) )
20 19 pm5.32da ( ( 𝐺 ∈ Abel ∧ 𝑆𝑋 ) → ( ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( ( ( invg𝐺 ) ‘ 𝐴 ) ( +g𝐺 ) 𝐵 ) ∈ 𝑆 ) ↔ ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐵 𝐴 ) ∈ 𝑆 ) ) )
21 df-3an ( ( 𝐴𝑋𝐵𝑋 ∧ ( ( ( invg𝐺 ) ‘ 𝐴 ) ( +g𝐺 ) 𝐵 ) ∈ 𝑆 ) ↔ ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( ( ( invg𝐺 ) ‘ 𝐴 ) ( +g𝐺 ) 𝐵 ) ∈ 𝑆 ) )
22 df-3an ( ( 𝐴𝑋𝐵𝑋 ∧ ( 𝐵 𝐴 ) ∈ 𝑆 ) ↔ ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐵 𝐴 ) ∈ 𝑆 ) )
23 20 21 22 3bitr4g ( ( 𝐺 ∈ Abel ∧ 𝑆𝑋 ) → ( ( 𝐴𝑋𝐵𝑋 ∧ ( ( ( invg𝐺 ) ‘ 𝐴 ) ( +g𝐺 ) 𝐵 ) ∈ 𝑆 ) ↔ ( 𝐴𝑋𝐵𝑋 ∧ ( 𝐵 𝐴 ) ∈ 𝑆 ) ) )
24 6 23 bitrd ( ( 𝐺 ∈ Abel ∧ 𝑆𝑋 ) → ( 𝐴 𝐵 ↔ ( 𝐴𝑋𝐵𝑋 ∧ ( 𝐵 𝐴 ) ∈ 𝑆 ) ) )