Metamath Proof Explorer


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