Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > ifhvhv0 | Structured version Visualization version GIF version |
Description: Prove if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ. (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ifhvhv0 | ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-hv0cl 28780 | . 2 ⊢ 0ℎ ∈ ℋ | |
2 | 1 | elimel 4534 | 1 ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2114 ifcif 4467 ℋchba 28696 0ℎc0v 28701 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-ext 2793 ax-hv0cl 28780 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ex 1781 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-if 4468 |
This theorem is referenced by: hvsubsub4 28837 hvnegdi 28844 hvsubeq0 28845 hvaddcan 28847 hvsubadd 28854 normlem9at 28898 normsq 28911 normsub0 28913 norm-ii 28915 norm-iii 28917 normsub 28920 normpyth 28922 norm3dif 28927 norm3lemt 28929 norm3adifi 28930 normpar 28932 polid 28936 bcs 28958 pjoc1 29211 pjoc2 29216 h1de2ci 29333 spansn 29336 elspansn 29343 elspansn2 29344 h1datom 29359 spansnj 29424 spansncv 29430 pjch1 29447 pjadji 29462 pjaddi 29463 pjinormi 29464 pjsubi 29465 pjmuli 29466 pjcjt2 29469 pjch 29471 pjopyth 29497 pjnorm 29501 pjpyth 29502 pjnel 29503 eigre 29612 eigorth 29615 lnopeq0lem2 29783 lnopunii 29789 lnophmi 29795 pjss2coi 29941 pjssmi 29942 pjssge0i 29943 pjdifnormi 29944 |
Copyright terms: Public domain | W3C validator |