Theorem ofcc

Description: Left operation by a constant on a mixed operation with a constant. (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Hypotheses	ofcc.1	$$⊢\phi \to A\in V$$
	ofcc.2	$$⊢\phi \to B\in W$$
	ofcc.3	$$⊢\phi \to C\in X$$
Assertion	ofcc	$$⊢\phi \to \left(A\times \left\{B\right\}\right){\circ }_{\mathrm{fc}}RC=A\times \left\{BRC\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ofcc.1	$$⊢\phi \to A\in V$$
2		ofcc.2	$$⊢\phi \to B\in W$$
3		ofcc.3	$$⊢\phi \to C\in X$$
4		fnconstg	$$⊢B\in W\to \left(A\times \left\{B\right\}\right)FnA$$
5	2 4	syl	$$⊢\phi \to \left(A\times \left\{B\right\}\right)FnA$$
6		fvconst2g	$$⊢\left(B\in W\wedge x\in A\right)\to \left(A\times \left\{B\right\}\right)\left(x\right)=B$$
7	2 6	sylan	$$⊢\left(\phi \wedge x\in A\right)\to \left(A\times \left\{B\right\}\right)\left(x\right)=B$$
8	5 1 3 7	ofcfval	$$⊢\phi \to \left(A\times \left\{B\right\}\right){\circ }_{\mathrm{fc}}RC=\left(x\in A⟼BRC\right)$$
9		fconstmpt	$$⊢A\times \left\{BRC\right\}=\left(x\in A⟼BRC\right)$$
10	8 9	eqtr4di	$$⊢\phi \to \left(A\times \left\{B\right\}\right){\circ }_{\mathrm{fc}}RC=A\times \left\{BRC\right\}$$