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