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

Theorem ifhvhv0 29393
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 29374 . 2 0 ∈ ℋ
21elimel 4529 1 if(𝐴 ∈ ℋ, 𝐴, 0) ∈ ℋ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  ifcif 4460  chba 29290  0c0v 29295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-hv0cl 29374
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-if 4461
This theorem is referenced by:  hvsubsub4  29431  hvnegdi  29438  hvsubeq0  29439  hvaddcan  29441  hvsubadd  29448  normlem9at  29492  normsq  29505  normsub0  29507  norm-ii  29509  norm-iii  29511  normsub  29514  normpyth  29516  norm3dif  29521  norm3lemt  29523  norm3adifi  29524  normpar  29526  polid  29530  bcs  29552  pjoc1  29805  pjoc2  29810  h1de2ci  29927  spansn  29930  elspansn  29937  elspansn2  29938  h1datom  29953  spansnj  30018  spansncv  30024  pjch1  30041  pjadji  30056  pjaddi  30057  pjinormi  30058  pjsubi  30059  pjmuli  30060  pjcjt2  30063  pjch  30065  pjopyth  30091  pjnorm  30095  pjpyth  30096  pjnel  30097  eigre  30206  eigorth  30209  lnopeq0lem2  30377  lnopunii  30383  lnophmi  30389  pjss2coi  30535  pjssmi  30536  pjssge0i  30537  pjdifnormi  30538
  Copyright terms: Public domain W3C validator