cncfuni

Description: A complex function on a subset of the complex numbers is continuous if its domain is the union of relatively open subsets over which the function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	cncfuni.acn	$⊢ φ \to A \subseteq ℂ$
	cncfuni.f	$⊢ φ \to F : A ⟶ ℂ$
	cncfuni.auni	$⊢ φ \to A \subseteq ⋃ B$
	cncfuni.opn	$⊢ (φ \land b \in B) \to A \cap b \in (TopOpen (ℂ_{fld}) ↾_{𝑡} A)$
	cncfuni.fcn	$⊢ (φ \land b \in B) \to ({F ↾}_{b}) : (A \cap b) \underset{cn}{⟶} ℂ$
Assertion	cncfuni	$⊢ φ \to F : A \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		cncfuni.acn	$⊢ φ \to A \subseteq ℂ$
2		cncfuni.f	$⊢ φ \to F : A ⟶ ℂ$
3		cncfuni.auni	$⊢ φ \to A \subseteq ⋃ B$
4		cncfuni.opn	$⊢ (φ \land b \in B) \to A \cap b \in (TopOpen (ℂ_{fld}) ↾_{𝑡} A)$
5		cncfuni.fcn	$⊢ (φ \land b \in B) \to ({F ↾}_{b}) : (A \cap b) \underset{cn}{⟶} ℂ$
6	3	sselda	$⊢ (φ \land x \in A) \to x \in ⋃ B$
7		eluni2	$⊢ x \in ⋃ B \leftrightarrow \exists b \in B x \in b$
8	6 7	sylib	$⊢ (φ \land x \in A) \to \exists b \in B x \in b$
9		simp1l	$⊢ ((φ \land x \in A) \land b \in B \land x \in b) \to φ$
10		simp2	$⊢ ((φ \land x \in A) \land b \in B \land x \in b) \to b \in B$
11		elin	$⊢ x \in (A \cap b) \leftrightarrow (x \in A \land x \in b)$
12	11	biimpri	$⊢ (x \in A \land x \in b) \to x \in (A \cap b)$
13	12	adantll	$⊢ ((φ \land x \in A) \land x \in b) \to x \in (A \cap b)$
14	13	3adant2	$⊢ ((φ \land x \in A) \land b \in B \land x \in b) \to x \in (A \cap b)$
15	2	fdmd	$⊢ φ \to dom F = A$
16	15	ineq2d	$⊢ φ \to b \cap dom F = b \cap A$
17		incom	$⊢ b \cap A = A \cap b$
18	16 17	eqtr2di	$⊢ φ \to A \cap b = b \cap dom F$
19	18	reseq2d	$⊢ φ \to {F ↾}_{(A \cap b)} = {F ↾}_{(b \cap dom F)}$
20		resindm	$⊢ {F ↾}_{(b \cap dom F)} = {F ↾}_{b}$
21	19 20	eqtrdi	$⊢ φ \to {F ↾}_{(A \cap b)} = {F ↾}_{b}$
22	1	ssinss1d	$⊢ φ \to A \cap b \subseteq ℂ$
23		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
24		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
25		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b) = TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)$
26	24	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
27		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
28	27	restid	$⊢ TopOpen (ℂ_{fld}) \in Top \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
29	26 28	ax-mp	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
30	29	eqcomi	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
31	24 25 30	cncfcn	$⊢ (A \cap b \subseteq ℂ \land ℂ \subseteq ℂ) \to (A \cap b) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) Cn TopOpen (ℂ_{fld})$
32	22 23 31	syl2anc	$⊢ φ \to (A \cap b) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) Cn TopOpen (ℂ_{fld})$
33	32	eqcomd	$⊢ φ \to (TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) Cn TopOpen (ℂ_{fld}) = (A \cap b) \underset{cn}{⟶} ℂ$
34	21 33	eleq12d	$⊢ φ \to ({F ↾}_{(A \cap b)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) Cn TopOpen (ℂ_{fld})) \leftrightarrow ({F ↾}_{b}) : (A \cap b) \underset{cn}{⟶} ℂ)$
35	34	adantr	$⊢ (φ \land b \in B) \to ({F ↾}_{(A \cap b)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) Cn TopOpen (ℂ_{fld})) \leftrightarrow ({F ↾}_{b}) : (A \cap b) \underset{cn}{⟶} ℂ)$
36	5 35	mpbird	$⊢ (φ \land b \in B) \to {F ↾}_{(A \cap b)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) Cn TopOpen (ℂ_{fld}))$
37	36	3adant3	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to {F ↾}_{(A \cap b)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) Cn TopOpen (ℂ_{fld}))$
38	24	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
39	38	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
40		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land A \cap b \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b) \in TopOn (A \cap b)$
41	39 22 40	syl2anc	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b) \in TopOn (A \cap b)$
42	41	3ad2ant1	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b) \in TopOn (A \cap b)$
43	38	a1i	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
44		cncnp	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b) \in TopOn (A \cap b) \land TopOpen (ℂ_{fld}) \in TopOn (ℂ)) \to ({F ↾}_{(A \cap b)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) Cn TopOpen (ℂ_{fld})) \leftrightarrow (({F ↾}_{(A \cap b)}) : A \cap b ⟶ ℂ \land \forall x \in (A \cap b) {F ↾}_{(A \cap b)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) CnP TopOpen (ℂ_{fld})) (x)))$
45	42 43 44	syl2anc	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to ({F ↾}_{(A \cap b)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) Cn TopOpen (ℂ_{fld})) \leftrightarrow (({F ↾}_{(A \cap b)}) : A \cap b ⟶ ℂ \land \forall x \in (A \cap b) {F ↾}_{(A \cap b)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) CnP TopOpen (ℂ_{fld})) (x)))$
46	37 45	mpbid	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to (({F ↾}_{(A \cap b)}) : A \cap b ⟶ ℂ \land \forall x \in (A \cap b) {F ↾}_{(A \cap b)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) CnP TopOpen (ℂ_{fld})) (x))$
47	46	simprd	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to \forall x \in (A \cap b) {F ↾}_{(A \cap b)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) CnP TopOpen (ℂ_{fld})) (x)$
48		simp3	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to x \in (A \cap b)$
49		rspa	$⊢ (\forall x \in (A \cap b) {F ↾}_{(A \cap b)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) CnP TopOpen (ℂ_{fld})) (x) \land x \in (A \cap b)) \to {F ↾}_{(A \cap b)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) CnP TopOpen (ℂ_{fld})) (x)$
50	47 48 49	syl2anc	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to {F ↾}_{(A \cap b)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) CnP TopOpen (ℂ_{fld})) (x)$
51	26	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in Top$
52		inss1	$⊢ A \cap b \subseteq A$
53	52	a1i	$⊢ φ \to A \cap b \subseteq A$
54		cnex	$⊢ ℂ \in V$
55	54	ssex	$⊢ A \subseteq ℂ \to A \in V$
56	1 55	syl	$⊢ φ \to A \in V$
57		restabs	$⊢ (TopOpen (ℂ_{fld}) \in Top \land A \cap b \subseteq A \land A \in V) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} A) ↾_{𝑡} (A \cap b) = TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)$
58	51 53 56 57	syl3anc	$⊢ φ \to (TopOpen (ℂ_{fld}) ↾_{𝑡} A) ↾_{𝑡} (A \cap b) = TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)$
59	58	eqcomd	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b) = (TopOpen (ℂ_{fld}) ↾_{𝑡} A) ↾_{𝑡} (A \cap b)$
60	59	oveq1d	$⊢ φ \to (TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) CnP TopOpen (ℂ_{fld}) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) ↾_{𝑡} (A \cap b)) CnP TopOpen (ℂ_{fld})$
61	60	fveq1d	$⊢ φ \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) CnP TopOpen (ℂ_{fld})) (x) = (((TopOpen (ℂ_{fld}) ↾_{𝑡} A) ↾_{𝑡} (A \cap b)) CnP TopOpen (ℂ_{fld})) (x)$
62	61	3ad2ant1	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cap b)) CnP TopOpen (ℂ_{fld})) (x) = (((TopOpen (ℂ_{fld}) ↾_{𝑡} A) ↾_{𝑡} (A \cap b)) CnP TopOpen (ℂ_{fld})) (x)$
63	50 62	eleqtrd	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to {F ↾}_{(A \cap b)} \in (((TopOpen (ℂ_{fld}) ↾_{𝑡} A) ↾_{𝑡} (A \cap b)) CnP TopOpen (ℂ_{fld})) (x)$
64		resttop	$⊢ (TopOpen (ℂ_{fld}) \in Top \land A \in V) \to TopOpen (ℂ_{fld}) ↾_{𝑡} A \in Top$
65	51 56 64	syl2anc	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} A \in Top$
66	65	3ad2ant1	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} A \in Top$
67	27	restuni	$⊢ (TopOpen (ℂ_{fld}) \in Top \land A \subseteq ℂ) \to A = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} A)$
68	51 1 67	syl2anc	$⊢ φ \to A = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} A)$
69	53 68	sseqtrd	$⊢ φ \to A \cap b \subseteq ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} A)$
70	69	3ad2ant1	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to A \cap b \subseteq ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} A)$
71	4	3adant3	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to A \cap b \in (TopOpen (ℂ_{fld}) ↾_{𝑡} A)$
72		eqid	$⊢ ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} A) = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} A)$
73	72	isopn3	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} A \in Top \land A \cap b \subseteq ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} A)) \to (A \cap b \in (TopOpen (ℂ_{fld}) ↾_{𝑡} A) \leftrightarrow int (TopOpen (ℂ_{fld}) ↾_{𝑡} A) (A \cap b) = A \cap b)$
74	66 70 73	syl2anc	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to (A \cap b \in (TopOpen (ℂ_{fld}) ↾_{𝑡} A) \leftrightarrow int (TopOpen (ℂ_{fld}) ↾_{𝑡} A) (A \cap b) = A \cap b)$
75	71 74	mpbid	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} A) (A \cap b) = A \cap b$
76	48 75	eleqtrrd	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to x \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} A) (A \cap b)$
77	68 2	feq2dd	$⊢ φ \to F : ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} A) ⟶ ℂ$
78	77	3ad2ant1	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to F : ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} A) ⟶ ℂ$
79	72 27	cnprest	$⊢ ((TopOpen (ℂ_{fld}) ↾_{𝑡} A \in Top \land A \cap b \subseteq ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} A)) \land (x \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} A) (A \cap b) \land F : ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} A) ⟶ ℂ)) \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x) \leftrightarrow {F ↾}_{(A \cap b)} \in (((TopOpen (ℂ_{fld}) ↾_{𝑡} A) ↾_{𝑡} (A \cap b)) CnP TopOpen (ℂ_{fld})) (x))$
80	66 70 76 78 79	syl22anc	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x) \leftrightarrow {F ↾}_{(A \cap b)} \in (((TopOpen (ℂ_{fld}) ↾_{𝑡} A) ↾_{𝑡} (A \cap b)) CnP TopOpen (ℂ_{fld})) (x))$
81	63 80	mpbird	$⊢ (φ \land b \in B \land x \in (A \cap b)) \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x)$
82	9 10 14 81	syl3anc	$⊢ ((φ \land x \in A) \land b \in B \land x \in b) \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x)$
83	82	rexlimdv3a	$⊢ (φ \land x \in A) \to (\exists b \in B x \in b \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x))$
84	8 83	mpd	$⊢ (φ \land x \in A) \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x)$
85	84	ralrimiva	$⊢ φ \to \forall x \in A F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x)$
86		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land A \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} A \in TopOn (A)$
87	39 1 86	syl2anc	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} A \in TopOn (A)$
88		cncnp	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} A \in TopOn (A) \land TopOpen (ℂ_{fld}) \in TopOn (ℂ)) \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) Cn TopOpen (ℂ_{fld})) \leftrightarrow (F : A ⟶ ℂ \land \forall x \in A F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x)))$
89	87 39 88	syl2anc	$⊢ φ \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) Cn TopOpen (ℂ_{fld})) \leftrightarrow (F : A ⟶ ℂ \land \forall x \in A F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) CnP TopOpen (ℂ_{fld})) (x)))$
90	2 85 89	mpbir2and	$⊢ φ \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} A) Cn TopOpen (ℂ_{fld}))$
91		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} A = TopOpen (ℂ_{fld}) ↾_{𝑡} A$
92	24 91 30	cncfcn	$⊢ (A \subseteq ℂ \land ℂ \subseteq ℂ) \to A \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} A) Cn TopOpen (ℂ_{fld})$
93	1 23 92	syl2anc	$⊢ φ \to A \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} A) Cn TopOpen (ℂ_{fld})$
94	90 93	eleqtrrd	$⊢ φ \to F : A \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem cncfuni

Proof