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