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

Theorem ifhvhv0 30852
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 30833 . 2 0 ∈ ℋ
21elimel 4601 1 if(𝐴 ∈ ℋ, 𝐴, 0) ∈ ℋ
Colors of variables: wff setvar class
Syntax hints:  wcel 2098  ifcif 4532  chba 30749  0c0v 30754
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-ext 2699  ax-hv0cl 30833
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-if 4533
This theorem is referenced by:  hvsubsub4  30890  hvnegdi  30897  hvsubeq0  30898  hvaddcan  30900  hvsubadd  30907  normlem9at  30951  normsq  30964  normsub0  30966  norm-ii  30968  norm-iii  30970  normsub  30973  normpyth  30975  norm3dif  30980  norm3lemt  30982  norm3adifi  30983  normpar  30985  polid  30989  bcs  31011  pjoc1  31264  pjoc2  31269  h1de2ci  31386  spansn  31389  elspansn  31396  elspansn2  31397  h1datom  31412  spansnj  31477  spansncv  31483  pjch1  31500  pjadji  31515  pjaddi  31516  pjinormi  31517  pjsubi  31518  pjmuli  31519  pjcjt2  31522  pjch  31524  pjopyth  31550  pjnorm  31554  pjpyth  31555  pjnel  31556  eigre  31665  eigorth  31668  lnopeq0lem2  31836  lnopunii  31842  lnophmi  31848  pjss2coi  31994  pjssmi  31995  pjssge0i  31996  pjdifnormi  31997
  Copyright terms: Public domain W3C validator