Theorem grplactfval

Description: The left group action of element A of group G . (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	grplactfval	|- ( A e. X -> ( F ` A ) = ( a e. X |-> ( A .+ a ) ) )

Proof

Step	Hyp	Ref	Expression
1		grplact.1	|- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )
2		grplact.2	|- X = ( Base ` G )
3		oveq1	|- ( g = A -> ( g .+ a ) = ( A .+ a ) )
4	3	mpteq2dv	|- ( g = A -> ( a e. X |-> ( g .+ a ) ) = ( a e. X |-> ( A .+ a ) ) )
5	4 1 2	mptfvmpt	|- ( A e. X -> ( F ` A ) = ( a e. X |-> ( A .+ a ) ) )