Metamath Proof Explorer

Theorem 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 ∈ X | u ⊕ ˙ A = A
orbsta.r ⊢ ∼ ˙ = G ~ QG H
orbsta.f ⊢ F = ran ⁡ k ∈ X ⟼ k ∼ ˙ k ⊕ ˙ A
orbsta.o ⊢ O = x y | x y ⊆ Y ∧ ∃ g ∈ X g ⊕ ˙ x = y
Assertion orbsta ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y → F : X / ∼ ˙ ⟶ 1-1 onto A O

Proof

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