Description: The left group action of element A of group G . (Contributed by Paul Chapman, 18-Mar-2008)
Ref | Expression | ||
---|---|---|---|
Hypotheses | grplact.1 | ||
grplact.2 | |||
Assertion | grplactfval |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grplact.1 | ||
2 | grplact.2 | ||
3 | oveq1 | ||
4 | 3 | mpteq2dv | |
5 | 4 1 2 | mptfvmpt |