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 fovrnd
 |-  ( ( ( .(+) 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 )