Metamath Proof Explorer


Theorem qusecsub

Description: Two subgroup cosets are equal if and only if the difference of their representatives is a member of the subgroup. (Contributed by AV, 7-Mar-2025)

Ref Expression
Hypotheses qusecsub.x 𝐵 = ( Base ‘ 𝐺 )
qusecsub.n = ( -g𝐺 )
qusecsub.r = ( 𝐺 ~QG 𝑆 )
Assertion qusecsub ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( [ 𝑋 ] = [ 𝑌 ] ↔ ( 𝑌 𝑋 ) ∈ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 qusecsub.x 𝐵 = ( Base ‘ 𝐺 )
2 qusecsub.n = ( -g𝐺 )
3 qusecsub.r = ( 𝐺 ~QG 𝑆 )
4 1 subgss ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆𝐵 )
5 4 anim2i ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 ∈ Abel ∧ 𝑆𝐵 ) )
6 5 adantr ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝐺 ∈ Abel ∧ 𝑆𝐵 ) )
7 1 2 3 eqgabl ( ( 𝐺 ∈ Abel ∧ 𝑆𝐵 ) → ( 𝑋 𝑌 ↔ ( 𝑋𝐵𝑌𝐵 ∧ ( 𝑌 𝑋 ) ∈ 𝑆 ) ) )
8 6 7 syl ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 𝑌 ↔ ( 𝑋𝐵𝑌𝐵 ∧ ( 𝑌 𝑋 ) ∈ 𝑆 ) ) )
9 1 3 eqger ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → Er 𝐵 )
10 9 ad2antlr ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ) → Er 𝐵 )
11 simprl ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ) → 𝑋𝐵 )
12 10 11 erth ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 𝑌 ↔ [ 𝑋 ] = [ 𝑌 ] ) )
13 df-3an ( ( 𝑋𝐵𝑌𝐵 ∧ ( 𝑌 𝑋 ) ∈ 𝑆 ) ↔ ( ( 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑌 𝑋 ) ∈ 𝑆 ) )
14 ibar ( ( 𝑋𝐵𝑌𝐵 ) → ( ( 𝑌 𝑋 ) ∈ 𝑆 ↔ ( ( 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑌 𝑋 ) ∈ 𝑆 ) ) )
15 14 adantl ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( ( 𝑌 𝑋 ) ∈ 𝑆 ↔ ( ( 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑌 𝑋 ) ∈ 𝑆 ) ) )
16 13 15 bitr4id ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( ( 𝑋𝐵𝑌𝐵 ∧ ( 𝑌 𝑋 ) ∈ 𝑆 ) ↔ ( 𝑌 𝑋 ) ∈ 𝑆 ) )
17 8 12 16 3bitr3d ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( [ 𝑋 ] = [ 𝑌 ] ↔ ( 𝑌 𝑋 ) ∈ 𝑆 ) )