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

Proof

Step	Hyp	Ref	Expression
1		fprodcn.d	$⊢ Ⅎ k φ$
2		fprodcn.k	$⊢ K = TopOpen (ℂ_{fld})$
3		fprodcn.j	$⊢ φ \to J \in TopOn (X)$
4		fprodcn.a	$⊢ φ \to A \in Fin$
5		fprodcn.b	$⊢ (φ \land k \in A) \to (x \in X ⟼ B) \in (J Cn K)$
6		prodeq1	$⊢ y = \emptyset \to \prod_{k \in y} B = \prod_{k \in \emptyset} B$
7	6	mpteq2dv	$⊢ y = \emptyset \to (x \in X ⟼ \prod_{k \in y} B) = (x \in X ⟼ \prod_{k \in \emptyset} B)$
8	7	eleq1d	$⊢ y = \emptyset \to ((x \in X ⟼ \prod_{k \in y} B) \in (J Cn K) \leftrightarrow (x \in X ⟼ \prod_{k \in \emptyset} B) \in (J Cn K))$
9		prodeq1	$⊢ y = z \to \prod_{k \in y} B = \prod_{k \in z} B$
10	9	mpteq2dv	$⊢ y = z \to (x \in X ⟼ \prod_{k \in y} B) = (x \in X ⟼ \prod_{k \in z} B)$
11	10	eleq1d	$⊢ y = z \to ((x \in X ⟼ \prod_{k \in y} B) \in (J Cn K) \leftrightarrow (x \in X ⟼ \prod_{k \in z} B) \in (J Cn K))$
12		prodeq1	$⊢ y = z \cup \{w\} \to \prod_{k \in y} B = \prod_{k \in z \cup \{w\}} B$
13	12	mpteq2dv	$⊢ y = z \cup \{w\} \to (x \in X ⟼ \prod_{k \in y} B) = (x \in X ⟼ \prod_{k \in z \cup \{w\}} B)$
14	13	eleq1d	$⊢ y = z \cup \{w\} \to ((x \in X ⟼ \prod_{k \in y} B) \in (J Cn K) \leftrightarrow (x \in X ⟼ \prod_{k \in z \cup \{w\}} B) \in (J Cn K))$
15		prodeq1	$⊢ y = A \to \prod_{k \in y} B = \prod_{k \in A} B$
16	15	mpteq2dv	$⊢ y = A \to (x \in X ⟼ \prod_{k \in y} B) = (x \in X ⟼ \prod_{k \in A} B)$
17	16	eleq1d	$⊢ y = A \to ((x \in X ⟼ \prod_{k \in y} B) \in (J Cn K) \leftrightarrow (x \in X ⟼ \prod_{k \in A} B) \in (J Cn K))$
18		prod0	$⊢ \prod_{k \in \emptyset} B = 1$
19	18	mpteq2i	$⊢ (x \in X ⟼ \prod_{k \in \emptyset} B) = (x \in X ⟼ 1)$
20		eqidd	$⊢ x = y \to 1 = 1$
21	20	cbvmptv	$⊢ (x \in X ⟼ 1) = (y \in X ⟼ 1)$
22	19 21	eqtri	$⊢ (x \in X ⟼ \prod_{k \in \emptyset} B) = (y \in X ⟼ 1)$
23	22	a1i	$⊢ φ \to (x \in X ⟼ \prod_{k \in \emptyset} B) = (y \in X ⟼ 1)$
24	2	cnfldtopon	$⊢ K \in TopOn (ℂ)$
25	24	a1i	$⊢ φ \to K \in TopOn (ℂ)$
26		1cnd	$⊢ φ \to 1 \in ℂ$
27	3 25 26	cnmptc	$⊢ φ \to (y \in X ⟼ 1) \in (J Cn K)$
28	23 27	eqeltrd	$⊢ φ \to (x \in X ⟼ \prod_{k \in \emptyset} B) \in (J Cn K)$
29		nfcv	$⊢ \underline{Ⅎ} y \prod_{k \in z \cup \{w\}} B$
30		nfcv	$⊢ \underline{Ⅎ} x (z \cup \{w\})$
31		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ B$
32	30 31	nfcprod	$⊢ \underline{Ⅎ} x \prod_{k \in z \cup \{w\}} ⦋ y / x ⦌ B$
33		csbeq1a	$⊢ x = y \to B = ⦋ y / x ⦌ B$
34	33	prodeq2ad	$⊢ x = y \to \prod_{k \in z \cup \{w\}} B = \prod_{k \in z \cup \{w\}} ⦋ y / x ⦌ B$
35	29 32 34	cbvmpt	$⊢ (x \in X ⟼ \prod_{k \in z \cup \{w\}} B) = (y \in X ⟼ \prod_{k \in z \cup \{w\}} ⦋ y / x ⦌ B)$
36	35	a1i	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land (x \in X ⟼ \prod_{k \in z} B) \in (J Cn K)) \to (x \in X ⟼ \prod_{k \in z \cup \{w\}} B) = (y \in X ⟼ \prod_{k \in z \cup \{w\}} ⦋ y / x ⦌ B)$
37		nfv	$⊢ Ⅎ k (z \subseteq A \land w \in (A ∖ z))$
38	1 37	nfan	$⊢ Ⅎ k (φ \land (z \subseteq A \land w \in (A ∖ z)))$
39		nfcv	$⊢ \underline{Ⅎ} k X$
40		nfcv	$⊢ \underline{Ⅎ} k z$
41	40	nfcprod1	$⊢ \underline{Ⅎ} k \prod_{k \in z} B$
42	39 41	nfmpt	$⊢ \underline{Ⅎ} k (x \in X ⟼ \prod_{k \in z} B)$
43		nfcv	$⊢ \underline{Ⅎ} k (J Cn K)$
44	42 43	nfel	$⊢ Ⅎ k (x \in X ⟼ \prod_{k \in z} B) \in (J Cn K)$
45	38 44	nfan	$⊢ Ⅎ k ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land (x \in X ⟼ \prod_{k \in z} B) \in (J Cn K))$
46	3	ad2antrr	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land (x \in X ⟼ \prod_{k \in z} B) \in (J Cn K)) \to J \in TopOn (X)$
47	4	ad2antrr	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land (x \in X ⟼ \prod_{k \in z} B) \in (J Cn K)) \to A \in Fin$
48		nfcv	$⊢ \underline{Ⅎ} y B$
49	48 31 33	cbvmpt	$⊢ (x \in X ⟼ B) = (y \in X ⟼ ⦋ y / x ⦌ B)$
50	49	eqcomi	$⊢ (y \in X ⟼ ⦋ y / x ⦌ B) = (x \in X ⟼ B)$
51	50	a1i	$⊢ (φ \land k \in A) \to (y \in X ⟼ ⦋ y / x ⦌ B) = (x \in X ⟼ B)$
52	51 5	eqeltrd	$⊢ (φ \land k \in A) \to (y \in X ⟼ ⦋ y / x ⦌ B) \in (J Cn K)$
53	52	ad4ant14	$⊢ (((φ \land (z \subseteq A \land w \in (A ∖ z))) \land (x \in X ⟼ \prod_{k \in z} B) \in (J Cn K)) \land k \in A) \to (y \in X ⟼ ⦋ y / x ⦌ B) \in (J Cn K)$
54		simplrl	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land (x \in X ⟼ \prod_{k \in z} B) \in (J Cn K)) \to z \subseteq A$
55		simplrr	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land (x \in X ⟼ \prod_{k \in z} B) \in (J Cn K)) \to w \in (A ∖ z)$
56		nfcv	$⊢ \underline{Ⅎ} y \prod_{k \in z} B$
57		nfcv	$⊢ \underline{Ⅎ} x z$
58	57 31	nfcprod	$⊢ \underline{Ⅎ} x \prod_{k \in z} ⦋ y / x ⦌ B$
59	33	prodeq2sdv	$⊢ x = y \to \prod_{k \in z} B = \prod_{k \in z} ⦋ y / x ⦌ B$
60	56 58 59	cbvmpt	$⊢ (x \in X ⟼ \prod_{k \in z} B) = (y \in X ⟼ \prod_{k \in z} ⦋ y / x ⦌ B)$
61	60	eleq1i	$⊢ (x \in X ⟼ \prod_{k \in z} B) \in (J Cn K) \leftrightarrow (y \in X ⟼ \prod_{k \in z} ⦋ y / x ⦌ B) \in (J Cn K)$
62	61	biimpi	$⊢ (x \in X ⟼ \prod_{k \in z} B) \in (J Cn K) \to (y \in X ⟼ \prod_{k \in z} ⦋ y / x ⦌ B) \in (J Cn K)$
63	62	adantl	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land (x \in X ⟼ \prod_{k \in z} B) \in (J Cn K)) \to (y \in X ⟼ \prod_{k \in z} ⦋ y / x ⦌ B) \in (J Cn K)$
64	45 2 46 47 53 54 55 63	fprodcnlem	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land (x \in X ⟼ \prod_{k \in z} B) \in (J Cn K)) \to (y \in X ⟼ \prod_{k \in z \cup \{w\}} ⦋ y / x ⦌ B) \in (J Cn K)$
65	36 64	eqeltrd	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land (x \in X ⟼ \prod_{k \in z} B) \in (J Cn K)) \to (x \in X ⟼ \prod_{k \in z \cup \{w\}} B) \in (J Cn K)$
66	65	ex	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to ((x \in X ⟼ \prod_{k \in z} B) \in (J Cn K) \to (x \in X ⟼ \prod_{k \in z \cup \{w\}} B) \in (J Cn K))$
67	8 11 14 17 28 66 4	findcard2d	$⊢ φ \to (x \in X ⟼ \prod_{k \in A} B) \in (J Cn K)$

Metamath Proof Explorer

Theorem fprodcn

Proof