This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐺 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( [ 𝑋 ] ∼ = [ 𝑌 ] ∼ ↔ ( 𝑌 − 𝑋 ) ∈ 𝑆 ) )