![]() |
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 30833 | . 2 ⊢ 0ℎ ∈ ℋ | |
2 | 1 | elimel 4601 | 1 ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2098 ifcif 4532 ℋchba 30749 0ℎc0v 30754 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2699 ax-hv0cl 30833 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-ex 1774 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-if 4533 |
This theorem is referenced by: hvsubsub4 30890 hvnegdi 30897 hvsubeq0 30898 hvaddcan 30900 hvsubadd 30907 normlem9at 30951 normsq 30964 normsub0 30966 norm-ii 30968 norm-iii 30970 normsub 30973 normpyth 30975 norm3dif 30980 norm3lemt 30982 norm3adifi 30983 normpar 30985 polid 30989 bcs 31011 pjoc1 31264 pjoc2 31269 h1de2ci 31386 spansn 31389 elspansn 31396 elspansn2 31397 h1datom 31412 spansnj 31477 spansncv 31483 pjch1 31500 pjadji 31515 pjaddi 31516 pjinormi 31517 pjsubi 31518 pjmuli 31519 pjcjt2 31522 pjch 31524 pjopyth 31550 pjnorm 31554 pjpyth 31555 pjnel 31556 eigre 31665 eigorth 31668 lnopeq0lem2 31836 lnopunii 31842 lnophmi 31848 pjss2coi 31994 pjssmi 31995 pjssge0i 31996 pjdifnormi 31997 |
Copyright terms: Public domain | W3C validator |