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 e. X | ( u .(+) A ) = A }
orbsta.r 
|- .~ = ( G ~QG H )
orbsta.f 
|- F = ran ( k e. X |-> <. [ k ] .~ , ( k .(+) A ) >. )
orbsta.o 
|- O = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }
Assertion orbsta 
|- ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> F : ( X /. .~ ) -1-1-onto-> [ A ] O )

Proof

Step Hyp Ref Expression
1 gasta.1 
 |-  X = ( Base ` G )
2 gasta.2 
 |-  H = { u e. X | ( u .(+) A ) = A }
3 orbsta.r 
 |-  .~ = ( G ~QG H )
4 orbsta.f 
 |-  F = ran ( k e. X |-> <. [ k ] .~ , ( k .(+) A ) >. )
5 orbsta.o 
 |-  O = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }
6 1 2 3 4 orbstafun 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> Fun F )
7 simpr 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> A e. Y )
8 7 adantr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ k e. X ) -> A e. Y )
9 1 gaf 
 |-  ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) --> Y )
10 9 adantr 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> .(+) : ( X X. Y ) --> Y )
11 10 adantr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ k e. X ) -> .(+) : ( X X. Y ) --> Y )
12 simpr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ k e. X ) -> k e. X )
13 11 12 8 fovcdmd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ k e. X ) -> ( k .(+) A ) e. 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 e. X /\ ( k .(+) A ) = ( k .(+) A ) ) -> E. h e. X ( h .(+) A ) = ( k .(+) A ) )
18 12 14 17 sylancl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ k e. X ) -> E. h e. X ( h .(+) A ) = ( k .(+) A ) )
19 5 gaorb 
 |-  ( A O ( k .(+) A ) <-> ( A e. Y /\ ( k .(+) A ) e. Y /\ E. h e. X ( h .(+) A ) = ( k .(+) A ) ) )
20 8 13 18 19 syl3anbrc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ k e. X ) -> A O ( k .(+) A ) )
21 ovex 
 |-  ( k .(+) A ) e. _V
22 elecg 
 |-  ( ( ( k .(+) A ) e. _V /\ A e. Y ) -> ( ( k .(+) A ) e. [ A ] O <-> A O ( k .(+) A ) ) )
23 21 8 22 sylancr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ k e. X ) -> ( ( k .(+) A ) e. [ A ] O <-> A O ( k .(+) A ) ) )
24 20 23 mpbird 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ k e. X ) -> ( k .(+) A ) e. [ A ] O )
25 1 2 gastacl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> H e. ( SubGrp ` G ) )
26 1 3 eqger 
 |-  ( H e. ( SubGrp ` G ) -> .~ Er X )
27 25 26 syl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> .~ Er X )
28 1 fvexi 
 |-  X e. _V
29 28 a1i 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> X e. _V )
30 4 24 27 29 qliftf 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> ( Fun F <-> F : ( X /. .~ ) --> [ A ] O ) )
31 6 30 mpbid 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. 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 -> ( A. b e. ( X /. .~ ) ( ( F ` [ z ] .~ ) = ( F ` b ) -> [ z ] .~ = b ) <-> A. b e. ( 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 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ z e. X ) -> ( F ` [ z ] .~ ) = ( z .(+) A ) )
42 41 adantrr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( z e. X /\ w e. X ) ) -> ( F ` [ z ] .~ ) = ( z .(+) A ) )
43 1 2 3 4 orbstaval 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ w e. X ) -> ( F ` [ w ] .~ ) = ( w .(+) A ) )
44 43 adantrl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( z e. X /\ w e. X ) ) -> ( F ` [ w ] .~ ) = ( w .(+) A ) )
45 42 44 eqeq12d 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( z e. X /\ w e. X ) ) -> ( ( F ` [ z ] .~ ) = ( F ` [ w ] .~ ) <-> ( z .(+) A ) = ( w .(+) A ) ) )
46 1 2 3 gastacos 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( z e. X /\ w e. X ) ) -> ( z .~ w <-> ( z .(+) A ) = ( w .(+) A ) ) )
47 27 adantr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( z e. X /\ w e. X ) ) -> .~ Er X )
48 simprl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( z e. X /\ w e. X ) ) -> z e. X )
49 47 48 erth 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( z e. X /\ w e. X ) ) -> ( z .~ w <-> [ z ] .~ = [ w ] .~ ) )
50 45 46 49 3bitr2d 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( z e. X /\ w e. X ) ) -> ( ( F ` [ z ] .~ ) = ( F ` [ w ] .~ ) <-> [ z ] .~ = [ w ] .~ ) )
51 50 biimpd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( z e. X /\ w e. X ) ) -> ( ( F ` [ z ] .~ ) = ( F ` [ w ] .~ ) -> [ z ] .~ = [ w ] .~ ) )
52 51 anassrs 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ z e. X ) /\ w e. X ) -> ( ( F ` [ z ] .~ ) = ( F ` [ w ] .~ ) -> [ z ] .~ = [ w ] .~ ) )
53 32 40 52 ectocld 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ z e. X ) /\ b e. ( X /. .~ ) ) -> ( ( F ` [ z ] .~ ) = ( F ` b ) -> [ z ] .~ = b ) )
54 53 ralrimiva 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ z e. X ) -> A. b e. ( X /. .~ ) ( ( F ` [ z ] .~ ) = ( F ` b ) -> [ z ] .~ = b ) )
55 32 36 54 ectocld 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ a e. ( X /. .~ ) ) -> A. b e. ( X /. .~ ) ( ( F ` a ) = ( F ` b ) -> a = b ) )
56 55 ralrimiva 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> A. a e. ( X /. .~ ) A. b e. ( X /. .~ ) ( ( F ` a ) = ( F ` b ) -> a = b ) )
57 dff13 
 |-  ( F : ( X /. .~ ) -1-1-> [ A ] O <-> ( F : ( X /. .~ ) --> [ A ] O /\ A. a e. ( X /. .~ ) A. b e. ( X /. .~ ) ( ( F ` a ) = ( F ` b ) -> a = b ) ) )
58 31 56 57 sylanbrc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> F : ( X /. .~ ) -1-1-> [ A ] O )
59 vex 
 |-  h e. _V
60 elecg 
 |-  ( ( h e. _V /\ A e. Y ) -> ( h e. [ A ] O <-> A O h ) )
61 59 7 60 sylancr 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> ( h e. [ A ] O <-> A O h ) )
62 5 gaorb 
 |-  ( A O h <-> ( A e. Y /\ h e. Y /\ E. w e. X ( w .(+) A ) = h ) )
63 61 62 bitrdi 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> ( h e. [ A ] O <-> ( A e. Y /\ h e. Y /\ E. w e. X ( w .(+) A ) = h ) ) )
64 63 biimpa 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ h e. [ A ] O ) -> ( A e. Y /\ h e. Y /\ E. w e. X ( w .(+) A ) = h ) )
65 64 simp3d 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ h e. [ A ] O ) -> E. w e. X ( w .(+) A ) = h )
66 3 ovexi 
 |-  .~ e. _V
67 66 ecelqsi 
 |-  ( w e. X -> [ w ] .~ e. ( X /. .~ ) )
68 43 eqcomd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ w e. X ) -> ( w .(+) A ) = ( F ` [ w ] .~ ) )
69 fveq2 
 |-  ( z = [ w ] .~ -> ( F ` z ) = ( F ` [ w ] .~ ) )
