eqgfval

Description: Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-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	eqgfval	$⊢ (G \in V \land S \subseteq X) \to R = \{⟨x, y⟩ \| (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \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		elex	$⊢ G \in V \to G \in V$
6	1	fvexi	$⊢ X \in V$
7	6	ssex	$⊢ S \subseteq X \to S \in V$
8		simpl	$⊢ (g = G \land s = S) \to g = G$
9	8	fveq2d	$⊢ (g = G \land s = S) \to {Base}_{g} = {Base}_{G}$
10	9 1	eqtr4di	$⊢ (g = G \land s = S) \to {Base}_{g} = X$
11	10	sseq2d	$⊢ (g = G \land s = S) \to (\{x, y\} \subseteq {Base}_{g} \leftrightarrow \{x, y\} \subseteq X)$
12	8	fveq2d	$⊢ (g = G \land s = S) \to +_{g} = +_{G}$
13	12 3	eqtr4di	$⊢ (g = G \land s = S) \to +_{g} = \underset{˙}{+}$
14	8	fveq2d	$⊢ (g = G \land s = S) \to {inv}_{g} (g) = {inv}_{g} (G)$
15	14 2	eqtr4di	$⊢ (g = G \land s = S) \to {inv}_{g} (g) = N$
16	15	fveq1d	$⊢ (g = G \land s = S) \to {inv}_{g} (g) (x) = N (x)$
17		eqidd	$⊢ (g = G \land s = S) \to y = y$
18	13 16 17	oveq123d	$⊢ (g = G \land s = S) \to {inv}_{g} (g) (x) +_{g} y = N (x) \underset{˙}{+} y$
19		simpr	$⊢ (g = G \land s = S) \to s = S$
20	18 19	eleq12d	$⊢ (g = G \land s = S) \to ({inv}_{g} (g) (x) +_{g} y \in s \leftrightarrow N (x) \underset{˙}{+} y \in S)$
21	11 20	anbi12d	$⊢ (g = G \land s = S) \to ((\{x, y\} \subseteq {Base}_{g} \land {inv}_{g} (g) (x) +_{g} y \in s) \leftrightarrow (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S))$
22	21	opabbidv	$⊢ (g = G \land s = S) \to \{⟨x, y⟩ \| (\{x, y\} \subseteq {Base}_{g} \land {inv}_{g} (g) (x) +_{g} y \in s)\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S)\}$
23		df-eqg	$⊢ ~_{QG} = (g \in V, s \in V ⟼ \{⟨x, y⟩ \| (\{x, y\} \subseteq {Base}_{g} \land {inv}_{g} (g) (x) +_{g} y \in s)\})$
24	6 6	xpex	$⊢ X \times X \in V$
25		simpl	$⊢ (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S) \to \{x, y\} \subseteq X$
26		vex	$⊢ x \in V$
27		vex	$⊢ y \in V$
28	26 27	prss	$⊢ (x \in X \land y \in X) \leftrightarrow \{x, y\} \subseteq X$
29	25 28	sylibr	$⊢ (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S) \to (x \in X \land y \in X)$
30	29	ssopab2i	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S)\} \subseteq \{⟨x, y⟩ \| (x \in X \land y \in X)\}$
31		df-xp	$⊢ X \times X = \{⟨x, y⟩ \| (x \in X \land y \in X)\}$
32	30 31	sseqtrri	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S)\} \subseteq X \times X$
33	24 32	ssexi	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S)\} \in V$
34	22 23 33	ovmpoa	$⊢ (G \in V \land S \in V) \to G ~_{QG} S = \{⟨x, y⟩ \| (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S)\}$
35	4 34	syl5eq	$⊢ (G \in V \land S \in V) \to R = \{⟨x, y⟩ \| (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S)\}$
36	5 7 35	syl2an	$⊢ (G \in V \land S \subseteq X) \to R = \{⟨x, y⟩ \| (\{x, y\} \subseteq X \land N (x) \underset{˙}{+} y \in S)\}$

Metamath Proof Explorer

Theorem eqgfval

Proof