metf1o

Description: Use a bijection with a metric space to construct a metric on a set. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Hypothesis	metf1o.2	$⊢ N = (x \in Y, y \in Y ⟼ F (x) M F (y))$
	Assertion	metf1o	$⊢ (Y \in A \land M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \to N \in Met (Y)$

Proof

Step	Hyp	Ref	Expression
1		metf1o.2	$⊢ N = (x \in Y, y \in Y ⟼ F (x) M F (y))$
2		f1of	$⊢ F : Y \underset{1-1 onto}{⟶} X \to F : Y ⟶ X$
3		ffvelrn	$⊢ (F : Y ⟶ X \land x \in Y) \to F (x) \in X$
4	3	ex	$⊢ F : Y ⟶ X \to (x \in Y \to F (x) \in X)$
5		ffvelrn	$⊢ (F : Y ⟶ X \land y \in Y) \to F (y) \in X$
6	5	ex	$⊢ F : Y ⟶ X \to (y \in Y \to F (y) \in X)$
7	4 6	anim12d	$⊢ F : Y ⟶ X \to ((x \in Y \land y \in Y) \to (F (x) \in X \land F (y) \in X))$
8	2 7	syl	$⊢ F : Y \underset{1-1 onto}{⟶} X \to ((x \in Y \land y \in Y) \to (F (x) \in X \land F (y) \in X))$
9		metcl	$⊢ (M \in Met (X) \land F (x) \in X \land F (y) \in X) \to F (x) M F (y) \in ℝ$
10	9	3expib	$⊢ M \in Met (X) \to ((F (x) \in X \land F (y) \in X) \to F (x) M F (y) \in ℝ)$
11	8 10	sylan9r	$⊢ (M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \to ((x \in Y \land y \in Y) \to F (x) M F (y) \in ℝ)$
12	11	3adant1	$⊢ (Y \in A \land M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \to ((x \in Y \land y \in Y) \to F (x) M F (y) \in ℝ)$
13	12	ralrimivv	$⊢ (Y \in A \land M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \to \forall x \in Y \forall y \in Y F (x) M F (y) \in ℝ$
14	1	fmpo	$⊢ \forall x \in Y \forall y \in Y F (x) M F (y) \in ℝ \leftrightarrow N : Y \times Y ⟶ ℝ$
15	13 14	sylib	$⊢ (Y \in A \land M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \to N : Y \times Y ⟶ ℝ$
16		fveq2	$⊢ x = u \to F (x) = F (u)$
17	16	oveq1d	$⊢ x = u \to F (x) M F (y) = F (u) M F (y)$
18		fveq2	$⊢ y = v \to F (y) = F (v)$
19	18	oveq2d	$⊢ y = v \to F (u) M F (y) = F (u) M F (v)$
20		ovex	$⊢ F (u) M F (v) \in V$
21	17 19 1 20	ovmpo	$⊢ (u \in Y \land v \in Y) \to u N v = F (u) M F (v)$
22	21	eqeq1d	$⊢ (u \in Y \land v \in Y) \to (u N v = 0 \leftrightarrow F (u) M F (v) = 0)$
23	22	adantl	$⊢ ((M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \land (u \in Y \land v \in Y)) \to (u N v = 0 \leftrightarrow F (u) M F (v) = 0)$
24		ffvelrn	$⊢ (F : Y ⟶ X \land u \in Y) \to F (u) \in X$
25	24	ex	$⊢ F : Y ⟶ X \to (u \in Y \to F (u) \in X)$
26		ffvelrn	$⊢ (F : Y ⟶ X \land v \in Y) \to F (v) \in X$
27	26	ex	$⊢ F : Y ⟶ X \to (v \in Y \to F (v) \in X)$
28	25 27	anim12d	$⊢ F : Y ⟶ X \to ((u \in Y \land v \in Y) \to (F (u) \in X \land F (v) \in X))$
29	2 28	syl	$⊢ F : Y \underset{1-1 onto}{⟶} X \to ((u \in Y \land v \in Y) \to (F (u) \in X \land F (v) \in X))$
30	29	imp	$⊢ (F : Y \underset{1-1 onto}{⟶} X \land (u \in Y \land v \in Y)) \to (F (u) \in X \land F (v) \in X)$
31	30	adantll	$⊢ ((M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \land (u \in Y \land v \in Y)) \to (F (u) \in X \land F (v) \in X)$
32		meteq0	$⊢ (M \in Met (X) \land F (u) \in X \land F (v) \in X) \to (F (u) M F (v) = 0 \leftrightarrow F (u) = F (v))$
33	32	3expb	$⊢ (M \in Met (X) \land (F (u) \in X \land F (v) \in X)) \to (F (u) M F (v) = 0 \leftrightarrow F (u) = F (v))$
34	33	adantlr	$⊢ ((M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \land (F (u) \in X \land F (v) \in X)) \to (F (u) M F (v) = 0 \leftrightarrow F (u) = F (v))$
35	31 34	syldan	$⊢ ((M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \land (u \in Y \land v \in Y)) \to (F (u) M F (v) = 0 \leftrightarrow F (u) = F (v))$
36		f1of1	$⊢ F : Y \underset{1-1 onto}{⟶} X \to F : Y \underset{1-1}{⟶} X$
37		f1fveq	$⊢ (F : Y \underset{1-1}{⟶} X \land (u \in Y \land v \in Y)) \to (F (u) = F (v) \leftrightarrow u = v)$
38	36 37	sylan	$⊢ (F : Y \underset{1-1 onto}{⟶} X \land (u \in Y \land v \in Y)) \to (F (u) = F (v) \leftrightarrow u = v)$
39	38	adantll	$⊢ ((M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \land (u \in Y \land v \in Y)) \to (F (u) = F (v) \leftrightarrow u = v)$
40	23 35 39	3bitrd	$⊢ ((M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \land (u \in Y \land v \in Y)) \to (u N v = 0 \leftrightarrow u = v)$
41		ffvelrn	$⊢ (F : Y ⟶ X \land w \in Y) \to F (w) \in X$
42	41	ex	$⊢ F : Y ⟶ X \to (w \in Y \to F (w) \in X)$
43	28 42	anim12d	$⊢ F : Y ⟶ X \to (((u \in Y \land v \in Y) \land w \in Y) \to ((F (u) \in X \land F (v) \in X) \land F (w) \in X))$
44	2 43	syl	$⊢ F : Y \underset{1-1 onto}{⟶} X \to (((u \in Y \land v \in Y) \land w \in Y) \to ((F (u) \in X \land F (v) \in X) \land F (w) \in X))$
45	44	imp	$⊢ (F : Y \underset{1-1 onto}{⟶} X \land ((u \in Y \land v \in Y) \land w \in Y)) \to ((F (u) \in X \land F (v) \in X) \land F (w) \in X)$
46	45	adantll	$⊢ ((M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \land ((u \in Y \land v \in Y) \land w \in Y)) \to ((F (u) \in X \land F (v) \in X) \land F (w) \in X)$
47		mettri2	$⊢ (M \in Met (X) \land (F (w) \in X \land F (u) \in X \land F (v) \in X)) \to F (u) M F (v) \leq (F (w) M F (u)) + (F (w) M F (v))$
48	47	expcom	$⊢ (F (w) \in X \land F (u) \in X \land F (v) \in X) \to (M \in Met (X) \to F (u) M F (v) \leq (F (w) M F (u)) + (F (w) M F (v)))$
49	48	3expb	$⊢ (F (w) \in X \land (F (u) \in X \land F (v) \in X)) \to (M \in Met (X) \to F (u) M F (v) \leq (F (w) M F (u)) + (F (w) M F (v)))$
50	49	ancoms	$⊢ ((F (u) \in X \land F (v) \in X) \land F (w) \in X) \to (M \in Met (X) \to F (u) M F (v) \leq (F (w) M F (u)) + (F (w) M F (v)))$
51	50	impcom	$⊢ (M \in Met (X) \land ((F (u) \in X \land F (v) \in X) \land F (w) \in X)) \to F (u) M F (v) \leq (F (w) M F (u)) + (F (w) M F (v))$
52	51	adantlr	$⊢ ((M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \land ((F (u) \in X \land F (v) \in X) \land F (w) \in X)) \to F (u) M F (v) \leq (F (w) M F (u)) + (F (w) M F (v))$
53	46 52	syldan	$⊢ ((M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \land ((u \in Y \land v \in Y) \land w \in Y)) \to F (u) M F (v) \leq (F (w) M F (u)) + (F (w) M F (v))$
54	53	anassrs	$⊢ (((M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \land (u \in Y \land v \in Y)) \land w \in Y) \to F (u) M F (v) \leq (F (w) M F (u)) + (F (w) M F (v))$
55	21	adantr	$⊢ ((u \in Y \land v \in Y) \land w \in Y) \to u N v = F (u) M F (v)$
56		fveq2	$⊢ x = w \to F (x) = F (w)$
57	56	oveq1d	$⊢ x = w \to F (x) M F (y) = F (w) M F (y)$
58		fveq2	$⊢ y = u \to F (y) = F (u)$
59	58	oveq2d	$⊢ y = u \to F (w) M F (y) = F (w) M F (u)$
60		ovex	$⊢ F (w) M F (u) \in V$
61	57 59 1 60	ovmpo	$⊢ (w \in Y \land u \in Y) \to w N u = F (w) M F (u)$
62	61	ancoms	$⊢ (u \in Y \land w \in Y) \to w N u = F (w) M F (u)$
63	62	adantlr	$⊢ ((u \in Y \land v \in Y) \land w \in Y) \to w N u = F (w) M F (u)$
64	18	oveq2d	$⊢ y = v \to F (w) M F (y) = F (w) M F (v)$
65		ovex	$⊢ F (w) M F (v) \in V$
66	57 64 1 65	ovmpo	$⊢ (w \in Y \land v \in Y) \to w N v = F (w) M F (v)$
67	66	ancoms	$⊢ (v \in Y \land w \in Y) \to w N v = F (w) M F (v)$
68	67	adantll	$⊢ ((u \in Y \land v \in Y) \land w \in Y) \to w N v = F (w) M F (v)$
69	63 68	oveq12d	$⊢ ((u \in Y \land v \in Y) \land w \in Y) \to (w N u) + (w N v) = (F (w) M F (u)) + (F (w) M F (v))$
70	55 69	breq12d	$⊢ ((u \in Y \land v \in Y) \land w \in Y) \to (u N v \leq (w N u) + (w N v) \leftrightarrow F (u) M F (v) \leq (F (w) M F (u)) + (F (w) M F (v)))$
71	70	adantll	$⊢ (((M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \land (u \in Y \land v \in Y)) \land w \in Y) \to (u N v \leq (w N u) + (w N v) \leftrightarrow F (u) M F (v) \leq (F (w) M F (u)) + (F (w) M F (v)))$
72	54 71	mpbird	$⊢ (((M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \land (u \in Y \land v \in Y)) \land w \in Y) \to u N v \leq (w N u) + (w N v)$
73	72	ralrimiva	$⊢ ((M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \land (u \in Y \land v \in Y)) \to \forall w \in Y u N v \leq (w N u) + (w N v)$
74	40 73	jca	$⊢ ((M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \land (u \in Y \land v \in Y)) \to ((u N v = 0 \leftrightarrow u = v) \land \forall w \in Y u N v \leq (w N u) + (w N v))$
75	74	3adantl1	$⊢ ((Y \in A \land M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \land (u \in Y \land v \in Y)) \to ((u N v = 0 \leftrightarrow u = v) \land \forall w \in Y u N v \leq (w N u) + (w N v))$
76	75	ex	$⊢ (Y \in A \land M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \to ((u \in Y \land v \in Y) \to ((u N v = 0 \leftrightarrow u = v) \land \forall w \in Y u N v \leq (w N u) + (w N v)))$
77	76	ralrimivv	$⊢ (Y \in A \land M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \to \forall u \in Y \forall v \in Y ((u N v = 0 \leftrightarrow u = v) \land \forall w \in Y u N v \leq (w N u) + (w N v))$
78		ismet	$⊢ Y \in A \to (N \in Met (Y) \leftrightarrow (N : Y \times Y ⟶ ℝ \land \forall u \in Y \forall v \in Y ((u N v = 0 \leftrightarrow u = v) \land \forall w \in Y u N v \leq (w N u) + (w N v))))$
79	78	3ad2ant1	$⊢ (Y \in A \land M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \to (N \in Met (Y) \leftrightarrow (N : Y \times Y ⟶ ℝ \land \forall u \in Y \forall v \in Y ((u N v = 0 \leftrightarrow u = v) \land \forall w \in Y u N v \leq (w N u) + (w N v))))$
80	15 77 79	mpbir2and	$⊢ (Y \in A \land M \in Met (X) \land F : Y \underset{1-1 onto}{⟶} X) \to N \in Met (Y)$

Metamath Proof Explorer

Theorem metf1o

Proof