Metamath Proof Explorer

Theorem fsumcn

Description: A finite sum of functions to complex numbers from a common topological space is continuous. The class expression for B normally contains free variables k and x to index it. (Contributed by NM, 8-Aug-2007) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses fsumcn.3 ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
fsumcn.4 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
fsumcn.5 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsumcn.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
Assertion fsumcn ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 fsumcn.3 ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
2 fsumcn.4 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 fsumcn.5 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
4 fsumcn.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
5 ssid ⊢ 𝐴 ⊆ 𝐴
6 sseq1 ⊢ ( 𝑤 = ∅ → ( 𝑤 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴 ) )
7 sumeq1 ⊢ ( 𝑤 = ∅ → Σ 𝑘 ∈ 𝑤 𝐵 = Σ 𝑘 ∈ ∅ 𝐵 )
8 7 mpteq2dv ⊢ ( 𝑤 = ∅ → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ∅ 𝐵 ) )
9 8 eleq1d ⊢ ( 𝑤 = ∅ → ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ∅ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
10 6 9 imbi12d ⊢ ( 𝑤 = ∅ → ( ( 𝑤 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ↔ ( ∅ ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ∅ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) )
11 10 imbi2d ⊢ ( 𝑤 = ∅ → ( ( 𝜑 → ( 𝑤 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) ↔ ( 𝜑 → ( ∅ ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ∅ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) ) )
12 sseq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴 ) )
13 sumeq1 ⊢ ( 𝑤 = 𝑦 → Σ 𝑘 ∈ 𝑤 𝐵 = Σ 𝑘 ∈ 𝑦 𝐵 )
14 13 mpteq2dv ⊢ ( 𝑤 = 𝑦 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) )
15 14 eleq1d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
16 12 15 imbi12d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ↔ ( 𝑦 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) )
17 16 imbi2d ⊢ ( 𝑤 = 𝑦 → ( ( 𝜑 → ( 𝑤 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) ↔ ( 𝜑 → ( 𝑦 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) ) )
18 sseq1 ⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑤 ⊆ 𝐴 ↔ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) )
19 sumeq1 ⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → Σ 𝑘 ∈ 𝑤 𝐵 = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
20 19 mpteq2dv ⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) )
21 20 eleq1d ⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
22 18 21 imbi12d ⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑤 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ↔ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) )
23 22 imbi2d ⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝜑 → ( 𝑤 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) ↔ ( 𝜑 → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) ) )
24 sseq1 ⊢ ( 𝑤 = 𝐴 → ( 𝑤 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
25 sumeq1 ⊢ ( 𝑤 = 𝐴 → Σ 𝑘 ∈ 𝑤 𝐵 = Σ 𝑘 ∈ 𝐴 𝐵 )
26 25 mpteq2dv ⊢ ( 𝑤 = 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) )
27 26 eleq1d ⊢ ( 𝑤 = 𝐴 → ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
28 24 27 imbi12d ⊢ ( 𝑤 = 𝐴 → ( ( 𝑤 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ↔ ( 𝐴 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) )
29 28 imbi2d ⊢ ( 𝑤 = 𝐴 → ( ( 𝜑 → ( 𝑤 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) ↔ ( 𝜑 → ( 𝐴 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) ) )
30 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝐵 = 0
31 30 mpteq2i ⊢ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ∅ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ 0 )
32 1 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
33 32 a1i ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ℂ ) )
34 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
35 2 33 34 cnmptc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 0 ) ∈ ( 𝐽 Cn 𝐾 ) )
36 31 35 eqeltrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ∅ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
37 36 a1d ⊢ ( 𝜑 → ( ∅ ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ∅ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
38 ssun1 ⊢ 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } )
39 sstr ⊢ ( ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) → 𝑦 ⊆ 𝐴 )
40 38 39 mpan ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → 𝑦 ⊆ 𝐴 )
41 40 imim1i ⊢ ( ( 𝑦 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
42 simplr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) → ¬ 𝑧 ∈ 𝑦 )
43 disjsn ⊢ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑦 )
44 42 43 sylibr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ )
45 eqidd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑦 ∪ { 𝑧 } ) = ( 𝑦 ∪ { 𝑧 } ) )
46 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐴 ∈ Fin )
47 simprl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 )
48 46 47 ssfid ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
49 simplll ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝜑 )
50 47 sselda ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑘 ∈ 𝐴 )
51 simplrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑥 ∈ 𝑋 )
52 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
53 32 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐾 ∈ ( TopOn ‘ ℂ ) )
54 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ℂ )
55 52 53 4 54 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ℂ )
56 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 )
57 56 fmpt ⊢ ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ ℂ ↔ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ℂ )
58 55 57 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝑋 𝐵 ∈ ℂ )
59 rsp ⊢ ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ ℂ → ( 𝑥 ∈ 𝑋 → 𝐵 ∈ ℂ ) )
60 58 59 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 → 𝐵 ∈ ℂ ) )
61 60 imp ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
62 49 50 51 61 syl21anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝐵 ∈ ℂ )
63 44 45 48 62 fsumsplit ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( Σ 𝑘 ∈ 𝑦 𝐵 + Σ 𝑘 ∈ { 𝑧 } 𝐵 ) )
64 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) → ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 )
65 64 unssbd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) → { 𝑧 } ⊆ 𝐴 )
66 vex ⊢ 𝑧 ∈ V
67 66 snss ⊢ ( 𝑧 ∈ 𝐴 ↔ { 𝑧 } ⊆ 𝐴 )
68 65 67 sylibr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) → 𝑧 ∈ 𝐴 )
69 68 adantrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑧 ∈ 𝐴 )
70 60 impancom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑘 ∈ 𝐴 → 𝐵 ∈ ℂ ) )
71 70 ralrimiv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ )
72 71 ad2ant2rl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ )
73 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝐵
74 73 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ
75 csbeq1a ⊢ ( 𝑘 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
76 75 eleq1d ⊢ ( 𝑘 = 𝑧 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
77 74 76 rspc ⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
78 69 72 77 sylc ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ )
79 sumsns ⊢ ( ( 𝑧 ∈ 𝐴 ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑧 } 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
80 69 78 79 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) → Σ 𝑘 ∈ { 𝑧 } 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
81 80 oveq2d ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) → ( Σ 𝑘 ∈ 𝑦 𝐵 + Σ 𝑘 ∈ { 𝑧 } 𝐵 ) = ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
82 63 81 eqtrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
83 82 anassrs ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
84 83 mpteq2dva ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
85 84 adantrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
86 nfcv ⊢ Ⅎ 𝑤 ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
87 nfcv ⊢ Ⅎ 𝑥 𝑦
88 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ 𝐵
89 87 88 nfsum ⊢ Ⅎ 𝑥 Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐵
90 nfcv ⊢ Ⅎ 𝑥 +
91 nfcv ⊢ Ⅎ 𝑥 𝑧
92 91 88 nfcsbw ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑘 ⦌ ⦋ 𝑤 / 𝑥 ⦌ 𝐵
93 89 90 92 nfov ⊢ Ⅎ 𝑥 ( Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
94 csbeq1a ⊢ ( 𝑥 = 𝑤 → 𝐵 = ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
95 94 sumeq2sdv ⊢ ( 𝑥 = 𝑤 → Σ 𝑘 ∈ 𝑦 𝐵 = Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
96 94 csbeq2dv ⊢ ( 𝑥 = 𝑤 → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
97 95 96 oveq12d ⊢ ( 𝑥 = 𝑤 → ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) = ( Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) )
98 86 93 97 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ 𝑦 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) = ( 𝑤 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) )
99 85 98 eqtrdi ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ( 𝑤 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) ) )
100 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
101 nfcv ⊢ Ⅎ 𝑤 Σ 𝑘 ∈ 𝑦 𝐵
102 101 89 95 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) = ( 𝑤 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
103 simprr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
104 102 103 eqeltrrid ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) → ( 𝑤 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
105 nfcv ⊢ Ⅎ 𝑤 ⦋ 𝑧 / 𝑘 ⦌ 𝐵
106 105 92 96 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) = ( 𝑤 ∈ 𝑋 ↦ ⦋ 𝑧 / 𝑘 ⦌ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
107 68 adantrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) → 𝑧 ∈ 𝐴 )
108 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
109 108 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) → ∀ 𝑘 ∈ 𝐴 ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
110 nfcv ⊢ Ⅎ 𝑘 𝑋
111 110 73 nfmpt ⊢ Ⅎ 𝑘 ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
112 111 nfel1 ⊢ Ⅎ 𝑘 ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 )
113 75 mpteq2dv ⊢ ( 𝑘 = 𝑧 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
114 113 eleq1d ⊢ ( 𝑘 = 𝑧 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
115 112 114 rspc ⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) → ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
116 107 109 115 sylc ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
117 106 116 eqeltrrid ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) → ( 𝑤 ∈ 𝑋 ↦ ⦋ 𝑧 / 𝑘 ⦌ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
118 1 addcn ⊢ + ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
119 118 a1i ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) → + ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) )
120 100 104 117 119 cnmpt12f ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) → ( 𝑤 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐵 + ⦋ 𝑧 / 𝑘 ⦌ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
121 99 120 eqeltrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
122 121 exp32 ⊢ ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) )
123 122 a2d ⊢ ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) )
124 41 123 syl5 ⊢ ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( 𝑦 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) )
125 124 expcom ⊢ ( ¬ 𝑧 ∈ 𝑦 → ( 𝜑 → ( ( 𝑦 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) ) )
126 125 adantl ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( 𝜑 → ( ( 𝑦 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) ) )
127 126 a2d ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( 𝜑 → ( 𝑦 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) → ( 𝜑 → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) ) )
128 11 17 23 29 37 127 findcard2s ⊢ ( 𝐴 ∈ Fin → ( 𝜑 → ( 𝐴 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) )
129 3 128 mpcom ⊢ ( 𝜑 → ( 𝐴 ⊆ 𝐴 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
130 5 129 mpi ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )