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	$⊢ Ⅎ k φ$
	fprodcnlem.k	$⊢ K = TopOpen (ℂ_{fld})$
	fprodcnlem.j	$⊢ φ \to J \in TopOn (X)$
	fprodcnlem.a	$⊢ φ \to A \in Fin$
	fprodcnlem.b	$⊢ (φ \land k \in A) \to (x \in X ⟼ B) \in (J Cn K)$
	fprodcnlem.z	$⊢ φ \to Z \subseteq A$
	fprodcnlem.w	$⊢ φ \to W \in (A ∖ Z)$
	fprodcnlem.p	$⊢ φ \to (x \in X ⟼ \prod_{k \in Z} B) \in (J Cn K)$
Assertion	fprodcnlem	$⊢ φ \to (x \in X ⟼ \prod_{k \in Z \cup \{W\}} B) \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		fprodcnlem.1	$⊢ Ⅎ k φ$
2		fprodcnlem.k	$⊢ K = TopOpen (ℂ_{fld})$
3		fprodcnlem.j	$⊢ φ \to J \in TopOn (X)$
4		fprodcnlem.a	$⊢ φ \to A \in Fin$
5		fprodcnlem.b	$⊢ (φ \land k \in A) \to (x \in X ⟼ B) \in (J Cn K)$
6		fprodcnlem.z	$⊢ φ \to Z \subseteq A$
7		fprodcnlem.w	$⊢ φ \to W \in (A ∖ Z)$
8		fprodcnlem.p	$⊢ φ \to (x \in X ⟼ \prod_{k \in Z} B) \in (J Cn K)$
9		nfv	$⊢ Ⅎ k x \in X$
10	1 9	nfan	$⊢ Ⅎ k (φ \land x \in X)$
11		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ W / k ⦌ B$
12	4 6	ssfid	$⊢ φ \to Z \in Fin$
13	12	adantr	$⊢ (φ \land x \in X) \to Z \in Fin$
14	7	adantr	$⊢ (φ \land x \in X) \to W \in (A ∖ Z)$
15	14	eldifbd	$⊢ (φ \land x \in X) \to \neg W \in Z$
16	6	sselda	$⊢ (φ \land k \in Z) \to k \in A$
17	16	adantlr	$⊢ ((φ \land x \in X) \land k \in Z) \to k \in A$
18	3	adantr	$⊢ (φ \land k \in A) \to J \in TopOn (X)$
19	2	cnfldtopon	$⊢ K \in TopOn (ℂ)$
20	19	a1i	$⊢ (φ \land k \in A) \to K \in TopOn (ℂ)$
21		cnf2	$⊢ (J \in TopOn (X) \land K \in TopOn (ℂ) \land (x \in X ⟼ B) \in (J Cn K)) \to (x \in X ⟼ B) : X ⟶ ℂ$
22	18 20 5 21	syl3anc	$⊢ (φ \land k \in A) \to (x \in X ⟼ B) : X ⟶ ℂ$
23		eqid	$⊢ (x \in X ⟼ B) = (x \in X ⟼ B)$
24	23	fmpt	$⊢ \forall x \in X B \in ℂ \leftrightarrow (x \in X ⟼ B) : X ⟶ ℂ$
25	22 24	sylibr	$⊢ (φ \land k \in A) \to \forall x \in X B \in ℂ$
26	25	adantlr	$⊢ ((φ \land x \in X) \land k \in A) \to \forall x \in X B \in ℂ$
27		simplr	$⊢ ((φ \land x \in X) \land k \in A) \to x \in X$
28		rspa	$⊢ (\forall x \in X B \in ℂ \land x \in X) \to B \in ℂ$
29	26 27 28	syl2anc	$⊢ ((φ \land x \in X) \land k \in A) \to B \in ℂ$
30	17 29	syldan	$⊢ ((φ \land x \in X) \land k \in Z) \to B \in ℂ$
31		csbeq1a	$⊢ k = W \to B = ⦋ W / k ⦌ B$
32	14	eldifad	$⊢ (φ \land x \in X) \to W \in A$
33		nfv	$⊢ Ⅎ k W \in A$
34	10 33	nfan	$⊢ Ⅎ k ((φ \land x \in X) \land W \in A)$
35	11	nfel1	$⊢ Ⅎ k ⦋ W / k ⦌ B \in ℂ$
36	34 35	nfim	$⊢ Ⅎ k (((φ \land x \in X) \land W \in A) \to ⦋ W / k ⦌ B \in ℂ)$
37		eleq1	$⊢ k = W \to (k \in A \leftrightarrow W \in A)$
38	37	anbi2d	$⊢ k = W \to (((φ \land x \in X) \land k \in A) \leftrightarrow ((φ \land x \in X) \land W \in A))$
39	31	eleq1d	$⊢ k = W \to (B \in ℂ \leftrightarrow ⦋ W / k ⦌ B \in ℂ)$
40	38 39	imbi12d	$⊢ k = W \to ((((φ \land x \in X) \land k \in A) \to B \in ℂ) \leftrightarrow (((φ \land x \in X) \land W \in A) \to ⦋ W / k ⦌ B \in ℂ))$
41	36 40 29	vtoclg1f	$⊢ W \in A \to (((φ \land x \in X) \land W \in A) \to ⦋ W / k ⦌ B \in ℂ)$
42	41	anabsi7	$⊢ ((φ \land x \in X) \land W \in A) \to ⦋ W / k ⦌ B \in ℂ$
43	32 42	mpdan	$⊢ (φ \land x \in X) \to ⦋ W / k ⦌ B \in ℂ$
44	10 11 13 14 15 30 31 43	fprodsplitsn	$⊢ (φ \land x \in X) \to \prod_{k \in Z \cup \{W\}} B = \prod_{k \in Z} B ⦋ W / k ⦌ B$
45	44	mpteq2dva	$⊢ φ \to (x \in X ⟼ \prod_{k \in Z \cup \{W\}} B) = (x \in X ⟼ \prod_{k \in Z} B ⦋ W / k ⦌ B)$
46	7	eldifad	$⊢ φ \to W \in A$
47	1 33	nfan	$⊢ Ⅎ k (φ \land W \in A)$
48		nfcv	$⊢ \underline{Ⅎ} k X$
49	48 11	nfmpt	$⊢ \underline{Ⅎ} k (x \in X ⟼ ⦋ W / k ⦌ B)$
50	49	nfel1	$⊢ Ⅎ k (x \in X ⟼ ⦋ W / k ⦌ B) \in (J Cn K)$
51	47 50	nfim	$⊢ Ⅎ k ((φ \land W \in A) \to (x \in X ⟼ ⦋ W / k ⦌ B) \in (J Cn K))$
52	37	anbi2d	$⊢ k = W \to ((φ \land k \in A) \leftrightarrow (φ \land W \in A))$
53	31	mpteq2dv	$⊢ k = W \to (x \in X ⟼ B) = (x \in X ⟼ ⦋ W / k ⦌ B)$
54	53	eleq1d	$⊢ k = W \to ((x \in X ⟼ B) \in (J Cn K) \leftrightarrow (x \in X ⟼ ⦋ W / k ⦌ B) \in (J Cn K))$
55	52 54	imbi12d	$⊢ k = W \to (((φ \land k \in A) \to (x \in X ⟼ B) \in (J Cn K)) \leftrightarrow ((φ \land W \in A) \to (x \in X ⟼ ⦋ W / k ⦌ B) \in (J Cn K)))$
56	51 55 5	vtoclg1f	$⊢ W \in A \to ((φ \land W \in A) \to (x \in X ⟼ ⦋ W / k ⦌ B) \in (J Cn K))$
57	56	anabsi7	$⊢ (φ \land W \in A) \to (x \in X ⟼ ⦋ W / k ⦌ B) \in (J Cn K)$
58	46 57	mpdan	$⊢ φ \to (x \in X ⟼ ⦋ W / k ⦌ B) \in (J Cn K)$
59	19	a1i	$⊢ φ \to K \in TopOn (ℂ)$
60	2	mpomulcn	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) \in ((K \times_{t} K) Cn K)$
61	60	a1i	$⊢ φ \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((K \times_{t} K) Cn K)$
62		oveq12	$⊢ (u = \prod_{k \in Z} B \land v = ⦋ W / k ⦌ B) \to u v = \prod_{k \in Z} B ⦋ W / k ⦌ B$
63	3 8 58 59 59 61 62	cnmpt12	$⊢ φ \to (x \in X ⟼ \prod_{k \in Z} B ⦋ W / k ⦌ B) \in (J Cn K)$
64	45 63	eqeltrd	$⊢ φ \to (x \in X ⟼ \prod_{k \in Z \cup \{W\}} B) \in (J Cn K)$

Metamath Proof Explorer

Theorem fprodcnlem

Proof