Theorem ofcof

Description: Relate function operation with operation with a constant. (Contributed by Thierry Arnoux, 3-Oct-2018)

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

Proof

Step	Hyp	Ref	Expression
1		ofcof.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		ofcof.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		ofcof.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
4	1	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
5		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
6	4 2 3 5	ofcfval	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) )
7		fnconstg	⊢ ( 𝐶 ∈ 𝑊 → ( 𝐴 × { 𝐶 } ) Fn 𝐴 )
8	3 7	syl	⊢ ( 𝜑 → ( 𝐴 × { 𝐶 } ) Fn 𝐴 )
9		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
10		fvconst2g	⊢ ( ( 𝐶 ∈ 𝑊 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐶 } ) ‘ 𝑥 ) = 𝐶 )
11	3 10	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐶 } ) ‘ 𝑥 ) = 𝐶 )
12	4 8 2 2 9 5 11	offval	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 ( 𝐴 × { 𝐶 } ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) )
13	6 12	eqtr4d	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝐹 ∘f 𝑅 ( 𝐴 × { 𝐶 } ) ) )