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

Theorem ifhvhv0 30013
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 29994 . 2 0 ∈ ℋ
21elimel 4559 1 if(𝐴 ∈ ℋ, 𝐴, 0) ∈ ℋ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  ifcif 4490  chba 29910  0c0v 29915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-hv0cl 29994
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4491
This theorem is referenced by:  hvsubsub4  30051  hvnegdi  30058  hvsubeq0  30059  hvaddcan  30061  hvsubadd  30068  normlem9at  30112  normsq  30125  normsub0  30127  norm-ii  30129  norm-iii  30131  normsub  30134  normpyth  30136  norm3dif  30141  norm3lemt  30143  norm3adifi  30144  normpar  30146  polid  30150  bcs  30172  pjoc1  30425  pjoc2  30430  h1de2ci  30547  spansn  30550  elspansn  30557  elspansn2  30558  h1datom  30573  spansnj  30638  spansncv  30644  pjch1  30661  pjadji  30676  pjaddi  30677  pjinormi  30678  pjsubi  30679  pjmuli  30680  pjcjt2  30683  pjch  30685  pjopyth  30711  pjnorm  30715  pjpyth  30716  pjnel  30717  eigre  30826  eigorth  30829  lnopeq0lem2  30997  lnopunii  31003  lnophmi  31009  pjss2coi  31155  pjssmi  31156  pjssge0i  31157  pjdifnormi  31158
  Copyright terms: Public domain W3C validator