Theorem offvalfv

Description: The function operation expressed as a mapping with function values. (Contributed by AV, 6-Apr-2019)

	Ref	Expression
Hypotheses	offvalfv.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	offvalfv.f	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	offvalfv.g	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
Assertion	offvalfv	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		offvalfv.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		offvalfv.f	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
3		offvalfv.g	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
4		fnfvelrn	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
5	2 4	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
6		fnfvelrn	⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ran 𝐺 )
7	3 6	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ran 𝐺 )
8		dffn5	⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
9	2 8	sylib	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
10		dffn5	⊢ ( 𝐺 Fn 𝐴 ↔ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑥 ) ) )
11	3 10	sylib	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑥 ) ) )
12	1 5 7 9 11	offval2	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )