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 ⊢ 𝐹 = ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 + 𝑎 ) ) )
grplact.2 ⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion grplactval ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) = ( 𝐴 + 𝐵 ) )

Proof

Step Hyp Ref Expression
1 grplact.1 ⊢ 𝐹 = ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 + 𝑎 ) ) )
2 grplact.2 ⊢ 𝑋 = ( Base ‘ 𝐺 )
3 1 2 grplactfval ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐹 ‘ 𝐴 ) = ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) ) )
4 3 fveq1d ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) = ( ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) ) ‘ 𝐵 ) )
5 oveq2 ⊢ ( 𝑎 = 𝐵 → ( 𝐴 + 𝑎 ) = ( 𝐴 + 𝐵 ) )
6 eqid ⊢ ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) ) = ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) )
7 ovex ⊢ ( 𝐴 + 𝐵 ) ∈ V
8 5 6 7 fvmpt ⊢ ( 𝐵 ∈ 𝑋 → ( ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) ) ‘ 𝐵 ) = ( 𝐴 + 𝐵 ) )
9 4 8 sylan9eq ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) = ( 𝐴 + 𝐵 ) )