ismrer1

Description: An isometry between RR and RR ^ 1 . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	ismrer1.1	$⊢ R = {(abs \circ -) ↾}_{ℝ^{2}}$
	ismrer1.2	$⊢ F = (x \in ℝ ⟼ \{A\} \times \{x\})$
Assertion	ismrer1	$⊢ A \in V \to F \in (R Ismty ℝ^{n} (\{A\}))$

Proof

Step	Hyp	Ref	Expression
1		ismrer1.1	$⊢ R = {(abs \circ -) ↾}_{ℝ^{2}}$
2		ismrer1.2	$⊢ F = (x \in ℝ ⟼ \{A\} \times \{x\})$
3		sneq	$⊢ y = A \to \{y\} = \{A\}$
4	3	xpeq1d	$⊢ y = A \to \{y\} \times \{x\} = \{A\} \times \{x\}$
5	4	mpteq2dv	$⊢ y = A \to (x \in ℝ ⟼ \{y\} \times \{x\}) = (x \in ℝ ⟼ \{A\} \times \{x\})$
6	5 2	eqtr4di	$⊢ y = A \to (x \in ℝ ⟼ \{y\} \times \{x\}) = F$
7		f1oeq1	$⊢ (x \in ℝ ⟼ \{y\} \times \{x\}) = F \to ((x \in ℝ ⟼ \{y\} \times \{x\}) : ℝ \underset{1-1 onto}{⟶} ℝ^{\{y\}} \leftrightarrow F : ℝ \underset{1-1 onto}{⟶} ℝ^{\{y\}})$
8	6 7	syl	$⊢ y = A \to ((x \in ℝ ⟼ \{y\} \times \{x\}) : ℝ \underset{1-1 onto}{⟶} ℝ^{\{y\}} \leftrightarrow F : ℝ \underset{1-1 onto}{⟶} ℝ^{\{y\}})$
9	3	oveq2d	$⊢ y = A \to ℝ^{\{y\}} = ℝ^{\{A\}}$
10		f1oeq3	$⊢ ℝ^{\{y\}} = ℝ^{\{A\}} \to (F : ℝ \underset{1-1 onto}{⟶} ℝ^{\{y\}} \leftrightarrow F : ℝ \underset{1-1 onto}{⟶} ℝ^{\{A\}})$
11	9 10	syl	$⊢ y = A \to (F : ℝ \underset{1-1 onto}{⟶} ℝ^{\{y\}} \leftrightarrow F : ℝ \underset{1-1 onto}{⟶} ℝ^{\{A\}})$
12	8 11	bitrd	$⊢ y = A \to ((x \in ℝ ⟼ \{y\} \times \{x\}) : ℝ \underset{1-1 onto}{⟶} ℝ^{\{y\}} \leftrightarrow F : ℝ \underset{1-1 onto}{⟶} ℝ^{\{A\}})$
13		eqid	$⊢ \{y\} = \{y\}$
14		reex	$⊢ ℝ \in V$
15		vex	$⊢ y \in V$
16		eqid	$⊢ (x \in ℝ ⟼ \{y\} \times \{x\}) = (x \in ℝ ⟼ \{y\} \times \{x\})$
17	13 14 15 16	mapsnf1o3	$⊢ (x \in ℝ ⟼ \{y\} \times \{x\}) : ℝ \underset{1-1 onto}{⟶} ℝ^{\{y\}}$
18	12 17	vtoclg	$⊢ A \in V \to F : ℝ \underset{1-1 onto}{⟶} ℝ^{\{A\}}$
19		sneq	$⊢ x = y \to \{x\} = \{y\}$
20	19	xpeq2d	$⊢ x = y \to \{A\} \times \{x\} = \{A\} \times \{y\}$
21		snex	$⊢ \{A\} \in V$
22		snex	$⊢ \{x\} \in V$
23	21 22	xpex	$⊢ \{A\} \times \{x\} \in V$
24	20 2 23	fvmpt3i	$⊢ y \in ℝ \to F (y) = \{A\} \times \{y\}$
25	24	fveq1d	$⊢ y \in ℝ \to F (y) (A) = (\{A\} \times \{y\}) (A)$
26	25	adantr	$⊢ (y \in ℝ \land z \in ℝ) \to F (y) (A) = (\{A\} \times \{y\}) (A)$
27		snidg	$⊢ A \in V \to A \in \{A\}$
28		fvconst2g	$⊢ (y \in V \land A \in \{A\}) \to (\{A\} \times \{y\}) (A) = y$
29	15 27 28	sylancr	$⊢ A \in V \to (\{A\} \times \{y\}) (A) = y$
30	26 29	sylan9eqr	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to F (y) (A) = y$
31		sneq	$⊢ x = z \to \{x\} = \{z\}$
32	31	xpeq2d	$⊢ x = z \to \{A\} \times \{x\} = \{A\} \times \{z\}$
33	32 2 23	fvmpt3i	$⊢ z \in ℝ \to F (z) = \{A\} \times \{z\}$
34	33	fveq1d	$⊢ z \in ℝ \to F (z) (A) = (\{A\} \times \{z\}) (A)$
35	34	adantl	$⊢ (y \in ℝ \land z \in ℝ) \to F (z) (A) = (\{A\} \times \{z\}) (A)$
36		vex	$⊢ z \in V$
37		fvconst2g	$⊢ (z \in V \land A \in \{A\}) \to (\{A\} \times \{z\}) (A) = z$
38	36 27 37	sylancr	$⊢ A \in V \to (\{A\} \times \{z\}) (A) = z$
39	35 38	sylan9eqr	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to F (z) (A) = z$
40	30 39	oveq12d	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to F (y) (A) - F (z) (A) = y - z$
41	40	oveq1d	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to {(F (y) (A) - F (z) (A))}^{2} = {(y - z)}^{2}$
42		resubcl	$⊢ (y \in ℝ \land z \in ℝ) \to y - z \in ℝ$
43	42	adantl	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to y - z \in ℝ$
44		absresq	$⊢ y - z \in ℝ \to {\|y - z\|}^{2} = {(y - z)}^{2}$
45	43 44	syl	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to {\|y - z\|}^{2} = {(y - z)}^{2}$
46	41 45	eqtr4d	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to {(F (y) (A) - F (z) (A))}^{2} = {\|y - z\|}^{2}$
47	43	recnd	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to y - z \in ℂ$
48	47	abscld	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to \|y - z\| \in ℝ$
49	48	recnd	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to \|y - z\| \in ℂ$
50	49	sqcld	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to {\|y - z\|}^{2} \in ℂ$
51	46 50	eqeltrd	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to {(F (y) (A) - F (z) (A))}^{2} \in ℂ$
52		fveq2	$⊢ k = A \to F (y) (k) = F (y) (A)$
53		fveq2	$⊢ k = A \to F (z) (k) = F (z) (A)$
54	52 53	oveq12d	$⊢ k = A \to F (y) (k) - F (z) (k) = F (y) (A) - F (z) (A)$
55	54	oveq1d	$⊢ k = A \to {(F (y) (k) - F (z) (k))}^{2} = {(F (y) (A) - F (z) (A))}^{2}$
56	55	sumsn	$⊢ (A \in V \land {(F (y) (A) - F (z) (A))}^{2} \in ℂ) \to \sum_{k \in \{A\}} {(F (y) (k) - F (z) (k))}^{2} = {(F (y) (A) - F (z) (A))}^{2}$
57	51 56	syldan	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to \sum_{k \in \{A\}} {(F (y) (k) - F (z) (k))}^{2} = {(F (y) (A) - F (z) (A))}^{2}$
58	57 46	eqtrd	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to \sum_{k \in \{A\}} {(F (y) (k) - F (z) (k))}^{2} = {\|y - z\|}^{2}$
59	58	fveq2d	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to \sqrt{\sum_{k \in \{A\}} {(F (y) (k) - F (z) (k))}^{2}} = \sqrt{{\|y - z\|}^{2}}$
60	47	absge0d	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to 0 \leq \|y - z\|$
61	48 60	sqrtsqd	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to \sqrt{{\|y - z\|}^{2}} = \|y - z\|$
62	59 61	eqtrd	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to \sqrt{\sum_{k \in \{A\}} {(F (y) (k) - F (z) (k))}^{2}} = \|y - z\|$
63		f1of	$⊢ F : ℝ \underset{1-1 onto}{⟶} ℝ^{\{A\}} \to F : ℝ ⟶ ℝ^{\{A\}}$
64	18 63	syl	$⊢ A \in V \to F : ℝ ⟶ ℝ^{\{A\}}$
65	64	ffvelrnda	$⊢ (A \in V \land y \in ℝ) \to F (y) \in (ℝ^{\{A\}})$
66	64	ffvelrnda	$⊢ (A \in V \land z \in ℝ) \to F (z) \in (ℝ^{\{A\}})$
67	65 66	anim12dan	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to (F (y) \in (ℝ^{\{A\}}) \land F (z) \in (ℝ^{\{A\}}))$
68		snfi	$⊢ \{A\} \in Fin$
69		eqid	$⊢ ℝ^{\{A\}} = ℝ^{\{A\}}$
70	69	rrnmval	$⊢ (\{A\} \in Fin \land F (y) \in (ℝ^{\{A\}}) \land F (z) \in (ℝ^{\{A\}})) \to F (y) ℝ^{n} (\{A\}) F (z) = \sqrt{\sum_{k \in \{A\}} {(F (y) (k) - F (z) (k))}^{2}}$
71	68 70	mp3an1	$⊢ (F (y) \in (ℝ^{\{A\}}) \land F (z) \in (ℝ^{\{A\}})) \to F (y) ℝ^{n} (\{A\}) F (z) = \sqrt{\sum_{k \in \{A\}} {(F (y) (k) - F (z) (k))}^{2}}$
72	67 71	syl	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to F (y) ℝ^{n} (\{A\}) F (z) = \sqrt{\sum_{k \in \{A\}} {(F (y) (k) - F (z) (k))}^{2}}$
73	1	remetdval	$⊢ (y \in ℝ \land z \in ℝ) \to y R z = \|y - z\|$
74	73	adantl	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to y R z = \|y - z\|$
75	62 72 74	3eqtr4rd	$⊢ (A \in V \land (y \in ℝ \land z \in ℝ)) \to y R z = F (y) ℝ^{n} (\{A\}) F (z)$
76	75	ralrimivva	$⊢ A \in V \to \forall y \in ℝ \forall z \in ℝ y R z = F (y) ℝ^{n} (\{A\}) F (z)$
77	1	rexmet	$⊢ R \in ∞Met (ℝ)$
78	69	rrnmet	$⊢ \{A\} \in Fin \to ℝ^{n} (\{A\}) \in Met (ℝ^{\{A\}})$
79		metxmet	$⊢ ℝ^{n} (\{A\}) \in Met (ℝ^{\{A\}}) \to ℝ^{n} (\{A\}) \in ∞Met (ℝ^{\{A\}})$
80	68 78 79	mp2b	$⊢ ℝ^{n} (\{A\}) \in ∞Met (ℝ^{\{A\}})$
81		isismty	$⊢ (R \in ∞Met (ℝ) \land ℝ^{n} (\{A\}) \in ∞Met (ℝ^{\{A\}})) \to (F \in (R Ismty ℝ^{n} (\{A\})) \leftrightarrow (F : ℝ \underset{1-1 onto}{⟶} ℝ^{\{A\}} \land \forall y \in ℝ \forall z \in ℝ y R z = F (y) ℝ^{n} (\{A\}) F (z)))$
82	77 80 81	mp2an	$⊢ F \in (R Ismty ℝ^{n} (\{A\})) \leftrightarrow (F : ℝ \underset{1-1 onto}{⟶} ℝ^{\{A\}} \land \forall y \in ℝ \forall z \in ℝ y R z = F (y) ℝ^{n} (\{A\}) F (z))$
83	18 76 82	sylanbrc	$⊢ A \in V \to F \in (R Ismty ℝ^{n} (\{A\}))$

Metamath Proof Explorer

Theorem ismrer1

Proof