Metamath Proof Explorer


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→ ℂ ) )