Theorem imasf1omet

Description: The image of a metric is a metric. (Contributed by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Hypotheses	imasf1oxmet.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
	imasf1oxmet.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
	imasf1oxmet.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
	imasf1oxmet.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
	imasf1oxmet.e	⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
	imasf1oxmet.d	⊢ 𝐷 = ( dist ‘ 𝑈 )
	imasf1omet.m	⊢ ( 𝜑 → 𝐸 ∈ ( Met ‘ 𝑉 ) )
Assertion	imasf1omet	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		imasf1oxmet.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2		imasf1oxmet.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3		imasf1oxmet.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
4		imasf1oxmet.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5		imasf1oxmet.e	⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
6		imasf1oxmet.d	⊢ 𝐷 = ( dist ‘ 𝑈 )
7		imasf1omet.m	⊢ ( 𝜑 → 𝐸 ∈ ( Met ‘ 𝑉 ) )
8		metxmet	⊢ ( 𝐸 ∈ ( Met ‘ 𝑉 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
9	7 8	syl	⊢ ( 𝜑 → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
10	1 2 3 4 5 6 9	imasf1oxmet	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )
11		f1ofo	⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 : 𝑉 –onto→ 𝐵 )
12	3 11	syl	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
13		eqid	⊢ ( dist ‘ 𝑅 ) = ( dist ‘ 𝑅 )
14	1 2 12 4 13 6	imasdsfn	⊢ ( 𝜑 → 𝐷 Fn ( 𝐵 × 𝐵 ) )
15	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑈 = ( 𝐹 “s 𝑅 ) )
16	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑉 = ( Base ‘ 𝑅 ) )
17	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
18	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑅 ∈ 𝑍 )
19	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
20		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑎 ∈ 𝑉 )
21		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑏 ∈ 𝑉 )
22	15 16 17 18 5 6 19 20 21	imasdsf1o	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 𝐸 𝑏 ) )
23		metcl	⊢ ( ( 𝐸 ∈ ( Met ‘ 𝑉 ) ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑎 𝐸 𝑏 ) ∈ ℝ )
24	23	3expb	⊢ ( ( 𝐸 ∈ ( Met ‘ 𝑉 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( 𝑎 𝐸 𝑏 ) ∈ ℝ )
25	7 24	sylan	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( 𝑎 𝐸 𝑏 ) ∈ ℝ )
26	22 25	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ )
27	26	ralrimivva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ )
28		f1ofn	⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 Fn 𝑉 )
29	3 28	syl	⊢ ( 𝜑 → 𝐹 Fn 𝑉 )
30		oveq2	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) )
31	30	eleq1d	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ↔ ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ ) )
32	31	ralrn	⊢ ( 𝐹 Fn 𝑉 → ( ∀ 𝑦 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ↔ ∀ 𝑏 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ ) )
33	29 32	syl	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ↔ ∀ 𝑏 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ ) )
34		forn	⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
35	12 34	syl	⊢ ( 𝜑 → ran 𝐹 = 𝐵 )
36	35	raleqdv	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ) )
37	33 36	bitr3d	⊢ ( 𝜑 → ( ∀ 𝑏 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ) )
38	37	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ) )
39	27 38	mpbid	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ )
40		oveq1	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( 𝑥 𝐷 𝑦 ) = ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) )
41	40	eleq1d	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ ↔ ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ) )
42	41	ralbidv	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ) )
43	42	ralrn	⊢ ( 𝐹 Fn 𝑉 → ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ) )
44	29 43	syl	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ) )
45	35	raleqdv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ ) )
46	44 45	bitr3d	⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ ) )
47	39 46	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ )
48		ffnov	⊢ ( 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ℝ ↔ ( 𝐷 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ ) )
49	14 47 48	sylanbrc	⊢ ( 𝜑 → 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ℝ )
50		ismet2	⊢ ( 𝐷 ∈ ( Met ‘ 𝐵 ) ↔ ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ℝ ) )
51	10 49 50	sylanbrc	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝐵 ) )