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