qndenserrnbl

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	qndenserrnbl.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
	qndenserrnbl.x	⊢ ( 𝜑 → 𝑋 ∈ ( ℝ ↑_m 𝐼 ) )
	qndenserrnbl.d	⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
	qndenserrnbl.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ⁺ )
Assertion	qndenserrnbl	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( ℚ ↑_m 𝐼 ) 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		qndenserrnbl.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
2		qndenserrnbl.x	⊢ ( 𝜑 → 𝑋 ∈ ( ℝ ↑_m 𝐼 ) )
3		qndenserrnbl.d	⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
4		qndenserrnbl.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ⁺ )
5		0ex	⊢ ∅ ∈ V
6	5	snid	⊢ ∅ ∈ { ∅ }
7	6	a1i	⊢ ( ( 𝜑 ∧ 𝐼 = ∅ ) → ∅ ∈ { ∅ } )
8		oveq2	⊢ ( 𝐼 = ∅ → ( ℚ ↑_m 𝐼 ) = ( ℚ ↑_m ∅ ) )
9		qex	⊢ ℚ ∈ V
10		mapdm0	⊢ ( ℚ ∈ V → ( ℚ ↑_m ∅ ) = { ∅ } )
11	9 10	ax-mp	⊢ ( ℚ ↑_m ∅ ) = { ∅ }
12	11	a1i	⊢ ( 𝐼 = ∅ → ( ℚ ↑_m ∅ ) = { ∅ } )
13	8 12	eqtr2d	⊢ ( 𝐼 = ∅ → { ∅ } = ( ℚ ↑_m 𝐼 ) )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝐼 = ∅ ) → { ∅ } = ( ℚ ↑_m 𝐼 ) )
15	7 14	eleqtrd	⊢ ( ( 𝜑 ∧ 𝐼 = ∅ ) → ∅ ∈ ( ℚ ↑_m 𝐼 ) )
16	3	rrxmetfi	⊢ ( 𝐼 ∈ Fin → 𝐷 ∈ ( Met ‘ ( ℝ ↑_m 𝐼 ) ) )
17	1 16	syl	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ ( ℝ ↑_m 𝐼 ) ) )
18		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ ( ℝ ↑_m 𝐼 ) ) → 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑_m 𝐼 ) ) )
19	17 18	syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑_m 𝐼 ) ) )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝐼 = ∅ ) → 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑_m 𝐼 ) ) )
21	2	adantr	⊢ ( ( 𝜑 ∧ 𝐼 = ∅ ) → 𝑋 ∈ ( ℝ ↑_m 𝐼 ) )
22		oveq2	⊢ ( 𝐼 = ∅ → ( ℝ ↑_m 𝐼 ) = ( ℝ ↑_m ∅ ) )
23		reex	⊢ ℝ ∈ V
24		mapdm0	⊢ ( ℝ ∈ V → ( ℝ ↑_m ∅ ) = { ∅ } )
25	23 24	ax-mp	⊢ ( ℝ ↑_m ∅ ) = { ∅ }
26	25	a1i	⊢ ( 𝐼 = ∅ → ( ℝ ↑_m ∅ ) = { ∅ } )
27	22 26	eqtrd	⊢ ( 𝐼 = ∅ → ( ℝ ↑_m 𝐼 ) = { ∅ } )
28	27	adantl	⊢ ( ( 𝜑 ∧ 𝐼 = ∅ ) → ( ℝ ↑_m 𝐼 ) = { ∅ } )
29	21 28	eleqtrd	⊢ ( ( 𝜑 ∧ 𝐼 = ∅ ) → 𝑋 ∈ { ∅ } )
30		elsng	⊢ ( 𝑋 ∈ ( ℝ ↑_m 𝐼 ) → ( 𝑋 ∈ { ∅ } ↔ 𝑋 = ∅ ) )
31	2 30	syl	⊢ ( 𝜑 → ( 𝑋 ∈ { ∅ } ↔ 𝑋 = ∅ ) )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝐼 = ∅ ) → ( 𝑋 ∈ { ∅ } ↔ 𝑋 = ∅ ) )
33	29 32	mpbid	⊢ ( ( 𝜑 ∧ 𝐼 = ∅ ) → 𝑋 = ∅ )
34	33	eqcomd	⊢ ( ( 𝜑 ∧ 𝐼 = ∅ ) → ∅ = 𝑋 )
35	34 21	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐼 = ∅ ) → ∅ ∈ ( ℝ ↑_m 𝐼 ) )
36	4	rpxrd	⊢ ( 𝜑 → 𝐸 ∈ ℝ^* )
37	4	rpgt0d	⊢ ( 𝜑 → 0 < 𝐸 )
38	36 37	jca	⊢ ( 𝜑 → ( 𝐸 ∈ ℝ^* ∧ 0 < 𝐸 ) )
39	38	adantr	⊢ ( ( 𝜑 ∧ 𝐼 = ∅ ) → ( 𝐸 ∈ ℝ^* ∧ 0 < 𝐸 ) )
40		xblcntr	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑_m 𝐼 ) ) ∧ ∅ ∈ ( ℝ ↑_m 𝐼 ) ∧ ( 𝐸 ∈ ℝ^* ∧ 0 < 𝐸 ) ) → ∅ ∈ ( ∅ ( ball ‘ 𝐷 ) 𝐸 ) )
41	20 35 39 40	syl3anc	⊢ ( ( 𝜑 ∧ 𝐼 = ∅ ) → ∅ ∈ ( ∅ ( ball ‘ 𝐷 ) 𝐸 ) )
42	34	oveq1d	⊢ ( ( 𝜑 ∧ 𝐼 = ∅ ) → ( ∅ ( ball ‘ 𝐷 ) 𝐸 ) = ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) )
43	41 42	eleqtrd	⊢ ( ( 𝜑 ∧ 𝐼 = ∅ ) → ∅ ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) )
44		eleq1	⊢ ( 𝑦 = ∅ → ( 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ↔ ∅ ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ) )
45	44	rspcev	⊢ ( ( ∅ ∈ ( ℚ ↑_m 𝐼 ) ∧ ∅ ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ) → ∃ 𝑦 ∈ ( ℚ ↑_m 𝐼 ) 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) )
46	15 43 45	syl2anc	⊢ ( ( 𝜑 ∧ 𝐼 = ∅ ) → ∃ 𝑦 ∈ ( ℚ ↑_m 𝐼 ) 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) )
47	1	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐼 = ∅ ) → 𝐼 ∈ Fin )
48		neqne	⊢ ( ¬ 𝐼 = ∅ → 𝐼 ≠ ∅ )
49	48	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐼 = ∅ ) → 𝐼 ≠ ∅ )
50	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐼 = ∅ ) → 𝑋 ∈ ( ℝ ↑_m 𝐼 ) )
51	4	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐼 = ∅ ) → 𝐸 ∈ ℝ⁺ )
52	47 49 50 3 51	qndenserrnbllem	⊢ ( ( 𝜑 ∧ ¬ 𝐼 = ∅ ) → ∃ 𝑦 ∈ ( ℚ ↑_m 𝐼 ) 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) )
53	46 52	pm2.61dan	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( ℚ ↑_m 𝐼 ) 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) )

Metamath Proof Explorer

Theorem qndenserrnbl

Proof