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

Theorem ifhvhv0 31041
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 31022 . 2 0 ∈ ℋ
21elimel 4595 1 if(𝐴 ∈ ℋ, 𝐴, 0) ∈ ℋ
Colors of variables: wff setvar class
Syntax hints:  wcel 2108  ifcif 4525  chba 30938  0c0v 30943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-hv0cl 31022
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526
This theorem is referenced by:  hvsubsub4  31079  hvnegdi  31086  hvsubeq0  31087  hvaddcan  31089  hvsubadd  31096  normlem9at  31140  normsq  31153  normsub0  31155  norm-ii  31157  norm-iii  31159  normsub  31162  normpyth  31164  norm3dif  31169  norm3lemt  31171  norm3adifi  31172  normpar  31174  polid  31178  bcs  31200  pjoc1  31453  pjoc2  31458  h1de2ci  31575  spansn  31578  elspansn  31585  elspansn2  31586  h1datom  31601  spansnj  31666  spansncv  31672  pjch1  31689  pjadji  31704  pjaddi  31705  pjinormi  31706  pjsubi  31707  pjmuli  31708  pjcjt2  31711  pjch  31713  pjopyth  31739  pjnorm  31743  pjpyth  31744  pjnel  31745  eigre  31854  eigorth  31857  lnopeq0lem2  32025  lnopunii  32031  lnophmi  32037  pjss2coi  32183  pjssmi  32184  pjssge0i  32185  pjdifnormi  32186
  Copyright terms: Public domain W3C validator