This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem orbstafun

Description: Existence and uniqueness for the function of orbsta . (Contributed by Mario Carneiro, 15-Jan-2015) (Proof shortened by Mario Carneiro, 23-Dec-2016)

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 ) >. )
Assertion orbstafun 
|- ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> Fun F )

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 ovexd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ k e. X ) -> ( k .(+) A ) e. _V )
6 1 2 gastacl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> H e. ( SubGrp ` G ) )
7 1 3 eqger 
 |-  ( H e. ( SubGrp ` G ) -> .~ Er X )
8 6 7 syl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> .~ Er X )
9 1 fvexi 
 |-  X e. _V
10 9 a1i 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> X e. _V )
11 oveq1 
 |-  ( k = h -> ( k .(+) A ) = ( h .(+) A ) )
12 simpr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ k .~ h ) -> k .~ h )
13 subgrcl 
 |-  ( H e. ( SubGrp ` G ) -> G e. Grp )
14 1 subgss 
 |-  ( H e. ( SubGrp ` G ) -> H C_ X )
15 eqid 
 |-  ( invg ` G ) = ( invg ` G )
16 eqid 
 |-  ( +g ` G ) = ( +g ` G )
17 1 15 16 3 eqgval 
 |-  ( ( G e. Grp /\ H C_ X ) -> ( k .~ h <-> ( k e. X /\ h e. X /\ ( ( ( invg ` G ) ` k ) ( +g ` G ) h ) e. H ) ) )
18 13 14 17 syl2anc 
 |-  ( H e. ( SubGrp ` G ) -> ( k .~ h <-> ( k e. X /\ h e. X /\ ( ( ( invg ` G ) ` k ) ( +g ` G ) h ) e. H ) ) )
19 6 18 syl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> ( k .~ h <-> ( k e. X /\ h e. X /\ ( ( ( invg ` G ) ` k ) ( +g ` G ) h ) e. H ) ) )
20 19 biimpa 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ k .~ h ) -> ( k e. X /\ h e. X /\ ( ( ( invg ` G ) ` k ) ( +g ` G ) h ) e. H ) )
21 20 simp1d 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ k .~ h ) -> k e. X )
22 20 simp2d 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ k .~ h ) -> h e. X )
23 21 22 jca 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ k .~ h ) -> ( k e. X /\ h e. X ) )
24 1 2 3 gastacos 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( k e. X /\ h e. X ) ) -> ( k .~ h <-> ( k .(+) A ) = ( h .(+) A ) ) )
25 23 24 syldan 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ k .~ h ) -> ( k .~ h <-> ( k .(+) A ) = ( h .(+) A ) ) )
26 12 25 mpbid 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ k .~ h ) -> ( k .(+) A ) = ( h .(+) A ) )
27 4 5 8 10 11 26 qliftfund 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> Fun F )