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

Theorem ifhvhv0 31340
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 31321 . 2 0 ∈ ℋ
21elimel 4556 1 if(𝐴 ∈ ℋ, 𝐴, 0) ∈ ℋ
Colors of variables: wff setvar class
Syntax hints:  wcel 2141  ifcif 4486  chba 31237  0c0v 31242
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-hv0cl 31321
This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4487
This theorem is referenced by:  hvsubsub4  31378  hvnegdi  31385  hvsubeq0  31386  hvaddcan  31388  hvsubadd  31395  normlem9at  31439  normsq  31452  normsub0  31454  norm-ii  31456  norm-iii  31458  normsub  31461  normpyth  31463  norm3dif  31468  norm3lemt  31470  norm3adifi  31471  normpar  31473  polid  31477  bcs  31499  pjoc1  31752  pjoc2  31757  h1de2ci  31874  spansn  31877  elspansn  31884  elspansn2  31885  h1datom  31900  spansnj  31965  spansncv  31971  pjch1  31988  pjadji  32003  pjaddi  32004  pjinormi  32005  pjsubi  32006  pjmuli  32007  pjcjt2  32010  pjch  32012  pjopyth  32038  pjnorm  32042  pjpyth  32043  pjnel  32044  eigre  32153  eigorth  32156  lnopeq0lem2  32324  lnopunii  32330  lnophmi  32336  pjss2coi  32482  pjssmi  32483  pjssge0i  32484  pjdifnormi  32485
  Copyright terms: Public domain W3C validator