cncfco

Description: The composition of two continuous maps on complex numbers is also continuous. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 25-Aug-2014)

	Ref	Expression
Hypotheses	cncfco.4	$⊢ φ \to F : A \underset{cn}{⟶} B$
	cncfco.5	$⊢ φ \to G : B \underset{cn}{⟶} C$
Assertion	cncfco	$⊢ φ \to (G \circ F) : A \underset{cn}{⟶} C$

Proof

Step	Hyp	Ref	Expression
1		cncfco.4	$⊢ φ \to F : A \underset{cn}{⟶} B$
2		cncfco.5	$⊢ φ \to G : B \underset{cn}{⟶} C$
3		cncff	$⊢ G : B \underset{cn}{⟶} C \to G : B ⟶ C$
4	2 3	syl	$⊢ φ \to G : B ⟶ C$
5		cncff	$⊢ F : A \underset{cn}{⟶} B \to F : A ⟶ B$
6	1 5	syl	$⊢ φ \to F : A ⟶ B$
7		fco	$⊢ (G : B ⟶ C \land F : A ⟶ B) \to (G \circ F) : A ⟶ C$
8	4 6 7	syl2anc	$⊢ φ \to (G \circ F) : A ⟶ C$
9	2	adantr	$⊢ (φ \land (x \in A \land y \in ℝ^{+})) \to G : B \underset{cn}{⟶} C$
10	6	adantr	$⊢ (φ \land (x \in A \land y \in ℝ^{+})) \to F : A ⟶ B$
11		simprl	$⊢ (φ \land (x \in A \land y \in ℝ^{+})) \to x \in A$
12	10 11	ffvelrnd	$⊢ (φ \land (x \in A \land y \in ℝ^{+})) \to F (x) \in B$
13		simprr	$⊢ (φ \land (x \in A \land y \in ℝ^{+})) \to y \in ℝ^{+}$
14		cncfi	$⊢ (G : B \underset{cn}{⟶} C \land F (x) \in B \land y \in ℝ^{+}) \to \exists u \in ℝ^{+} \forall v \in B (\|v - F (x)\| < u \to \|G (v) - G (F (x))\| < y)$
15	9 12 13 14	syl3anc	$⊢ (φ \land (x \in A \land y \in ℝ^{+})) \to \exists u \in ℝ^{+} \forall v \in B (\|v - F (x)\| < u \to \|G (v) - G (F (x))\| < y)$
16	1	ad2antrr	$⊢ ((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \to F : A \underset{cn}{⟶} B$
17		simplrl	$⊢ ((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \to x \in A$
18		simpr	$⊢ ((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \to u \in ℝ^{+}$
19		cncfi	$⊢ (F : A \underset{cn}{⟶} B \land x \in A \land u \in ℝ^{+}) \to \exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|F (w) - F (x)\| < u)$
20	16 17 18 19	syl3anc	$⊢ ((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \to \exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|F (w) - F (x)\| < u)$
21	6	ad3antrrr	$⊢ (((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land (z \in ℝ^{+} \land w \in A)) \to F : A ⟶ B$
22		simprr	$⊢ (((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land (z \in ℝ^{+} \land w \in A)) \to w \in A$
23	21 22	ffvelrnd	$⊢ (((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land (z \in ℝ^{+} \land w \in A)) \to F (w) \in B$
24		fvoveq1	$⊢ v = F (w) \to \|v - F (x)\| = \|F (w) - F (x)\|$
25	24	breq1d	$⊢ v = F (w) \to (\|v - F (x)\| < u \leftrightarrow \|F (w) - F (x)\| < u)$
26	25	imbrov2fvoveq	$⊢ v = F (w) \to ((\|v - F (x)\| < u \to \|G (v) - G (F (x))\| < y) \leftrightarrow (\|F (w) - F (x)\| < u \to \|G (F (w)) - G (F (x))\| < y))$
27	26	rspcv	$⊢ F (w) \in B \to (\forall v \in B (\|v - F (x)\| < u \to \|G (v) - G (F (x))\| < y) \to (\|F (w) - F (x)\| < u \to \|G (F (w)) - G (F (x))\| < y))$
28	23 27	syl	$⊢ (((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land (z \in ℝ^{+} \land w \in A)) \to (\forall v \in B (\|v - F (x)\| < u \to \|G (v) - G (F (x))\| < y) \to (\|F (w) - F (x)\| < u \to \|G (F (w)) - G (F (x))\| < y))$
29		fvco3	$⊢ (F : A ⟶ B \land w \in A) \to (G \circ F) (w) = G (F (w))$
30	21 22 29	syl2anc	$⊢ (((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land (z \in ℝ^{+} \land w \in A)) \to (G \circ F) (w) = G (F (w))$
31	17	adantr	$⊢ (((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land (z \in ℝ^{+} \land w \in A)) \to x \in A$
32		fvco3	$⊢ (F : A ⟶ B \land x \in A) \to (G \circ F) (x) = G (F (x))$
33	21 31 32	syl2anc	$⊢ (((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land (z \in ℝ^{+} \land w \in A)) \to (G \circ F) (x) = G (F (x))$
34	30 33	oveq12d	$⊢ (((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land (z \in ℝ^{+} \land w \in A)) \to (G \circ F) (w) - (G \circ F) (x) = G (F (w)) - G (F (x))$
35	34	fveq2d	$⊢ (((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land (z \in ℝ^{+} \land w \in A)) \to \|(G \circ F) (w) - (G \circ F) (x)\| = \|G (F (w)) - G (F (x))\|$
36	35	breq1d	$⊢ (((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land (z \in ℝ^{+} \land w \in A)) \to (\|(G \circ F) (w) - (G \circ F) (x)\| < y \leftrightarrow \|G (F (w)) - G (F (x))\| < y)$
37	36	imbi2d	$⊢ (((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land (z \in ℝ^{+} \land w \in A)) \to ((\|F (w) - F (x)\| < u \to \|(G \circ F) (w) - (G \circ F) (x)\| < y) \leftrightarrow (\|F (w) - F (x)\| < u \to \|G (F (w)) - G (F (x))\| < y))$
38	28 37	sylibrd	$⊢ (((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land (z \in ℝ^{+} \land w \in A)) \to (\forall v \in B (\|v - F (x)\| < u \to \|G (v) - G (F (x))\| < y) \to (\|F (w) - F (x)\| < u \to \|(G \circ F) (w) - (G \circ F) (x)\| < y))$
39	38	imp	$⊢ ((((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land (z \in ℝ^{+} \land w \in A)) \land \forall v \in B (\|v - F (x)\| < u \to \|G (v) - G (F (x))\| < y)) \to (\|F (w) - F (x)\| < u \to \|(G \circ F) (w) - (G \circ F) (x)\| < y)$
40	39	an32s	$⊢ ((((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land \forall v \in B (\|v - F (x)\| < u \to \|G (v) - G (F (x))\| < y)) \land (z \in ℝ^{+} \land w \in A)) \to (\|F (w) - F (x)\| < u \to \|(G \circ F) (w) - (G \circ F) (x)\| < y)$
41	40	imim2d	$⊢ ((((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land \forall v \in B (\|v - F (x)\| < u \to \|G (v) - G (F (x))\| < y)) \land (z \in ℝ^{+} \land w \in A)) \to ((\|w - x\| < z \to \|F (w) - F (x)\| < u) \to (\|w - x\| < z \to \|(G \circ F) (w) - (G \circ F) (x)\| < y))$
42	41	anassrs	$⊢ (((((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land \forall v \in B (\|v - F (x)\| < u \to \|G (v) - G (F (x))\| < y)) \land z \in ℝ^{+}) \land w \in A) \to ((\|w - x\| < z \to \|F (w) - F (x)\| < u) \to (\|w - x\| < z \to \|(G \circ F) (w) - (G \circ F) (x)\| < y))$
43	42	ralimdva	$⊢ ((((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land \forall v \in B (\|v - F (x)\| < u \to \|G (v) - G (F (x))\| < y)) \land z \in ℝ^{+}) \to (\forall w \in A (\|w - x\| < z \to \|F (w) - F (x)\| < u) \to \forall w \in A (\|w - x\| < z \to \|(G \circ F) (w) - (G \circ F) (x)\| < y))$
44	43	reximdva	$⊢ (((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \land \forall v \in B (\|v - F (x)\| < u \to \|G (v) - G (F (x))\| < y)) \to (\exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|F (w) - F (x)\| < u) \to \exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|(G \circ F) (w) - (G \circ F) (x)\| < y))$
45	44	ex	$⊢ ((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \to (\forall v \in B (\|v - F (x)\| < u \to \|G (v) - G (F (x))\| < y) \to (\exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|F (w) - F (x)\| < u) \to \exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|(G \circ F) (w) - (G \circ F) (x)\| < y)))$
46	20 45	mpid	$⊢ ((φ \land (x \in A \land y \in ℝ^{+})) \land u \in ℝ^{+}) \to (\forall v \in B (\|v - F (x)\| < u \to \|G (v) - G (F (x))\| < y) \to \exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|(G \circ F) (w) - (G \circ F) (x)\| < y))$
47	46	rexlimdva	$⊢ (φ \land (x \in A \land y \in ℝ^{+})) \to (\exists u \in ℝ^{+} \forall v \in B (\|v - F (x)\| < u \to \|G (v) - G (F (x))\| < y) \to \exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|(G \circ F) (w) - (G \circ F) (x)\| < y))$
48	15 47	mpd	$⊢ (φ \land (x \in A \land y \in ℝ^{+})) \to \exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|(G \circ F) (w) - (G \circ F) (x)\| < y)$
49	48	ralrimivva	$⊢ φ \to \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|(G \circ F) (w) - (G \circ F) (x)\| < y)$
50		cncfrss	$⊢ F : A \underset{cn}{⟶} B \to A \subseteq ℂ$
51	1 50	syl	$⊢ φ \to A \subseteq ℂ$
52		cncfrss2	$⊢ G : B \underset{cn}{⟶} C \to C \subseteq ℂ$
53	2 52	syl	$⊢ φ \to C \subseteq ℂ$
54		elcncf2	$⊢ (A \subseteq ℂ \land C \subseteq ℂ) \to ((G \circ F) : A \underset{cn}{⟶} C \leftrightarrow ((G \circ F) : A ⟶ C \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|(G \circ F) (w) - (G \circ F) (x)\| < y)))$
55	51 53 54	syl2anc	$⊢ φ \to ((G \circ F) : A \underset{cn}{⟶} C \leftrightarrow ((G \circ F) : A ⟶ C \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|(G \circ F) (w) - (G \circ F) (x)\| < y)))$
56	8 49 55	mpbir2and	$⊢ φ \to (G \circ F) : A \underset{cn}{⟶} C$

Metamath Proof Explorer

Theorem cncfco

Proof