Theorem grplactval

Description: The value of the left group action of element A of group G at B . (Contributed by Paul Chapman, 18-Mar-2008)

	Ref	Expression
Hypotheses	grplact.1	|- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )
	grplact.2	|- X = ( Base ` G )
Assertion	grplactval	|- ( ( A e. X /\ B e. X ) -> ( ( F ` A ) ` B ) = ( A .+ B ) )

Proof

Step	Hyp	Ref	Expression
1		grplact.1	|- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )
2		grplact.2	|- X = ( Base ` G )
3	1 2	grplactfval	|- ( A e. X -> ( F ` A ) = ( a e. X |-> ( A .+ a ) ) )
4	3	fveq1d	|- ( A e. X -> ( ( F ` A ) ` B ) = ( ( a e. X |-> ( A .+ a ) ) ` B ) )
5		oveq2	|- ( a = B -> ( A .+ a ) = ( A .+ B ) )
6		eqid	|- ( a e. X |-> ( A .+ a ) ) = ( a e. X |-> ( A .+ a ) )
7		ovex	|- ( A .+ B ) e. _V
8	5 6 7	fvmpt	|- ( B e. X -> ( ( a e. X |-> ( A .+ a ) ) ` B ) = ( A .+ B ) )
9	4 8	sylan9eq	|- ( ( A e. X /\ B e. X ) -> ( ( F ` A ) ` B ) = ( A .+ B ) )