pstmxmet - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > pstmxmet		Structured version Visualization version GIF version

Theorem pstmxmet 33332

Description: The metric induced by a pseudometric is a full-fledged metric on the equivalence classes of the metric identification. (Contributed by Thierry Arnoux, 11-Feb-2018.)

**Hypothesis**
Ref	Expression
pstmval.1	⊢ ∼ = (~_Met‘𝐷)

**Assertion**
Ref	Expression
pstmxmet	⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) ∈ (∞Met‘(𝑋 / ∼ )))

Proof of Theorem pstmxmet Dummy variables 𝑎 𝑏 𝑐 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2724	. . . . 5 ⊢ (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧 ∣ ∃𝑎 ∈ 𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)}) = (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧 ∣ ∃𝑎 ∈ 𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)})
2		vex 3470	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3470	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	ab2rexex 7959	. . . . . 6 ⊢ {𝑧 ∣ ∃𝑎 ∈ 𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)} ∈ V
5	4	uniex 7724	. . . . 5 ⊢ ∪ {𝑧 ∣ ∃𝑎 ∈ 𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)} ∈ V
6	1, 5	fnmpoi 8049	. . . 4 ⊢ (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧 ∣ ∃𝑎 ∈ 𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)}) Fn ((𝑋 / ∼ ) × (𝑋 / ∼ ))
7		pstmval.1	. . . . . 6 ⊢ ∼ = (~_Met‘𝐷)
8	7	pstmval 33330	. . . . 5 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) = (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧 ∣ ∃𝑎 ∈ 𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)}))
9	8	fneq1d 6632	. . . 4 ⊢ (𝐷 ∈ (PsMet‘𝑋) → ((pstoMet‘𝐷) Fn ((𝑋 / ∼ ) × (𝑋 / ∼ )) ↔ (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧 ∣ ∃𝑎 ∈ 𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)}) Fn ((𝑋 / ∼ ) × (𝑋 / ∼ ))))
10	6, 9	mpbiri 258	. . 3 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) Fn ((𝑋 / ∼ ) × (𝑋 / ∼ )))
11		simpllr 773	. . . . . . . . 9 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → 𝑥 = [𝑎] ∼ )
12		simpr 484	. . . . . . . . 9 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → 𝑦 = [𝑏] ∼ )
13	11, 12	oveq12d 7419	. . . . . . . 8 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → (𝑥(pstoMet‘𝐷)𝑦) = ([𝑎] ∼ (pstoMet‘𝐷)[𝑏] ∼ ))
14		simp-5l 782	. . . . . . . . 9 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → 𝐷 ∈ (PsMet‘𝑋))
15		simp-4r 781	. . . . . . . . 9 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → 𝑎 ∈ 𝑋)
16		simplr 766	. . . . . . . . 9 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → 𝑏 ∈ 𝑋)
17	7	pstmfval 33331	. . . . . . . . 9 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ([𝑎] ∼ (pstoMet‘𝐷)[𝑏] ∼ ) = (𝑎𝐷𝑏))
18	14, 15, 16, 17	syl3anc 1368	. . . . . . . 8 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → ([𝑎] ∼ (pstoMet‘𝐷)[𝑏] ∼ ) = (𝑎𝐷𝑏))
19	13, 18	eqtrd 2764	. . . . . . 7 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → (𝑥(pstoMet‘𝐷)𝑦) = (𝑎𝐷𝑏))
20		psmetf 24122	. . . . . . . . 9 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ^*)
21	14, 20	syl 17	. . . . . . . 8 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → 𝐷:(𝑋 × 𝑋)⟶ℝ^*)
22	21, 15, 16	fovcdmd 7572	. . . . . . 7 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → (𝑎𝐷𝑏) ∈ ℝ^*)
23	19, 22	eqeltrd 2825	. . . . . 6 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → (𝑥(pstoMet‘𝐷)𝑦) ∈ ℝ^*)
24		elqsi 8759	. . . . . . . 8 ⊢ (𝑦 ∈ (𝑋 / ∼ ) → ∃𝑏 ∈ 𝑋 𝑦 = [𝑏] ∼ )
25	24	ad2antll 726	. . . . . . 7 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) → ∃𝑏 ∈ 𝑋 𝑦 = [𝑏] ∼ )
26	25	ad2antrr 723	. . . . . 6 ⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) → ∃𝑏 ∈ 𝑋 𝑦 = [𝑏] ∼ )
27	23, 26	r19.29a 3154	. . . . 5 ⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) → (𝑥(pstoMet‘𝐷)𝑦) ∈ ℝ^*)
28		elqsi 8759	. . . . . 6 ⊢ (𝑥 ∈ (𝑋 / ∼ ) → ∃𝑎 ∈ 𝑋 𝑥 = [𝑎] ∼ )
29	28	ad2antrl 725	. . . . 5 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) → ∃𝑎 ∈ 𝑋 𝑥 = [𝑎] ∼ )
30	27, 29	r19.29a 3154	. . . 4 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) → (𝑥(pstoMet‘𝐷)𝑦) ∈ ℝ^*)
31	30	ralrimivva 3192	. . 3 ⊢ (𝐷 ∈ (PsMet‘𝑋) → ∀𝑥 ∈ (𝑋 / ∼ )∀𝑦 ∈ (𝑋 / ∼ )(𝑥(pstoMet‘𝐷)𝑦) ∈ ℝ^*)
32		ffnov 7527	. . 3 ⊢ ((pstoMet‘𝐷):((𝑋 / ∼ ) × (𝑋 / ∼ ))⟶ℝ^* ↔ ((pstoMet‘𝐷) Fn ((𝑋 / ∼ ) × (𝑋 / ∼ )) ∧ ∀𝑥 ∈ (𝑋 / ∼ )∀𝑦 ∈ (𝑋 / ∼ )(𝑥(pstoMet‘𝐷)𝑦) ∈ ℝ^*))
33	10, 31, 32	sylanbrc 582	. 2 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷):((𝑋 / ∼ ) × (𝑋 / ∼ ))⟶ℝ^*)
34	17	3expa 1115	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑏 ∈ 𝑋) → ([𝑎] ∼ (pstoMet‘𝐷)[𝑏] ∼ ) = (𝑎𝐷𝑏))
35	34	eqeq1d 2726	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑏 ∈ 𝑋) → (([𝑎] ∼ (pstoMet‘𝐷)[𝑏] ∼ ) = 0 ↔ (𝑎𝐷𝑏) = 0))
36	7	breqi 5144	. . . . . . . . . . . 12 ⊢ (𝑎 ∼ 𝑏 ↔ 𝑎(~_Met‘𝐷)𝑏)
37		metidv 33327	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎(~_Met‘𝐷)𝑏 ↔ (𝑎𝐷𝑏) = 0))
38	37	anassrs 467	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑏 ∈ 𝑋) → (𝑎(~_Met‘𝐷)𝑏 ↔ (𝑎𝐷𝑏) = 0))
39	36, 38	bitrid 283	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑏 ∈ 𝑋) → (𝑎 ∼ 𝑏 ↔ (𝑎𝐷𝑏) = 0))
40		metider 33329	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (~_Met‘𝐷) Er 𝑋)
41	40	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑏 ∈ 𝑋) → (~_Met‘𝐷) Er 𝑋)
42		ereq1 8705	. . . . . . . . . . . . . 14 ⊢ ( ∼ = (~_Met‘𝐷) → ( ∼ Er 𝑋 ↔ (~_Met‘𝐷) Er 𝑋))
43	7, 42	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ( ∼ Er 𝑋 ↔ (~_Met‘𝐷) Er 𝑋)
44	41, 43	sylibr 233	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑏 ∈ 𝑋) → ∼ Er 𝑋)
45		simplr 766	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑏 ∈ 𝑋) → 𝑎 ∈ 𝑋)
46	44, 45	erth 8747	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑏 ∈ 𝑋) → (𝑎 ∼ 𝑏 ↔ [𝑎] ∼ = [𝑏] ∼ ))
47	35, 39, 46	3bitr2d 307	. . . . . . . . . 10 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑏 ∈ 𝑋) → (([𝑎] ∼ (pstoMet‘𝐷)[𝑏] ∼ ) = 0 ↔ [𝑎] ∼ = [𝑏] ∼ ))
48	47	adantllr 716	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑏 ∈ 𝑋) → (([𝑎] ∼ (pstoMet‘𝐷)[𝑏] ∼ ) = 0 ↔ [𝑎] ∼ = [𝑏] ∼ ))
49	48	adantlr 712	. . . . . . . 8 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) → (([𝑎] ∼ (pstoMet‘𝐷)[𝑏] ∼ ) = 0 ↔ [𝑎] ∼ = [𝑏] ∼ ))
50	49	adantr 480	. . . . . . 7 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → (([𝑎] ∼ (pstoMet‘𝐷)[𝑏] ∼ ) = 0 ↔ [𝑎] ∼ = [𝑏] ∼ ))
51	13	eqeq1d 2726	. . . . . . 7 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → ((𝑥(pstoMet‘𝐷)𝑦) = 0 ↔ ([𝑎] ∼ (pstoMet‘𝐷)[𝑏] ∼ ) = 0))
52	11, 12	eqeq12d 2740	. . . . . . 7 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → (𝑥 = 𝑦 ↔ [𝑎] ∼ = [𝑏] ∼ ))
53	50, 51, 52	3bitr4d 311	. . . . . 6 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → ((𝑥(pstoMet‘𝐷)𝑦) = 0 ↔ 𝑥 = 𝑦))
54	53, 26	r19.29a 3154	. . . . 5 ⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) → ((𝑥(pstoMet‘𝐷)𝑦) = 0 ↔ 𝑥 = 𝑦))
55	54, 29	r19.29a 3154	. . . 4 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) → ((𝑥(pstoMet‘𝐷)𝑦) = 0 ↔ 𝑥 = 𝑦))
56		simp-6l 784	. . . . . . . . . . . . . 14 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → 𝐷 ∈ (PsMet‘𝑋))
57		simplr 766	. . . . . . . . . . . . . 14 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → 𝑐 ∈ 𝑋)
58		simp-6r 785	. . . . . . . . . . . . . 14 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → 𝑎 ∈ 𝑋)
59		simp-4r 781	. . . . . . . . . . . . . 14 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → 𝑏 ∈ 𝑋)
60		psmettri2 24125	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +_𝑒 (𝑐𝐷𝑏)))
61	56, 57, 58, 59, 60	syl13anc 1369	. . . . . . . . . . . . 13 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +_𝑒 (𝑐𝐷𝑏)))
62		simp-5r 783	. . . . . . . . . . . . . . 15 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → 𝑥 = [𝑎] ∼ )
63		simpllr 773	. . . . . . . . . . . . . . 15 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → 𝑦 = [𝑏] ∼ )
64	62, 63	oveq12d 7419	. . . . . . . . . . . . . 14 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → (𝑥(pstoMet‘𝐷)𝑦) = ([𝑎] ∼ (pstoMet‘𝐷)[𝑏] ∼ ))
65	56, 58, 59, 17	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → ([𝑎] ∼ (pstoMet‘𝐷)[𝑏] ∼ ) = (𝑎𝐷𝑏))
66	64, 65	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → (𝑥(pstoMet‘𝐷)𝑦) = (𝑎𝐷𝑏))
67		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → 𝑧 = [𝑐] ∼ )
68	67, 62	oveq12d 7419	. . . . . . . . . . . . . . 15 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → (𝑧(pstoMet‘𝐷)𝑥) = ([𝑐] ∼ (pstoMet‘𝐷)[𝑎] ∼ ))
69	7	pstmfval 33331	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋) → ([𝑐] ∼ (pstoMet‘𝐷)[𝑎] ∼ ) = (𝑐𝐷𝑎))
70	56, 57, 58, 69	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → ([𝑐] ∼ (pstoMet‘𝐷)[𝑎] ∼ ) = (𝑐𝐷𝑎))
71	68, 70	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → (𝑧(pstoMet‘𝐷)𝑥) = (𝑐𝐷𝑎))
72	67, 63	oveq12d 7419	. . . . . . . . . . . . . . 15 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → (𝑧(pstoMet‘𝐷)𝑦) = ([𝑐] ∼ (pstoMet‘𝐷)[𝑏] ∼ ))
73	7	pstmfval 33331	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑐 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ([𝑐] ∼ (pstoMet‘𝐷)[𝑏] ∼ ) = (𝑐𝐷𝑏))
74	56, 57, 59, 73	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → ([𝑐] ∼ (pstoMet‘𝐷)[𝑏] ∼ ) = (𝑐𝐷𝑏))
75	72, 74	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → (𝑧(pstoMet‘𝐷)𝑦) = (𝑐𝐷𝑏))
76	71, 75	oveq12d 7419	. . . . . . . . . . . . 13 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → ((𝑧(pstoMet‘𝐷)𝑥) +_𝑒 (𝑧(pstoMet‘𝐷)𝑦)) = ((𝑐𝐷𝑎) +_𝑒 (𝑐𝐷𝑏)))
77	61, 66, 76	3brtr4d 5170	. . . . . . . . . . . 12 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → (𝑥(pstoMet‘𝐷)𝑦) ≤ ((𝑧(pstoMet‘𝐷)𝑥) +_𝑒 (𝑧(pstoMet‘𝐷)𝑦)))
78	77	adantl6r 761	. . . . . . . . . . 11 ⊢ ((((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑧 ∈ (𝑋 / ∼ )) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) ∧ 𝑐 ∈ 𝑋) ∧ 𝑧 = [𝑐] ∼ ) → (𝑥(pstoMet‘𝐷)𝑦) ≤ ((𝑧(pstoMet‘𝐷)𝑥) +_𝑒 (𝑧(pstoMet‘𝐷)𝑦)))
79		elqsi 8759	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝑋 / ∼ ) → ∃𝑐 ∈ 𝑋 𝑧 = [𝑐] ∼ )
80	79	ad5antlr 732	. . . . . . . . . . 11 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑧 ∈ (𝑋 / ∼ )) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → ∃𝑐 ∈ 𝑋 𝑧 = [𝑐] ∼ )
81	78, 80	r19.29a 3154	. . . . . . . . . 10 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑧 ∈ (𝑋 / ∼ )) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → (𝑥(pstoMet‘𝐷)𝑦) ≤ ((𝑧(pstoMet‘𝐷)𝑥) +_𝑒 (𝑧(pstoMet‘𝐷)𝑦)))
82	81	adantl5r 760	. . . . . . . . 9 ⊢ (((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑦 ∈ (𝑋 / ∼ )) ∧ 𝑧 ∈ (𝑋 / ∼ )) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) ∧ 𝑏 ∈ 𝑋) ∧ 𝑦 = [𝑏] ∼ ) → (𝑥(pstoMet‘𝐷)𝑦) ≤ ((𝑧(pstoMet‘𝐷)𝑥) +_𝑒 (𝑧(pstoMet‘𝐷)𝑦)))
83	24	ad4antlr 730	. . . . . . . . 9 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑦 ∈ (𝑋 / ∼ )) ∧ 𝑧 ∈ (𝑋 / ∼ )) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) → ∃𝑏 ∈ 𝑋 𝑦 = [𝑏] ∼ )
84	82, 83	r19.29a 3154	. . . . . . . 8 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑦 ∈ (𝑋 / ∼ )) ∧ 𝑧 ∈ (𝑋 / ∼ )) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) → (𝑥(pstoMet‘𝐷)𝑦) ≤ ((𝑧(pstoMet‘𝐷)𝑥) +_𝑒 (𝑧(pstoMet‘𝐷)𝑦)))
85	84	adantl4r 752	. . . . . . 7 ⊢ ((((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ (𝑋 / ∼ )) ∧ 𝑦 ∈ (𝑋 / ∼ )) ∧ 𝑧 ∈ (𝑋 / ∼ )) ∧ 𝑎 ∈ 𝑋) ∧ 𝑥 = [𝑎] ∼ ) → (𝑥(pstoMet‘𝐷)𝑦) ≤ ((𝑧(pstoMet‘𝐷)𝑥) +_𝑒 (𝑧(pstoMet‘𝐷)𝑦)))
86	28	ad3antlr 728	. . . . . . 7 ⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ (𝑋 / ∼ )) ∧ 𝑦 ∈ (𝑋 / ∼ )) ∧ 𝑧 ∈ (𝑋 / ∼ )) → ∃𝑎 ∈ 𝑋 𝑥 = [𝑎] ∼ )
87	85, 86	r19.29a 3154	. . . . . 6 ⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ (𝑋 / ∼ )) ∧ 𝑦 ∈ (𝑋 / ∼ )) ∧ 𝑧 ∈ (𝑋 / ∼ )) → (𝑥(pstoMet‘𝐷)𝑦) ≤ ((𝑧(pstoMet‘𝐷)𝑥) +_𝑒 (𝑧(pstoMet‘𝐷)𝑦)))
88	87	ralrimiva 3138	. . . . 5 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ (𝑋 / ∼ )) ∧ 𝑦 ∈ (𝑋 / ∼ )) → ∀𝑧 ∈ (𝑋 / ∼ )(𝑥(pstoMet‘𝐷)𝑦) ≤ ((𝑧(pstoMet‘𝐷)𝑥) +_𝑒 (𝑧(pstoMet‘𝐷)𝑦)))
89	88	anasss 466	. . . 4 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) → ∀𝑧 ∈ (𝑋 / ∼ )(𝑥(pstoMet‘𝐷)𝑦) ≤ ((𝑧(pstoMet‘𝐷)𝑥) +_𝑒 (𝑧(pstoMet‘𝐷)𝑦)))
90	55, 89	jca 511	. . 3 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ (𝑋 / ∼ ) ∧ 𝑦 ∈ (𝑋 / ∼ ))) → (((𝑥(pstoMet‘𝐷)𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ (𝑋 / ∼ )(𝑥(pstoMet‘𝐷)𝑦) ≤ ((𝑧(pstoMet‘𝐷)𝑥) +_𝑒 (𝑧(pstoMet‘𝐷)𝑦))))
91	90	ralrimivva 3192	. 2 ⊢ (𝐷 ∈ (PsMet‘𝑋) → ∀𝑥 ∈ (𝑋 / ∼ )∀𝑦 ∈ (𝑋 / ∼ )(((𝑥(pstoMet‘𝐷)𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ (𝑋 / ∼ )(𝑥(pstoMet‘𝐷)𝑦) ≤ ((𝑧(pstoMet‘𝐷)𝑥) +_𝑒 (𝑧(pstoMet‘𝐷)𝑦))))
92		elfvex 6919	. . 3 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 ∈ V)
93		qsexg 8764	. . 3 ⊢ (𝑋 ∈ V → (𝑋 / ∼ ) ∈ V)
94		isxmet 24140	. . 3 ⊢ ((𝑋 / ∼ ) ∈ V → ((pstoMet‘𝐷) ∈ (∞Met‘(𝑋 / ∼ )) ↔ ((pstoMet‘𝐷):((𝑋 / ∼ ) × (𝑋 / ∼ ))⟶ℝ^* ∧ ∀𝑥 ∈ (𝑋 / ∼ )∀𝑦 ∈ (𝑋 / ∼ )(((𝑥(pstoMet‘𝐷)𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ (𝑋 / ∼ )(𝑥(pstoMet‘𝐷)𝑦) ≤ ((𝑧(pstoMet‘𝐷)𝑥) +_𝑒 (𝑧(pstoMet‘𝐷)𝑦))))))
95	92, 93, 94	3syl 18	. 2 ⊢ (𝐷 ∈ (PsMet‘𝑋) → ((pstoMet‘𝐷) ∈ (∞Met‘(𝑋 / ∼ )) ↔ ((pstoMet‘𝐷):((𝑋 / ∼ ) × (𝑋 / ∼ ))⟶ℝ^* ∧ ∀𝑥 ∈ (𝑋 / ∼ )∀𝑦 ∈ (𝑋 / ∼ )(((𝑥(pstoMet‘𝐷)𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ (𝑋 / ∼ )(𝑥(pstoMet‘𝐷)𝑦) ≤ ((𝑧(pstoMet‘𝐷)𝑥) +_𝑒 (𝑧(pstoMet‘𝐷)𝑦))))))
96	33, 91, 95	mpbir2and 710	1 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) ∈ (∞Met‘(𝑋 / ∼ )))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1533 ∈ wcel 2098 {cab 2701 ∀wral 3053 ∃wrex 3062 Vcvv 3466 ∪ cuni 4899 class class class wbr 5138 × cxp 5664 Fn wfn 6528 ⟶wf 6529 ‘cfv 6533 (class class class)co 7401 ∈ cmpo 7403 Er wer 8695 [cec 8696 / cqs 8697 0cc0 11105 ℝ^*cxr 11243 ≤ cle 11245 +_𝑒 cxad 13086 PsMetcpsmet 21207 ∞Metcxmet 21208 ~_Metcmetid 33321 pstoMetcpstm 33322

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-rep 5275 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7718 ax-cnex 11161 ax-resscn 11162 ax-1cn 11163 ax-icn 11164 ax-addcl 11165 ax-addrcl 11166 ax-mulcl 11167 ax-mulrcl 11168 ax-mulcom 11169 ax-addass 11170 ax-mulass 11171 ax-distr 11172 ax-i2m1 11173 ax-1ne0 11174 ax-1rid 11175 ax-rnegex 11176 ax-rrecex 11177 ax-cnre 11178 ax-pre-lttri 11179 ax-pre-lttrn 11180 ax-pre-ltadd 11181 ax-pre-mulgt0 11182

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-nel 3039 df-ral 3054 df-rex 3063 df-rmo 3368 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-iun 4989 df-br 5139 df-opab 5201 df-mpt 5222 df-id 5564 df-po 5578 df-so 5579 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7357 df-ov 7404 df-oprab 7405 df-mpo 7406 df-1st 7968 df-2nd 7969 df-er 8698 df-ec 8700 df-qs 8704 df-map 8817 df-en 8935 df-dom 8936 df-sdom 8937 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-div 11868 df-2 12271 df-rp 12971 df-xneg 13088 df-xadd 13089 df-xmul 13090 df-psmet 21215 df-xmet 21216 df-metid 33323 df-pstm 33324

This theorem is referenced by: (None)

W3C validator