orbsta

Description: The Orbit-Stabilizer theorem. The mapping F is a bijection from the cosets of the stabilizer subgroup of A to the orbit of A . (Contributed by Mario Carneiro, 15-Jan-2015)

	Ref	Expression
Hypotheses	gasta.1	$⊢ X = {Base}_{G}$
	gasta.2	$⊢ H = \{u \in X \| u \underset{˙}{\oplus} A = A\}$
	orbsta.r	$⊢ \underset{˙}{\sim} = G ~_{QG} H$
	orbsta.f	$⊢ F = ran (k \in X ⟼ ⟨[k] \underset{˙}{\sim}, k \underset{˙}{\oplus} A⟩)$
	orbsta.o	$⊢ O = \{⟨x, y⟩ \| (\{x, y\} \subseteq Y \land \exists g \in X g \underset{˙}{\oplus} x = y)\}$
Assertion	orbsta	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to F : X / \underset{˙}{\sim} \underset{1-1 onto}{⟶} [A] O$

Proof

Step	Hyp	Ref	Expression
1		gasta.1	$⊢ X = {Base}_{G}$
2		gasta.2	$⊢ H = \{u \in X \| u \underset{˙}{\oplus} A = A\}$
3		orbsta.r	$⊢ \underset{˙}{\sim} = G ~_{QG} H$
4		orbsta.f	$⊢ F = ran (k \in X ⟼ ⟨[k] \underset{˙}{\sim}, k \underset{˙}{\oplus} A⟩)$
5		orbsta.o	$⊢ O = \{⟨x, y⟩ \| (\{x, y\} \subseteq Y \land \exists g \in X g \underset{˙}{\oplus} x = y)\}$
6	1 2 3 4	orbstafun	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to Fun F$
7		simpr	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to A \in Y$
8	7	adantr	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land k \in X) \to A \in Y$
9	1	gaf	$⊢ \underset{˙}{\oplus} \in (G GrpAct Y) \to \underset{˙}{\oplus} : X \times Y ⟶ Y$
10	9	adantr	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to \underset{˙}{\oplus} : X \times Y ⟶ Y$
11	10	adantr	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land k \in X) \to \underset{˙}{\oplus} : X \times Y ⟶ Y$
12		simpr	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land k \in X) \to k \in X$
13	11 12 8	fovcdmd	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land k \in X) \to k \underset{˙}{\oplus} A \in Y$
14		eqid	$⊢ k \underset{˙}{\oplus} A = k \underset{˙}{\oplus} A$
15		oveq1	$⊢ h = k \to h \underset{˙}{\oplus} A = k \underset{˙}{\oplus} A$
16	15	eqeq1d	$⊢ h = k \to (h \underset{˙}{\oplus} A = k \underset{˙}{\oplus} A \leftrightarrow k \underset{˙}{\oplus} A = k \underset{˙}{\oplus} A)$
17	16	rspcev	$⊢ (k \in X \land k \underset{˙}{\oplus} A = k \underset{˙}{\oplus} A) \to \exists h \in X h \underset{˙}{\oplus} A = k \underset{˙}{\oplus} A$
18	12 14 17	sylancl	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land k \in X) \to \exists h \in X h \underset{˙}{\oplus} A = k \underset{˙}{\oplus} A$
19	5	gaorb	$⊢ A O (k \underset{˙}{\oplus} A) \leftrightarrow (A \in Y \land k \underset{˙}{\oplus} A \in Y \land \exists h \in X h \underset{˙}{\oplus} A = k \underset{˙}{\oplus} A)$
20	8 13 18 19	syl3anbrc	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land k \in X) \to A O (k \underset{˙}{\oplus} A)$
21		ovex	$⊢ k \underset{˙}{\oplus} A \in V$
22		elecg	$⊢ (k \underset{˙}{\oplus} A \in V \land A \in Y) \to (k \underset{˙}{\oplus} A \in [A] O \leftrightarrow A O (k \underset{˙}{\oplus} A))$
23	21 8 22	sylancr	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land k \in X) \to (k \underset{˙}{\oplus} A \in [A] O \leftrightarrow A O (k \underset{˙}{\oplus} A))$
24	20 23	mpbird	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land k \in X) \to k \underset{˙}{\oplus} A \in [A] O$
25	1 2	gastacl	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to H \in SubGrp (G)$
26	1 3	eqger	$⊢ H \in SubGrp (G) \to \underset{˙}{\sim} Er X$
27	25 26	syl	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to \underset{˙}{\sim} Er X$
28	1	fvexi	$⊢ X \in V$
29	28	a1i	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to X \in V$
30	4 24 27 29	qliftf	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to (Fun F \leftrightarrow F : X / \underset{˙}{\sim} ⟶ [A] O)$
31	6 30	mpbid	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to F : X / \underset{˙}{\sim} ⟶ [A] O$
32		eqid	$⊢ X / \underset{˙}{\sim} = X / \underset{˙}{\sim}$
33		fveqeq2	$⊢ [z] \underset{˙}{\sim} = a \to (F ([z] \underset{˙}{\sim}) = F (b) \leftrightarrow F (a) = F (b))$
34		eqeq1	$⊢ [z] \underset{˙}{\sim} = a \to ([z] \underset{˙}{\sim} = b \leftrightarrow a = b)$
35	33 34	imbi12d	$⊢ [z] \underset{˙}{\sim} = a \to ((F ([z] \underset{˙}{\sim}) = F (b) \to [z] \underset{˙}{\sim} = b) \leftrightarrow (F (a) = F (b) \to a = b))$
36	35	ralbidv	$⊢ [z] \underset{˙}{\sim} = a \to (\forall b \in (X / \underset{˙}{\sim}) (F ([z] \underset{˙}{\sim}) = F (b) \to [z] \underset{˙}{\sim} = b) \leftrightarrow \forall b \in (X / \underset{˙}{\sim}) (F (a) = F (b) \to a = b))$
37		fveq2	$⊢ [w] \underset{˙}{\sim} = b \to F ([w] \underset{˙}{\sim}) = F (b)$
38	37	eqeq2d	$⊢ [w] \underset{˙}{\sim} = b \to (F ([z] \underset{˙}{\sim}) = F ([w] \underset{˙}{\sim}) \leftrightarrow F ([z] \underset{˙}{\sim}) = F (b))$
39		eqeq2	$⊢ [w] \underset{˙}{\sim} = b \to ([z] \underset{˙}{\sim} = [w] \underset{˙}{\sim} \leftrightarrow [z] \underset{˙}{\sim} = b)$
40	38 39	imbi12d	$⊢ [w] \underset{˙}{\sim} = b \to ((F ([z] \underset{˙}{\sim}) = F ([w] \underset{˙}{\sim}) \to [z] \underset{˙}{\sim} = [w] \underset{˙}{\sim}) \leftrightarrow (F ([z] \underset{˙}{\sim}) = F (b) \to [z] \underset{˙}{\sim} = b))$
41	1 2 3 4	orbstaval	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land z \in X) \to F ([z] \underset{˙}{\sim}) = z \underset{˙}{\oplus} A$
42	41	adantrr	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land (z \in X \land w \in X)) \to F ([z] \underset{˙}{\sim}) = z \underset{˙}{\oplus} A$
43	1 2 3 4	orbstaval	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land w \in X) \to F ([w] \underset{˙}{\sim}) = w \underset{˙}{\oplus} A$
44	43	adantrl	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land (z \in X \land w \in X)) \to F ([w] \underset{˙}{\sim}) = w \underset{˙}{\oplus} A$
45	42 44	eqeq12d	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land (z \in X \land w \in X)) \to (F ([z] \underset{˙}{\sim}) = F ([w] \underset{˙}{\sim}) \leftrightarrow z \underset{˙}{\oplus} A = w \underset{˙}{\oplus} A)$
46	1 2 3	gastacos	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land (z \in X \land w \in X)) \to (z \underset{˙}{\sim} w \leftrightarrow z \underset{˙}{\oplus} A = w \underset{˙}{\oplus} A)$
47	27	adantr	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land (z \in X \land w \in X)) \to \underset{˙}{\sim} Er X$
48		simprl	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land (z \in X \land w \in X)) \to z \in X$
49	47 48	erth	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land (z \in X \land w \in X)) \to (z \underset{˙}{\sim} w \leftrightarrow [z] \underset{˙}{\sim} = [w] \underset{˙}{\sim})$
50	45 46 49	3bitr2d	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land (z \in X \land w \in X)) \to (F ([z] \underset{˙}{\sim}) = F ([w] \underset{˙}{\sim}) \leftrightarrow [z] \underset{˙}{\sim} = [w] \underset{˙}{\sim})$
51	50	biimpd	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land (z \in X \land w \in X)) \to (F ([z] \underset{˙}{\sim}) = F ([w] \underset{˙}{\sim}) \to [z] \underset{˙}{\sim} = [w] \underset{˙}{\sim})$
52	51	anassrs	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land z \in X) \land w \in X) \to (F ([z] \underset{˙}{\sim}) = F ([w] \underset{˙}{\sim}) \to [z] \underset{˙}{\sim} = [w] \underset{˙}{\sim})$
53	32 40 52	ectocld	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land z \in X) \land b \in (X / \underset{˙}{\sim})) \to (F ([z] \underset{˙}{\sim}) = F (b) \to [z] \underset{˙}{\sim} = b)$
54	53	ralrimiva	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land z \in X) \to \forall b \in (X / \underset{˙}{\sim}) (F ([z] \underset{˙}{\sim}) = F (b) \to [z] \underset{˙}{\sim} = b)$
55	32 36 54	ectocld	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land a \in (X / \underset{˙}{\sim})) \to \forall b \in (X / \underset{˙}{\sim}) (F (a) = F (b) \to a = b)$
56	55	ralrimiva	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to \forall a \in (X / \underset{˙}{\sim}) \forall b \in (X / \underset{˙}{\sim}) (F (a) = F (b) \to a = b)$
57		dff13	$⊢ F : X / \underset{˙}{\sim} \underset{1-1}{⟶} [A] O \leftrightarrow (F : X / \underset{˙}{\sim} ⟶ [A] O \land \forall a \in (X / \underset{˙}{\sim}) \forall b \in (X / \underset{˙}{\sim}) (F (a) = F (b) \to a = b))$
58	31 56 57	sylanbrc	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to F : X / \underset{˙}{\sim} \underset{1-1}{⟶} [A] O$
59		vex	$⊢ h \in V$
60		elecg	$⊢ (h \in V \land A \in Y) \to (h \in [A] O \leftrightarrow A O h)$
61	59 7 60	sylancr	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to (h \in [A] O \leftrightarrow A O h)$
62	5	gaorb	$⊢ A O h \leftrightarrow (A \in Y \land h \in Y \land \exists w \in X w \underset{˙}{\oplus} A = h)$
63	61 62	bitrdi	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to (h \in [A] O \leftrightarrow (A \in Y \land h \in Y \land \exists w \in X w \underset{˙}{\oplus} A = h))$
64	63	biimpa	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land h \in [A] O) \to (A \in Y \land h \in Y \land \exists w \in X w \underset{˙}{\oplus} A = h)$
65	64	simp3d	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land h \in [A] O) \to \exists w \in X w \underset{˙}{\oplus} A = h$
66	3	ovexi	$⊢ \underset{˙}{\sim} \in V$
67	66	ecelqsi	$⊢ w \in X \to [w] \underset{˙}{\sim} \in (X / \underset{˙}{\sim})$
68	43	eqcomd	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land w \in X) \to w \underset{˙}{\oplus} A = F ([w] \underset{˙}{\sim})$
69		fveq2	$⊢ z = [w] \underset{˙}{\sim} \to F (z) = F ([w] \underset{˙}{\sim})$
70	69	rspceeqv	$⊢ ([w] \underset{˙}{\sim} \in (X / \underset{˙}{\sim}) \land w \underset{˙}{\oplus} A = F ([w] \underset{˙}{\sim})) \to \exists z \in (X / \underset{˙}{\sim}) w \underset{˙}{\oplus} A = F (z)$
71	67 68 70	syl2an2	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land w \in X) \to \exists z \in (X / \underset{˙}{\sim}) w \underset{˙}{\oplus} A = F (z)$
72		eqeq1	$⊢ w \underset{˙}{\oplus} A = h \to (w \underset{˙}{\oplus} A = F (z) \leftrightarrow h = F (z))$
73	72	rexbidv	$⊢ w \underset{˙}{\oplus} A = h \to (\exists z \in (X / \underset{˙}{\sim}) w \underset{˙}{\oplus} A = F (z) \leftrightarrow \exists z \in (X / \underset{˙}{\sim}) h = F (z))$
74	71 73	syl5ibcom	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land w \in X) \to (w \underset{˙}{\oplus} A = h \to \exists z \in (X / \underset{˙}{\sim}) h = F (z))$
75	74	rexlimdva	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to (\exists w \in X w \underset{˙}{\oplus} A = h \to \exists z \in (X / \underset{˙}{\sim}) h = F (z))$
76	75	imp	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land \exists w \in X w \underset{˙}{\oplus} A = h) \to \exists z \in (X / \underset{˙}{\sim}) h = F (z)$
77	65 76	syldan	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land h \in [A] O) \to \exists z \in (X / \underset{˙}{\sim}) h = F (z)$
78	77	ralrimiva	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to \forall h \in [A] O \exists z \in (X / \underset{˙}{\sim}) h = F (z)$
79		dffo3	$⊢ F : X / \underset{˙}{\sim} \underset{onto}{⟶} [A] O \leftrightarrow (F : X / \underset{˙}{\sim} ⟶ [A] O \land \forall h \in [A] O \exists z \in (X / \underset{˙}{\sim}) h = F (z))$
80	31 78 79	sylanbrc	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to F : X / \underset{˙}{\sim} \underset{onto}{⟶} [A] O$
81		df-f1o	$⊢ F : X / \underset{˙}{\sim} \underset{1-1 onto}{⟶} [A] O \leftrightarrow (F : X / \underset{˙}{\sim} \underset{1-1}{⟶} [A] O \land F : X / \underset{˙}{\sim} \underset{onto}{⟶} [A] O)$
82	58 80 81	sylanbrc	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to F : X / \underset{˙}{\sim} \underset{1-1 onto}{⟶} [A] O$

Metamath Proof Explorer

Theorem orbsta

Proof