HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  ifhvhv0 Structured version   Visualization version   GIF version

Theorem ifhvhv0 28423
Description: Prove if(𝐴 ∈ ℋ, 𝐴, 0) ∈ ℋ. (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.)
Assertion
Ref Expression
ifhvhv0 if(𝐴 ∈ ℋ, 𝐴, 0) ∈ ℋ

Proof of Theorem ifhvhv0
StepHypRef Expression
1 ax-hv0cl 28404 . 2 0 ∈ ℋ
21elimel 4373 1 if(𝐴 ∈ ℋ, 𝐴, 0) ∈ ℋ
Colors of variables: wff setvar class
Syntax hints:  wcel 2164  ifcif 4306  chba 28320  0c0v 28325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803  ax-hv0cl 28404
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-if 4307
This theorem is referenced by:  hvsubsub4  28461  hvnegdi  28468  hvsubeq0  28469  hvaddcan  28471  hvsubadd  28478  normlem9at  28522  normsq  28535  normsub0  28537  norm-ii  28539  norm-iii  28541  normsub  28544  normpyth  28546  norm3dif  28551  norm3lemt  28553  norm3adifi  28554  normpar  28556  polid  28560  bcs  28582  pjoc1  28837  pjoc2  28842  h1de2ci  28959  spansn  28962  elspansn  28969  elspansn2  28970  h1datom  28985  spansnj  29050  spansncv  29056  pjch1  29073  pjadji  29088  pjaddi  29089  pjinormi  29090  pjsubi  29091  pjmuli  29092  pjcjt2  29095  pjch  29097  pjopyth  29123  pjnorm  29127  pjpyth  29128  pjnel  29129  eigre  29238  eigorth  29241  lnopeq0lem2  29409  lnopunii  29415  lnophmi  29421  pjss2coi  29567  pjssmi  29568  pjssge0i  29569  pjdifnormi  29570
  Copyright terms: Public domain W3C validator