eqgabl

Description: Value of the subgroup coset equivalence relation on an abelian group. (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	eqgabl.x	$⊢ X = {Base}_{G}$
	eqgabl.n	$⊢ \underset{˙}{-} = -_{G}$
	eqgabl.r	$⊢ \underset{˙}{\sim} = G ~_{QG} S$
Assertion	eqgabl	$⊢ (G \in Abel \land S \subseteq X) \to (A \underset{˙}{\sim} B \leftrightarrow (A \in X \land B \in X \land B \underset{˙}{-} A \in S))$

Proof

Step	Hyp	Ref	Expression
1		eqgabl.x	$⊢ X = {Base}_{G}$
2		eqgabl.n	$⊢ \underset{˙}{-} = -_{G}$
3		eqgabl.r	$⊢ \underset{˙}{\sim} = G ~_{QG} S$
4		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
5		eqid	$⊢ +_{G} = +_{G}$
6	1 4 5 3	eqgval	$⊢ (G \in Abel \land S \subseteq X) \to (A \underset{˙}{\sim} B \leftrightarrow (A \in X \land B \in X \land {inv}_{g} (G) (A) +_{G} B \in S))$
7		simpll	$⊢ ((G \in Abel \land S \subseteq X) \land (A \in X \land B \in X)) \to G \in Abel$
8		ablgrp	$⊢ G \in Abel \to G \in Grp$
9	8	ad2antrr	$⊢ ((G \in Abel \land S \subseteq X) \land (A \in X \land B \in X)) \to G \in Grp$
10		simprl	$⊢ ((G \in Abel \land S \subseteq X) \land (A \in X \land B \in X)) \to A \in X$
11	1 4	grpinvcl	$⊢ (G \in Grp \land A \in X) \to {inv}_{g} (G) (A) \in X$
12	9 10 11	syl2anc	$⊢ ((G \in Abel \land S \subseteq X) \land (A \in X \land B \in X)) \to {inv}_{g} (G) (A) \in X$
13		simprr	$⊢ ((G \in Abel \land S \subseteq X) \land (A \in X \land B \in X)) \to B \in X$
14	1 5	ablcom	$⊢ (G \in Abel \land {inv}_{g} (G) (A) \in X \land B \in X) \to {inv}_{g} (G) (A) +_{G} B = B +_{G} {inv}_{g} (G) (A)$
15	7 12 13 14	syl3anc	$⊢ ((G \in Abel \land S \subseteq X) \land (A \in X \land B \in X)) \to {inv}_{g} (G) (A) +_{G} B = B +_{G} {inv}_{g} (G) (A)$
16	1 5 4 2	grpsubval	$⊢ (B \in X \land A \in X) \to B \underset{˙}{-} A = B +_{G} {inv}_{g} (G) (A)$
17	13 10 16	syl2anc	$⊢ ((G \in Abel \land S \subseteq X) \land (A \in X \land B \in X)) \to B \underset{˙}{-} A = B +_{G} {inv}_{g} (G) (A)$
18	15 17	eqtr4d	$⊢ ((G \in Abel \land S \subseteq X) \land (A \in X \land B \in X)) \to {inv}_{g} (G) (A) +_{G} B = B \underset{˙}{-} A$
19	18	eleq1d	$⊢ ((G \in Abel \land S \subseteq X) \land (A \in X \land B \in X)) \to ({inv}_{g} (G) (A) +_{G} B \in S \leftrightarrow B \underset{˙}{-} A \in S)$
20	19	pm5.32da	$⊢ (G \in Abel \land S \subseteq X) \to (((A \in X \land B \in X) \land {inv}_{g} (G) (A) +_{G} B \in S) \leftrightarrow ((A \in X \land B \in X) \land B \underset{˙}{-} A \in S))$
21		df-3an	$⊢ (A \in X \land B \in X \land {inv}_{g} (G) (A) +_{G} B \in S) \leftrightarrow ((A \in X \land B \in X) \land {inv}_{g} (G) (A) +_{G} B \in S)$
22		df-3an	$⊢ (A \in X \land B \in X \land B \underset{˙}{-} A \in S) \leftrightarrow ((A \in X \land B \in X) \land B \underset{˙}{-} A \in S)$
23	20 21 22	3bitr4g	$⊢ (G \in Abel \land S \subseteq X) \to ((A \in X \land B \in X \land {inv}_{g} (G) (A) +_{G} B \in S) \leftrightarrow (A \in X \land B \in X \land B \underset{˙}{-} A \in S))$
24	6 23	bitrd	$⊢ (G \in Abel \land S \subseteq X) \to (A \underset{˙}{\sim} B \leftrightarrow (A \in X \land B \in X \land B \underset{˙}{-} A \in S))$

Metamath Proof Explorer

Theorem eqgabl

Proof