mpomulcn

Description: Complex number multiplication is a continuous function. Version of mulcn using maps-to notation, which does not require ax-mulf . (Contributed by GG, 16-Mar-2025)

		Ref	Expression
	Hypothesis	mpomulcn.j	$⊢ J = TopOpen (ℂ_{fld})$
	Assertion	mpomulcn	$⊢ (x \in ℂ, y \in ℂ ⟼ x y) \in ((J \times_{t} J) Cn J)$

Proof

Step	Hyp	Ref	Expression
1		mpomulcn.j	$⊢ J = TopOpen (ℂ_{fld})$
2		mpomulf	$⊢ (x \in ℂ, y \in ℂ ⟼ x y) : ℂ \times ℂ ⟶ ℂ$
3		mulcn2	$⊢ (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \to \exists z \in ℝ^{+} \exists w \in ℝ^{+} \forall d \in ℂ \forall e \in ℂ ((\|d - b\| < z \land \|e - c\| < w) \to \|d e - b c\| < a)$
4		simplr	$⊢ ((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \to u \in ℂ$
5		simplll	$⊢ (((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \land d = u) \to v \in ℂ$
6		simplr	$⊢ ((((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \land d = u) \land e = v) \to d = u$
7	6	fvoveq1d	$⊢ ((((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \land d = u) \land e = v) \to \|d - b\| = \|u - b\|$
8	7	breq1d	$⊢ ((((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \land d = u) \land e = v) \to (\|d - b\| < z \leftrightarrow \|u - b\| < z)$
9		simpr	$⊢ ((((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \land d = u) \land e = v) \to e = v$
10	9	fvoveq1d	$⊢ ((((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \land d = u) \land e = v) \to \|e - c\| = \|v - c\|$
11	10	breq1d	$⊢ ((((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \land d = u) \land e = v) \to (\|e - c\| < w \leftrightarrow \|v - c\| < w)$
12	8 11	anbi12d	$⊢ ((((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \land d = u) \land e = v) \to ((\|d - b\| < z \land \|e - c\| < w) \leftrightarrow (\|u - b\| < z \land \|v - c\| < w))$
13		simplr	$⊢ (((v \in ℂ \land u \in ℂ) \land d = u) \land e = v) \to d = u$
14	13	eqcomd	$⊢ (((v \in ℂ \land u \in ℂ) \land d = u) \land e = v) \to u = d$
15		simpr	$⊢ (((v \in ℂ \land u \in ℂ) \land d = u) \land e = v) \to e = v$
16	15	eqcomd	$⊢ (((v \in ℂ \land u \in ℂ) \land d = u) \land e = v) \to v = e$
17	14 16	oveq12d	$⊢ (((v \in ℂ \land u \in ℂ) \land d = u) \land e = v) \to u v = d e$
18		oveq1	$⊢ x = u \to x y = u y$
19		oveq2	$⊢ y = v \to u y = u v$
20	18 19	cbvmpov	$⊢ (x \in ℂ, y \in ℂ ⟼ x y) = (u \in ℂ, v \in ℂ ⟼ u v)$
21	20	a1i	$⊢ ⊤ \to (x \in ℂ, y \in ℂ ⟼ x y) = (u \in ℂ, v \in ℂ ⟼ u v)$
22		eqidd	$⊢ ⊤ \to ⟨u, v⟩ = ⟨u, v⟩$
23		simp2	$⊢ (⊤ \land u \in ℂ \land v \in ℂ) \to u \in ℂ$
24		simp3	$⊢ (⊤ \land u \in ℂ \land v \in ℂ) \to v \in ℂ$
25	23 24	mulcld	$⊢ (⊤ \land u \in ℂ \land v \in ℂ) \to u v \in ℂ$
26	21 22 25	fvmpopr2d	$⊢ (⊤ \land u \in ℂ \land v \in ℂ) \to (x \in ℂ, y \in ℂ ⟼ x y) (⟨u, v⟩) = u v$
27	26	eqcomd	$⊢ (⊤ \land u \in ℂ \land v \in ℂ) \to u v = (x \in ℂ, y \in ℂ ⟼ x y) (⟨u, v⟩)$
28	27	3expib	$⊢ ⊤ \to ((u \in ℂ \land v \in ℂ) \to u v = (x \in ℂ, y \in ℂ ⟼ x y) (⟨u, v⟩))$
29	28	mptru	$⊢ (u \in ℂ \land v \in ℂ) \to u v = (x \in ℂ, y \in ℂ ⟼ x y) (⟨u, v⟩)$
30		df-ov	$⊢ u (x \in ℂ, y \in ℂ ⟼ x y) v = (x \in ℂ, y \in ℂ ⟼ x y) (⟨u, v⟩)$
31	29 30	eqtr4di	$⊢ (u \in ℂ \land v \in ℂ) \to u v = u (x \in ℂ, y \in ℂ ⟼ x y) v$
32	31	ancoms	$⊢ (v \in ℂ \land u \in ℂ) \to u v = u (x \in ℂ, y \in ℂ ⟼ x y) v$
33	32	adantr	$⊢ ((v \in ℂ \land u \in ℂ) \land d = u) \to u v = u (x \in ℂ, y \in ℂ ⟼ x y) v$
34	33	adantr	$⊢ (((v \in ℂ \land u \in ℂ) \land d = u) \land e = v) \to u v = u (x \in ℂ, y \in ℂ ⟼ x y) v$
35	17 34	eqtr3d	$⊢ (((v \in ℂ \land u \in ℂ) \land d = u) \land e = v) \to d e = u (x \in ℂ, y \in ℂ ⟼ x y) v$
36	35	adantllr	$⊢ ((((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \land d = u) \land e = v) \to d e = u (x \in ℂ, y \in ℂ ⟼ x y) v$
37		df-ov	$⊢ b (x \in ℂ, y \in ℂ ⟼ x y) c = (x \in ℂ, y \in ℂ ⟼ x y) (⟨b, c⟩)$
38		oveq1	$⊢ x = b \to x y = b y$
39		oveq2	$⊢ y = c \to b y = b c$
40	38 39	cbvmpov	$⊢ (x \in ℂ, y \in ℂ ⟼ x y) = (b \in ℂ, c \in ℂ ⟼ b c)$
41	40	a1i	$⊢ a \in ℝ^{+} \to (x \in ℂ, y \in ℂ ⟼ x y) = (b \in ℂ, c \in ℂ ⟼ b c)$
42		eqidd	$⊢ a \in ℝ^{+} \to ⟨b, c⟩ = ⟨b, c⟩$
43		simp2	$⊢ (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \to b \in ℂ$
44		simp3	$⊢ (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \to c \in ℂ$
45	43 44	mulcld	$⊢ (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \to b c \in ℂ$
46	41 42 45	fvmpopr2d	$⊢ (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \to (x \in ℂ, y \in ℂ ⟼ x y) (⟨b, c⟩) = b c$
47	37 46	eqtr2id	$⊢ (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \to b c = b (x \in ℂ, y \in ℂ ⟼ x y) c$
48	47	ad3antlr	$⊢ ((((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \land d = u) \land e = v) \to b c = b (x \in ℂ, y \in ℂ ⟼ x y) c$
49	36 48	oveq12d	$⊢ ((((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \land d = u) \land e = v) \to d e - b c = (u (x \in ℂ, y \in ℂ ⟼ x y) v) - (b (x \in ℂ, y \in ℂ ⟼ x y) c)$
50	49	fveq2d	$⊢ ((((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \land d = u) \land e = v) \to \|d e - b c\| = \|(u (x \in ℂ, y \in ℂ ⟼ x y) v) - (b (x \in ℂ, y \in ℂ ⟼ x y) c)\|$
51	50	breq1d	$⊢ ((((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \land d = u) \land e = v) \to (\|d e - b c\| < a \leftrightarrow \|(u (x \in ℂ, y \in ℂ ⟼ x y) v) - (b (x \in ℂ, y \in ℂ ⟼ x y) c)\| < a)$
52	12 51	imbi12d	$⊢ ((((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \land d = u) \land e = v) \to (((\|d - b\| < z \land \|e - c\| < w) \to \|d e - b c\| < a) \leftrightarrow ((\|u - b\| < z \land \|v - c\| < w) \to \|(u (x \in ℂ, y \in ℂ ⟼ x y) v) - (b (x \in ℂ, y \in ℂ ⟼ x y) c)\| < a))$
53	5 52	rspcdv	$⊢ (((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \land d = u) \to (\forall e \in ℂ ((\|d - b\| < z \land \|e - c\| < w) \to \|d e - b c\| < a) \to ((\|u - b\| < z \land \|v - c\| < w) \to \|(u (x \in ℂ, y \in ℂ ⟼ x y) v) - (b (x \in ℂ, y \in ℂ ⟼ x y) c)\| < a))$
54	4 53	rspcimdv	$⊢ ((v \in ℂ \land u \in ℂ) \land (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ)) \to (\forall d \in ℂ \forall e \in ℂ ((\|d - b\| < z \land \|e - c\| < w) \to \|d e - b c\| < a) \to ((\|u - b\| < z \land \|v - c\| < w) \to \|(u (x \in ℂ, y \in ℂ ⟼ x y) v) - (b (x \in ℂ, y \in ℂ ⟼ x y) c)\| < a))$
55	54	expimpd	$⊢ (v \in ℂ \land u \in ℂ) \to (((a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \land \forall d \in ℂ \forall e \in ℂ ((\|d - b\| < z \land \|e - c\| < w) \to \|d e - b c\| < a)) \to ((\|u - b\| < z \land \|v - c\| < w) \to \|(u (x \in ℂ, y \in ℂ ⟼ x y) v) - (b (x \in ℂ, y \in ℂ ⟼ x y) c)\| < a))$
56	55	ex	$⊢ v \in ℂ \to (u \in ℂ \to (((a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \land \forall d \in ℂ \forall e \in ℂ ((\|d - b\| < z \land \|e - c\| < w) \to \|d e - b c\| < a)) \to ((\|u - b\| < z \land \|v - c\| < w) \to \|(u (x \in ℂ, y \in ℂ ⟼ x y) v) - (b (x \in ℂ, y \in ℂ ⟼ x y) c)\| < a)))$
57	56	com13	$⊢ ((a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \land \forall d \in ℂ \forall e \in ℂ ((\|d - b\| < z \land \|e - c\| < w) \to \|d e - b c\| < a)) \to (u \in ℂ \to (v \in ℂ \to ((\|u - b\| < z \land \|v - c\| < w) \to \|(u (x \in ℂ, y \in ℂ ⟼ x y) v) - (b (x \in ℂ, y \in ℂ ⟼ x y) c)\| < a)))$
58	57	ralrimdv	$⊢ ((a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \land \forall d \in ℂ \forall e \in ℂ ((\|d - b\| < z \land \|e - c\| < w) \to \|d e - b c\| < a)) \to (u \in ℂ \to \forall v \in ℂ ((\|u - b\| < z \land \|v - c\| < w) \to \|(u (x \in ℂ, y \in ℂ ⟼ x y) v) - (b (x \in ℂ, y \in ℂ ⟼ x y) c)\| < a))$
59	58	ex	$⊢ (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \to (\forall d \in ℂ \forall e \in ℂ ((\|d - b\| < z \land \|e - c\| < w) \to \|d e - b c\| < a) \to (u \in ℂ \to \forall v \in ℂ ((\|u - b\| < z \land \|v - c\| < w) \to \|(u (x \in ℂ, y \in ℂ ⟼ x y) v) - (b (x \in ℂ, y \in ℂ ⟼ x y) c)\| < a)))$
60	59	ralrimdv	$⊢ (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \to (\forall d \in ℂ \forall e \in ℂ ((\|d - b\| < z \land \|e - c\| < w) \to \|d e - b c\| < a) \to \forall u \in ℂ \forall v \in ℂ ((\|u - b\| < z \land \|v - c\| < w) \to \|(u (x \in ℂ, y \in ℂ ⟼ x y) v) - (b (x \in ℂ, y \in ℂ ⟼ x y) c)\| < a))$
61	60	reximdv	$⊢ (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \to (\exists w \in ℝ^{+} \forall d \in ℂ \forall e \in ℂ ((\|d - b\| < z \land \|e - c\| < w) \to \|d e - b c\| < a) \to \exists w \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((\|u - b\| < z \land \|v - c\| < w) \to \|(u (x \in ℂ, y \in ℂ ⟼ x y) v) - (b (x \in ℂ, y \in ℂ ⟼ x y) c)\| < a))$
62	61	reximdv	$⊢ (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \to (\exists z \in ℝ^{+} \exists w \in ℝ^{+} \forall d \in ℂ \forall e \in ℂ ((\|d - b\| < z \land \|e - c\| < w) \to \|d e - b c\| < a) \to \exists z \in ℝ^{+} \exists w \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((\|u - b\| < z \land \|v - c\| < w) \to \|(u (x \in ℂ, y \in ℂ ⟼ x y) v) - (b (x \in ℂ, y \in ℂ ⟼ x y) c)\| < a))$
63	3 62	mpd	$⊢ (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \to \exists z \in ℝ^{+} \exists w \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((\|u - b\| < z \land \|v - c\| < w) \to \|(u (x \in ℂ, y \in ℂ ⟼ x y) v) - (b (x \in ℂ, y \in ℂ ⟼ x y) c)\| < a)$
64	1 2 63	addcnlem	$⊢ (x \in ℂ, y \in ℂ ⟼ x y) \in ((J \times_{t} J) Cn J)$

Metamath Proof Explorer

Theorem mpomulcn

Proof