Metamath Proof Explorer


Theorem grplactval

Description: The value of the left group action of element A of group G at B . (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 grplactval A X B X F A B = A + ˙ B

Proof

Step Hyp Ref Expression
1 grplact.1 F = g X a X g + ˙ a
2 grplact.2 X = Base G
3 1 2 grplactfval A X F A = a X A + ˙ a
4 3 fveq1d A X F A B = a X A + ˙ a B
5 oveq2 a = B A + ˙ a = A + ˙ B
6 eqid a X A + ˙ a = a X A + ˙ a
7 ovex A + ˙ B V
8 5 6 7 fvmpt B X a X A + ˙ a B = A + ˙ B
9 4 8 sylan9eq A X B X F A B = A + ˙ B