imasf1omet

Description: The image of a metric is a metric. (Contributed by Mario Carneiro, 21-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)$
	imasf1omet.m	$⊢ φ \to E \in Met (V)$
Assertion	imasf1omet	$⊢ φ \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		imasf1omet.m	$⊢ φ \to E \in Met (V)$
8		metxmet	$⊢ E \in Met (V) \to E \in ∞Met (V)$
9	7 8	syl	$⊢ φ \to E \in ∞Met (V)$
10	1 2 3 4 5 6 9	imasf1oxmet	$⊢ φ \to D \in ∞Met (B)$
11		f1ofo	$⊢ F : V \underset{1-1 onto}{⟶} B \to F : V \underset{onto}{⟶} B$
12	3 11	syl	$⊢ φ \to F : V \underset{onto}{⟶} B$
13		eqid	$⊢ dist (R) = dist (R)$
14	1 2 12 4 13 6	imasdsfn	$⊢ φ \to D Fn (B \times B)$
15	1	adantr	$⊢ (φ \land (a \in V \land b \in V)) \to U = F “_{𝑠} R$
16	2	adantr	$⊢ (φ \land (a \in V \land b \in V)) \to V = {Base}_{R}$
17	3	adantr	$⊢ (φ \land (a \in V \land b \in V)) \to F : V \underset{1-1 onto}{⟶} B$
18	4	adantr	$⊢ (φ \land (a \in V \land b \in V)) \to R \in Z$
19	9	adantr	$⊢ (φ \land (a \in V \land b \in V)) \to E \in ∞Met (V)$
20		simprl	$⊢ (φ \land (a \in V \land b \in V)) \to a \in V$
21		simprr	$⊢ (φ \land (a \in V \land b \in V)) \to b \in V$
22	15 16 17 18 5 6 19 20 21	imasdsf1o	$⊢ (φ \land (a \in V \land b \in V)) \to F (a) D F (b) = a E b$
23		metcl	$⊢ (E \in Met (V) \land a \in V \land b \in V) \to a E b \in ℝ$
24	23	3expb	$⊢ (E \in Met (V) \land (a \in V \land b \in V)) \to a E b \in ℝ$
25	7 24	sylan	$⊢ (φ \land (a \in V \land b \in V)) \to a E b \in ℝ$
26	22 25	eqeltrd	$⊢ (φ \land (a \in V \land b \in V)) \to F (a) D F (b) \in ℝ$
27	26	ralrimivva	$⊢ φ \to \forall a \in V \forall b \in V F (a) D F (b) \in ℝ$
28		f1ofn	$⊢ F : V \underset{1-1 onto}{⟶} B \to F Fn V$
29	3 28	syl	$⊢ φ \to F Fn V$
30		oveq2	$⊢ y = F (b) \to F (a) D y = F (a) D F (b)$
31	30	eleq1d	$⊢ y = F (b) \to (F (a) D y \in ℝ \leftrightarrow F (a) D F (b) \in ℝ)$
32	31	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 ℝ)$
33	29 32	syl	$⊢ φ \to (\forall y \in ran F F (a) D y \in ℝ \leftrightarrow \forall b \in V F (a) D F (b) \in ℝ)$
34		forn	$⊢ F : V \underset{onto}{⟶} B \to ran F = B$
35	12 34	syl	$⊢ φ \to ran F = B$
36	35	raleqdv	$⊢ φ \to (\forall y \in ran F F (a) D y \in ℝ \leftrightarrow \forall y \in B F (a) D y \in ℝ)$
37	33 36	bitr3d	$⊢ φ \to (\forall b \in V F (a) D F (b) \in ℝ \leftrightarrow \forall y \in B F (a) D y \in ℝ)$
38	37	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 ℝ)$
39	27 38	mpbid	$⊢ φ \to \forall a \in V \forall y \in B F (a) D y \in ℝ$
40		oveq1	$⊢ x = F (a) \to x D y = F (a) D y$
41	40	eleq1d	$⊢ x = F (a) \to (x D y \in ℝ \leftrightarrow F (a) D y \in ℝ)$
42	41	ralbidv	$⊢ x = F (a) \to (\forall y \in B x D y \in ℝ \leftrightarrow \forall y \in B F (a) D y \in ℝ)$
43	42	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 ℝ)$
44	29 43	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 ℝ)$
45	35	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 ℝ)$
46	44 45	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 ℝ)$
47	39 46	mpbid	$⊢ φ \to \forall x \in B \forall y \in B x D y \in ℝ$
48		ffnov	$⊢ D : B \times B ⟶ ℝ \leftrightarrow (D Fn (B \times B) \land \forall x \in B \forall y \in B x D y \in ℝ)$
49	14 47 48	sylanbrc	$⊢ φ \to D : B \times B ⟶ ℝ$
50		ismet2	$⊢ D \in Met (B) \leftrightarrow (D \in ∞Met (B) \land D : B \times B ⟶ ℝ)$
51	10 49 50	sylanbrc	$⊢ φ \to D \in Met (B)$

Metamath Proof Explorer

Theorem imasf1omet

Proof