Theorem ofcfval

Description: Value of an operation applied to a function and a constant. (Contributed by Thierry Arnoux, 30-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		ofcfval.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		ofcfval.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		ofcfval.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
4		ofcfval.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
5		df-ofc	⊢ ∘f/c 𝑅 = ( 𝑓 ∈ V , 𝑐 ∈ V ↦ ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 𝑐 ) ) )
6	5	a1i	⊢ ( 𝜑 → ∘f/c 𝑅 = ( 𝑓 ∈ V , 𝑐 ∈ V ↦ ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 𝑐 ) ) ) )
7		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑐 = 𝐶 ) ) → 𝑓 = 𝐹 )
8	7	dmeqd	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑐 = 𝐶 ) ) → dom 𝑓 = dom 𝐹 )
9	7	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑐 = 𝐶 ) ) → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
10		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑐 = 𝐶 ) ) → 𝑐 = 𝐶 )
11	9 10	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑐 = 𝐶 ) ) → ( ( 𝑓 ‘ 𝑥 ) 𝑅 𝑐 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) )
12	8 11	mpteq12dv	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑐 = 𝐶 ) ) → ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 𝑐 ) ) = ( 𝑥 ∈ dom 𝐹 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) )
13		fnex	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
14	1 2 13	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ V )
15	3	elexd	⊢ ( 𝜑 → 𝐶 ∈ V )
16	1	fndmd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
17	16 2	eqeltrd	⊢ ( 𝜑 → dom 𝐹 ∈ 𝑉 )
18	17	mptexd	⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝐹 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) ∈ V )
19	6 12 14 15 18	ovmpod	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝑥 ∈ dom 𝐹 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) )
20	16	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴 ) )
21	20	pm5.32i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) )
22	21 4	sylbi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
23	22	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) = ( 𝐵 𝑅 𝐶 ) )
24	16 23	mpteq12dva	⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝐹 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )
25	19 24	eqtrd	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )