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

Theorem ifhvhv0 26510
Description: Prove  if ( A  e.  ~H ,  A ,  0h )  e.  ~H (common case). (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.)
Assertion
Ref Expression
ifhvhv0  |-  if ( A  e.  ~H ,  A ,  0h )  e.  ~H

Proof of Theorem ifhvhv0
StepHypRef Expression
1 ax-hv0cl 26491 . 2  |-  0h  e.  ~H
21elimel 3977 1  |-  if ( A  e.  ~H ,  A ,  0h )  e.  ~H
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1870   ifcif 3915   ~Hchil 26407   0hc0v 26412
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-hv0cl 26491
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-if 3916
This theorem is referenced by:  hvsubsub4  26548  hvnegdi  26555  hvsubeq0  26556  hvaddcan  26558  hvsubadd  26565  normlem9at  26609  normsq  26622  normsub0  26624  norm-ii  26626  norm-iii  26628  normsub  26631  normpyth  26633  norm3dif  26638  norm3lemt  26640  norm3adifi  26641  normpar  26643  polid  26647  bcs  26669  pjoc1  26922  pjoc2  26927  h1de2ci  27044  spansn  27047  elspansn  27054  elspansn2  27055  h1datom  27070  spansnj  27135  spansncv  27141  pjch1  27158  pjadji  27173  pjaddi  27174  pjinormi  27175  pjsubi  27176  pjmuli  27177  pjcjt2  27180  pjch  27182  pjopyth  27208  pjnorm  27212  pjpyth  27213  pjnel  27214  eigre  27323  eigorth  27326  lnopeq0lem2  27494  lnopunii  27500  lnophmi  27506  pjss2coi  27652  pjssmi  27653  pjssge0i  27654  pjdifnormi  27655
  Copyright terms: Public domain W3C validator