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	\|- B = ( Base ` G )
		qusecsub.n	\|- .- = ( -g ` G )
		qusecsub.r	\|- .~ = ( G ~QG S )
	Assertion	qusecsub	\|- ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> ( [ X ] .~ = [ Y ] .~ <-> ( Y .- X ) e. S ) )

Proof

Step	Hyp	Ref	Expression
1		qusecsub.x	\|- B = ( Base ` G )
2		qusecsub.n	\|- .- = ( -g ` G )
3		qusecsub.r	\|- .~ = ( G ~QG S )
4	1	subgss	\|- ( S e. ( SubGrp ` G ) -> S C_ B )
5	4	anim2i	\|- ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> ( G e. Abel /\ S C_ B ) )
6	5	adantr	\|- ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> ( G e. Abel /\ S C_ B ) )
7	1 2 3	eqgabl	\|- ( ( G e. Abel /\ S C_ B ) -> ( X .~ Y <-> ( X e. B /\ Y e. B /\ ( Y .- X ) e. S ) ) )
8	6 7	syl	\|- ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> ( X .~ Y <-> ( X e. B /\ Y e. B /\ ( Y .- X ) e. S ) ) )
9	1 3	eqger	\|- ( S e. ( SubGrp ` G ) -> .~ Er B )
10	9	ad2antlr	\|- ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> .~ Er B )
11		simprl	\|- ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> X e. B )
12	10 11	erth	\|- ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> ( X .~ Y <-> [ X ] .~ = [ Y ] .~ ) )
13		df-3an	\|- ( ( X e. B /\ Y e. B /\ ( Y .- X ) e. S ) <-> ( ( X e. B /\ Y e. B ) /\ ( Y .- X ) e. S ) )
14		ibar	\|- ( ( X e. B /\ Y e. B ) -> ( ( Y .- X ) e. S <-> ( ( X e. B /\ Y e. B ) /\ ( Y .- X ) e. S ) ) )
15	14	adantl	\|- ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> ( ( Y .- X ) e. S <-> ( ( X e. B /\ Y e. B ) /\ ( Y .- X ) e. S ) ) )
16	13 15	bitr4id	\|- ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> ( ( X e. B /\ Y e. B /\ ( Y .- X ) e. S ) <-> ( Y .- X ) e. S ) )
17	8 12 16	3bitr3d	\|- ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> ( [ X ] .~ = [ Y ] .~ <-> ( Y .- X ) e. S ) )