Metamath Proof Explorer

Theorem fprodcn

Description: A finite product 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 Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses fprodcn.d ⊢ Ⅎ 𝑘 𝜑
fprodcn.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
fprodcn.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
fprodcn.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fprodcn.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
Assertion fprodcn ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 fprodcn.d ⊢ Ⅎ 𝑘 𝜑
2 fprodcn.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
3 fprodcn.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 fprodcn.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
5 fprodcn.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
6 prodeq1 ⊢ ( 𝑦 = ∅ → ∏ 𝑘 ∈ 𝑦 𝐵 = ∏ 𝑘 ∈ ∅ 𝐵 )
7 6 mpteq2dv ⊢ ( 𝑦 = ∅ → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑦 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ∅ 𝐵 ) )
8 7 eleq1d ⊢ ( 𝑦 = ∅ → ( ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ∅ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
9 prodeq1 ⊢ ( 𝑦 = 𝑧 → ∏ 𝑘 ∈ 𝑦 𝐵 = ∏ 𝑘 ∈ 𝑧 𝐵 )
10 9 mpteq2dv ⊢ ( 𝑦 = 𝑧 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑦 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) )
11 10 eleq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
12 prodeq1 ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑤 } ) → ∏ 𝑘 ∈ 𝑦 𝐵 = ∏ 𝑘 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 )
13 12 mpteq2dv ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑤 } ) → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑦 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ) )
14 13 eleq1d ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑤 } ) → ( ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
15 prodeq1 ⊢ ( 𝑦 = 𝐴 → ∏ 𝑘 ∈ 𝑦 𝐵 = ∏ 𝑘 ∈ 𝐴 𝐵 )
16 15 mpteq2dv ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑦 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝐴 𝐵 ) )
17 16 eleq1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑦 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
18 prod0 ⊢ ∏ 𝑘 ∈ ∅ 𝐵 = 1
19 18 mpteq2i ⊢ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ∅ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ 1 )
20 eqidd ⊢ ( 𝑥 = 𝑦 → 1 = 1 )
21 20 cbvmptv ⊢ ( 𝑥 ∈ 𝑋 ↦ 1 ) = ( 𝑦 ∈ 𝑋 ↦ 1 )
22 19 21 eqtri ⊢ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ∅ 𝐵 ) = ( 𝑦 ∈ 𝑋 ↦ 1 )
23 22 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ∅ 𝐵 ) = ( 𝑦 ∈ 𝑋 ↦ 1 ) )
24 2 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
25 24 a1i ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ℂ ) )
26 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
27 3 25 26 cnmptc ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑋 ↦ 1 ) ∈ ( 𝐽 Cn 𝐾 ) )
28 23 27 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ∅ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
29 nfcv ⊢ Ⅎ 𝑦 ∏ 𝑘 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵
30 nfcv ⊢ Ⅎ 𝑥 ( 𝑧 ∪ { 𝑤 } )
31 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
32 30 31 nfcprod ⊢ Ⅎ 𝑥 ∏ 𝑘 ∈ ( 𝑧 ∪ { 𝑤 } ) ⦋ 𝑦 / 𝑥 ⦌ 𝐵
33 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
34 33 prodeq2ad ⊢ ( 𝑥 = 𝑦 → ∏ 𝑘 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 = ∏ 𝑘 ∈ ( 𝑧 ∪ { 𝑤 } ) ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
35 29 32 34 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ) = ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ( 𝑧 ∪ { 𝑤 } ) ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
36 35 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ) = ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ( 𝑧 ∪ { 𝑤 } ) ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
37 nfv ⊢ Ⅎ 𝑘 ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) )
38 1 37 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) )
39 nfcv ⊢ Ⅎ 𝑘 𝑋
40 nfcv ⊢ Ⅎ 𝑘 𝑧
41 40 nfcprod1 ⊢ Ⅎ 𝑘 ∏ 𝑘 ∈ 𝑧 𝐵
42 39 41 nfmpt ⊢ Ⅎ 𝑘 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 )
43 nfcv ⊢ Ⅎ 𝑘 ( 𝐽 Cn 𝐾 )
44 42 43 nfel ⊢ Ⅎ 𝑘 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) ∈ ( 𝐽 Cn 𝐾 )
45 38 44 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
46 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
47 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐴 ∈ Fin )
48 nfcv ⊢ Ⅎ 𝑦 𝐵
49 48 31 33 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
50 49 eqcomi ⊢ ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 )
51 50 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
52 51 5 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
53 52 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
54 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → 𝑧 ⊆ 𝐴 )
55 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) )
56 nfcv ⊢ Ⅎ 𝑦 ∏ 𝑘 ∈ 𝑧 𝐵
57 nfcv ⊢ Ⅎ 𝑥 𝑧
58 57 31 nfcprod ⊢ Ⅎ 𝑥 ∏ 𝑘 ∈ 𝑧 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
59 33 prodeq2sdv ⊢ ( 𝑥 = 𝑦 → ∏ 𝑘 ∈ 𝑧 𝐵 = ∏ 𝑘 ∈ 𝑧 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
60 56 58 59 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) = ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
61 60 eleq1i ⊢ ( ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
62 61 biimpi ⊢ ( ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) → ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
63 62 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
64 45 2 46 47 53 54 55 63 fprodcnlem ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ( 𝑧 ∪ { 𝑤 } ) ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
65 36 64 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
66 65 ex ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑧 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
67 8 11 14 17 28 66 4 findcard2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )