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