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	⊢ Ⅎ 𝑥 𝐹
	mulc1cncfg.2	⊢ Ⅎ 𝑥 𝜑
	mulc1cncfg.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )
	mulc1cncfg.4	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion	mulc1cncfg	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( 𝐴 –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		mulc1cncfg.1	⊢ Ⅎ 𝑥 𝐹
2		mulc1cncfg.2	⊢ Ⅎ 𝑥 𝜑
3		mulc1cncfg.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )
4		mulc1cncfg.4	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
5		eqid	⊢ ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) )
6	5	mulc1cncf	⊢ ( 𝐵 ∈ ℂ → ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )
7	4 6	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )
8		cncff	⊢ ( ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) → ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) : ℂ ⟶ ℂ )
9	7 8	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) : ℂ ⟶ ℂ )
10		cncff	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
11	3 10	syl	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
12		fcompt	⊢ ( ( ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) : ℂ ⟶ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) ∘ 𝐹 ) = ( 𝑡 ∈ 𝐴 ↦ ( ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
13	9 11 12	syl2anc	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) ∘ 𝐹 ) = ( 𝑡 ∈ 𝐴 ↦ ( ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
14	11	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
15	4	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
16	15 14	mulcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) → ( 𝐵 · ( 𝐹 ‘ 𝑡 ) ) ∈ ℂ )
17		nfcv	⊢ Ⅎ 𝑥 𝑡
18	1 17	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑡 )
19		nfcv	⊢ Ⅎ 𝑥 𝐵
20		nfcv	⊢ Ⅎ 𝑥 ·
21	19 20 18	nfov	⊢ Ⅎ 𝑥 ( 𝐵 · ( 𝐹 ‘ 𝑡 ) )
22		oveq2	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑡 ) → ( 𝐵 · 𝑥 ) = ( 𝐵 · ( 𝐹 ‘ 𝑡 ) ) )
23	18 21 22 5	fvmptf	⊢ ( ( ( 𝐹 ‘ 𝑡 ) ∈ ℂ ∧ ( 𝐵 · ( 𝐹 ‘ 𝑡 ) ) ∈ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑡 ) ) = ( 𝐵 · ( 𝐹 ‘ 𝑡 ) ) )
24	14 16 23	syl2anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑡 ) ) = ( 𝐵 · ( 𝐹 ‘ 𝑡 ) ) )
25	24	mpteq2dva	⊢ ( 𝜑 → ( 𝑡 ∈ 𝐴 ↦ ( ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝐴 ↦ ( 𝐵 · ( 𝐹 ‘ 𝑡 ) ) ) )
26		nfcv	⊢ Ⅎ 𝑡 𝐵
27		nfcv	⊢ Ⅎ 𝑡 ·
28		nfcv	⊢ Ⅎ 𝑡 ( 𝐹 ‘ 𝑥 )
29	26 27 28	nfov	⊢ Ⅎ 𝑡 ( 𝐵 · ( 𝐹 ‘ 𝑥 ) )
30		fveq2	⊢ ( 𝑡 = 𝑥 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑥 ) )
31	30	oveq2d	⊢ ( 𝑡 = 𝑥 → ( 𝐵 · ( 𝐹 ‘ 𝑡 ) ) = ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) )
32	21 29 31	cbvmpt	⊢ ( 𝑡 ∈ 𝐴 ↦ ( 𝐵 · ( 𝐹 ‘ 𝑡 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) )
33	25 32	eqtrdi	⊢ ( 𝜑 → ( 𝑡 ∈ 𝐴 ↦ ( ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑡 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) )
34	13 33	eqtrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) )
35	3 7	cncfco	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( 𝐵 · 𝑥 ) ) ∘ 𝐹 ) ∈ ( 𝐴 –cn→ ℂ ) )
36	34 35	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( 𝐴 –cn→ ℂ ) )