Theorem pstmval

Description: Value of the metric induced by a pseudometric D . (Contributed by Thierry Arnoux, 7-Feb-2018)

	Ref	Expression
Hypothesis	pstmval.1	⊢ ∼ = ( ~Met ‘ 𝐷 )
Assertion	pstmval	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( pstoMet ‘ 𝐷 ) = ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		pstmval.1	⊢ ∼ = ( ~Met ‘ 𝐷 )
2		df-pstm	⊢ pstoMet = ( 𝑑 ∈ ∪ ran PsMet ↦ ( 𝑎 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) , 𝑏 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) )
3	2	a1i	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → pstoMet = ( 𝑑 ∈ ∪ ran PsMet ↦ ( 𝑎 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) , 𝑏 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) ) )
4		psmetdmdm	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 = dom dom 𝐷 )
5	4	adantr	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → 𝑋 = dom dom 𝐷 )
6		dmeq	⊢ ( 𝑑 = 𝐷 → dom 𝑑 = dom 𝐷 )
7	6	dmeqd	⊢ ( 𝑑 = 𝐷 → dom dom 𝑑 = dom dom 𝐷 )
8	7	adantl	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → dom dom 𝑑 = dom dom 𝐷 )
9	5 8	eqtr4d	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → 𝑋 = dom dom 𝑑 )
10		qseq1	⊢ ( 𝑋 = dom dom 𝑑 → ( 𝑋 / ∼ ) = ( dom dom 𝑑 / ∼ ) )
11	9 10	syl	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑋 / ∼ ) = ( dom dom 𝑑 / ∼ ) )
12		fveq2	⊢ ( 𝑑 = 𝐷 → ( ~Met ‘ 𝑑 ) = ( ~Met ‘ 𝐷 ) )
13	1 12	eqtr4id	⊢ ( 𝑑 = 𝐷 → ∼ = ( ~Met ‘ 𝑑 ) )
14		qseq2	⊢ ( ∼ = ( ~Met ‘ 𝑑 ) → ( dom dom 𝑑 / ∼ ) = ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) )
15	13 14	syl	⊢ ( 𝑑 = 𝐷 → ( dom dom 𝑑 / ∼ ) = ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) )
16	15	adantl	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( dom dom 𝑑 / ∼ ) = ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) )
17	11 16	eqtr2d	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) = ( 𝑋 / ∼ ) )
18		mpoeq12	⊢ ( ( ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) = ( 𝑋 / ∼ ) ∧ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) = ( 𝑋 / ∼ ) ) → ( 𝑎 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) , 𝑏 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) = ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) )
19	17 17 18	syl2anc	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑎 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) , 𝑏 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) = ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) )
20		simp1r	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑎 ∈ ( 𝑋 / ∼ ) ∧ 𝑏 ∈ ( 𝑋 / ∼ ) ) → 𝑑 = 𝐷 )
21	20	oveqd	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑎 ∈ ( 𝑋 / ∼ ) ∧ 𝑏 ∈ ( 𝑋 / ∼ ) ) → ( 𝑥 𝑑 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
22	21	eqeq2d	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑎 ∈ ( 𝑋 / ∼ ) ∧ 𝑏 ∈ ( 𝑋 / ∼ ) ) → ( 𝑧 = ( 𝑥 𝑑 𝑦 ) ↔ 𝑧 = ( 𝑥 𝐷 𝑦 ) ) )
23	22	2rexbidv	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑎 ∈ ( 𝑋 / ∼ ) ∧ 𝑏 ∈ ( 𝑋 / ∼ ) ) → ( ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) ↔ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) ) )
24	23	abbidv	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑎 ∈ ( 𝑋 / ∼ ) ∧ 𝑏 ∈ ( 𝑋 / ∼ ) ) → { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } = { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) } )
25	24	unieqd	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑎 ∈ ( 𝑋 / ∼ ) ∧ 𝑏 ∈ ( 𝑋 / ∼ ) ) → ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } = ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) } )
26	25	mpoeq3dva	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) = ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) } ) )
27	19 26	eqtrd	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑎 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) , 𝑏 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) = ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) } ) )
28		elfvdm	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ dom PsMet )
29		fveq2	⊢ ( 𝑥 = 𝑋 → ( PsMet ‘ 𝑥 ) = ( PsMet ‘ 𝑋 ) )
30	29	eleq2d	⊢ ( 𝑥 = 𝑋 → ( 𝐷 ∈ ( PsMet ‘ 𝑥 ) ↔ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) )
31	30	rspcev	⊢ ( ( 𝑋 ∈ dom PsMet ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ∃ 𝑥 ∈ dom PsMet 𝐷 ∈ ( PsMet ‘ 𝑥 ) )
32	28 31	mpancom	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∃ 𝑥 ∈ dom PsMet 𝐷 ∈ ( PsMet ‘ 𝑥 ) )
33		df-psmet	⊢ PsMet = ( 𝑥 ∈ V ↦ { 𝑑 ∈ ( ℝ* ↑m ( 𝑥 × 𝑥 ) ) ∣ ∀ 𝑎 ∈ 𝑥 ( ( 𝑎 𝑑 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑥 ∀ 𝑐 ∈ 𝑥 ( 𝑎 𝑑 𝑏 ) ≤ ( ( 𝑐 𝑑 𝑎 ) +𝑒 ( 𝑐 𝑑 𝑏 ) ) ) } )
34	33	funmpt2	⊢ Fun PsMet
35		elunirn	⊢ ( Fun PsMet → ( 𝐷 ∈ ∪ ran PsMet ↔ ∃ 𝑥 ∈ dom PsMet 𝐷 ∈ ( PsMet ‘ 𝑥 ) ) )
36	34 35	ax-mp	⊢ ( 𝐷 ∈ ∪ ran PsMet ↔ ∃ 𝑥 ∈ dom PsMet 𝐷 ∈ ( PsMet ‘ 𝑥 ) )
37	32 36	sylibr	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 ∈ ∪ ran PsMet )
38		elfvex	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ V )
39		qsexg	⊢ ( 𝑋 ∈ V → ( 𝑋 / ∼ ) ∈ V )
40	38 39	syl	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑋 / ∼ ) ∈ V )
41		mpoexga	⊢ ( ( ( 𝑋 / ∼ ) ∈ V ∧ ( 𝑋 / ∼ ) ∈ V ) → ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) } ) ∈ V )
42	40 40 41	syl2anc	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) } ) ∈ V )
43	3 27 37 42	fvmptd	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( pstoMet ‘ 𝐷 ) = ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) } ) )