This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
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→ ℂ ) )