Theorem ofcval

Description: Evaluate a function/constant operation at a point. (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Hypotheses	ofcfval.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	ofcfval.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ofcfval.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
	ofcval.6	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = 𝐵 )
Assertion	ofcval	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ∘f/c 𝑅 𝐶 ) ‘ 𝑋 ) = ( 𝐵 𝑅 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		ofcfval.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		ofcfval.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		ofcfval.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
4		ofcval.6	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = 𝐵 )
5		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
6	1 2 3 5	ofcfval	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) )
7	6	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) )
8		simpr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
9	8	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑥 = 𝑋 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
10	9	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑥 = 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) = ( ( 𝐹 ‘ 𝑋 ) 𝑅 𝐶 ) )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
12		ovexd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) 𝑅 𝐶 ) ∈ V )
13	7 10 11 12	fvmptd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ∘f/c 𝑅 𝐶 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) 𝑅 𝐶 ) )
14	4	oveq1d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) 𝑅 𝐶 ) = ( 𝐵 𝑅 𝐶 ) )
15	13 14	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ∘f/c 𝑅 𝐶 ) ‘ 𝑋 ) = ( 𝐵 𝑅 𝐶 ) )