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

Metamath Proof Explorer

Theorem ismrer1

Proof