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	$⊢ \underset{˙}{-} = -_{G}$
		qusecsub.r	$⊢ \underset{˙}{\sim} = G ~_{QG} S$
	Assertion	qusecsub	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (X \in B \land Y \in B)) \to ([X] \underset{˙}{\sim} = [Y] \underset{˙}{\sim} \leftrightarrow Y \underset{˙}{-} X \in S)$

Proof

Step	Hyp	Ref	Expression
1		qusecsub.x	$⊢ B = {Base}_{G}$
2		qusecsub.n	$⊢ \underset{˙}{-} = -_{G}$
3		qusecsub.r	$⊢ \underset{˙}{\sim} = G ~_{QG} S$
4	1	subgss	$⊢ S \in SubGrp (G) \to S \subseteq B$
5	4	anim2i	$⊢ (G \in Abel \land S \in SubGrp (G)) \to (G \in Abel \land S \subseteq B)$
6	5	adantr	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (X \in B \land Y \in B)) \to (G \in Abel \land S \subseteq B)$
7	1 2 3	eqgabl	$⊢ (G \in Abel \land S \subseteq B) \to (X \underset{˙}{\sim} Y \leftrightarrow (X \in B \land Y \in B \land Y \underset{˙}{-} X \in S))$
8	6 7	syl	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (X \in B \land Y \in B)) \to (X \underset{˙}{\sim} Y \leftrightarrow (X \in B \land Y \in B \land Y \underset{˙}{-} X \in S))$
9	1 3	eqger	$⊢ S \in SubGrp (G) \to \underset{˙}{\sim} Er B$
10	9	ad2antlr	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (X \in B \land Y \in B)) \to \underset{˙}{\sim} Er B$
11		simprl	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (X \in B \land Y \in B)) \to X \in B$
12	10 11	erth	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (X \in B \land Y \in B)) \to (X \underset{˙}{\sim} Y \leftrightarrow [X] \underset{˙}{\sim} = [Y] \underset{˙}{\sim})$
13		df-3an	$⊢ (X \in B \land Y \in B \land Y \underset{˙}{-} X \in S) \leftrightarrow ((X \in B \land Y \in B) \land Y \underset{˙}{-} X \in S)$
14		ibar	$⊢ (X \in B \land Y \in B) \to (Y \underset{˙}{-} X \in S \leftrightarrow ((X \in B \land Y \in B) \land Y \underset{˙}{-} X \in S))$
15	14	adantl	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (X \in B \land Y \in B)) \to (Y \underset{˙}{-} X \in S \leftrightarrow ((X \in B \land Y \in B) \land Y \underset{˙}{-} X \in S))$
16	13 15	bitr4id	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (X \in B \land Y \in B)) \to ((X \in B \land Y \in B \land Y \underset{˙}{-} X \in S) \leftrightarrow Y \underset{˙}{-} X \in S)$
17	8 12 16	3bitr3d	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (X \in B \land Y \in B)) \to ([X] \underset{˙}{\sim} = [Y] \underset{˙}{\sim} \leftrightarrow Y \underset{˙}{-} X \in S)$