eqgval

Description: Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015) (Revised by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	eqgval.x	$⊢ X = {Base}_{G}$
	eqgval.n	$⊢ N = {inv}_{g} (G)$
	eqgval.p	$⊢ \underset{˙}{+} = +_{G}$
	eqgval.r	$⊢ R = G ~_{QG} S$
Assertion	eqgval	$⊢ (G \in V \land S \subseteq X) \to (A R B \leftrightarrow (A \in X \land B \in X \land N (A) \underset{˙}{+} B \in S))$

Proof

Step	Hyp	Ref	Expression
1		eqgval.x	$⊢ X = {Base}_{G}$
2		eqgval.n	$⊢ N = {inv}_{g} (G)$
3		eqgval.p	$⊢ \underset{˙}{+} = +_{G}$
4		eqgval.r	$⊢ R = G ~_{QG} S$
5	1 2 3 4	eqgfval	$⊢ (G \in V \land S \subseteq X) \to R = \{⟨x, y⟩ \| (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S)\}$
6	5	breqd	$⊢ (G \in V \land S \subseteq X) \to (A R B \leftrightarrow A \{⟨x, y⟩ \| (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S)\} B)$
7		brabv	$⊢ A \{⟨x, y⟩ \| (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S)\} B \to (A \in V \land B \in V)$
8	7	adantl	$⊢ ((G \in V \land S \subseteq X) \land A \{⟨x, y⟩ \| (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S)\} B) \to (A \in V \land B \in V)$
9		simpr1	$⊢ ((G \in V \land S \subseteq X) \land (A \in X \land B \in X \land N (A) \underset{˙}{+} B \in S)) \to A \in X$
10	9	elexd	$⊢ ((G \in V \land S \subseteq X) \land (A \in X \land B \in X \land N (A) \underset{˙}{+} B \in S)) \to A \in V$
11		simpr2	$⊢ ((G \in V \land S \subseteq X) \land (A \in X \land B \in X \land N (A) \underset{˙}{+} B \in S)) \to B \in X$
12	11	elexd	$⊢ ((G \in V \land S \subseteq X) \land (A \in X \land B \in X \land N (A) \underset{˙}{+} B \in S)) \to B \in V$
13	10 12	jca	$⊢ ((G \in V \land S \subseteq X) \land (A \in X \land B \in X \land N (A) \underset{˙}{+} B \in S)) \to (A \in V \land B \in V)$
14		vex	$⊢ x \in V$
15		vex	$⊢ y \in V$
16	14 15	prss	$⊢ (x \in X \land y \in X) \leftrightarrow \{x, y\} \subseteq X$
17		eleq1	$⊢ x = A \to (x \in X \leftrightarrow A \in X)$
18		eleq1	$⊢ y = B \to (y \in X \leftrightarrow B \in X)$
19	17 18	bi2anan9	$⊢ (x = A \land y = B) \to ((x \in X \land y \in X) \leftrightarrow (A \in X \land B \in X))$
20	16 19	bitr3id	$⊢ (x = A \land y = B) \to (\{x, y\} \subseteq X \leftrightarrow (A \in X \land B \in X))$
21		fveq2	$⊢ x = A \to N (x) = N (A)$
22		id	$⊢ y = B \to y = B$
23	21 22	oveqan12d	$⊢ (x = A \land y = B) \to N (x) \underset{˙}{+} y = N (A) \underset{˙}{+} B$
24	23	eleq1d	$⊢ (x = A \land y = B) \to (N (x) \underset{˙}{+} y \in S \leftrightarrow N (A) \underset{˙}{+} B \in S)$
25	20 24	anbi12d	$⊢ (x = A \land y = B) \to ((\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S) \leftrightarrow ((A \in X \land B \in X) \land N (A) \underset{˙}{+} B \in S))$
26		df-3an	$⊢ (A \in X \land B \in X \land N (A) \underset{˙}{+} B \in S) \leftrightarrow ((A \in X \land B \in X) \land N (A) \underset{˙}{+} B \in S)$
27	25 26	bitr4di	$⊢ (x = A \land y = B) \to ((\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S) \leftrightarrow (A \in X \land B \in X \land N (A) \underset{˙}{+} B \in S))$
28		eqid	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S)\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S)\}$
29	27 28	brabga	$⊢ (A \in V \land B \in V) \to (A \{⟨x, y⟩ \| (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S)\} B \leftrightarrow (A \in X \land B \in X \land N (A) \underset{˙}{+} B \in S))$
30	8 13 29	pm5.21nd	$⊢ (G \in V \land S \subseteq X) \to (A \{⟨x, y⟩ \| (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S)\} B \leftrightarrow (A \in X \land B \in X \land N (A) \underset{˙}{+} B \in S))$
31	6 30	bitrd	$⊢ (G \in V \land S \subseteq X) \to (A R B \leftrightarrow (A \in X \land B \in X \land N (A) \underset{˙}{+} B \in S))$

Metamath Proof Explorer

Theorem eqgval

Proof