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

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 𝐾 ) )