rrxmvallem

Description: Support of the function used for building the distance . (Contributed by Thierry Arnoux, 30-Jun-2019)

		Ref	Expression
	Hypothesis	rrxmval.1	$⊢ X = \{h \in (ℝ^{I}) \| {finSupp}_{0} (h)\}$
	Assertion	rrxmvallem	$⊢ (I \in V \land F \in X \land G \in X) \to (k \in I ⟼ {(F (k) - G (k))}^{2}) supp 0 \subseteq {supp}_{0} (F) \cup {supp}_{0} (G)$

Proof

Step	Hyp	Ref	Expression
1		rrxmval.1	$⊢ X = \{h \in (ℝ^{I}) \| {finSupp}_{0} (h)\}$
2		simprl	$⊢ (((I \in V \land F \in X \land G \in X) \land x \in I) \land (F (x) = 0 \land G (x) = 0)) \to F (x) = 0$
3		0cn	$⊢ 0 \in ℂ$
4	2 3	eqeltrdi	$⊢ (((I \in V \land F \in X \land G \in X) \land x \in I) \land (F (x) = 0 \land G (x) = 0)) \to F (x) \in ℂ$
5		simprr	$⊢ (((I \in V \land F \in X \land G \in X) \land x \in I) \land (F (x) = 0 \land G (x) = 0)) \to G (x) = 0$
6	2 5	eqtr4d	$⊢ (((I \in V \land F \in X \land G \in X) \land x \in I) \land (F (x) = 0 \land G (x) = 0)) \to F (x) = G (x)$
7	4 6	subeq0bd	$⊢ (((I \in V \land F \in X \land G \in X) \land x \in I) \land (F (x) = 0 \land G (x) = 0)) \to F (x) - G (x) = 0$
8	7	sq0id	$⊢ (((I \in V \land F \in X \land G \in X) \land x \in I) \land (F (x) = 0 \land G (x) = 0)) \to {(F (x) - G (x))}^{2} = 0$
9	8	ex	$⊢ ((I \in V \land F \in X \land G \in X) \land x \in I) \to ((F (x) = 0 \land G (x) = 0) \to {(F (x) - G (x))}^{2} = 0)$
10		ioran	$⊢ \neg (F (x) \neq 0 \lor G (x) \neq 0) \leftrightarrow (\neg F (x) \neq 0 \land \neg G (x) \neq 0)$
11		nne	$⊢ \neg F (x) \neq 0 \leftrightarrow F (x) = 0$
12		nne	$⊢ \neg G (x) \neq 0 \leftrightarrow G (x) = 0$
13	11 12	anbi12i	$⊢ (\neg F (x) \neq 0 \land \neg G (x) \neq 0) \leftrightarrow (F (x) = 0 \land G (x) = 0)$
14	10 13	bitri	$⊢ \neg (F (x) \neq 0 \lor G (x) \neq 0) \leftrightarrow (F (x) = 0 \land G (x) = 0)$
15	14	a1i	$⊢ ((I \in V \land F \in X \land G \in X) \land x \in I) \to (\neg (F (x) \neq 0 \lor G (x) \neq 0) \leftrightarrow (F (x) = 0 \land G (x) = 0))$
16		eqidd	$⊢ ((I \in V \land F \in X \land G \in X) \land x \in I) \to (k \in I ⟼ {(F (k) - G (k))}^{2}) = (k \in I ⟼ {(F (k) - G (k))}^{2})$
17		simpr	$⊢ (((I \in V \land F \in X \land G \in X) \land x \in I) \land k = x) \to k = x$
18	17	fveq2d	$⊢ (((I \in V \land F \in X \land G \in X) \land x \in I) \land k = x) \to F (k) = F (x)$
19	17	fveq2d	$⊢ (((I \in V \land F \in X \land G \in X) \land x \in I) \land k = x) \to G (k) = G (x)$
20	18 19	oveq12d	$⊢ (((I \in V \land F \in X \land G \in X) \land x \in I) \land k = x) \to F (k) - G (k) = F (x) - G (x)$
21	20	oveq1d	$⊢ (((I \in V \land F \in X \land G \in X) \land x \in I) \land k = x) \to {(F (k) - G (k))}^{2} = {(F (x) - G (x))}^{2}$
22		simpr	$⊢ ((I \in V \land F \in X \land G \in X) \land x \in I) \to x \in I$
23		ovex	$⊢ {(F (x) - G (x))}^{2} \in V$
24	23	a1i	$⊢ ((I \in V \land F \in X \land G \in X) \land x \in I) \to {(F (x) - G (x))}^{2} \in V$
25	16 21 22 24	fvmptd	$⊢ ((I \in V \land F \in X \land G \in X) \land x \in I) \to (k \in I ⟼ {(F (k) - G (k))}^{2}) (x) = {(F (x) - G (x))}^{2}$
26	25	neeq1d	$⊢ ((I \in V \land F \in X \land G \in X) \land x \in I) \to ((k \in I ⟼ {(F (k) - G (k))}^{2}) (x) \neq 0 \leftrightarrow {(F (x) - G (x))}^{2} \neq 0)$
27	26	bicomd	$⊢ ((I \in V \land F \in X \land G \in X) \land x \in I) \to ({(F (x) - G (x))}^{2} \neq 0 \leftrightarrow (k \in I ⟼ {(F (k) - G (k))}^{2}) (x) \neq 0)$
28	27	necon1bbid	$⊢ ((I \in V \land F \in X \land G \in X) \land x \in I) \to (\neg (k \in I ⟼ {(F (k) - G (k))}^{2}) (x) \neq 0 \leftrightarrow {(F (x) - G (x))}^{2} = 0)$
29	9 15 28	3imtr4d	$⊢ ((I \in V \land F \in X \land G \in X) \land x \in I) \to (\neg (F (x) \neq 0 \lor G (x) \neq 0) \to \neg (k \in I ⟼ {(F (k) - G (k))}^{2}) (x) \neq 0)$
30	29	con4d	$⊢ ((I \in V \land F \in X \land G \in X) \land x \in I) \to ((k \in I ⟼ {(F (k) - G (k))}^{2}) (x) \neq 0 \to (F (x) \neq 0 \lor G (x) \neq 0))$
31	30	ss2rabdv	$⊢ (I \in V \land F \in X \land G \in X) \to \{x \in I \| (k \in I ⟼ {(F (k) - G (k))}^{2}) (x) \neq 0\} \subseteq \{x \in I \| (F (x) \neq 0 \lor G (x) \neq 0)\}$
32		unrab	$⊢ \{x \in I \| F (x) \neq 0\} \cup \{x \in I \| G (x) \neq 0\} = \{x \in I \| (F (x) \neq 0 \lor G (x) \neq 0)\}$
33	31 32	sseqtrrdi	$⊢ (I \in V \land F \in X \land G \in X) \to \{x \in I \| (k \in I ⟼ {(F (k) - G (k))}^{2}) (x) \neq 0\} \subseteq \{x \in I \| F (x) \neq 0\} \cup \{x \in I \| G (x) \neq 0\}$
34		simp1	$⊢ (I \in V \land F \in X \land G \in X) \to I \in V$
35		ovex	$⊢ {(F (k) - G (k))}^{2} \in V$
36		eqid	$⊢ (k \in I ⟼ {(F (k) - G (k))}^{2}) = (k \in I ⟼ {(F (k) - G (k))}^{2})$
37	35 36	fnmpti	$⊢ (k \in I ⟼ {(F (k) - G (k))}^{2}) Fn I$
38		suppvalfn	$⊢ ((k \in I ⟼ {(F (k) - G (k))}^{2}) Fn I \land I \in V \land 0 \in ℂ) \to (k \in I ⟼ {(F (k) - G (k))}^{2}) supp 0 = \{x \in I \| (k \in I ⟼ {(F (k) - G (k))}^{2}) (x) \neq 0\}$
39	37 3 38	mp3an13	$⊢ I \in V \to (k \in I ⟼ {(F (k) - G (k))}^{2}) supp 0 = \{x \in I \| (k \in I ⟼ {(F (k) - G (k))}^{2}) (x) \neq 0\}$
40	34 39	syl	$⊢ (I \in V \land F \in X \land G \in X) \to (k \in I ⟼ {(F (k) - G (k))}^{2}) supp 0 = \{x \in I \| (k \in I ⟼ {(F (k) - G (k))}^{2}) (x) \neq 0\}$
41		elrabi	$⊢ F \in \{h \in (ℝ^{I}) \| {finSupp}_{0} (h)\} \to F \in (ℝ^{I})$
42	41 1	eleq2s	$⊢ F \in X \to F \in (ℝ^{I})$
43		elmapi	$⊢ F \in (ℝ^{I}) \to F : I ⟶ ℝ$
44		ffn	$⊢ F : I ⟶ ℝ \to F Fn I$
45	42 43 44	3syl	$⊢ F \in X \to F Fn I$
46	45	3ad2ant2	$⊢ (I \in V \land F \in X \land G \in X) \to F Fn I$
47	3	a1i	$⊢ (I \in V \land F \in X \land G \in X) \to 0 \in ℂ$
48		suppvalfn	$⊢ (F Fn I \land I \in V \land 0 \in ℂ) \to F supp 0 = \{x \in I \| F (x) \neq 0\}$
49	46 34 47 48	syl3anc	$⊢ (I \in V \land F \in X \land G \in X) \to F supp 0 = \{x \in I \| F (x) \neq 0\}$
50		elrabi	$⊢ G \in \{h \in (ℝ^{I}) \| {finSupp}_{0} (h)\} \to G \in (ℝ^{I})$
51	50 1	eleq2s	$⊢ G \in X \to G \in (ℝ^{I})$
52		elmapi	$⊢ G \in (ℝ^{I}) \to G : I ⟶ ℝ$
53		ffn	$⊢ G : I ⟶ ℝ \to G Fn I$
54	51 52 53	3syl	$⊢ G \in X \to G Fn I$
55	54	3ad2ant3	$⊢ (I \in V \land F \in X \land G \in X) \to G Fn I$
56		suppvalfn	$⊢ (G Fn I \land I \in V \land 0 \in ℂ) \to G supp 0 = \{x \in I \| G (x) \neq 0\}$
57	55 34 47 56	syl3anc	$⊢ (I \in V \land F \in X \land G \in X) \to G supp 0 = \{x \in I \| G (x) \neq 0\}$
58	49 57	uneq12d	$⊢ (I \in V \land F \in X \land G \in X) \to {supp}_{0} (F) \cup {supp}_{0} (G) = \{x \in I \| F (x) \neq 0\} \cup \{x \in I \| G (x) \neq 0\}$
59	33 40 58	3sstr4d	$⊢ (I \in V \land F \in X \land G \in X) \to (k \in I ⟼ {(F (k) - G (k))}^{2}) supp 0 \subseteq {supp}_{0} (F) \cup {supp}_{0} (G)$

Metamath Proof Explorer

Theorem rrxmvallem

Proof