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

Theorem ifhvhv0 28188
 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 28169 . 2 0 ∈ ℋ
21elimel 4294 1 if(𝐴 ∈ ℋ, 𝐴, 0) ∈ ℋ
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2139  ifcif 4230   ℋchil 28085  0ℎc0v 28090 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-hv0cl 28169 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-if 4231 This theorem is referenced by:  hvsubsub4  28226  hvnegdi  28233  hvsubeq0  28234  hvaddcan  28236  hvsubadd  28243  normlem9at  28287  normsq  28300  normsub0  28302  norm-ii  28304  norm-iii  28306  normsub  28309  normpyth  28311  norm3dif  28316  norm3lemt  28318  norm3adifi  28319  normpar  28321  polid  28325  bcs  28347  pjoc1  28602  pjoc2  28607  h1de2ci  28724  spansn  28727  elspansn  28734  elspansn2  28735  h1datom  28750  spansnj  28815  spansncv  28821  pjch1  28838  pjadji  28853  pjaddi  28854  pjinormi  28855  pjsubi  28856  pjmuli  28857  pjcjt2  28860  pjch  28862  pjopyth  28888  pjnorm  28892  pjpyth  28893  pjnel  28894  eigre  29003  eigorth  29006  lnopeq0lem2  29174  lnopunii  29180  lnophmi  29186  pjss2coi  29332  pjssmi  29333  pjssge0i  29334  pjdifnormi  29335
 Copyright terms: Public domain W3C validator