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) Avoid ax-mulf . (Revised by GG, 19-Apr-2025)

	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		nfv	⊢ Ⅎ 𝑘 𝑊 ∈ 𝐴
34	10 33	nfan	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑊 ∈ 𝐴 )
35	11	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ∈ ℂ
36	34 35	nfim	⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑊 ∈ 𝐴 ) → ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ∈ ℂ )
37		eleq1	⊢ ( 𝑘 = 𝑊 → ( 𝑘 ∈ 𝐴 ↔ 𝑊 ∈ 𝐴 ) )
38	37	anbi2d	⊢ ( 𝑘 = 𝑊 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑊 ∈ 𝐴 ) ) )
39	31	eleq1d	⊢ ( 𝑘 = 𝑊 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
40	38 39	imbi12d	⊢ ( 𝑘 = 𝑊 → ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) ↔ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑊 ∈ 𝐴 ) → ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) )
41	36 40 29	vtoclg1f	⊢ ( 𝑊 ∈ 𝐴 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑊 ∈ 𝐴 ) → ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
42	41	anabsi7	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑊 ∈ 𝐴 ) → ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ∈ ℂ )
43	32 42	mpdan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ∈ ℂ )
44	10 11 13 14 15 30 31 43	fprodsplitsn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∏ 𝑘 ∈ ( 𝑍 ∪ { 𝑊 } ) 𝐵 = ( ∏ 𝑘 ∈ 𝑍 𝐵 · ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) )
45	44	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ( 𝑍 ∪ { 𝑊 } ) 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ ( ∏ 𝑘 ∈ 𝑍 𝐵 · ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ) )
46	7	eldifad	⊢ ( 𝜑 → 𝑊 ∈ 𝐴 )
47	1 33	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑊 ∈ 𝐴 )
48		nfcv	⊢ Ⅎ 𝑘 𝑋
49	48 11	nfmpt	⊢ Ⅎ 𝑘 ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 )
50	49	nfel1	⊢ Ⅎ 𝑘 ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 )
51	47 50	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑊 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
52	37	anbi2d	⊢ ( 𝑘 = 𝑊 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑊 ∈ 𝐴 ) ) )
53	31	mpteq2dv	⊢ ( 𝑘 = 𝑊 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) )
54	53	eleq1d	⊢ ( 𝑘 = 𝑊 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
55	52 54	imbi12d	⊢ ( 𝑘 = 𝑊 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ↔ ( ( 𝜑 ∧ 𝑊 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) )
56	51 55 5	vtoclg1f	⊢ ( 𝑊 ∈ 𝐴 → ( ( 𝜑 ∧ 𝑊 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
57	56	anabsi7	⊢ ( ( 𝜑 ∧ 𝑊 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
58	46 57	mpdan	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
59	19	a1i	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ℂ ) )
60	2	mpomulcn	⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
61	60	a1i	⊢ ( 𝜑 → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) )
62		oveq12	⊢ ( ( 𝑢 = ∏ 𝑘 ∈ 𝑍 𝐵 ∧ 𝑣 = ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) → ( 𝑢 · 𝑣 ) = ( ∏ 𝑘 ∈ 𝑍 𝐵 · ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) )
63	3 8 58 59 59 61 62	cnmpt12	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ∏ 𝑘 ∈ 𝑍 𝐵 · ⦋ 𝑊 / 𝑘 ⦌ 𝐵 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
64	45 63	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ( 𝑍 ∪ { 𝑊 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )