Theorem mulc1cncfg

Description: A version of mulc1cncf using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 30-Jun-2017)

	Ref	Expression
Hypotheses	mulc1cncfg.1	$$⊢\underset{\_}{Ⅎ}xF$$
	mulc1cncfg.2	$$⊢Ⅎx\phi$$
	mulc1cncfg.3	$$⊢\phi \to F:A\underset{cn}{⟶}ℂ$$
	mulc1cncfg.4	$$⊢\phi \to B\in ℂ$$
Assertion	mulc1cncfg	$$⊢\phi \to \left(x\in A⟼BF\left(x\right)\right):A\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		mulc1cncfg.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		mulc1cncfg.2	$$⊢Ⅎx\phi$$
3		mulc1cncfg.3	$$⊢\phi \to F:A\underset{cn}{⟶}ℂ$$
4		mulc1cncfg.4	$$⊢\phi \to B\in ℂ$$
5		eqid	$$⊢\left(x\in ℂ⟼Bx\right)=\left(x\in ℂ⟼Bx\right)$$
6	5	mulc1cncf	$$⊢B\in ℂ\to \left(x\in ℂ⟼Bx\right):ℂ\underset{cn}{⟶}ℂ$$
7	4 6	syl	$$⊢\phi \to \left(x\in ℂ⟼Bx\right):ℂ\underset{cn}{⟶}ℂ$$
8		cncff	$$⊢\left(x\in ℂ⟼Bx\right):ℂ\underset{cn}{⟶}ℂ\to \left(x\in ℂ⟼Bx\right):ℂ⟶ℂ$$
9	7 8	syl	$$⊢\phi \to \left(x\in ℂ⟼Bx\right):ℂ⟶ℂ$$
10		cncff	$$⊢F:A\underset{cn}{⟶}ℂ\to F:A⟶ℂ$$
11	3 10	syl	$$⊢\phi \to F:A⟶ℂ$$
12		fcompt	$$⊢\left(\left(x\in ℂ⟼Bx\right):ℂ⟶ℂ\wedge F:A⟶ℂ\right)\to \left(x\in ℂ⟼Bx\right)\circ F=\left(t\in A⟼\left(x\in ℂ⟼Bx\right)\left(F\left(t\right)\right)\right)$$
13	9 11 12	syl2anc	$$⊢\phi \to \left(x\in ℂ⟼Bx\right)\circ F=\left(t\in A⟼\left(x\in ℂ⟼Bx\right)\left(F\left(t\right)\right)\right)$$
14	11	ffvelcdmda	$$⊢\left(\phi \wedge t\in A\right)\to F\left(t\right)\in ℂ$$
15	4	adantr	$$⊢\left(\phi \wedge t\in A\right)\to B\in ℂ$$
16	15 14	mulcld	$$⊢\left(\phi \wedge t\in A\right)\to BF\left(t\right)\in ℂ$$
17		nfcv	$$⊢\underset{\_}{Ⅎ}xt$$
18	1 17	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(t\right)$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
20		nfcv	$$⊢\underset{\_}{Ⅎ}x\times$$
21	19 20 18	nfov	$$⊢\underset{\_}{Ⅎ}xBF\left(t\right)$$
22		oveq2	$$⊢x=F\left(t\right)\to Bx=BF\left(t\right)$$
23	18 21 22 5	fvmptf	$$⊢\left(F\left(t\right)\in ℂ\wedge BF\left(t\right)\in ℂ\right)\to \left(x\in ℂ⟼Bx\right)\left(F\left(t\right)\right)=BF\left(t\right)$$
24	14 16 23	syl2anc	$$⊢\left(\phi \wedge t\in A\right)\to \left(x\in ℂ⟼Bx\right)\left(F\left(t\right)\right)=BF\left(t\right)$$
25	24	mpteq2dva	$$⊢\phi \to \left(t\in A⟼\left(x\in ℂ⟼Bx\right)\left(F\left(t\right)\right)\right)=\left(t\in A⟼BF\left(t\right)\right)$$
26		nfcv	$$⊢\underset{\_}{Ⅎ}tB$$
27		nfcv	$$⊢\underset{\_}{Ⅎ}t\times$$
28		nfcv	$$⊢\underset{\_}{Ⅎ}tF\left(x\right)$$
29	26 27 28	nfov	$$⊢\underset{\_}{Ⅎ}tBF\left(x\right)$$
30		fveq2	$$⊢t=x\to F\left(t\right)=F\left(x\right)$$
31	30	oveq2d	$$⊢t=x\to BF\left(t\right)=BF\left(x\right)$$
32	21 29 31	cbvmpt	$$⊢\left(t\in A⟼BF\left(t\right)\right)=\left(x\in A⟼BF\left(x\right)\right)$$
33	25 32	eqtrdi	$$⊢\phi \to \left(t\in A⟼\left(x\in ℂ⟼Bx\right)\left(F\left(t\right)\right)\right)=\left(x\in A⟼BF\left(x\right)\right)$$
34	13 33	eqtrd	$$⊢\phi \to \left(x\in ℂ⟼Bx\right)\circ F=\left(x\in A⟼BF\left(x\right)\right)$$
35	3 7	cncfco	$$⊢\phi \to \left(\left(x\in ℂ⟼Bx\right)\circ F\right):A\underset{cn}{⟶}ℂ$$
36	34 35	eqeltrrd	$$⊢\phi \to \left(x\in A⟼BF\left(x\right)\right):A\underset{cn}{⟶}ℂ$$