MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xmetres2 Structured version   Visualization version   GIF version
Theorem xmetres2 24295
Description: Restriction of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xmetres2 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) β†’ (𝐷 β†Ύ (𝑅 Γ— 𝑅)) ∈ (∞Metβ€˜π‘…))
Proof of Theorem xmetres2
Dummy variables π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfvdm 6939 . . . 4 (𝐷 ∈ (∞Metβ€˜π‘‹) β†’ 𝑋 ∈ dom ∞Met)
21adantr 479 . . 3 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) β†’ 𝑋 ∈ dom ∞Met)
3 simpr 483 . . 3 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) β†’ 𝑅 βŠ† 𝑋)
42, 3ssexd 5328 . 2 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) β†’ 𝑅 ∈ V)
5 xmetf 24263 . . . 4 (𝐷 ∈ (∞Metβ€˜π‘‹) β†’ 𝐷:(𝑋 Γ— 𝑋)βŸΆβ„*)
65adantr 479 . . 3 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) β†’ 𝐷:(𝑋 Γ— 𝑋)βŸΆβ„*)
7 xpss12 5697 . . . 4 ((𝑅 βŠ† 𝑋 ∧ 𝑅 βŠ† 𝑋) β†’ (𝑅 Γ— 𝑅) βŠ† (𝑋 Γ— 𝑋))
83, 7sylancom 586 . . 3 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) β†’ (𝑅 Γ— 𝑅) βŠ† (𝑋 Γ— 𝑋))
96, 8fssresd 6769 . 2 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) β†’ (𝐷 β†Ύ (𝑅 Γ— 𝑅)):(𝑅 Γ— 𝑅)βŸΆβ„*)
10 ovres 7594 . . . . 5 ((π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) β†’ (π‘₯(𝐷 β†Ύ (𝑅 Γ— 𝑅))𝑦) = (π‘₯𝐷𝑦))
1110adantl 480 . . . 4 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (π‘₯(𝐷 β†Ύ (𝑅 Γ— 𝑅))𝑦) = (π‘₯𝐷𝑦))
1211eqeq1d 2730 . . 3 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((π‘₯(𝐷 β†Ύ (𝑅 Γ— 𝑅))𝑦) = 0 ↔ (π‘₯𝐷𝑦) = 0))
13 simpll 765 . . . 4 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
14 simplr 767 . . . . 5 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ 𝑅 βŠ† 𝑋)
15 simprl 769 . . . . 5 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ π‘₯ ∈ 𝑅)
1614, 15sseldd 3983 . . . 4 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ π‘₯ ∈ 𝑋)
17 simprr 771 . . . . 5 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ 𝑦 ∈ 𝑅)
1814, 17sseldd 3983 . . . 4 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ 𝑦 ∈ 𝑋)
19 xmeteq0 24272 . . . 4 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ((π‘₯𝐷𝑦) = 0 ↔ π‘₯ = 𝑦))
2013, 16, 18, 19syl3anc 1368 . . 3 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((π‘₯𝐷𝑦) = 0 ↔ π‘₯ = 𝑦))
2112, 20bitrd 278 . 2 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((π‘₯(𝐷 β†Ύ (𝑅 Γ— 𝑅))𝑦) = 0 ↔ π‘₯ = 𝑦))
22 simpll 765 . . . 4 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
23 simplr 767 . . . . 5 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) β†’ 𝑅 βŠ† 𝑋)
24 simpr3 1193 . . . . 5 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) β†’ 𝑧 ∈ 𝑅)
2523, 24sseldd 3983 . . . 4 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) β†’ 𝑧 ∈ 𝑋)
26163adantr3 1168 . . . 4 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) β†’ π‘₯ ∈ 𝑋)
27183adantr3 1168 . . . 4 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) β†’ 𝑦 ∈ 𝑋)
28 xmettri2 24274 . . . 4 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ (𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)))
2922, 25, 26, 27, 28syl13anc 1369 . . 3 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)))
30113adantr3 1168 . . 3 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) β†’ (π‘₯(𝐷 β†Ύ (𝑅 Γ— 𝑅))𝑦) = (π‘₯𝐷𝑦))
31 simpr1 1191 . . . . 5 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) β†’ π‘₯ ∈ 𝑅)
3224, 31ovresd 7595 . . . 4 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) β†’ (𝑧(𝐷 β†Ύ (𝑅 Γ— 𝑅))π‘₯) = (𝑧𝐷π‘₯))
33 simpr2 1192 . . . . 5 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) β†’ 𝑦 ∈ 𝑅)
3424, 33ovresd 7595 . . . 4 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) β†’ (𝑧(𝐷 β†Ύ (𝑅 Γ— 𝑅))𝑦) = (𝑧𝐷𝑦))
3532, 34oveq12d 7444 . . 3 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) β†’ ((𝑧(𝐷 β†Ύ (𝑅 Γ— 𝑅))π‘₯) +𝑒 (𝑧(𝐷 β†Ύ (𝑅 Γ— 𝑅))𝑦)) = ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)))
3629, 30, 353brtr4d 5184 . 2 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) β†’ (π‘₯(𝐷 β†Ύ (𝑅 Γ— 𝑅))𝑦) ≀ ((𝑧(𝐷 β†Ύ (𝑅 Γ— 𝑅))π‘₯) +𝑒 (𝑧(𝐷 β†Ύ (𝑅 Γ— 𝑅))𝑦)))
374, 9, 21, 36isxmetd 24260 1 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑅 βŠ† 𝑋) β†’ (𝐷 β†Ύ (𝑅 Γ— 𝑅)) ∈ (∞Metβ€˜π‘…))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  Vcvv 3473   βŠ† wss 3949   class class class wbr 5152   Γ— cxp 5680  dom cdm 5682   β†Ύ cres 5684  βŸΆwf 6549  β€˜cfv 6553  (class class class)co 7426  0cc0 11148  β„*cxr 11287   ≀ cle 11289   +𝑒 cxad 13132  βˆžMetcxmet 21278
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 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7748  ax-cnex 11204  ax-resscn 11205
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-fv 6561  df-ov 7429  df-oprab 7430  df-mpo 7431  df-map 8855  df-xr 11292  df-xmet 21286
This theorem is referenced by:  metres2  24297  xmetres  24298  xpsxmet  24314  xpsdsval  24315  xmetresbl  24371  tmsxms  24423  imasf1oxms  24426  metrest  24461  prdsxms  24467  tmsxpsval  24475  nrginvrcn  24637  divcnOLD  24812  divcn  24814  iitopon  24827  cncfmet  24857  cfilres  25252  dvlip2  25956  ftc1lem6  26004  ulmdvlem1  26364  ulmdvlem3  26366  abelth  26406  cxpcn3  26711  rlimcnp  26925  minvecolem4b  30716  minvecolem4  30718  ftc1cnnc  37206  blbnd  37301  ismtyres  37322  reheibor  37353
  Copyright terms: Public domain W3C validator