Theorem ofcof

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

	Ref	Expression
Hypotheses	ofcof.1	$$⊢\phi \to F:A⟶B$$
	ofcof.2	$$⊢\phi \to A\in V$$
	ofcof.3	$$⊢\phi \to C\in W$$
Assertion	ofcof	$$⊢\phi \to F{\circ }_{\mathrm{fc}}RC=F{R}_f\left(A\times \left\{C\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ofcof.1	$$⊢\phi \to F:A⟶B$$
2		ofcof.2	$$⊢\phi \to A\in V$$
3		ofcof.3	$$⊢\phi \to C\in W$$
4	1	ffnd	$$⊢\phi \to FFnA$$
5		eqidd	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=F\left(x\right)$$
6	4 2 3 5	ofcfval	$$⊢\phi \to F{\circ }_{\mathrm{fc}}RC=\left(x\in A⟼F\left(x\right)RC\right)$$
7		fnconstg	$$⊢C\in W\to \left(A\times \left\{C\right\}\right)FnA$$
8	3 7	syl	$$⊢\phi \to \left(A\times \left\{C\right\}\right)FnA$$
9		inidm	$$⊢A\cap A=A$$
10		fvconst2g	$$⊢\left(C\in W\wedge x\in A\right)\to \left(A\times \left\{C\right\}\right)\left(x\right)=C$$
11	3 10	sylan	$$⊢\left(\phi \wedge x\in A\right)\to \left(A\times \left\{C\right\}\right)\left(x\right)=C$$
12	4 8 2 2 9 5 11	offval	$$⊢\phi \to F{R}_f\left(A\times \left\{C\right\}\right)=\left(x\in A⟼F\left(x\right)RC\right)$$
13	6 12	eqtr4d	$$⊢\phi \to F{\circ }_{\mathrm{fc}}RC=F{R}_f\left(A\times \left\{C\right\}\right)$$