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