Metamath Proof Explorer


Theorem fsum2cn

Description: Version of fsumcn for two-argument mappings. (Contributed by Mario Carneiro, 6-May-2014)

Ref Expression
Hypotheses fsumcn.3 𝐾 = ( TopOpen ‘ ℂfld )
fsumcn.4 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
fsumcn.5 ( 𝜑𝐴 ∈ Fin )
fsum2cn.7 ( 𝜑𝐿 ∈ ( TopOn ‘ 𝑌 ) )
fsum2cn.8 ( ( 𝜑𝑘𝐴 ) → ( 𝑥𝑋 , 𝑦𝑌𝐵 ) ∈ ( ( 𝐽 ×t 𝐿 ) Cn 𝐾 ) )
Assertion fsum2cn ( 𝜑 → ( 𝑥𝑋 , 𝑦𝑌 ↦ Σ 𝑘𝐴 𝐵 ) ∈ ( ( 𝐽 ×t 𝐿 ) Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 fsumcn.3 𝐾 = ( TopOpen ‘ ℂfld )
2 fsumcn.4 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 fsumcn.5 ( 𝜑𝐴 ∈ Fin )
4 fsum2cn.7 ( 𝜑𝐿 ∈ ( TopOn ‘ 𝑌 ) )
5 fsum2cn.8 ( ( 𝜑𝑘𝐴 ) → ( 𝑥𝑋 , 𝑦𝑌𝐵 ) ∈ ( ( 𝐽 ×t 𝐿 ) Cn 𝐾 ) )
6 nfcv 𝑢 Σ 𝑘𝐴 𝐵
7 nfcv 𝑣 Σ 𝑘𝐴 𝐵
8 nfcv 𝑥 𝐴
9 nfcv 𝑥 𝑣
10 nfcsb1v 𝑥 𝑢 / 𝑥 𝐵
11 9 10 nfcsbw 𝑥 𝑣 / 𝑦 𝑢 / 𝑥 𝐵
12 8 11 nfsum 𝑥 Σ 𝑘𝐴 𝑣 / 𝑦 𝑢 / 𝑥 𝐵
13 nfcv 𝑦 𝐴
14 nfcsb1v 𝑦 𝑣 / 𝑦 𝑢 / 𝑥 𝐵
15 13 14 nfsum 𝑦 Σ 𝑘𝐴 𝑣 / 𝑦 𝑢 / 𝑥 𝐵
16 csbeq1a ( 𝑥 = 𝑢𝐵 = 𝑢 / 𝑥 𝐵 )
17 csbeq1a ( 𝑦 = 𝑣 𝑢 / 𝑥 𝐵 = 𝑣 / 𝑦 𝑢 / 𝑥 𝐵 )
18 16 17 sylan9eq ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → 𝐵 = 𝑣 / 𝑦 𝑢 / 𝑥 𝐵 )
19 18 sumeq2sdv ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → Σ 𝑘𝐴 𝐵 = Σ 𝑘𝐴 𝑣 / 𝑦 𝑢 / 𝑥 𝐵 )
20 6 7 12 15 19 cbvmpo ( 𝑥𝑋 , 𝑦𝑌 ↦ Σ 𝑘𝐴 𝐵 ) = ( 𝑢𝑋 , 𝑣𝑌 ↦ Σ 𝑘𝐴 𝑣 / 𝑦 𝑢 / 𝑥 𝐵 )
21 vex 𝑢 ∈ V
22 vex 𝑣 ∈ V
23 21 22 op2ndd ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 2nd𝑧 ) = 𝑣 )
24 23 csbeq1d ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 2nd𝑧 ) / 𝑦 ( 1st𝑧 ) / 𝑥 𝐵 = 𝑣 / 𝑦 ( 1st𝑧 ) / 𝑥 𝐵 )
25 21 22 op1std ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 1st𝑧 ) = 𝑢 )
26 25 csbeq1d ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 1st𝑧 ) / 𝑥 𝐵 = 𝑢 / 𝑥 𝐵 )
27 26 csbeq2dv ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → 𝑣 / 𝑦 ( 1st𝑧 ) / 𝑥 𝐵 = 𝑣 / 𝑦 𝑢 / 𝑥 𝐵 )
28 24 27 eqtrd ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 2nd𝑧 ) / 𝑦 ( 1st𝑧 ) / 𝑥 𝐵 = 𝑣 / 𝑦 𝑢 / 𝑥 𝐵 )
29 28 sumeq2sdv ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → Σ 𝑘𝐴 ( 2nd𝑧 ) / 𝑦 ( 1st𝑧 ) / 𝑥 𝐵 = Σ 𝑘𝐴 𝑣 / 𝑦 𝑢 / 𝑥 𝐵 )
30 29 mpompt ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ Σ 𝑘𝐴 ( 2nd𝑧 ) / 𝑦 ( 1st𝑧 ) / 𝑥 𝐵 ) = ( 𝑢𝑋 , 𝑣𝑌 ↦ Σ 𝑘𝐴 𝑣 / 𝑦 𝑢 / 𝑥 𝐵 )
31 20 30 eqtr4i ( 𝑥𝑋 , 𝑦𝑌 ↦ Σ 𝑘𝐴 𝐵 ) = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ Σ 𝑘𝐴 ( 2nd𝑧 ) / 𝑦 ( 1st𝑧 ) / 𝑥 𝐵 )
32 txtopon ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
33 2 4 32 syl2anc ( 𝜑 → ( 𝐽 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
34 nfcv 𝑢 𝐵
35 nfcv 𝑣 𝐵
36 34 35 11 14 18 cbvmpo ( 𝑥𝑋 , 𝑦𝑌𝐵 ) = ( 𝑢𝑋 , 𝑣𝑌 𝑣 / 𝑦 𝑢 / 𝑥 𝐵 )
37 28 mpompt ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 2nd𝑧 ) / 𝑦 ( 1st𝑧 ) / 𝑥 𝐵 ) = ( 𝑢𝑋 , 𝑣𝑌 𝑣 / 𝑦 𝑢 / 𝑥 𝐵 )
38 36 37 eqtr4i ( 𝑥𝑋 , 𝑦𝑌𝐵 ) = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 2nd𝑧 ) / 𝑦 ( 1st𝑧 ) / 𝑥 𝐵 )
39 38 5 eqeltrrid ( ( 𝜑𝑘𝐴 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 2nd𝑧 ) / 𝑦 ( 1st𝑧 ) / 𝑥 𝐵 ) ∈ ( ( 𝐽 ×t 𝐿 ) Cn 𝐾 ) )
40 1 33 3 39 fsumcn ( 𝜑 → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ Σ 𝑘𝐴 ( 2nd𝑧 ) / 𝑦 ( 1st𝑧 ) / 𝑥 𝐵 ) ∈ ( ( 𝐽 ×t 𝐿 ) Cn 𝐾 ) )
41 31 40 eqeltrid ( 𝜑 → ( 𝑥𝑋 , 𝑦𝑌 ↦ Σ 𝑘𝐴 𝐵 ) ∈ ( ( 𝐽 ×t 𝐿 ) Cn 𝐾 ) )