MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovresd Structured version   Unicode version

Theorem ovresd 6426
Description: Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)
Hypotheses
Ref Expression
ovresd.1  |-  ( ph  ->  A  e.  X )
ovresd.2  |-  ( ph  ->  B  e.  X )
Assertion
Ref Expression
ovresd  |-  ( ph  ->  ( A ( D  |`  ( X  X.  X
) ) B )  =  ( A D B ) )

Proof of Theorem ovresd
StepHypRef Expression
1 ovresd.1 . 2  |-  ( ph  ->  A  e.  X )
2 ovresd.2 . 2  |-  ( ph  ->  B  e.  X )
3 ovres 6425 . 2  |-  ( ( A  e.  X  /\  B  e.  X )  ->  ( A ( D  |`  ( X  X.  X
) ) B )  =  ( A D B ) )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A ( D  |`  ( X  X.  X
) ) B )  =  ( A D B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1407    e. wcel 1844    X. cxp 4823    |` cres 4827  (class class class)co 6280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-sep 4519  ax-nul 4527  ax-pr 4632
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3063  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-sn 3975  df-pr 3977  df-op 3981  df-uni 4194  df-br 4398  df-opab 4456  df-xp 4831  df-res 4837  df-iota 5535  df-fv 5579  df-ov 6283
This theorem is referenced by:  sscres  15438  fullsubc  15465  fullresc  15466  funcres2c  15516  psmetres2  21112  xmetres2  21158  prdsdsf  21164  xpsdsval  21178  xmssym  21262  xmstri2  21263  mstri2  21264  xmstri  21265  mstri  21266  xmstri3  21267  mstri3  21268  msrtri  21269  tmsxpsval  21335  ngptgp  21444  nlmvscn  21490  nrginvrcn  21494  nghmcn  21546  cnmpt1ds  21641  cnmpt2ds  21642  ipcn  21980  caussi  22030  causs  22031  minveclem2  22135  minveclem3b  22137  minveclem3  22138  minveclem4  22141  minveclem6  22143  ftc1lem6  22736  ulmdvlem1  23089  abelth  23130  cxpcn3  23420  rlimcnp  23623  hhssnv  26607  qqhcn  28437  qqhucn  28438  ftc1cnnc  31475  ismtyres  31599  isdrngo2  31656  rngchom  38299  ringchom  38345  irinitoringc  38401  rhmsubclem4  38421
  Copyright terms: Public domain W3C validator