![]() |
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 27988 | . 2 ⊢ 0ℎ ∈ ℋ | |
2 | 1 | elimel 4183 | 1 ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2030 ifcif 4119 ℋchil 27904 0ℎc0v 27909 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-hv0cl 27988 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-if 4120 |
This theorem is referenced by: hvsubsub4 28045 hvnegdi 28052 hvsubeq0 28053 hvaddcan 28055 hvsubadd 28062 normlem9at 28106 normsq 28119 normsub0 28121 norm-ii 28123 norm-iii 28125 normsub 28128 normpyth 28130 norm3dif 28135 norm3lemt 28137 norm3adifi 28138 normpar 28140 polid 28144 bcs 28166 pjoc1 28421 pjoc2 28426 h1de2ci 28543 spansn 28546 elspansn 28553 elspansn2 28554 h1datom 28569 spansnj 28634 spansncv 28640 pjch1 28657 pjadji 28672 pjaddi 28673 pjinormi 28674 pjsubi 28675 pjmuli 28676 pjcjt2 28679 pjch 28681 pjopyth 28707 pjnorm 28711 pjpyth 28712 pjnel 28713 eigre 28822 eigorth 28825 lnopeq0lem2 28993 lnopunii 28999 lnophmi 29005 pjss2coi 29151 pjssmi 29152 pjssge0i 29153 pjdifnormi 29154 |
Copyright terms: Public domain | W3C validator |