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

Proof

Step	Hyp	Ref	Expression
1		grplact.1	⊢ 𝐹 = ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 + 𝑎 ) ) )
2		grplact.2	⊢ 𝑋 = ( Base ‘ 𝐺 )
3		oveq1	⊢ ( 𝑔 = 𝐴 → ( 𝑔 + 𝑎 ) = ( 𝐴 + 𝑎 ) )
4	3	mpteq2dv	⊢ ( 𝑔 = 𝐴 → ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 + 𝑎 ) ) = ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) ) )
5	4 1 2	mptfvmpt	⊢ ( 𝐴 ∈ 𝑋 → ( 𝐹 ‘ 𝐴 ) = ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) ) )