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 29374 | . 2 ⊢ 0ℎ ∈ ℋ | |
2 | 1 | elimel 4529 | 1 ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 ifcif 4460 ℋchba 29290 0ℎc0v 29295 |
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 2710 ax-hv0cl 29374 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-ex 1783 df-sb 2069 df-clab 2717 df-cleq 2731 df-clel 2817 df-if 4461 |
This theorem is referenced by: hvsubsub4 29431 hvnegdi 29438 hvsubeq0 29439 hvaddcan 29441 hvsubadd 29448 normlem9at 29492 normsq 29505 normsub0 29507 norm-ii 29509 norm-iii 29511 normsub 29514 normpyth 29516 norm3dif 29521 norm3lemt 29523 norm3adifi 29524 normpar 29526 polid 29530 bcs 29552 pjoc1 29805 pjoc2 29810 h1de2ci 29927 spansn 29930 elspansn 29937 elspansn2 29938 h1datom 29953 spansnj 30018 spansncv 30024 pjch1 30041 pjadji 30056 pjaddi 30057 pjinormi 30058 pjsubi 30059 pjmuli 30060 pjcjt2 30063 pjch 30065 pjopyth 30091 pjnorm 30095 pjpyth 30096 pjnel 30097 eigre 30206 eigorth 30209 lnopeq0lem2 30377 lnopunii 30383 lnophmi 30389 pjss2coi 30535 pjssmi 30536 pjssge0i 30537 pjdifnormi 30538 |
Copyright terms: Public domain | W3C validator |