Theorem fprodcnlem

Description: A finite product of functions to complex numbers from a common topological space is continuous. Induction step. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	fprodcnlem.1	⊢ Ⅎ 𝑘 𝜑
	fprodcnlem.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
	fprodcnlem.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	fprodcnlem.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fprodcnlem.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
	fprodcnlem.z	⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
	fprodcnlem.w	⊢ ( 𝜑 → 𝑊 ∈ ( 𝐴 ∖ 𝑍 ) )
	fprodcnlem.p	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑍 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
Assertion	fprodcnlem	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ( 𝑍 ∪ { 𝑊 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		fprodcnlem.1	⊢ Ⅎ 𝑘 𝜑
2		fprodcnlem.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
3		fprodcnlem.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4		fprodcnlem.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
5		fprodcnlem.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
6		fprodcnlem.z	⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
7		fprodcnlem.w	⊢ ( 𝜑 → 𝑊 ∈ ( 𝐴 ∖ 𝑍 ) )
8		fprodcnlem.p	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ 𝑍 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
9		nfv	⊢ Ⅎ 𝑘 𝑥 ∈ 𝑋
10	1 9	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑥 ∈ 𝑋 )
11		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑊 / 𝑘 ⦌ 𝐵
12	4 6	ssfid	⊢ ( 𝜑 → 𝑍 ∈ Fin )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑍 ∈ Fin )
14	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑊 ∈ ( 𝐴 ∖ 𝑍 ) )
15	14	eldifbd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ¬ 𝑊 ∈ 𝑍 )
16	6	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝐴 )
17	16	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝐴 )
18	3	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
19	2	cnfldtopon	⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
20	19	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐾 ∈ ( TopOn ‘ ℂ ) )
21		cnf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ℂ )
22	18 20 5 21	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ℂ )
23		eqid	⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 )
24	23	fmpt	⊢ ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ ℂ ↔ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ℂ )
25	22 24	sylibr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝑋 𝐵 ∈ ℂ )
26	25	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝑋 𝐵 ∈ ℂ )
27		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → 𝑥 ∈ 𝑋 )
28		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ ℂ ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
29	26 27 28	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
30	17 29	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
31		csbeq1a	⊢ ( 𝑘 = 𝑊 → 𝐵 = ⦋ 𝑊 / 𝑘 ⦌ 𝐵 )
32	14	eldifad	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑊 ∈ 𝐴 )
33		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑊 ∈ 𝐴 ) → 𝑊 ∈ 𝐴 )
34		nfcv	⊢ Ⅎ 𝑘 𝑊
35		nfv	⊢ Ⅎ 𝑘 𝑊 ∈ 𝐴
36	10 35	nfan	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑊 ∈ 𝐴 )
37	11	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ∈ ℂ
38	36 37	nfim	⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑊 ∈ 𝐴 ) → ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ∈ ℂ )
39		eleq1	⊢ ( 𝑘 = 𝑊 → ( 𝑘 ∈ 𝐴 ↔ 𝑊 ∈ 𝐴 ) )
40	39	anbi2d	⊢ ( 𝑘 = 𝑊 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑊 ∈ 𝐴 ) ) )
41	31	eleq1d	⊢ ( 𝑘 = 𝑊 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
42	40 41	imbi12d	⊢ ( 𝑘 = 𝑊 → ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) ↔ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑊 ∈ 𝐴 ) → ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) )
43	34 38 42 29	vtoclgf	⊢ ( 𝑊 ∈ 𝐴 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑊 ∈ 𝐴 ) → ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
44	33 43	mpcom	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑊 ∈ 𝐴 ) → ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ∈ ℂ )
45	32 44	mpdan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ∈ ℂ )
46	10 11 13 14 15 30 31 45	fprodsplitsn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∏ 𝑘 ∈ ( 𝑍 ∪ { 𝑊 } ) 𝐵 = ( ∏ 𝑘 ∈ 𝑍 𝐵 · ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) )
47	46	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ( 𝑍 ∪ { 𝑊 } ) 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ ( ∏ 𝑘 ∈ 𝑍 𝐵 · ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ) )
48	7	eldifad	⊢ ( 𝜑 → 𝑊 ∈ 𝐴 )
49	1 35	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑊 ∈ 𝐴 )
50		nfcv	⊢ Ⅎ 𝑘 𝑋
51	50 11	nfmpt	⊢ Ⅎ 𝑘 ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 )
52		nfcv	⊢ Ⅎ 𝑘 ( 𝐽 Cn 𝐾 )
53	51 52	nfel	⊢ Ⅎ 𝑘 ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 )
54	49 53	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑊 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
55	39	anbi2d	⊢ ( 𝑘 = 𝑊 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑊 ∈ 𝐴 ) ) )
56	31	mpteq2dv	⊢ ( 𝑘 = 𝑊 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) )
57	56	eleq1d	⊢ ( 𝑘 = 𝑊 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
58	55 57	imbi12d	⊢ ( 𝑘 = 𝑊 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ↔ ( ( 𝜑 ∧ 𝑊 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) )
59	5	idi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
60	34 54 58 59	vtoclgf	⊢ ( 𝑊 ∈ 𝐴 → ( ( 𝜑 ∧ 𝑊 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
61	60	anabsi7	⊢ ( ( 𝜑 ∧ 𝑊 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
62	48 61	mpdan	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
63	2	mulcn	⊢ · ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
64	63	a1i	⊢ ( 𝜑 → · ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) )
65	3 8 62 64	cnmpt12f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ∏ 𝑘 ∈ 𝑍 𝐵 · ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
66	47 65	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ( 𝑍 ∪ { 𝑊 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )