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	$⊢ Ⅎ 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		simpr	$⊢ ((φ \land x \in X) \land W \in A) \to W \in A$
34		nfcv	$⊢ \underline{Ⅎ} k W$
35		nfv	$⊢ Ⅎ k W \in A$
36	10 35	nfan	$⊢ Ⅎ k ((φ \land x \in X) \land W \in A)$
37	11	nfel1	$⊢ Ⅎ k ⦋ W / k ⦌ B \in ℂ$
38	36 37	nfim	$⊢ Ⅎ k (((φ \land x \in X) \land W \in A) \to ⦋ W / k ⦌ B \in ℂ)$
39		eleq1	$⊢ k = W \to (k \in A \leftrightarrow W \in A)$
40	39	anbi2d	$⊢ k = W \to (((φ \land x \in X) \land k \in A) \leftrightarrow ((φ \land x \in X) \land W \in A))$
41	31	eleq1d	$⊢ k = W \to (B \in ℂ \leftrightarrow ⦋ W / k ⦌ B \in ℂ)$
42	40 41	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 ℂ))$
43	34 38 42 29	vtoclgf	$⊢ W \in A \to (((φ \land x \in X) \land W \in A) \to ⦋ W / k ⦌ B \in ℂ)$
44	33 43	mpcom	$⊢ ((φ \land x \in X) \land W \in A) \to ⦋ W / k ⦌ B \in ℂ$
45	32 44	mpdan	$⊢ (φ \land x \in X) \to ⦋ W / k ⦌ B \in ℂ$
46	10 11 13 14 15 30 31 45	fprodsplitsn	$⊢ (φ \land x \in X) \to \prod_{k \in Z \cup \{W\}} B = \prod_{k \in Z} B ⦋ W / k ⦌ B$
47	46	mpteq2dva	$⊢ φ \to (x \in X ⟼ \prod_{k \in Z \cup \{W\}} B) = (x \in X ⟼ \prod_{k \in Z} B ⦋ W / k ⦌ B)$
48	7	eldifad	$⊢ φ \to W \in A$
49	1 35	nfan	$⊢ Ⅎ k (φ \land W \in A)$
50		nfcv	$⊢ \underline{Ⅎ} k X$
51	50 11	nfmpt	$⊢ \underline{Ⅎ} k (x \in X ⟼ ⦋ W / k ⦌ B)$
52		nfcv	$⊢ \underline{Ⅎ} k (J Cn K)$
53	51 52	nfel	$⊢ Ⅎ k (x \in X ⟼ ⦋ W / k ⦌ B) \in (J Cn K)$
54	49 53	nfim	$⊢ Ⅎ k ((φ \land W \in A) \to (x \in X ⟼ ⦋ W / k ⦌ B) \in (J Cn K))$
55	39	anbi2d	$⊢ k = W \to ((φ \land k \in A) \leftrightarrow (φ \land W \in A))$
56	31	mpteq2dv	$⊢ k = W \to (x \in X ⟼ B) = (x \in X ⟼ ⦋ W / k ⦌ B)$
57	56	eleq1d	$⊢ k = W \to ((x \in X ⟼ B) \in (J Cn K) \leftrightarrow (x \in X ⟼ ⦋ W / k ⦌ B) \in (J Cn K))$
58	55 57	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)))$
59	5	idi	$⊢ (φ \land k \in A) \to (x \in X ⟼ B) \in (J Cn K)$
60	34 54 58 59	vtoclgf	$⊢ W \in A \to ((φ \land W \in A) \to (x \in X ⟼ ⦋ W / k ⦌ B) \in (J Cn K))$
61	60	anabsi7	$⊢ (φ \land W \in A) \to (x \in X ⟼ ⦋ W / k ⦌ B) \in (J Cn K)$
62	48 61	mpdan	$⊢ φ \to (x \in X ⟼ ⦋ W / k ⦌ B) \in (J Cn K)$
63	2	mulcn	$⊢ \times \in ((K \times_{t} K) Cn K)$
64	63	a1i	$⊢ φ \to \times \in ((K \times_{t} K) Cn K)$
65	3 8 62 64	cnmpt12f	$⊢ φ \to (x \in X ⟼ \prod_{k \in Z} B ⦋ W / k ⦌ B) \in (J Cn K)$
66	47 65	eqeltrd	$⊢ φ \to (x \in X ⟼ \prod_{k \in Z \cup \{W\}} B) \in (J Cn K)$

Metamath Proof Explorer

Theorem fprodcnlem

Proof