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

Theorem ifhvhv0 25762
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 25743 . 2  |-  0h  e.  ~H
21elimel 4008 1  |-  if ( A  e.  ~H ,  A ,  0h )  e.  ~H
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767   ifcif 3945   ~Hchil 25659   0hc0v 25664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-hv0cl 25743
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3946
This theorem is referenced by:  hvsubsub4  25800  hvnegdi  25807  hvsubeq0  25808  hvaddcan  25810  hvsubadd  25817  normlem9at  25861  normsq  25874  normsub0  25876  norm-ii  25878  norm-iii  25880  normsub  25883  normpyth  25885  norm3dif  25890  norm3lemt  25892  norm3adifi  25893  normpar  25895  polid  25899  bcs  25921  pjoc1  26175  pjoc2  26180  h1de2ci  26297  spansn  26300  elspansn  26307  elspansn2  26308  h1datom  26323  spansnj  26388  spansncv  26394  pjch1  26411  pjadji  26426  pjaddi  26427  pjinormi  26428  pjsubi  26429  pjmuli  26430  pjcjt2  26433  pjch  26435  pjopyth  26461  pjnorm  26465  pjpyth  26466  pjnel  26467  eigre  26577  eigorth  26580  lnopeq0lem2  26748  lnopunii  26754  lnophmi  26760  pjss2coi  26906  pjssmi  26907  pjssge0i  26908  pjdifnormi  26909
  Copyright terms: Public domain W3C validator