mulc1cncf

Description: Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007) (Revised by Mario Carneiro, 30-Apr-2014)

		Ref	Expression
	Hypothesis	mulc1cncf.1	$⊢ F = (x \in ℂ ⟼ A x)$
	Assertion	mulc1cncf	$⊢ A \in ℂ \to F : ℂ \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		mulc1cncf.1	$⊢ F = (x \in ℂ ⟼ A x)$
2		mulcl	$⊢ (A \in ℂ \land x \in ℂ) \to A x \in ℂ$
3	2 1	fmptd	$⊢ A \in ℂ \to F : ℂ ⟶ ℂ$
4		simprr	$⊢ (A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \to z \in ℝ^{+}$
5		simpl	$⊢ (A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \to A \in ℂ$
6		simprl	$⊢ (A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \to y \in ℂ$
7		mulcn2	$⊢ (z \in ℝ^{+} \land A \in ℂ \land y \in ℂ) \to \exists t \in ℝ^{+} \exists w \in ℝ^{+} \forall v \in ℂ \forall u \in ℂ ((\|v - A\| < t \land \|u - y\| < w) \to \|v u - A y\| < z)$
8	4 5 6 7	syl3anc	$⊢ (A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \to \exists t \in ℝ^{+} \exists w \in ℝ^{+} \forall v \in ℂ \forall u \in ℂ ((\|v - A\| < t \land \|u - y\| < w) \to \|v u - A y\| < z)$
9		fvoveq1	$⊢ v = A \to \|v - A\| = \|A - A\|$
10	9	breq1d	$⊢ v = A \to (\|v - A\| < t \leftrightarrow \|A - A\| < t)$
11	10	anbi1d	$⊢ v = A \to ((\|v - A\| < t \land \|u - y\| < w) \leftrightarrow (\|A - A\| < t \land \|u - y\| < w))$
12		oveq1	$⊢ v = A \to v u = A u$
13	12	fvoveq1d	$⊢ v = A \to \|v u - A y\| = \|A u - A y\|$
14	13	breq1d	$⊢ v = A \to (\|v u - A y\| < z \leftrightarrow \|A u - A y\| < z)$
15	11 14	imbi12d	$⊢ v = A \to (((\|v - A\| < t \land \|u - y\| < w) \to \|v u - A y\| < z) \leftrightarrow ((\|A - A\| < t \land \|u - y\| < w) \to \|A u - A y\| < z))$
16	15	ralbidv	$⊢ v = A \to (\forall u \in ℂ ((\|v - A\| < t \land \|u - y\| < w) \to \|v u - A y\| < z) \leftrightarrow \forall u \in ℂ ((\|A - A\| < t \land \|u - y\| < w) \to \|A u - A y\| < z))$
17	16	rspcv	$⊢ A \in ℂ \to (\forall v \in ℂ \forall u \in ℂ ((\|v - A\| < t \land \|u - y\| < w) \to \|v u - A y\| < z) \to \forall u \in ℂ ((\|A - A\| < t \land \|u - y\| < w) \to \|A u - A y\| < z))$
18	17	ad2antrr	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land (t \in ℝ^{+} \land w \in ℝ^{+})) \to (\forall v \in ℂ \forall u \in ℂ ((\|v - A\| < t \land \|u - y\| < w) \to \|v u - A y\| < z) \to \forall u \in ℂ ((\|A - A\| < t \land \|u - y\| < w) \to \|A u - A y\| < z))$
19		subid	$⊢ A \in ℂ \to A - A = 0$
20	19	ad2antrr	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land ((t \in ℝ^{+} \land w \in ℝ^{+}) \land u \in ℂ)) \to A - A = 0$
21	20	abs00bd	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land ((t \in ℝ^{+} \land w \in ℝ^{+}) \land u \in ℂ)) \to \|A - A\| = 0$
22		simprll	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land ((t \in ℝ^{+} \land w \in ℝ^{+}) \land u \in ℂ)) \to t \in ℝ^{+}$
23	22	rpgt0d	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land ((t \in ℝ^{+} \land w \in ℝ^{+}) \land u \in ℂ)) \to 0 < t$
24	21 23	eqbrtrd	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land ((t \in ℝ^{+} \land w \in ℝ^{+}) \land u \in ℂ)) \to \|A - A\| < t$
25	24	biantrurd	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land ((t \in ℝ^{+} \land w \in ℝ^{+}) \land u \in ℂ)) \to (\|u - y\| < w \leftrightarrow (\|A - A\| < t \land \|u - y\| < w))$
26		simprr	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land ((t \in ℝ^{+} \land w \in ℝ^{+}) \land u \in ℂ)) \to u \in ℂ$
27		oveq2	$⊢ x = u \to A x = A u$
28		ovex	$⊢ A u \in V$
29	27 1 28	fvmpt	$⊢ u \in ℂ \to F (u) = A u$
30	26 29	syl	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land ((t \in ℝ^{+} \land w \in ℝ^{+}) \land u \in ℂ)) \to F (u) = A u$
31		simplrl	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land ((t \in ℝ^{+} \land w \in ℝ^{+}) \land u \in ℂ)) \to y \in ℂ$
32		oveq2	$⊢ x = y \to A x = A y$
33		ovex	$⊢ A y \in V$
34	32 1 33	fvmpt	$⊢ y \in ℂ \to F (y) = A y$
35	31 34	syl	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land ((t \in ℝ^{+} \land w \in ℝ^{+}) \land u \in ℂ)) \to F (y) = A y$
36	30 35	oveq12d	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land ((t \in ℝ^{+} \land w \in ℝ^{+}) \land u \in ℂ)) \to F (u) - F (y) = A u - A y$
37	36	fveq2d	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land ((t \in ℝ^{+} \land w \in ℝ^{+}) \land u \in ℂ)) \to \|F (u) - F (y)\| = \|A u - A y\|$
38	37	breq1d	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land ((t \in ℝ^{+} \land w \in ℝ^{+}) \land u \in ℂ)) \to (\|F (u) - F (y)\| < z \leftrightarrow \|A u - A y\| < z)$
39	25 38	imbi12d	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land ((t \in ℝ^{+} \land w \in ℝ^{+}) \land u \in ℂ)) \to ((\|u - y\| < w \to \|F (u) - F (y)\| < z) \leftrightarrow ((\|A - A\| < t \land \|u - y\| < w) \to \|A u - A y\| < z))$
40	39	anassrs	$⊢ (((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land (t \in ℝ^{+} \land w \in ℝ^{+})) \land u \in ℂ) \to ((\|u - y\| < w \to \|F (u) - F (y)\| < z) \leftrightarrow ((\|A - A\| < t \land \|u - y\| < w) \to \|A u - A y\| < z))$
41	40	ralbidva	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land (t \in ℝ^{+} \land w \in ℝ^{+})) \to (\forall u \in ℂ (\|u - y\| < w \to \|F (u) - F (y)\| < z) \leftrightarrow \forall u \in ℂ ((\|A - A\| < t \land \|u - y\| < w) \to \|A u - A y\| < z))$
42	18 41	sylibrd	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land (t \in ℝ^{+} \land w \in ℝ^{+})) \to (\forall v \in ℂ \forall u \in ℂ ((\|v - A\| < t \land \|u - y\| < w) \to \|v u - A y\| < z) \to \forall u \in ℂ (\|u - y\| < w \to \|F (u) - F (y)\| < z))$
43	42	anassrs	$⊢ (((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land t \in ℝ^{+}) \land w \in ℝ^{+}) \to (\forall v \in ℂ \forall u \in ℂ ((\|v - A\| < t \land \|u - y\| < w) \to \|v u - A y\| < z) \to \forall u \in ℂ (\|u - y\| < w \to \|F (u) - F (y)\| < z))$
44	43	reximdva	$⊢ ((A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \land t \in ℝ^{+}) \to (\exists w \in ℝ^{+} \forall v \in ℂ \forall u \in ℂ ((\|v - A\| < t \land \|u - y\| < w) \to \|v u - A y\| < z) \to \exists w \in ℝ^{+} \forall u \in ℂ (\|u - y\| < w \to \|F (u) - F (y)\| < z))$
45	44	rexlimdva	$⊢ (A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \to (\exists t \in ℝ^{+} \exists w \in ℝ^{+} \forall v \in ℂ \forall u \in ℂ ((\|v - A\| < t \land \|u - y\| < w) \to \|v u - A y\| < z) \to \exists w \in ℝ^{+} \forall u \in ℂ (\|u - y\| < w \to \|F (u) - F (y)\| < z))$
46	8 45	mpd	$⊢ (A \in ℂ \land (y \in ℂ \land z \in ℝ^{+})) \to \exists w \in ℝ^{+} \forall u \in ℂ (\|u - y\| < w \to \|F (u) - F (y)\| < z)$
47	46	ralrimivva	$⊢ A \in ℂ \to \forall y \in ℂ \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall u \in ℂ (\|u - y\| < w \to \|F (u) - F (y)\| < z)$
48		ssid	$⊢ ℂ \subseteq ℂ$
49		elcncf2	$⊢ (ℂ \subseteq ℂ \land ℂ \subseteq ℂ) \to (F : ℂ \underset{cn}{⟶} ℂ \leftrightarrow (F : ℂ ⟶ ℂ \land \forall y \in ℂ \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall u \in ℂ (\|u - y\| < w \to \|F (u) - F (y)\| < z)))$
50	48 48 49	mp2an	$⊢ F : ℂ \underset{cn}{⟶} ℂ \leftrightarrow (F : ℂ ⟶ ℂ \land \forall y \in ℂ \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall u \in ℂ (\|u - y\| < w \to \|F (u) - F (y)\| < z))$
51	3 47 50	sylanbrc	$⊢ A \in ℂ \to F : ℂ \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem mulc1cncf

Proof