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 ) |