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