fprodcncf

Description: The finite product of continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fprodcncf.a	$⊢ φ \to A \subseteq ℂ$
	fprodcncf.b	$⊢ φ \to B \in Fin$
	fprodcncf.c	$⊢ (φ \land x \in A \land k \in B) \to C \in ℂ$
	fprodcncf.cn	$⊢ (φ \land k \in B) \to (x \in A ⟼ C) : A \underset{cn}{⟶} ℂ$
Assertion	fprodcncf	$⊢ φ \to (x \in A ⟼ \prod_{k \in B} C) : A \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		fprodcncf.a	$⊢ φ \to A \subseteq ℂ$
2		fprodcncf.b	$⊢ φ \to B \in Fin$
3		fprodcncf.c	$⊢ (φ \land x \in A \land k \in B) \to C \in ℂ$
4		fprodcncf.cn	$⊢ (φ \land k \in B) \to (x \in A ⟼ C) : A \underset{cn}{⟶} ℂ$
5		prodeq1	$⊢ w = \emptyset \to \prod_{k \in w} C = \prod_{k \in \emptyset} C$
6	5	mpteq2dv	$⊢ w = \emptyset \to (x \in A ⟼ \prod_{k \in w} C) = (x \in A ⟼ \prod_{k \in \emptyset} C)$
7	6	eleq1d	$⊢ w = \emptyset \to ((x \in A ⟼ \prod_{k \in w} C) : A \underset{cn}{⟶} ℂ \leftrightarrow (x \in A ⟼ \prod_{k \in \emptyset} C) : A \underset{cn}{⟶} ℂ)$
8		prodeq1	$⊢ w = z \to \prod_{k \in w} C = \prod_{k \in z} C$
9	8	mpteq2dv	$⊢ w = z \to (x \in A ⟼ \prod_{k \in w} C) = (x \in A ⟼ \prod_{k \in z} C)$
10	9	eleq1d	$⊢ w = z \to ((x \in A ⟼ \prod_{k \in w} C) : A \underset{cn}{⟶} ℂ \leftrightarrow (x \in A ⟼ \prod_{k \in z} C) : A \underset{cn}{⟶} ℂ)$
11		prodeq1	$⊢ w = z \cup \{y\} \to \prod_{k \in w} C = \prod_{k \in z \cup \{y\}} C$
12	11	mpteq2dv	$⊢ w = z \cup \{y\} \to (x \in A ⟼ \prod_{k \in w} C) = (x \in A ⟼ \prod_{k \in z \cup \{y\}} C)$
13	12	eleq1d	$⊢ w = z \cup \{y\} \to ((x \in A ⟼ \prod_{k \in w} C) : A \underset{cn}{⟶} ℂ \leftrightarrow (x \in A ⟼ \prod_{k \in z \cup \{y\}} C) : A \underset{cn}{⟶} ℂ)$
14		prodeq1	$⊢ w = B \to \prod_{k \in w} C = \prod_{k \in B} C$
15	14	mpteq2dv	$⊢ w = B \to (x \in A ⟼ \prod_{k \in w} C) = (x \in A ⟼ \prod_{k \in B} C)$
16	15	eleq1d	$⊢ w = B \to ((x \in A ⟼ \prod_{k \in w} C) : A \underset{cn}{⟶} ℂ \leftrightarrow (x \in A ⟼ \prod_{k \in B} C) : A \underset{cn}{⟶} ℂ)$
17		prod0	$⊢ \prod_{k \in \emptyset} C = 1$
18	17	a1i	$⊢ φ \to \prod_{k \in \emptyset} C = 1$
19	18	mpteq2dv	$⊢ φ \to (x \in A ⟼ \prod_{k \in \emptyset} C) = (x \in A ⟼ 1)$
20		1cnd	$⊢ φ \to 1 \in ℂ$
21		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
22	1 20 21	constcncfg	$⊢ φ \to (x \in A ⟼ 1) : A \underset{cn}{⟶} ℂ$
23	19 22	eqeltrd	$⊢ φ \to (x \in A ⟼ \prod_{k \in \emptyset} C) : A \underset{cn}{⟶} ℂ$
24		nfcv	$⊢ \underline{Ⅎ} u \prod_{k \in z \cup \{y\}} C$
25		nfcv	$⊢ \underline{Ⅎ} x (z \cup \{y\})$
26		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ u / x ⦌ C$
27	25 26	nfcprod	$⊢ \underline{Ⅎ} x \prod_{k \in z \cup \{y\}} ⦋ u / x ⦌ C$
28		csbeq1a	$⊢ x = u \to C = ⦋ u / x ⦌ C$
29	28	adantr	$⊢ (x = u \land k \in (z \cup \{y\})) \to C = ⦋ u / x ⦌ C$
30	29	prodeq2dv	$⊢ x = u \to \prod_{k \in z \cup \{y\}} C = \prod_{k \in z \cup \{y\}} ⦋ u / x ⦌ C$
31	24 27 30	cbvmpt	$⊢ (x \in A ⟼ \prod_{k \in z \cup \{y\}} C) = (u \in A ⟼ \prod_{k \in z \cup \{y\}} ⦋ u / x ⦌ C)$
32	31	a1i	$⊢ ((φ \land (z \subseteq B \land y \in (B ∖ z))) \land (x \in A ⟼ \prod_{k \in z} C) : A \underset{cn}{⟶} ℂ) \to (x \in A ⟼ \prod_{k \in z \cup \{y\}} C) = (u \in A ⟼ \prod_{k \in z \cup \{y\}} ⦋ u / x ⦌ C)$
33		nfv	$⊢ Ⅎ k ((φ \land (z \subseteq B \land y \in (B ∖ z))) \land u \in A)$
34		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ y / k ⦌ ⦋ u / x ⦌ C$
35	2	adantr	$⊢ (φ \land z \subseteq B) \to B \in Fin$
36		simpr	$⊢ (φ \land z \subseteq B) \to z \subseteq B$
37		ssfi	$⊢ (B \in Fin \land z \subseteq B) \to z \in Fin$
38	35 36 37	syl2anc	$⊢ (φ \land z \subseteq B) \to z \in Fin$
39	38	adantrr	$⊢ (φ \land (z \subseteq B \land y \in (B ∖ z))) \to z \in Fin$
40	39	adantr	$⊢ ((φ \land (z \subseteq B \land y \in (B ∖ z))) \land u \in A) \to z \in Fin$
41		vex	$⊢ y \in V$
42	41	a1i	$⊢ ((φ \land (z \subseteq B \land y \in (B ∖ z))) \land u \in A) \to y \in V$
43		eldifn	$⊢ y \in (B ∖ z) \to \neg y \in z$
44	43	ad2antll	$⊢ (φ \land (z \subseteq B \land y \in (B ∖ z))) \to \neg y \in z$
45	44	adantr	$⊢ ((φ \land (z \subseteq B \land y \in (B ∖ z))) \land u \in A) \to \neg y \in z$
46		simplll	$⊢ (((φ \land (z \subseteq B \land y \in (B ∖ z))) \land u \in A) \land k \in z) \to φ$
47		simplr	$⊢ (((φ \land (z \subseteq B \land y \in (B ∖ z))) \land u \in A) \land k \in z) \to u \in A$
48	36	adantrr	$⊢ (φ \land (z \subseteq B \land y \in (B ∖ z))) \to z \subseteq B$
49	48	ad2antrr	$⊢ (((φ \land (z \subseteq B \land y \in (B ∖ z))) \land u \in A) \land k \in z) \to z \subseteq B$
50		simpr	$⊢ (((φ \land (z \subseteq B \land y \in (B ∖ z))) \land u \in A) \land k \in z) \to k \in z$
51	49 50	sseldd	$⊢ (((φ \land (z \subseteq B \land y \in (B ∖ z))) \land u \in A) \land k \in z) \to k \in B$
52		nfv	$⊢ Ⅎ x (φ \land u \in A \land k \in B)$
53	26	nfel1	$⊢ Ⅎ x ⦋ u / x ⦌ C \in ℂ$
54	52 53	nfim	$⊢ Ⅎ x ((φ \land u \in A \land k \in B) \to ⦋ u / x ⦌ C \in ℂ)$
55		eleq1w	$⊢ x = u \to (x \in A \leftrightarrow u \in A)$
56	55	3anbi2d	$⊢ x = u \to ((φ \land x \in A \land k \in B) \leftrightarrow (φ \land u \in A \land k \in B))$
57	28	eleq1d	$⊢ x = u \to (C \in ℂ \leftrightarrow ⦋ u / x ⦌ C \in ℂ)$
58	56 57	imbi12d	$⊢ x = u \to (((φ \land x \in A \land k \in B) \to C \in ℂ) \leftrightarrow ((φ \land u \in A \land k \in B) \to ⦋ u / x ⦌ C \in ℂ))$
59	54 58 3	chvarfv	$⊢ (φ \land u \in A \land k \in B) \to ⦋ u / x ⦌ C \in ℂ$
60	46 47 51 59	syl3anc	$⊢ (((φ \land (z \subseteq B \land y \in (B ∖ z))) \land u \in A) \land k \in z) \to ⦋ u / x ⦌ C \in ℂ$
61		csbeq1a	$⊢ k = y \to ⦋ u / x ⦌ C = ⦋ y / k ⦌ ⦋ u / x ⦌ C$
62		simpll	$⊢ ((φ \land (z \subseteq B \land y \in (B ∖ z))) \land u \in A) \to φ$
63		eldifi	$⊢ y \in (B ∖ z) \to y \in B$
64	63	ad2antll	$⊢ (φ \land (z \subseteq B \land y \in (B ∖ z))) \to y \in B$
65	64	adantr	$⊢ ((φ \land (z \subseteq B \land y \in (B ∖ z))) \land u \in A) \to y \in B$
66		simpr	$⊢ ((φ \land (z \subseteq B \land y \in (B ∖ z))) \land u \in A) \to u \in A$
67		simpll	$⊢ ((φ \land y \in B) \land u \in A) \to φ$
68		simpr	$⊢ ((φ \land y \in B) \land u \in A) \to u \in A$
69		simplr	$⊢ ((φ \land y \in B) \land u \in A) \to y \in B$
70		nfv	$⊢ Ⅎ k (φ \land u \in A \land y \in B)$
71		nfcv	$⊢ \underline{Ⅎ} k ℂ$
72	34 71	nfel	$⊢ Ⅎ k ⦋ y / k ⦌ ⦋ u / x ⦌ C \in ℂ$
73	70 72	nfim	$⊢ Ⅎ k ((φ \land u \in A \land y \in B) \to ⦋ y / k ⦌ ⦋ u / x ⦌ C \in ℂ)$
74		eleq1w	$⊢ k = y \to (k \in B \leftrightarrow y \in B)$
75	74	3anbi3d	$⊢ k = y \to ((φ \land u \in A \land k \in B) \leftrightarrow (φ \land u \in A \land y \in B))$
76	61	eleq1d	$⊢ k = y \to (⦋ u / x ⦌ C \in ℂ \leftrightarrow ⦋ y / k ⦌ ⦋ u / x ⦌ C \in ℂ)$
77	75 76	imbi12d	$⊢ k = y \to (((φ \land u \in A \land k \in B) \to ⦋ u / x ⦌ C \in ℂ) \leftrightarrow ((φ \land u \in A \land y \in B) \to ⦋ y / k ⦌ ⦋ u / x ⦌ C \in ℂ))$
78	73 77 59	chvarfv	$⊢ (φ \land u \in A \land y \in B) \to ⦋ y / k ⦌ ⦋ u / x ⦌ C \in ℂ$
79	67 68 69 78	syl3anc	$⊢ ((φ \land y \in B) \land u \in A) \to ⦋ y / k ⦌ ⦋ u / x ⦌ C \in ℂ$
80	62 65 66 79	syl21anc	$⊢ ((φ \land (z \subseteq B \land y \in (B ∖ z))) \land u \in A) \to ⦋ y / k ⦌ ⦋ u / x ⦌ C \in ℂ$
81	33 34 40 42 45 60 61 80	fprodsplitsn	$⊢ ((φ \land (z \subseteq B \land y \in (B ∖ z))) \land u \in A) \to \prod_{k \in z \cup \{y\}} ⦋ u / x ⦌ C = \prod_{k \in z} ⦋ u / x ⦌ C ⦋ y / k ⦌ ⦋ u / x ⦌ C$
82	81	mpteq2dva	$⊢ (φ \land (z \subseteq B \land y \in (B ∖ z))) \to (u \in A ⟼ \prod_{k \in z \cup \{y\}} ⦋ u / x ⦌ C) = (u \in A ⟼ \prod_{k \in z} ⦋ u / x ⦌ C ⦋ y / k ⦌ ⦋ u / x ⦌ C)$
83	82	adantr	$⊢ ((φ \land (z \subseteq B \land y \in (B ∖ z))) \land (x \in A ⟼ \prod_{k \in z} C) : A \underset{cn}{⟶} ℂ) \to (u \in A ⟼ \prod_{k \in z \cup \{y\}} ⦋ u / x ⦌ C) = (u \in A ⟼ \prod_{k \in z} ⦋ u / x ⦌ C ⦋ y / k ⦌ ⦋ u / x ⦌ C)$
84		nfcv	$⊢ \underline{Ⅎ} u \prod_{k \in z} C$
85		nfcv	$⊢ \underline{Ⅎ} x z$
86	85 26	nfcprod	$⊢ \underline{Ⅎ} x \prod_{k \in z} ⦋ u / x ⦌ C$
87	28	adantr	$⊢ (x = u \land k \in z) \to C = ⦋ u / x ⦌ C$
88	87	prodeq2dv	$⊢ x = u \to \prod_{k \in z} C = \prod_{k \in z} ⦋ u / x ⦌ C$
89	84 86 88	cbvmpt	$⊢ (x \in A ⟼ \prod_{k \in z} C) = (u \in A ⟼ \prod_{k \in z} ⦋ u / x ⦌ C)$
90	89	eqcomi	$⊢ (u \in A ⟼ \prod_{k \in z} ⦋ u / x ⦌ C) = (x \in A ⟼ \prod_{k \in z} C)$
91	90	a1i	$⊢ (x \in A ⟼ \prod_{k \in z} C) : A \underset{cn}{⟶} ℂ \to (u \in A ⟼ \prod_{k \in z} ⦋ u / x ⦌ C) = (x \in A ⟼ \prod_{k \in z} C)$
92		id	$⊢ (x \in A ⟼ \prod_{k \in z} C) : A \underset{cn}{⟶} ℂ \to (x \in A ⟼ \prod_{k \in z} C) : A \underset{cn}{⟶} ℂ$
93	91 92	eqeltrd	$⊢ (x \in A ⟼ \prod_{k \in z} C) : A \underset{cn}{⟶} ℂ \to (u \in A ⟼ \prod_{k \in z} ⦋ u / x ⦌ C) : A \underset{cn}{⟶} ℂ$
94	93	adantl	$⊢ ((φ \land (z \subseteq B \land y \in (B ∖ z))) \land (x \in A ⟼ \prod_{k \in z} C) : A \underset{cn}{⟶} ℂ) \to (u \in A ⟼ \prod_{k \in z} ⦋ u / x ⦌ C) : A \underset{cn}{⟶} ℂ$
95		nfv	$⊢ Ⅎ k (φ \land y \in B)$
96		nfcv	$⊢ \underline{Ⅎ} k A$
97	96 34	nfmpt	$⊢ \underline{Ⅎ} k (u \in A ⟼ ⦋ y / k ⦌ ⦋ u / x ⦌ C)$
98		nfcv	$⊢ \underline{Ⅎ} k (A \underset{cn}{⟶} ℂ)$
99	97 98	nfel	$⊢ Ⅎ k (u \in A ⟼ ⦋ y / k ⦌ ⦋ u / x ⦌ C) : A \underset{cn}{⟶} ℂ$
100	95 99	nfim	$⊢ Ⅎ k ((φ \land y \in B) \to (u \in A ⟼ ⦋ y / k ⦌ ⦋ u / x ⦌ C) : A \underset{cn}{⟶} ℂ)$
101	74	anbi2d	$⊢ k = y \to ((φ \land k \in B) \leftrightarrow (φ \land y \in B))$
102	61	adantr	$⊢ (k = y \land u \in A) \to ⦋ u / x ⦌ C = ⦋ y / k ⦌ ⦋ u / x ⦌ C$
103	102	mpteq2dva	$⊢ k = y \to (u \in A ⟼ ⦋ u / x ⦌ C) = (u \in A ⟼ ⦋ y / k ⦌ ⦋ u / x ⦌ C)$
104	103	eleq1d	$⊢ k = y \to ((u \in A ⟼ ⦋ u / x ⦌ C) : A \underset{cn}{⟶} ℂ \leftrightarrow (u \in A ⟼ ⦋ y / k ⦌ ⦋ u / x ⦌ C) : A \underset{cn}{⟶} ℂ)$
105	101 104	imbi12d	$⊢ k = y \to (((φ \land k \in B) \to (u \in A ⟼ ⦋ u / x ⦌ C) : A \underset{cn}{⟶} ℂ) \leftrightarrow ((φ \land y \in B) \to (u \in A ⟼ ⦋ y / k ⦌ ⦋ u / x ⦌ C) : A \underset{cn}{⟶} ℂ))$
106		nfcv	$⊢ \underline{Ⅎ} u C$
107	106 26 28	cbvmpt	$⊢ (x \in A ⟼ C) = (u \in A ⟼ ⦋ u / x ⦌ C)$
108	107 4	eqeltrrid	$⊢ (φ \land k \in B) \to (u \in A ⟼ ⦋ u / x ⦌ C) : A \underset{cn}{⟶} ℂ$
109	100 105 108	chvarfv	$⊢ (φ \land y \in B) \to (u \in A ⟼ ⦋ y / k ⦌ ⦋ u / x ⦌ C) : A \underset{cn}{⟶} ℂ$
110	64 109	syldan	$⊢ (φ \land (z \subseteq B \land y \in (B ∖ z))) \to (u \in A ⟼ ⦋ y / k ⦌ ⦋ u / x ⦌ C) : A \underset{cn}{⟶} ℂ$
111	110	adantr	$⊢ ((φ \land (z \subseteq B \land y \in (B ∖ z))) \land (x \in A ⟼ \prod_{k \in z} C) : A \underset{cn}{⟶} ℂ) \to (u \in A ⟼ ⦋ y / k ⦌ ⦋ u / x ⦌ C) : A \underset{cn}{⟶} ℂ$
112	94 111	mulcncf	$⊢ ((φ \land (z \subseteq B \land y \in (B ∖ z))) \land (x \in A ⟼ \prod_{k \in z} C) : A \underset{cn}{⟶} ℂ) \to (u \in A ⟼ \prod_{k \in z} ⦋ u / x ⦌ C ⦋ y / k ⦌ ⦋ u / x ⦌ C) : A \underset{cn}{⟶} ℂ$
113	83 112	eqeltrd	$⊢ ((φ \land (z \subseteq B \land y \in (B ∖ z))) \land (x \in A ⟼ \prod_{k \in z} C) : A \underset{cn}{⟶} ℂ) \to (u \in A ⟼ \prod_{k \in z \cup \{y\}} ⦋ u / x ⦌ C) : A \underset{cn}{⟶} ℂ$
114	32 113	eqeltrd	$⊢ ((φ \land (z \subseteq B \land y \in (B ∖ z))) \land (x \in A ⟼ \prod_{k \in z} C) : A \underset{cn}{⟶} ℂ) \to (x \in A ⟼ \prod_{k \in z \cup \{y\}} C) : A \underset{cn}{⟶} ℂ$
115	114	ex	$⊢ (φ \land (z \subseteq B \land y \in (B ∖ z))) \to ((x \in A ⟼ \prod_{k \in z} C) : A \underset{cn}{⟶} ℂ \to (x \in A ⟼ \prod_{k \in z \cup \{y\}} C) : A \underset{cn}{⟶} ℂ)$
116	7 10 13 16 23 115 2	findcard2d	$⊢ φ \to (x \in A ⟼ \prod_{k \in B} C) : A \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem fprodcncf

Proof