ismtyval

Description: The set of isometries between two metric spaces. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	ismtyval	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to M Ismty N = \{f \| (f : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = f (x) N f (y))\}$

Proof

Step	Hyp	Ref	Expression
1		df-ismty	$⊢ Ismty = (m \in ⋃ ran ∞Met, n \in ⋃ ran ∞Met ⟼ \{f \| (f : dom dom m \underset{1-1 onto}{⟶} dom dom n \land \forall x \in dom dom m \forall y \in dom dom m x m y = f (x) n f (y))\})$
2	1	a1i	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to Ismty = (m \in ⋃ ran ∞Met, n \in ⋃ ran ∞Met ⟼ \{f \| (f : dom dom m \underset{1-1 onto}{⟶} dom dom n \land \forall x \in dom dom m \forall y \in dom dom m x m y = f (x) n f (y))\})$
3		dmeq	$⊢ m = M \to dom m = dom M$
4		xmetf	$⊢ M \in ∞Met (X) \to M : X \times X ⟶ ℝ^{*}$
5	4	fdmd	$⊢ M \in ∞Met (X) \to dom M = X \times X$
6	3 5	sylan9eqr	$⊢ (M \in ∞Met (X) \land m = M) \to dom m = X \times X$
7	6	ad2ant2r	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (m = M \land n = N)) \to dom m = X \times X$
8	7	dmeqd	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (m = M \land n = N)) \to dom dom m = dom (X \times X)$
9		dmxpid	$⊢ dom (X \times X) = X$
10	8 9	eqtrdi	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (m = M \land n = N)) \to dom dom m = X$
11	10	f1oeq2d	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (m = M \land n = N)) \to (f : dom dom m \underset{1-1 onto}{⟶} dom dom n \leftrightarrow f : X \underset{1-1 onto}{⟶} dom dom n)$
12		dmeq	$⊢ n = N \to dom n = dom N$
13		xmetf	$⊢ N \in ∞Met (Y) \to N : Y \times Y ⟶ ℝ^{*}$
14	13	fdmd	$⊢ N \in ∞Met (Y) \to dom N = Y \times Y$
15	12 14	sylan9eqr	$⊢ (N \in ∞Met (Y) \land n = N) \to dom n = Y \times Y$
16	15	ad2ant2l	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (m = M \land n = N)) \to dom n = Y \times Y$
17	16	dmeqd	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (m = M \land n = N)) \to dom dom n = dom (Y \times Y)$
18		dmxpid	$⊢ dom (Y \times Y) = Y$
19	17 18	eqtrdi	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (m = M \land n = N)) \to dom dom n = Y$
20		f1oeq3	$⊢ dom dom n = Y \to (f : X \underset{1-1 onto}{⟶} dom dom n \leftrightarrow f : X \underset{1-1 onto}{⟶} Y)$
21	19 20	syl	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (m = M \land n = N)) \to (f : X \underset{1-1 onto}{⟶} dom dom n \leftrightarrow f : X \underset{1-1 onto}{⟶} Y)$
22	11 21	bitrd	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (m = M \land n = N)) \to (f : dom dom m \underset{1-1 onto}{⟶} dom dom n \leftrightarrow f : X \underset{1-1 onto}{⟶} Y)$
23		oveq	$⊢ m = M \to x m y = x M y$
24		oveq	$⊢ n = N \to f (x) n f (y) = f (x) N f (y)$
25	23 24	eqeqan12d	$⊢ (m = M \land n = N) \to (x m y = f (x) n f (y) \leftrightarrow x M y = f (x) N f (y))$
26	25	adantl	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (m = M \land n = N)) \to (x m y = f (x) n f (y) \leftrightarrow x M y = f (x) N f (y))$
27	10 26	raleqbidv	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (m = M \land n = N)) \to (\forall y \in dom dom m x m y = f (x) n f (y) \leftrightarrow \forall y \in X x M y = f (x) N f (y))$
28	10 27	raleqbidv	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (m = M \land n = N)) \to (\forall x \in dom dom m \forall y \in dom dom m x m y = f (x) n f (y) \leftrightarrow \forall x \in X \forall y \in X x M y = f (x) N f (y))$
29	22 28	anbi12d	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (m = M \land n = N)) \to ((f : dom dom m \underset{1-1 onto}{⟶} dom dom n \land \forall x \in dom dom m \forall y \in dom dom m x m y = f (x) n f (y)) \leftrightarrow (f : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = f (x) N f (y)))$
30	29	abbidv	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (m = M \land n = N)) \to \{f \| (f : dom dom m \underset{1-1 onto}{⟶} dom dom n \land \forall x \in dom dom m \forall y \in dom dom m x m y = f (x) n f (y))\} = \{f \| (f : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = f (x) N f (y))\}$
31		fvssunirn	$⊢ ∞Met (X) \subseteq ⋃ ran ∞Met$
32		simpl	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to M \in ∞Met (X)$
33	31 32	sselid	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to M \in ⋃ ran ∞Met$
34		fvssunirn	$⊢ ∞Met (Y) \subseteq ⋃ ran ∞Met$
35		simpr	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to N \in ∞Met (Y)$
36	34 35	sselid	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to N \in ⋃ ran ∞Met$
37		f1of	$⊢ f : X \underset{1-1 onto}{⟶} Y \to f : X ⟶ Y$
38	37	adantr	$⊢ (f : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = f (x) N f (y)) \to f : X ⟶ Y$
39		elfvdm	$⊢ N \in ∞Met (Y) \to Y \in dom ∞Met$
40		elfvdm	$⊢ M \in ∞Met (X) \to X \in dom ∞Met$
41		elmapg	$⊢ (Y \in dom ∞Met \land X \in dom ∞Met) \to (f \in (Y^{X}) \leftrightarrow f : X ⟶ Y)$
42	39 40 41	syl2anr	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to (f \in (Y^{X}) \leftrightarrow f : X ⟶ Y)$
43	38 42	syl5ibr	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to ((f : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = f (x) N f (y)) \to f \in (Y^{X}))$
44	43	abssdv	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to \{f \| (f : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = f (x) N f (y))\} \subseteq Y^{X}$
45		ovex	$⊢ Y^{X} \in V$
46	45	ssex	$⊢ \{f \| (f : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = f (x) N f (y))\} \subseteq Y^{X} \to \{f \| (f : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = f (x) N f (y))\} \in V$
47	44 46	syl	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to \{f \| (f : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = f (x) N f (y))\} \in V$
48	2 30 33 36 47	ovmpod	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to M Ismty N = \{f \| (f : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = f (x) N f (y))\}$

Metamath Proof Explorer

Theorem ismtyval

Proof