70 69 rspceeqv 
 |-  ( ( [ w ] .~ e. ( X /. .~ ) /\ ( w .(+) A ) = ( F ` [ w ] .~ ) ) -> E. z e. ( X /. .~ ) ( w .(+) A ) = ( F ` z ) )
71 67 68 70 syl2an2 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ w e. X ) -> E. z e. ( X /. .~ ) ( w .(+) A ) = ( F ` z ) )
72 eqeq1 
 |-  ( ( w .(+) A ) = h -> ( ( w .(+) A ) = ( F ` z ) <-> h = ( F ` z ) ) )
73 72 rexbidv 
 |-  ( ( w .(+) A ) = h -> ( E. z e. ( X /. .~ ) ( w .(+) A ) = ( F ` z ) <-> E. z e. ( X /. .~ ) h = ( F ` z ) ) )
74 71 73 syl5ibcom 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ w e. X ) -> ( ( w .(+) A ) = h -> E. z e. ( X /. .~ ) h = ( F ` z ) ) )
75 74 rexlimdva 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> ( E. w e. X ( w .(+) A ) = h -> E. z e. ( X /. .~ ) h = ( F ` z ) ) )
76 75 imp 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ E. w e. X ( w .(+) A ) = h ) -> E. z e. ( X /. .~ ) h = ( F ` z ) )
77 65 76 syldan 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ h e. [ A ] O ) -> E. z e. ( X /. .~ ) h = ( F ` z ) )
78 77 ralrimiva 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> A. h e. [ A ] O E. z e. ( X /. .~ ) h = ( F ` z ) )
79 dffo3 
 |-  ( F : ( X /. .~ ) -onto-> [ A ] O <-> ( F : ( X /. .~ ) --> [ A ] O /\ A. h e. [ A ] O E. z e. ( X /. .~ ) h = ( F ` z ) ) )
80 31 78 79 sylanbrc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. 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 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> F : ( X /. .~ ) -1-1-onto-> [ A ] O )