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 X a X g + ˙ a
grplact.2 X = Base G
Assertion grplactfval A X F A = a X A + ˙ a

Proof

Step Hyp Ref Expression
1 grplact.1 F = g X a X g + ˙ a
2 grplact.2 X = Base G
3 oveq1 g = A g + ˙ a = A + ˙ a
4 3 mpteq2dv g = A a X g + ˙ a = a X A + ˙ a
5 4 1 2 mptfvmpt A X F A = a X A + ˙ a