qndenserrnopnlem

Description: n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	qndenserrnopnlem.i	$⊢ φ \to I \in Fin$
	qndenserrnopnlem.j	$⊢ J = TopOpen (I)$
	qndenserrnopnlem.v	$⊢ φ \to V \in J$
	qndenserrnopnlem.x	$⊢ φ \to X \in V$
	qndenserrnopnlem.d	$⊢ D = dist (I)$
Assertion	qndenserrnopnlem	$⊢ φ \to \exists y \in (ℚ^{I}) y \in V$

Proof

Step	Hyp	Ref	Expression
1		qndenserrnopnlem.i	$⊢ φ \to I \in Fin$
2		qndenserrnopnlem.j	$⊢ J = TopOpen (I)$
3		qndenserrnopnlem.v	$⊢ φ \to V \in J$
4		qndenserrnopnlem.x	$⊢ φ \to X \in V$
5		qndenserrnopnlem.d	$⊢ D = dist (I)$
6	5	rrxmetfi	$⊢ I \in Fin \to D \in Met (ℝ^{I})$
7	1 6	syl	$⊢ φ \to D \in Met (ℝ^{I})$
8		metxmet	$⊢ D \in Met (ℝ^{I}) \to D \in ∞Met (ℝ^{I})$
9	7 8	syl	$⊢ φ \to D \in ∞Met (ℝ^{I})$
10	3 2	eleqtrdi	$⊢ φ \to V \in TopOpen (I)$
11	1	rrxtopnfi	$⊢ φ \to TopOpen (I) = MetOpen ((f \in (ℝ^{I}), g \in (ℝ^{I}) ⟼ \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}}))$
12	5	a1i	$⊢ φ \to D = dist (I)$
13		eqid	$⊢ I = I$
14		eqid	$⊢ ℝ^{I} = ℝ^{I}$
15	13 14	rrxdsfi	$⊢ I \in Fin \to dist (I) = (f \in (ℝ^{I}), g \in (ℝ^{I}) ⟼ \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}})$
16	1 15	syl	$⊢ φ \to dist (I) = (f \in (ℝ^{I}), g \in (ℝ^{I}) ⟼ \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}})$
17	12 16	eqtr2d	$⊢ φ \to (f \in (ℝ^{I}), g \in (ℝ^{I}) ⟼ \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}}) = D$
18	17	fveq2d	$⊢ φ \to MetOpen ((f \in (ℝ^{I}), g \in (ℝ^{I}) ⟼ \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}})) = MetOpen (D)$
19	11 18	eqtrd	$⊢ φ \to TopOpen (I) = MetOpen (D)$
20	10 19	eleqtrd	$⊢ φ \to V \in MetOpen (D)$
21		eqid	$⊢ MetOpen (D) = MetOpen (D)$
22	21	mopni2	$⊢ (D \in ∞Met (ℝ^{I}) \land V \in MetOpen (D) \land X \in V) \to \exists e \in ℝ^{+} X ball (D) e \subseteq V$
23	9 20 4 22	syl3anc	$⊢ φ \to \exists e \in ℝ^{+} X ball (D) e \subseteq V$
24	1	3ad2ant1	$⊢ (φ \land e \in ℝ^{+} \land X ball (D) e \subseteq V) \to I \in Fin$
25		rrxtps	$⊢ I \in Fin \to I \in TopSp$
26	1 25	syl	$⊢ φ \to I \in TopSp$
27		eqid	$⊢ {Base}_{I} = {Base}_{I}$
28	27 2	istps	$⊢ I \in TopSp \leftrightarrow J \in TopOn ({Base}_{I})$
29	26 28	sylib	$⊢ φ \to J \in TopOn ({Base}_{I})$
30	1 13 27	rrxbasefi	$⊢ φ \to {Base}_{I} = ℝ^{I}$
31	30	fveq2d	$⊢ φ \to TopOn ({Base}_{I}) = TopOn (ℝ^{I})$
32	29 31	eleqtrd	$⊢ φ \to J \in TopOn (ℝ^{I})$
33		toponss	$⊢ (J \in TopOn (ℝ^{I}) \land V \in J) \to V \subseteq ℝ^{I}$
34	32 3 33	syl2anc	$⊢ φ \to V \subseteq ℝ^{I}$
35	34 4	sseldd	$⊢ φ \to X \in (ℝ^{I})$
36	35	3ad2ant1	$⊢ (φ \land e \in ℝ^{+} \land X ball (D) e \subseteq V) \to X \in (ℝ^{I})$
37		simp2	$⊢ (φ \land e \in ℝ^{+} \land X ball (D) e \subseteq V) \to e \in ℝ^{+}$
38	24 36 5 37	qndenserrnbl	$⊢ (φ \land e \in ℝ^{+} \land X ball (D) e \subseteq V) \to \exists y \in (ℚ^{I}) y \in (X ball (D) e)$
39		ssel	$⊢ X ball (D) e \subseteq V \to (y \in (X ball (D) e) \to y \in V)$
40	39	adantr	$⊢ (X ball (D) e \subseteq V \land y \in (ℚ^{I})) \to (y \in (X ball (D) e) \to y \in V)$
41	40	3ad2antl3	$⊢ ((φ \land e \in ℝ^{+} \land X ball (D) e \subseteq V) \land y \in (ℚ^{I})) \to (y \in (X ball (D) e) \to y \in V)$
42	41	reximdva	$⊢ (φ \land e \in ℝ^{+} \land X ball (D) e \subseteq V) \to (\exists y \in (ℚ^{I}) y \in (X ball (D) e) \to \exists y \in (ℚ^{I}) y \in V)$
43	38 42	mpd	$⊢ (φ \land e \in ℝ^{+} \land X ball (D) e \subseteq V) \to \exists y \in (ℚ^{I}) y \in V$
44	43	3exp	$⊢ φ \to (e \in ℝ^{+} \to (X ball (D) e \subseteq V \to \exists y \in (ℚ^{I}) y \in V))$
45	44	rexlimdv	$⊢ φ \to (\exists e \in ℝ^{+} X ball (D) e \subseteq V \to \exists y \in (ℚ^{I}) y \in V)$
46	23 45	mpd	$⊢ φ \to \exists y \in (ℚ^{I}) y \in V$

Metamath Proof Explorer

Theorem qndenserrnopnlem

Proof