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		simplr	$⊢ ((v \in ℂ \land u \in ℂ) \land d = u) \to u \in ℂ$
19		simplll	$⊢ (((v \in ℂ \land u \in ℂ) \land d = u) \land e = v) \to v \in ℂ$
20		tru	$⊢ ⊤$
21		oveq1	$⊢ x = u \to x y = u y$
22		oveq2	$⊢ y = v \to u y = u v$
23	21 22	cbvmpov	$⊢ (x \in ℂ, y \in ℂ ⟼ x y) = (u \in ℂ, v \in ℂ ⟼ u v)$
24	23	a1i	$⊢ ⊤ \to (x \in ℂ, y \in ℂ ⟼ x y) = (u \in ℂ, v \in ℂ ⟼ u v)$
25		eqidd	$⊢ ⊤ \to ⟨u, v⟩ = ⟨u, v⟩$
26		mulcl	$⊢ (u \in ℂ \land v \in ℂ) \to u v \in ℂ$
27	26	3adant1	$⊢ (⊤ \land u \in ℂ \land v \in ℂ) \to u v \in ℂ$
28	24 25 27	fvmpopr2d	$⊢ (⊤ \land u \in ℂ \land v \in ℂ) \to (x \in ℂ, y \in ℂ ⟼ x y) (⟨u, v⟩) = u v$
29	28	eqcomd	$⊢ (⊤ \land u \in ℂ \land v \in ℂ) \to u v = (x \in ℂ, y \in ℂ ⟼ x y) (⟨u, v⟩)$
30	20 29	mp3an1	$⊢ (u \in ℂ \land v \in ℂ) \to u v = (x \in ℂ, y \in ℂ ⟼ x y) (⟨u, v⟩)$
31		df-ov	$⊢ u (x \in ℂ, y \in ℂ ⟼ x y) v = (x \in ℂ, y \in ℂ ⟼ x y) (⟨u, v⟩)$
32	30 31	eqtr4di	$⊢ (u \in ℂ \land v \in ℂ) \to u v = u (x \in ℂ, y \in ℂ ⟼ x y) v$
33	18 19 32	syl2an2r	$⊢ (((v \in ℂ \land u \in ℂ) \land d = u) \land e = v) \to u v = u (x \in ℂ, y \in ℂ ⟼ x y) v$
34	17 33	eqtr3d	$⊢ (((v \in ℂ \land u \in ℂ) \land d = u) \land e = v) \to d e = u (x \in ℂ, y \in ℂ ⟼ x y) v$
35	34	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$
36		df-ov	$⊢ b (x \in ℂ, y \in ℂ ⟼ x y) c = (x \in ℂ, y \in ℂ ⟼ x y) (⟨b, c⟩)$
37		oveq1	$⊢ x = b \to x y = b y$
38		oveq2	$⊢ y = c \to b y = b c$
39	37 38	cbvmpov	$⊢ (x \in ℂ, y \in ℂ ⟼ x y) = (b \in ℂ, c \in ℂ ⟼ b c)$
40	39	a1i	$⊢ a \in ℝ^{+} \to (x \in ℂ, y \in ℂ ⟼ x y) = (b \in ℂ, c \in ℂ ⟼ b c)$
41		eqidd	$⊢ a \in ℝ^{+} \to ⟨b, c⟩ = ⟨b, c⟩$
42		mulcl	$⊢ (b \in ℂ \land c \in ℂ) \to b c \in ℂ$
43	42	3adant1	$⊢ (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \to b c \in ℂ$
44	40 41 43	fvmpopr2d	$⊢ (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \to (x \in ℂ, y \in ℂ ⟼ x y) (⟨b, c⟩) = b c$
45	36 44	eqtr2id	$⊢ (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \to b c = b (x \in ℂ, y \in ℂ ⟼ x y) c$
46	45	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$
47	35 46	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)$
48	47	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)\|$
49	48	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)$
50	12 49	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))$
51	5 50	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))$
52	4 51	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))$
53	52	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))$
54	53	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)))$
55	54	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)))$
56	55	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))$
57	56	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)))$
58	57	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))$
59	58	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))$
60	59	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))$
61	3 60	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)$
62	1 2 61	addcnlem	$⊢ (x \in ℂ, y \in ℂ ⟼ x y) \in ((J \times_{t} J) Cn J)$

Metamath Proof Explorer

Theorem mpomulcn

Proof