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

Theorem ifhvhv0 27719
Description: Prove if(𝐴 ∈ ℋ, 𝐴, 0) ∈ ℋ (common case). (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 27700 . 2 0 ∈ ℋ
21elimel 4127 1 if(𝐴 ∈ ℋ, 𝐴, 0) ∈ ℋ
Colors of variables: wff setvar class
Syntax hints:  wcel 1992  ifcif 4063  chil 27616  0c0v 27621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-hv0cl 27700
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-if 4064
This theorem is referenced by:  hvsubsub4  27757  hvnegdi  27764  hvsubeq0  27765  hvaddcan  27767  hvsubadd  27774  normlem9at  27818  normsq  27831  normsub0  27833  norm-ii  27835  norm-iii  27837  normsub  27840  normpyth  27842  norm3dif  27847  norm3lemt  27849  norm3adifi  27850  normpar  27852  polid  27856  bcs  27878  pjoc1  28133  pjoc2  28138  h1de2ci  28255  spansn  28258  elspansn  28265  elspansn2  28266  h1datom  28281  spansnj  28346  spansncv  28352  pjch1  28369  pjadji  28384  pjaddi  28385  pjinormi  28386  pjsubi  28387  pjmuli  28388  pjcjt2  28391  pjch  28393  pjopyth  28419  pjnorm  28423  pjpyth  28424  pjnel  28425  eigre  28534  eigorth  28537  lnopeq0lem2  28705  lnopunii  28711  lnophmi  28717  pjss2coi  28863  pjssmi  28864  pjssge0i  28865  pjdifnormi  28866
  Copyright terms: Public domain W3C validator