Metamath Proof Explorer

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 psmetdmdm ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 = dom dom 𝐷 )
4 3 adantr ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → 𝑋 = dom dom 𝐷 )
5 dmeq ⊢ ( 𝑑 = 𝐷 → dom 𝑑 = dom 𝐷 )
6 5 dmeqd ⊢ ( 𝑑 = 𝐷 → dom dom 𝑑 = dom dom 𝐷 )
7 6 adantl ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → dom dom 𝑑 = dom dom 𝐷 )
8 4 7 eqtr4d ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → 𝑋 = dom dom 𝑑 )
9 qseq1 ⊢ ( 𝑋 = dom dom 𝑑 → ( 𝑋 / ∼ ) = ( dom dom 𝑑 / ∼ ) )
10 8 9 syl ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑋 / ∼ ) = ( dom dom 𝑑 / ∼ ) )
11 fveq2 ⊢ ( 𝑑 = 𝐷 → ( ~Met ‘ 𝑑 ) = ( ~Met ‘ 𝐷 ) )
12 1 11 eqtr4id ⊢ ( 𝑑 = 𝐷 → ∼ = ( ~Met ‘ 𝑑 ) )
13 12 qseq2d ⊢ ( 𝑑 = 𝐷 → ( dom dom 𝑑 / ∼ ) = ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) )
14 13 adantl ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( dom dom 𝑑 / ∼ ) = ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) )
15 10 14 eqtr2d ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) = ( 𝑋 / ∼ ) )
16 mpoeq12 ⊢ ( ( ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) = ( 𝑋 / ∼ ) ∧ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) = ( 𝑋 / ∼ ) ) → ( 𝑎 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) , 𝑏 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) = ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) )
17 15 15 16 syl2anc ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑎 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) , 𝑏 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) = ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) )
18 simp1r ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑎 ∈ ( 𝑋 / ∼ ) ∧ 𝑏 ∈ ( 𝑋 / ∼ ) ) → 𝑑 = 𝐷 )
19 18 oveqd ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑎 ∈ ( 𝑋 / ∼ ) ∧ 𝑏 ∈ ( 𝑋 / ∼ ) ) → ( 𝑥 𝑑 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
20 19 eqeq2d ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑎 ∈ ( 𝑋 / ∼ ) ∧ 𝑏 ∈ ( 𝑋 / ∼ ) ) → ( 𝑧 = ( 𝑥 𝑑 𝑦 ) ↔ 𝑧 = ( 𝑥 𝐷 𝑦 ) ) )
21 20 2rexbidv ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑎 ∈ ( 𝑋 / ∼ ) ∧ 𝑏 ∈ ( 𝑋 / ∼ ) ) → ( ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) ↔ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) ) )
22 21 abbidv ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑎 ∈ ( 𝑋 / ∼ ) ∧ 𝑏 ∈ ( 𝑋 / ∼ ) ) → { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } = { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) } )
23 22 unieqd ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑎 ∈ ( 𝑋 / ∼ ) ∧ 𝑏 ∈ ( 𝑋 / ∼ ) ) → ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } = ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) } )
24 23 mpoeq3dva ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) = ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) } ) )
25 17 24 eqtrd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑎 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) , 𝑏 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) = ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) } ) )
26 elfvunirn ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 ∈ ∪ ran PsMet )
27 elfvex ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ V )
28 qsexg ⊢ ( 𝑋 ∈ V → ( 𝑋 / ∼ ) ∈ V )
29 27 28 syl ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑋 / ∼ ) ∈ V )
30 mpoexga ⊢ ( ( ( 𝑋 / ∼ ) ∈ V ∧ ( 𝑋 / ∼ ) ∈ V ) → ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) } ) ∈ V )
31 29 29 30 syl2anc ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) } ) ∈ V )
32 2 25 26 31 fvmptd2 ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( pstoMet ‘ 𝐷 ) = ( 𝑎 ∈ ( 𝑋 / ∼ ) , 𝑏 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝐷 𝑦 ) } ) )