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	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) = ( 𝐴 + 𝐵 ) )