imasf1oxmet

Description: The image of an extended metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Hypotheses	imasf1oxmet.u	$⊢ φ \to U = F “_{𝑠} R$
	imasf1oxmet.v	$⊢ φ \to V = {Base}_{R}$
	imasf1oxmet.f	$⊢ φ \to F : V \underset{1-1 onto}{⟶} B$
	imasf1oxmet.r	$⊢ φ \to R \in Z$
	imasf1oxmet.e	$⊢ E = {dist (R) ↾}_{(V \times V)}$
	imasf1oxmet.d	$⊢ D = dist (U)$
	imasf1oxmet.m	$⊢ φ \to E \in ∞Met (V)$
Assertion	imasf1oxmet	$⊢ φ \to D \in ∞Met (B)$

Proof

Step	Hyp	Ref	Expression
1		imasf1oxmet.u	$⊢ φ \to U = F “_{𝑠} R$
2		imasf1oxmet.v	$⊢ φ \to V = {Base}_{R}$
3		imasf1oxmet.f	$⊢ φ \to F : V \underset{1-1 onto}{⟶} B$
4		imasf1oxmet.r	$⊢ φ \to R \in Z$
5		imasf1oxmet.e	$⊢ E = {dist (R) ↾}_{(V \times V)}$
6		imasf1oxmet.d	$⊢ D = dist (U)$
7		imasf1oxmet.m	$⊢ φ \to E \in ∞Met (V)$
8		f1ofo	$⊢ F : V \underset{1-1 onto}{⟶} B \to F : V \underset{onto}{⟶} B$
9	3 8	syl	$⊢ φ \to F : V \underset{onto}{⟶} B$
10		eqid	$⊢ dist (R) = dist (R)$
11	1 2 9 4 10 6	imasdsfn	$⊢ φ \to D Fn (B \times B)$
12	1	adantr	$⊢ (φ \land (a \in V \land b \in V)) \to U = F “_{𝑠} R$
13	2	adantr	$⊢ (φ \land (a \in V \land b \in V)) \to V = {Base}_{R}$
14	3	adantr	$⊢ (φ \land (a \in V \land b \in V)) \to F : V \underset{1-1 onto}{⟶} B$
15	4	adantr	$⊢ (φ \land (a \in V \land b \in V)) \to R \in Z$
16	7	adantr	$⊢ (φ \land (a \in V \land b \in V)) \to E \in ∞Met (V)$
17		simprl	$⊢ (φ \land (a \in V \land b \in V)) \to a \in V$
18		simprr	$⊢ (φ \land (a \in V \land b \in V)) \to b \in V$
19	12 13 14 15 5 6 16 17 18	imasdsf1o	$⊢ (φ \land (a \in V \land b \in V)) \to F (a) D F (b) = a E b$
20		xmetcl	$⊢ (E \in ∞Met (V) \land a \in V \land b \in V) \to a E b \in ℝ^{*}$
21	20	3expb	$⊢ (E \in ∞Met (V) \land (a \in V \land b \in V)) \to a E b \in ℝ^{*}$
22	7 21	sylan	$⊢ (φ \land (a \in V \land b \in V)) \to a E b \in ℝ^{*}$
23	19 22	eqeltrd	$⊢ (φ \land (a \in V \land b \in V)) \to F (a) D F (b) \in ℝ^{*}$
24	23	ralrimivva	$⊢ φ \to \forall a \in V \forall b \in V F (a) D F (b) \in ℝ^{*}$
25		f1ofn	$⊢ F : V \underset{1-1 onto}{⟶} B \to F Fn V$
26	3 25	syl	$⊢ φ \to F Fn V$
27		oveq2	$⊢ y = F (b) \to F (a) D y = F (a) D F (b)$
28	27	eleq1d	$⊢ y = F (b) \to (F (a) D y \in ℝ^{} \leftrightarrow F (a) D F (b) \in ℝ^{})$
29	28	ralrn	$⊢ F Fn V \to (\forall y \in ran F F (a) D y \in ℝ^{} \leftrightarrow \forall b \in V F (a) D F (b) \in ℝ^{})$
30	26 29	syl	$⊢ φ \to (\forall y \in ran F F (a) D y \in ℝ^{} \leftrightarrow \forall b \in V F (a) D F (b) \in ℝ^{})$
31		forn	$⊢ F : V \underset{onto}{⟶} B \to ran F = B$
32	9 31	syl	$⊢ φ \to ran F = B$
33	32	raleqdv	$⊢ φ \to (\forall y \in ran F F (a) D y \in ℝ^{} \leftrightarrow \forall y \in B F (a) D y \in ℝ^{})$
34	30 33	bitr3d	$⊢ φ \to (\forall b \in V F (a) D F (b) \in ℝ^{} \leftrightarrow \forall y \in B F (a) D y \in ℝ^{})$
35	34	ralbidv	$⊢ φ \to (\forall a \in V \forall b \in V F (a) D F (b) \in ℝ^{} \leftrightarrow \forall a \in V \forall y \in B F (a) D y \in ℝ^{})$
36	24 35	mpbid	$⊢ φ \to \forall a \in V \forall y \in B F (a) D y \in ℝ^{*}$
37		oveq1	$⊢ x = F (a) \to x D y = F (a) D y$
38	37	eleq1d	$⊢ x = F (a) \to (x D y \in ℝ^{} \leftrightarrow F (a) D y \in ℝ^{})$
39	38	ralbidv	$⊢ x = F (a) \to (\forall y \in B x D y \in ℝ^{} \leftrightarrow \forall y \in B F (a) D y \in ℝ^{})$
40	39	ralrn	$⊢ F Fn V \to (\forall x \in ran F \forall y \in B x D y \in ℝ^{} \leftrightarrow \forall a \in V \forall y \in B F (a) D y \in ℝ^{})$
41	26 40	syl	$⊢ φ \to (\forall x \in ran F \forall y \in B x D y \in ℝ^{} \leftrightarrow \forall a \in V \forall y \in B F (a) D y \in ℝ^{})$
42	32	raleqdv	$⊢ φ \to (\forall x \in ran F \forall y \in B x D y \in ℝ^{} \leftrightarrow \forall x \in B \forall y \in B x D y \in ℝ^{})$
43	41 42	bitr3d	$⊢ φ \to (\forall a \in V \forall y \in B F (a) D y \in ℝ^{} \leftrightarrow \forall x \in B \forall y \in B x D y \in ℝ^{})$
44	36 43	mpbid	$⊢ φ \to \forall x \in B \forall y \in B x D y \in ℝ^{*}$
45		ffnov	$⊢ D : B \times B ⟶ ℝ^{} \leftrightarrow (D Fn (B \times B) \land \forall x \in B \forall y \in B x D y \in ℝ^{})$
46	11 44 45	sylanbrc	$⊢ φ \to D : B \times B ⟶ ℝ^{*}$
47		xmeteq0	$⊢ (E \in ∞Met (V) \land a \in V \land b \in V) \to (a E b = 0 \leftrightarrow a = b)$
48	16 17 18 47	syl3anc	$⊢ (φ \land (a \in V \land b \in V)) \to (a E b = 0 \leftrightarrow a = b)$
49	19	eqeq1d	$⊢ (φ \land (a \in V \land b \in V)) \to (F (a) D F (b) = 0 \leftrightarrow a E b = 0)$
50		f1of1	$⊢ F : V \underset{1-1 onto}{⟶} B \to F : V \underset{1-1}{⟶} B$
51	3 50	syl	$⊢ φ \to F : V \underset{1-1}{⟶} B$
52		f1fveq	$⊢ (F : V \underset{1-1}{⟶} B \land (a \in V \land b \in V)) \to (F (a) = F (b) \leftrightarrow a = b)$
53	51 52	sylan	$⊢ (φ \land (a \in V \land b \in V)) \to (F (a) = F (b) \leftrightarrow a = b)$
54	48 49 53	3bitr4d	$⊢ (φ \land (a \in V \land b \in V)) \to (F (a) D F (b) = 0 \leftrightarrow F (a) = F (b))$
55	16	adantr	$⊢ ((φ \land (a \in V \land b \in V)) \land c \in V) \to E \in ∞Met (V)$
56		simpr	$⊢ ((φ \land (a \in V \land b \in V)) \land c \in V) \to c \in V$
57	17	adantr	$⊢ ((φ \land (a \in V \land b \in V)) \land c \in V) \to a \in V$
58	18	adantr	$⊢ ((φ \land (a \in V \land b \in V)) \land c \in V) \to b \in V$
59		xmettri2	$⊢ (E \in ∞Met (V) \land (c \in V \land a \in V \land b \in V)) \to a E b \leq (c E a) +_{𝑒} (c E b)$
60	55 56 57 58 59	syl13anc	$⊢ ((φ \land (a \in V \land b \in V)) \land c \in V) \to a E b \leq (c E a) +_{𝑒} (c E b)$
61	19	adantr	$⊢ ((φ \land (a \in V \land b \in V)) \land c \in V) \to F (a) D F (b) = a E b$
62	12	adantr	$⊢ ((φ \land (a \in V \land b \in V)) \land c \in V) \to U = F “_{𝑠} R$
63	13	adantr	$⊢ ((φ \land (a \in V \land b \in V)) \land c \in V) \to V = {Base}_{R}$
64	14	adantr	$⊢ ((φ \land (a \in V \land b \in V)) \land c \in V) \to F : V \underset{1-1 onto}{⟶} B$
65	15	adantr	$⊢ ((φ \land (a \in V \land b \in V)) \land c \in V) \to R \in Z$
66	62 63 64 65 5 6 55 56 57	imasdsf1o	$⊢ ((φ \land (a \in V \land b \in V)) \land c \in V) \to F (c) D F (a) = c E a$
67	62 63 64 65 5 6 55 56 58	imasdsf1o	$⊢ ((φ \land (a \in V \land b \in V)) \land c \in V) \to F (c) D F (b) = c E b$
68	66 67	oveq12d	$⊢ ((φ \land (a \in V \land b \in V)) \land c \in V) \to (F (c) D F (a)) +_{𝑒} (F (c) D F (b)) = (c E a) +_{𝑒} (c E b)$
69	60 61 68	3brtr4d	$⊢ ((φ \land (a \in V \land b \in V)) \land c \in V) \to F (a) D F (b) \leq (F (c) D F (a)) +_{𝑒} (F (c) D F (b))$
70	69	ralrimiva	$⊢ (φ \land (a \in V \land b \in V)) \to \forall c \in V F (a) D F (b) \leq (F (c) D F (a)) +_{𝑒} (F (c) D F (b))$
71		oveq1	$⊢ z = F (c) \to z D F (a) = F (c) D F (a)$
72		oveq1	$⊢ z = F (c) \to z D F (b) = F (c) D F (b)$
73	71 72	oveq12d	$⊢ z = F (c) \to (z D F (a)) +_{𝑒} (z D F (b)) = (F (c) D F (a)) +_{𝑒} (F (c) D F (b))$
74	73	breq2d	$⊢ z = F (c) \to (F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b)) \leftrightarrow F (a) D F (b) \leq (F (c) D F (a)) +_{𝑒} (F (c) D F (b)))$
75	74	ralrn	$⊢ F Fn V \to (\forall z \in ran F F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b)) \leftrightarrow \forall c \in V F (a) D F (b) \leq (F (c) D F (a)) +_{𝑒} (F (c) D F (b)))$
76	26 75	syl	$⊢ φ \to (\forall z \in ran F F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b)) \leftrightarrow \forall c \in V F (a) D F (b) \leq (F (c) D F (a)) +_{𝑒} (F (c) D F (b)))$
77	32	raleqdv	$⊢ φ \to (\forall z \in ran F F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b)) \leftrightarrow \forall z \in B F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b)))$
78	76 77	bitr3d	$⊢ φ \to (\forall c \in V F (a) D F (b) \leq (F (c) D F (a)) +_{𝑒} (F (c) D F (b)) \leftrightarrow \forall z \in B F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b)))$
79	78	adantr	$⊢ (φ \land (a \in V \land b \in V)) \to (\forall c \in V F (a) D F (b) \leq (F (c) D F (a)) +_{𝑒} (F (c) D F (b)) \leftrightarrow \forall z \in B F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b)))$
80	70 79	mpbid	$⊢ (φ \land (a \in V \land b \in V)) \to \forall z \in B F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b))$
81	54 80	jca	$⊢ (φ \land (a \in V \land b \in V)) \to ((F (a) D F (b) = 0 \leftrightarrow F (a) = F (b)) \land \forall z \in B F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b)))$
82	81	ralrimivva	$⊢ φ \to \forall a \in V \forall b \in V ((F (a) D F (b) = 0 \leftrightarrow F (a) = F (b)) \land \forall z \in B F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b)))$
83	27	eqeq1d	$⊢ y = F (b) \to (F (a) D y = 0 \leftrightarrow F (a) D F (b) = 0)$
84		eqeq2	$⊢ y = F (b) \to (F (a) = y \leftrightarrow F (a) = F (b))$
85	83 84	bibi12d	$⊢ y = F (b) \to ((F (a) D y = 0 \leftrightarrow F (a) = y) \leftrightarrow (F (a) D F (b) = 0 \leftrightarrow F (a) = F (b)))$
86		oveq2	$⊢ y = F (b) \to z D y = z D F (b)$
87	86	oveq2d	$⊢ y = F (b) \to (z D F (a)) +_{𝑒} (z D y) = (z D F (a)) +_{𝑒} (z D F (b))$
88	27 87	breq12d	$⊢ y = F (b) \to (F (a) D y \leq (z D F (a)) +_{𝑒} (z D y) \leftrightarrow F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b)))$
89	88	ralbidv	$⊢ y = F (b) \to (\forall z \in B F (a) D y \leq (z D F (a)) +_{𝑒} (z D y) \leftrightarrow \forall z \in B F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b)))$
90	85 89	anbi12d	$⊢ y = F (b) \to (((F (a) D y = 0 \leftrightarrow F (a) = y) \land \forall z \in B F (a) D y \leq (z D F (a)) +_{𝑒} (z D y)) \leftrightarrow ((F (a) D F (b) = 0 \leftrightarrow F (a) = F (b)) \land \forall z \in B F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b))))$
91	90	ralrn	$⊢ F Fn V \to (\forall y \in ran F ((F (a) D y = 0 \leftrightarrow F (a) = y) \land \forall z \in B F (a) D y \leq (z D F (a)) +_{𝑒} (z D y)) \leftrightarrow \forall b \in V ((F (a) D F (b) = 0 \leftrightarrow F (a) = F (b)) \land \forall z \in B F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b))))$
92	26 91	syl	$⊢ φ \to (\forall y \in ran F ((F (a) D y = 0 \leftrightarrow F (a) = y) \land \forall z \in B F (a) D y \leq (z D F (a)) +_{𝑒} (z D y)) \leftrightarrow \forall b \in V ((F (a) D F (b) = 0 \leftrightarrow F (a) = F (b)) \land \forall z \in B F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b))))$
93	32	raleqdv	$⊢ φ \to (\forall y \in ran F ((F (a) D y = 0 \leftrightarrow F (a) = y) \land \forall z \in B F (a) D y \leq (z D F (a)) +_{𝑒} (z D y)) \leftrightarrow \forall y \in B ((F (a) D y = 0 \leftrightarrow F (a) = y) \land \forall z \in B F (a) D y \leq (z D F (a)) +_{𝑒} (z D y)))$
94	92 93	bitr3d	$⊢ φ \to (\forall b \in V ((F (a) D F (b) = 0 \leftrightarrow F (a) = F (b)) \land \forall z \in B F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b))) \leftrightarrow \forall y \in B ((F (a) D y = 0 \leftrightarrow F (a) = y) \land \forall z \in B F (a) D y \leq (z D F (a)) +_{𝑒} (z D y)))$
95	94	ralbidv	$⊢ φ \to (\forall a \in V \forall b \in V ((F (a) D F (b) = 0 \leftrightarrow F (a) = F (b)) \land \forall z \in B F (a) D F (b) \leq (z D F (a)) +_{𝑒} (z D F (b))) \leftrightarrow \forall a \in V \forall y \in B ((F (a) D y = 0 \leftrightarrow F (a) = y) \land \forall z \in B F (a) D y \leq (z D F (a)) +_{𝑒} (z D y)))$
96	82 95	mpbid	$⊢ φ \to \forall a \in V \forall y \in B ((F (a) D y = 0 \leftrightarrow F (a) = y) \land \forall z \in B F (a) D y \leq (z D F (a)) +_{𝑒} (z D y))$
97	37	eqeq1d	$⊢ x = F (a) \to (x D y = 0 \leftrightarrow F (a) D y = 0)$
98		eqeq1	$⊢ x = F (a) \to (x = y \leftrightarrow F (a) = y)$
99	97 98	bibi12d	$⊢ x = F (a) \to ((x D y = 0 \leftrightarrow x = y) \leftrightarrow (F (a) D y = 0 \leftrightarrow F (a) = y))$
100		oveq2	$⊢ x = F (a) \to z D x = z D F (a)$
101	100	oveq1d	$⊢ x = F (a) \to (z D x) +_{𝑒} (z D y) = (z D F (a)) +_{𝑒} (z D y)$
102	37 101	breq12d	$⊢ x = F (a) \to (x D y \leq (z D x) +_{𝑒} (z D y) \leftrightarrow F (a) D y \leq (z D F (a)) +_{𝑒} (z D y))$
103	102	ralbidv	$⊢ x = F (a) \to (\forall z \in B x D y \leq (z D x) +_{𝑒} (z D y) \leftrightarrow \forall z \in B F (a) D y \leq (z D F (a)) +_{𝑒} (z D y))$
104	99 103	anbi12d	$⊢ x = F (a) \to (((x D y = 0 \leftrightarrow x = y) \land \forall z \in B x D y \leq (z D x) +_{𝑒} (z D y)) \leftrightarrow ((F (a) D y = 0 \leftrightarrow F (a) = y) \land \forall z \in B F (a) D y \leq (z D F (a)) +_{𝑒} (z D y)))$
105	104	ralbidv	$⊢ x = F (a) \to (\forall y \in B ((x D y = 0 \leftrightarrow x = y) \land \forall z \in B x D y \leq (z D x) +_{𝑒} (z D y)) \leftrightarrow \forall y \in B ((F (a) D y = 0 \leftrightarrow F (a) = y) \land \forall z \in B F (a) D y \leq (z D F (a)) +_{𝑒} (z D y)))$
106	105	ralrn	$⊢ F Fn V \to (\forall x \in ran F \forall y \in B ((x D y = 0 \leftrightarrow x = y) \land \forall z \in B x D y \leq (z D x) +_{𝑒} (z D y)) \leftrightarrow \forall a \in V \forall y \in B ((F (a) D y = 0 \leftrightarrow F (a) = y) \land \forall z \in B F (a) D y \leq (z D F (a)) +_{𝑒} (z D y)))$
107	26 106	syl	$⊢ φ \to (\forall x \in ran F \forall y \in B ((x D y = 0 \leftrightarrow x = y) \land \forall z \in B x D y \leq (z D x) +_{𝑒} (z D y)) \leftrightarrow \forall a \in V \forall y \in B ((F (a) D y = 0 \leftrightarrow F (a) = y) \land \forall z \in B F (a) D y \leq (z D F (a)) +_{𝑒} (z D y)))$
108	32	raleqdv	$⊢ φ \to (\forall x \in ran F \forall y \in B ((x D y = 0 \leftrightarrow x = y) \land \forall z \in B x D y \leq (z D x) +_{𝑒} (z D y)) \leftrightarrow \forall x \in B \forall y \in B ((x D y = 0 \leftrightarrow x = y) \land \forall z \in B x D y \leq (z D x) +_{𝑒} (z D y)))$
109	107 108	bitr3d	$⊢ φ \to (\forall a \in V \forall y \in B ((F (a) D y = 0 \leftrightarrow F (a) = y) \land \forall z \in B F (a) D y \leq (z D F (a)) +_{𝑒} (z D y)) \leftrightarrow \forall x \in B \forall y \in B ((x D y = 0 \leftrightarrow x = y) \land \forall z \in B x D y \leq (z D x) +_{𝑒} (z D y)))$
110	96 109	mpbid	$⊢ φ \to \forall x \in B \forall y \in B ((x D y = 0 \leftrightarrow x = y) \land \forall z \in B x D y \leq (z D x) +_{𝑒} (z D y))$
111	7	elfvexd	$⊢ φ \to V \in V$
112		focdmex	$⊢ V \in V \to (F : V \underset{onto}{⟶} B \to B \in V)$
113	111 9 112	sylc	$⊢ φ \to B \in V$
114		isxmet	$⊢ B \in V \to (D \in ∞Met (B) \leftrightarrow (D : B \times B ⟶ ℝ^{*} \land \forall x \in B \forall y \in B ((x D y = 0 \leftrightarrow x = y) \land \forall z \in B x D y \leq (z D x) +_{𝑒} (z D y))))$
115	113 114	syl	$⊢ φ \to (D \in ∞Met (B) \leftrightarrow (D : B \times B ⟶ ℝ^{*} \land \forall x \in B \forall y \in B ((x D y = 0 \leftrightarrow x = y) \land \forall z \in B x D y \leq (z D x) +_{𝑒} (z D y))))$
116	46 110 115	mpbir2and	$⊢ φ \to D \in ∞Met (B)$

Metamath Proof Explorer

Theorem imasf1oxmet

Proof