![]() |
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 28404 | . 2 ⊢ 0ℎ ∈ ℋ | |
2 | 1 | elimel 4373 | 1 ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2164 ifcif 4306 ℋchba 28320 0ℎc0v 28325 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 ax-hv0cl 28404 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-if 4307 |
This theorem is referenced by: hvsubsub4 28461 hvnegdi 28468 hvsubeq0 28469 hvaddcan 28471 hvsubadd 28478 normlem9at 28522 normsq 28535 normsub0 28537 norm-ii 28539 norm-iii 28541 normsub 28544 normpyth 28546 norm3dif 28551 norm3lemt 28553 norm3adifi 28554 normpar 28556 polid 28560 bcs 28582 pjoc1 28837 pjoc2 28842 h1de2ci 28959 spansn 28962 elspansn 28969 elspansn2 28970 h1datom 28985 spansnj 29050 spansncv 29056 pjch1 29073 pjadji 29088 pjaddi 29089 pjinormi 29090 pjsubi 29091 pjmuli 29092 pjcjt2 29095 pjch 29097 pjopyth 29123 pjnorm 29127 pjpyth 29128 pjnel 29129 eigre 29238 eigorth 29241 lnopeq0lem2 29409 lnopunii 29415 lnophmi 29421 pjss2coi 29567 pjssmi 29568 pjssge0i 29569 pjdifnormi 29570 |
Copyright terms: Public domain | W3C validator |