rrxtopnfi

Description: The topology of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020)

		Ref	Expression
	Hypothesis	rrxtopnfi.1	$⊢ φ \to I \in Fin$
	Assertion	rrxtopnfi	$⊢ φ \to TopOpen (msup) = MetOpen ((f \in (ℝ^{I}), g \in (ℝ^{I}) ⟼ \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}}))$

Proof

Step	Hyp	Ref	Expression
1		rrxtopnfi.1	$⊢ φ \to I \in Fin$
2	1	rrxtopn	$⊢ φ \to TopOpen (msup) = MetOpen ((f \in {Base}_{msup}, g \in {Base}_{msup} ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}}))$
3		eqid	$⊢ msup = msup$
4		eqid	$⊢ {Base}_{msup} = {Base}_{msup}$
5	1 3 4	rrxbasefi	$⊢ φ \to {Base}_{msup} = ℝ^{I}$
6	5	adantr	$⊢ (φ \land f \in {Base}_{msup}) \to {Base}_{msup} = ℝ^{I}$
7		simpl	$⊢ (φ \land (f \in {Base}_{msup} \land g \in {Base}_{msup})) \to φ$
8		simprl	$⊢ (φ \land (f \in {Base}_{msup} \land g \in {Base}_{msup})) \to f \in {Base}_{msup}$
9		simpr	$⊢ (φ \land f \in {Base}_{msup}) \to f \in {Base}_{msup}$
10	9 6	eleqtrd	$⊢ (φ \land f \in {Base}_{msup}) \to f \in (ℝ^{I})$
11	8 10	syldan	$⊢ (φ \land (f \in {Base}_{msup} \land g \in {Base}_{msup})) \to f \in (ℝ^{I})$
12		simprr	$⊢ (φ \land (f \in {Base}_{msup} \land g \in {Base}_{msup})) \to g \in {Base}_{msup}$
13		simpr	$⊢ (φ \land g \in {Base}_{msup}) \to g \in {Base}_{msup}$
14	5	adantr	$⊢ (φ \land g \in {Base}_{msup}) \to {Base}_{msup} = ℝ^{I}$
15	13 14	eleqtrd	$⊢ (φ \land g \in {Base}_{msup}) \to g \in (ℝ^{I})$
16	12 15	syldan	$⊢ (φ \land (f \in {Base}_{msup} \land g \in {Base}_{msup})) \to g \in (ℝ^{I})$
17		elmapi	$⊢ f \in (ℝ^{I}) \to f : I ⟶ ℝ$
18	17	adantr	$⊢ (f \in (ℝ^{I}) \land g \in (ℝ^{I})) \to f : I ⟶ ℝ$
19	18	ffvelcdmda	$⊢ ((f \in (ℝ^{I}) \land g \in (ℝ^{I})) \land x \in I) \to f (x) \in ℝ$
20		elmapi	$⊢ g \in (ℝ^{I}) \to g : I ⟶ ℝ$
21	20	adantl	$⊢ (f \in (ℝ^{I}) \land g \in (ℝ^{I})) \to g : I ⟶ ℝ$
22	21	ffvelcdmda	$⊢ ((f \in (ℝ^{I}) \land g \in (ℝ^{I})) \land x \in I) \to g (x) \in ℝ$
23	19 22	resubcld	$⊢ ((f \in (ℝ^{I}) \land g \in (ℝ^{I})) \land x \in I) \to f (x) - g (x) \in ℝ$
24	23	resqcld	$⊢ ((f \in (ℝ^{I}) \land g \in (ℝ^{I})) \land x \in I) \to {(f (x) - g (x))}^{2} \in ℝ$
25		eqid	$⊢ (x \in I ⟼ {(f (x) - g (x))}^{2}) = (x \in I ⟼ {(f (x) - g (x))}^{2})$
26	24 25	fmptd	$⊢ (f \in (ℝ^{I}) \land g \in (ℝ^{I})) \to (x \in I ⟼ {(f (x) - g (x))}^{2}) : I ⟶ ℝ$
27	26	3adant1	$⊢ (φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \to (x \in I ⟼ {(f (x) - g (x))}^{2}) : I ⟶ ℝ$
28	1	3ad2ant1	$⊢ (φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \to I \in Fin$
29		0red	$⊢ (φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \to 0 \in ℝ$
30	27 28 29	fidmfisupp	$⊢ (φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \to {finSupp}_{0} ((x \in I ⟼ {(f (x) - g (x))}^{2}))$
31		regsumsupp	$⊢ ((x \in I ⟼ {(f (x) - g (x))}^{2}) : I ⟶ ℝ \land {finSupp}_{0} ((x \in I ⟼ {(f (x) - g (x))}^{2})) \land I \in Fin) \to \underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2} = \sum_{k \in (x \in I ⟼ {(f (x) - g (x))}^{2}) supp 0} (x \in I ⟼ {(f (x) - g (x))}^{2}) (k)$
32	27 30 28 31	syl3anc	$⊢ (φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \to \underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2} = \sum_{k \in (x \in I ⟼ {(f (x) - g (x))}^{2}) supp 0} (x \in I ⟼ {(f (x) - g (x))}^{2}) (k)$
33		ax-resscn	$⊢ ℝ \subseteq ℂ$
34	33	a1i	$⊢ f \in (ℝ^{I}) \to ℝ \subseteq ℂ$
35	17 34	fssd	$⊢ f \in (ℝ^{I}) \to f : I ⟶ ℂ$
36	35	3ad2ant2	$⊢ (φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \to f : I ⟶ ℂ$
37	36	ffvelcdmda	$⊢ ((φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \land x \in I) \to f (x) \in ℂ$
38	33	a1i	$⊢ g \in (ℝ^{I}) \to ℝ \subseteq ℂ$
39	20 38	fssd	$⊢ g \in (ℝ^{I}) \to g : I ⟶ ℂ$
40	39	3ad2ant3	$⊢ (φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \to g : I ⟶ ℂ$
41	40	ffvelcdmda	$⊢ ((φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \land x \in I) \to g (x) \in ℂ$
42	37 41	subcld	$⊢ ((φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \land x \in I) \to f (x) - g (x) \in ℂ$
43	42	sqcld	$⊢ ((φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \land x \in I) \to {(f (x) - g (x))}^{2} \in ℂ$
44	43 25	fmptd	$⊢ (φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \to (x \in I ⟼ {(f (x) - g (x))}^{2}) : I ⟶ ℂ$
45	28 44	fsumsupp0	$⊢ (φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \to \sum_{k \in (x \in I ⟼ {(f (x) - g (x))}^{2}) supp 0} (x \in I ⟼ {(f (x) - g (x))}^{2}) (k) = \sum_{k \in I} (x \in I ⟼ {(f (x) - g (x))}^{2}) (k)$
46		eqidd	$⊢ ((φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \land k \in I) \to (x \in I ⟼ {(f (x) - g (x))}^{2}) = (x \in I ⟼ {(f (x) - g (x))}^{2})$
47		fveq2	$⊢ x = k \to f (x) = f (k)$
48		fveq2	$⊢ x = k \to g (x) = g (k)$
49	47 48	oveq12d	$⊢ x = k \to f (x) - g (x) = f (k) - g (k)$
50	49	oveq1d	$⊢ x = k \to {(f (x) - g (x))}^{2} = {(f (k) - g (k))}^{2}$
51	50	adantl	$⊢ (((φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \land k \in I) \land x = k) \to {(f (x) - g (x))}^{2} = {(f (k) - g (k))}^{2}$
52		simpr	$⊢ ((φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \land k \in I) \to k \in I$
53		ovexd	$⊢ ((φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \land k \in I) \to {(f (k) - g (k))}^{2} \in V$
54	46 51 52 53	fvmptd	$⊢ ((φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \land k \in I) \to (x \in I ⟼ {(f (x) - g (x))}^{2}) (k) = {(f (k) - g (k))}^{2}$
55	54	sumeq2dv	$⊢ (φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \to \sum_{k \in I} (x \in I ⟼ {(f (x) - g (x))}^{2}) (k) = \sum_{k \in I} {(f (k) - g (k))}^{2}$
56	32 45 55	3eqtrd	$⊢ (φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \to \underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2} = \sum_{k \in I} {(f (k) - g (k))}^{2}$
57	56	fveq2d	$⊢ (φ \land f \in (ℝ^{I}) \land g \in (ℝ^{I})) \to \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}} = \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}}$
58	7 11 16 57	syl3anc	$⊢ (φ \land (f \in {Base}_{msup} \land g \in {Base}_{msup})) \to \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}} = \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}}$
59	5 6 58	mpoeq123dva	$⊢ φ \to (f \in {Base}_{msup}, g \in {Base}_{msup} ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}}) = (f \in (ℝ^{I}), g \in (ℝ^{I}) ⟼ \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}})$
60	59	fveq2d	$⊢ φ \to MetOpen ((f \in {Base}_{msup}, g \in {Base}_{msup} ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}})) = MetOpen ((f \in (ℝ^{I}), g \in (ℝ^{I}) ⟼ \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}}))$
61	2 60	eqtrd	$⊢ φ \to TopOpen (msup) = MetOpen ((f \in (ℝ^{I}), g \in (ℝ^{I}) ⟼ \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}}))$

Metamath Proof Explorer

Theorem rrxtopnfi

Proof