This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. X |-> ( a e. X |-> ( g .+ a ) ) )
grplact.2 
|- X = ( Base ` G )
Assertion grplactval 
|- ( ( A e. X /\ B e. X ) -> ( ( F ` A ) ` B ) = ( A .+ B ) )

Proof

Step Hyp Ref Expression
1 grplact.1 
 |-  F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )
2 grplact.2 
 |-  X = ( Base ` G )
3 1 2 grplactfval 
 |-  ( A e. X -> ( F ` A ) = ( a e. X |-> ( A .+ a ) ) )
4 3 fveq1d 
 |-  ( A e. X -> ( ( F ` A ) ` B ) = ( ( a e. X |-> ( A .+ a ) ) ` B ) )
5 oveq2 
 |-  ( a = B -> ( A .+ a ) = ( A .+ B ) )
6 eqid 
 |-  ( a e. X |-> ( A .+ a ) ) = ( a e. X |-> ( A .+ a ) )
7 ovex 
 |-  ( A .+ B ) e. _V
8 5 6 7 fvmpt 
 |-  ( B e. X -> ( ( a e. X |-> ( A .+ a ) ) ` B ) = ( A .+ B ) )
9 4 8 sylan9eq 
 |-  ( ( A e. X /\ B e. X ) -> ( ( F ` A ) ` B ) = ( A .+ B ) )