rrxmval

Description: The value of the Euclidean metric. Compare with rrnmval . (Contributed by Thierry Arnoux, 30-Jun-2019)

	Ref	Expression
Hypotheses	rrxmval.1	$⊢ X = \{h \in (ℝ^{I}) \| {finSupp}_{0} (h)\}$
	rrxmval.d	$⊢ D = dist (I)$
Assertion	rrxmval	$⊢ (I \in V \land F \in X \land G \in X) \to F D G = \sqrt{\sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}}$

Proof

Step	Hyp	Ref	Expression
1		rrxmval.1	$⊢ X = \{h \in (ℝ^{I}) \| {finSupp}_{0} (h)\}$
2		rrxmval.d	$⊢ D = dist (I)$
3		eqid	$⊢ I = I$
4		eqid	$⊢ {Base}_{I} = {Base}_{I}$
5	3 4	rrxds	$⊢ I \in V \to (f \in {Base}_{I}, g \in {Base}_{I} ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}}) = dist (I)$
6	2 5	eqtr4id	$⊢ I \in V \to D = (f \in {Base}_{I}, g \in {Base}_{I} ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}})$
7	3 4	rrxbase	$⊢ I \in V \to {Base}_{I} = \{h \in (ℝ^{I}) \| {finSupp}_{0} (h)\}$
8	1 7	eqtr4id	$⊢ I \in V \to X = {Base}_{I}$
9		mpoeq12	$⊢ (X = {Base}_{I} \land X = {Base}_{I}) \to (f \in X, g \in X ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}}) = (f \in {Base}_{I}, g \in {Base}_{I} ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}})$
10	8 8 9	syl2anc	$⊢ I \in V \to (f \in X, g \in X ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}}) = (f \in {Base}_{I}, g \in {Base}_{I} ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}})$
11	6 10	eqtr4d	$⊢ I \in V \to D = (f \in X, g \in X ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}})$
12	11	3ad2ant1	$⊢ (I \in V \land F \in X \land G \in X) \to D = (f \in X, g \in X ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}})$
13		simprl	$⊢ ((I \in V \land F \in X \land G \in X) \land (f = F \land g = G)) \to f = F$
14	13	fveq1d	$⊢ ((I \in V \land F \in X \land G \in X) \land (f = F \land g = G)) \to f (x) = F (x)$
15		simprr	$⊢ ((I \in V \land F \in X \land G \in X) \land (f = F \land g = G)) \to g = G$
16	15	fveq1d	$⊢ ((I \in V \land F \in X \land G \in X) \land (f = F \land g = G)) \to g (x) = G (x)$
17	14 16	oveq12d	$⊢ ((I \in V \land F \in X \land G \in X) \land (f = F \land g = G)) \to f (x) - g (x) = F (x) - G (x)$
18	17	oveq1d	$⊢ ((I \in V \land F \in X \land G \in X) \land (f = F \land g = G)) \to {(f (x) - g (x))}^{2} = {(F (x) - G (x))}^{2}$
19	18	mpteq2dv	$⊢ ((I \in V \land F \in X \land G \in X) \land (f = F \land g = G)) \to (x \in I ⟼ {(f (x) - g (x))}^{2}) = (x \in I ⟼ {(F (x) - G (x))}^{2})$
20	19	oveq2d	$⊢ ((I \in V \land F \in X \land G \in X) \land (f = F \land g = G)) \to \underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2} = \underset{x \in I}{\sum_{ℝ_{fld}}} {(F (x) - G (x))}^{2}$
21		simp2	$⊢ (I \in V \land F \in X \land G \in X) \to F \in X$
22	1 21	rrxf	$⊢ (I \in V \land F \in X \land G \in X) \to F : I ⟶ ℝ$
23	22	ffvelcdmda	$⊢ ((I \in V \land F \in X \land G \in X) \land x \in I) \to F (x) \in ℝ$
24		simp3	$⊢ (I \in V \land F \in X \land G \in X) \to G \in X$
25	1 24	rrxf	$⊢ (I \in V \land F \in X \land G \in X) \to G : I ⟶ ℝ$
26	25	ffvelcdmda	$⊢ ((I \in V \land F \in X \land G \in X) \land x \in I) \to G (x) \in ℝ$
27	23 26	resubcld	$⊢ ((I \in V \land F \in X \land G \in X) \land x \in I) \to F (x) - G (x) \in ℝ$
28	27	resqcld	$⊢ ((I \in V \land F \in X \land G \in X) \land x \in I) \to {(F (x) - G (x))}^{2} \in ℝ$
29	28	fmpttd	$⊢ (I \in V \land F \in X \land G \in X) \to (x \in I ⟼ {(F (x) - G (x))}^{2}) : I ⟶ ℝ$
30	1 21	rrxfsupp	$⊢ (I \in V \land F \in X \land G \in X) \to F supp 0 \in Fin$
31	1 24	rrxfsupp	$⊢ (I \in V \land F \in X \land G \in X) \to G supp 0 \in Fin$
32		unfi	$⊢ (F supp 0 \in Fin \land G supp 0 \in Fin) \to {supp}_{0} (F) \cup {supp}_{0} (G) \in Fin$
33	30 31 32	syl2anc	$⊢ (I \in V \land F \in X \land G \in X) \to {supp}_{0} (F) \cup {supp}_{0} (G) \in Fin$
34	1	rrxmvallem	$⊢ (I \in V \land F \in X \land G \in X) \to (x \in I ⟼ {(F (x) - G (x))}^{2}) supp 0 \subseteq {supp}_{0} (F) \cup {supp}_{0} (G)$
35	33 34	ssfid	$⊢ (I \in V \land F \in X \land G \in X) \to (x \in I ⟼ {(F (x) - G (x))}^{2}) supp 0 \in Fin$
36		mptexg	$⊢ I \in V \to (x \in I ⟼ {(F (x) - G (x))}^{2}) \in V$
37		funmpt	$⊢ Fun (x \in I ⟼ {(F (x) - G (x))}^{2})$
38		0cn	$⊢ 0 \in ℂ$
39		funisfsupp	$⊢ (Fun (x \in I ⟼ {(F (x) - G (x))}^{2}) \land (x \in I ⟼ {(F (x) - G (x))}^{2}) \in V \land 0 \in ℂ) \to ({finSupp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2})) \leftrightarrow (x \in I ⟼ {(F (x) - G (x))}^{2}) supp 0 \in Fin)$
40	37 38 39	mp3an13	$⊢ (x \in I ⟼ {(F (x) - G (x))}^{2}) \in V \to ({finSupp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2})) \leftrightarrow (x \in I ⟼ {(F (x) - G (x))}^{2}) supp 0 \in Fin)$
41	36 40	syl	$⊢ I \in V \to ({finSupp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2})) \leftrightarrow (x \in I ⟼ {(F (x) - G (x))}^{2}) supp 0 \in Fin)$
42	41	3ad2ant1	$⊢ (I \in V \land F \in X \land G \in X) \to ({finSupp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2})) \leftrightarrow (x \in I ⟼ {(F (x) - G (x))}^{2}) supp 0 \in Fin)$
43	35 42	mpbird	$⊢ (I \in V \land F \in X \land G \in X) \to {finSupp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2}))$
44		simp1	$⊢ (I \in V \land F \in X \land G \in X) \to I \in V$
45		regsumsupp	$⊢ ((x \in I ⟼ {(F (x) - G (x))}^{2}) : I ⟶ ℝ \land {finSupp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2})) \land I \in V) \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)$
46	29 43 44 45	syl3anc	$⊢ (I \in V \land F \in X \land G \in X) \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)$
47		suppssdm	$⊢ (x \in I ⟼ {(F (x) - G (x))}^{2}) supp 0 \subseteq dom (x \in I ⟼ {(F (x) - G (x))}^{2})$
48		eqid	$⊢ (x \in I ⟼ {(F (x) - G (x))}^{2}) = (x \in I ⟼ {(F (x) - G (x))}^{2})$
49	48	dmmptss	$⊢ dom (x \in I ⟼ {(F (x) - G (x))}^{2}) \subseteq I$
50	47 49	sstri	$⊢ (x \in I ⟼ {(F (x) - G (x))}^{2}) supp 0 \subseteq I$
51	50	a1i	$⊢ (I \in V \land F \in X \land G \in X) \to (x \in I ⟼ {(F (x) - G (x))}^{2}) supp 0 \subseteq I$
52	51	sselda	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in {supp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2}))) \to k \in I$
53		eqidd	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in I) \to (x \in I ⟼ {(F (x) - G (x))}^{2}) = (x \in I ⟼ {(F (x) - G (x))}^{2})$
54		simpr	$⊢ (((I \in V \land F \in X \land G \in X) \land k \in I) \land x = k) \to x = k$
55	54	fveq2d	$⊢ (((I \in V \land F \in X \land G \in X) \land k \in I) \land x = k) \to F (x) = F (k)$
56	54	fveq2d	$⊢ (((I \in V \land F \in X \land G \in X) \land k \in I) \land x = k) \to G (x) = G (k)$
57	55 56	oveq12d	$⊢ (((I \in V \land F \in X \land G \in X) \land k \in I) \land x = k) \to F (x) - G (x) = F (k) - G (k)$
58	57	oveq1d	$⊢ (((I \in V \land F \in X \land G \in X) \land k \in I) \land x = k) \to {(F (x) - G (x))}^{2} = {(F (k) - G (k))}^{2}$
59		simpr	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in I) \to k \in I$
60		ovexd	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in I) \to {(F (k) - G (k))}^{2} \in V$
61	53 58 59 60	fvmptd	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in I) \to (x \in I ⟼ {(F (x) - G (x))}^{2}) (k) = {(F (k) - G (k))}^{2}$
62	61	eqcomd	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in I) \to {(F (k) - G (k))}^{2} = (x \in I ⟼ {(F (x) - G (x))}^{2}) (k)$
63	52 62	syldan	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in {supp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2}))) \to {(F (k) - G (k))}^{2} = (x \in I ⟼ {(F (x) - G (x))}^{2}) (k)$
64	63	sumeq2dv	$⊢ (I \in V \land F \in X \land G \in X) \to \sum_{k \in (x \in I ⟼ {(F (x) - G (x))}^{2}) supp 0} {(F (k) - G (k))}^{2} = \sum_{k \in (x \in I ⟼ {(F (x) - G (x))}^{2}) supp 0} (x \in I ⟼ {(F (x) - G (x))}^{2}) (k)$
65	46 64	eqtr4d	$⊢ (I \in V \land F \in X \land G \in X) \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} {(F (k) - G (k))}^{2}$
66	65	adantr	$⊢ ((I \in V \land F \in X \land G \in X) \land (f = F \land g = G)) \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} {(F (k) - G (k))}^{2}$
67	22	ffvelcdmda	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in I) \to F (k) \in ℝ$
68	67	recnd	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in I) \to F (k) \in ℂ$
69	25	ffvelcdmda	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in I) \to G (k) \in ℝ$
70	69	recnd	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in I) \to G (k) \in ℂ$
71	68 70	subcld	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in I) \to F (k) - G (k) \in ℂ$
72	71	sqcld	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in I) \to {(F (k) - G (k))}^{2} \in ℂ$
73	52 72	syldan	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in {supp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2}))) \to {(F (k) - G (k))}^{2} \in ℂ$
74	1 21	rrxsuppss	$⊢ (I \in V \land F \in X \land G \in X) \to F supp 0 \subseteq I$
75	1 24	rrxsuppss	$⊢ (I \in V \land F \in X \land G \in X) \to G supp 0 \subseteq I$
76	74 75	unssd	$⊢ (I \in V \land F \in X \land G \in X) \to {supp}_{0} (F) \cup {supp}_{0} (G) \subseteq I$
77	76	ssdifssd	$⊢ (I \in V \land F \in X \land G \in X) \to ({supp}_{0} (F) \cup {supp}_{0} (G)) ∖ {supp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2})) \subseteq I$
78	77	sselda	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in (({supp}_{0} (F) \cup {supp}_{0} (G)) ∖ {supp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2})))) \to k \in I$
79	78 62	syldan	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in (({supp}_{0} (F) \cup {supp}_{0} (G)) ∖ {supp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2})))) \to {(F (k) - G (k))}^{2} = (x \in I ⟼ {(F (x) - G (x))}^{2}) (k)$
80	76	ssdifd	$⊢ (I \in V \land F \in X \land G \in X) \to ({supp}_{0} (F) \cup {supp}_{0} (G)) ∖ {supp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2})) \subseteq I ∖ {supp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2}))$
81	80	sselda	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in (({supp}_{0} (F) \cup {supp}_{0} (G)) ∖ {supp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2})))) \to k \in (I ∖ {supp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2})))$
82		ssidd	$⊢ (I \in V \land F \in X \land G \in X) \to (x \in I ⟼ {(F (x) - G (x))}^{2}) supp 0 \subseteq (x \in I ⟼ {(F (x) - G (x))}^{2}) supp 0$
83		0cnd	$⊢ (I \in V \land F \in X \land G \in X) \to 0 \in ℂ$
84	29 82 44 83	suppssr	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in (I ∖ {supp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2})))) \to (x \in I ⟼ {(F (x) - G (x))}^{2}) (k) = 0$
85	81 84	syldan	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in (({supp}_{0} (F) \cup {supp}_{0} (G)) ∖ {supp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2})))) \to (x \in I ⟼ {(F (x) - G (x))}^{2}) (k) = 0$
86	79 85	eqtrd	$⊢ ((I \in V \land F \in X \land G \in X) \land k \in (({supp}_{0} (F) \cup {supp}_{0} (G)) ∖ {supp}_{0} ((x \in I ⟼ {(F (x) - G (x))}^{2})))) \to {(F (k) - G (k))}^{2} = 0$
87	34 73 86 33	fsumss	$⊢ (I \in V \land F \in X \land G \in X) \to \sum_{k \in (x \in I ⟼ {(F (x) - G (x))}^{2}) supp 0} {(F (k) - G (k))}^{2} = \sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}$
88	87	adantr	$⊢ ((I \in V \land F \in X \land G \in X) \land (f = F \land g = G)) \to \sum_{k \in (x \in I ⟼ {(F (x) - G (x))}^{2}) supp 0} {(F (k) - G (k))}^{2} = \sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}$
89	20 66 88	3eqtrd	$⊢ ((I \in V \land F \in X \land G \in X) \land (f = F \land g = G)) \to \underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2} = \sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}$
90	89	fveq2d	$⊢ ((I \in V \land F \in X \land G \in X) \land (f = F \land g = G)) \to \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}} = \sqrt{\sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}}$
91		fvexd	$⊢ (I \in V \land F \in X \land G \in X) \to \sqrt{\sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}} \in V$
92	12 90 21 24 91	ovmpod	$⊢ (I \in V \land F \in X \land G \in X) \to F D G = \sqrt{\sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}}$

Metamath Proof Explorer

Theorem rrxmval

Proof