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

Metamath Proof Explorer

Theorem orbstaval

Description: Value of the function at a given equivalence class element. (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 orbstaval 
|- ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ B e. X ) -> ( F ` [ B ] .~ ) = ( B .(+) A ) )

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 = B -> ( k .(+) A ) = ( B .(+) A ) )
12 1 2 3 4 orbstafun 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> Fun F )
13 4 5 8 10 11 12 qliftval 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ B e. X ) -> ( F ` [ B ] .~ ) = ( B .(+) A ) )