Theorem ofcfval4

Description: The function/constant operation expressed as an operation composition. (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Hypotheses	ofcfval4.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	ofcfval4.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ofcfval4.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
Assertion	ofcfval4	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑅 𝐶 ) ) ∘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		ofcfval4.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		ofcfval4.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		ofcfval4.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
4	1	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
5	4	mpteq1d	⊢ ( 𝜑 → ( 𝑦 ∈ dom 𝐹 ↦ ( ( 𝐹 ‘ 𝑦 ) 𝑅 𝐶 ) ) = ( 𝑦 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑦 ) 𝑅 𝐶 ) ) )
6	1 2	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
7		ofcfval3	⊢ ( ( 𝐹 ∈ V ∧ 𝐶 ∈ 𝑊 ) → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝑦 ∈ dom 𝐹 ↦ ( ( 𝐹 ‘ 𝑦 ) 𝑅 𝐶 ) ) )
8	6 3 7	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝑦 ∈ dom 𝐹 ↦ ( ( 𝐹 ‘ 𝑦 ) 𝑅 𝐶 ) ) )
9	1	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 )
10	1	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) )
11		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑅 𝐶 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑅 𝐶 ) ) )
12		oveq1	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝑥 𝑅 𝐶 ) = ( ( 𝐹 ‘ 𝑦 ) 𝑅 𝐶 ) )
13	9 10 11 12	fmptco	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑅 𝐶 ) ) ∘ 𝐹 ) = ( 𝑦 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑦 ) 𝑅 𝐶 ) ) )
14	5 8 13	3eqtr4d	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑅 𝐶 ) ) ∘ 𝐹 ) )