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

Theorem ifhvhv0 28784
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 28765 . 2 0 ∈ ℋ
21elimel 4510 1 if(𝐴 ∈ ℋ, 𝐴, 0) ∈ ℋ
Colors of variables: wff setvar class
Syntax hints:  wcel 2114  ifcif 4443  chba 28681  0c0v 28686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2792  ax-hv0cl 28765
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-if 4444
This theorem is referenced by:  hvsubsub4  28822  hvnegdi  28829  hvsubeq0  28830  hvaddcan  28832  hvsubadd  28839  normlem9at  28883  normsq  28896  normsub0  28898  norm-ii  28900  norm-iii  28902  normsub  28905  normpyth  28907  norm3dif  28912  norm3lemt  28914  norm3adifi  28915  normpar  28917  polid  28921  bcs  28943  pjoc1  29196  pjoc2  29201  h1de2ci  29318  spansn  29321  elspansn  29328  elspansn2  29329  h1datom  29344  spansnj  29409  spansncv  29415  pjch1  29432  pjadji  29447  pjaddi  29448  pjinormi  29449  pjsubi  29450  pjmuli  29451  pjcjt2  29454  pjch  29456  pjopyth  29482  pjnorm  29486  pjpyth  29487  pjnel  29488  eigre  29597  eigorth  29600  lnopeq0lem2  29768  lnopunii  29774  lnophmi  29780  pjss2coi  29926  pjssmi  29927  pjssge0i  29928  pjdifnormi  29929
  Copyright terms: Public domain W3C validator