| 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 31022 | . 2 ⊢ 0ℎ ∈ ℋ | |
| 2 | 1 | elimel 4595 | 1 ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 ifcif 4525 ℋchba 30938 0ℎc0v 30943 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-hv0cl 31022 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-if 4526 |
| This theorem is referenced by: hvsubsub4 31079 hvnegdi 31086 hvsubeq0 31087 hvaddcan 31089 hvsubadd 31096 normlem9at 31140 normsq 31153 normsub0 31155 norm-ii 31157 norm-iii 31159 normsub 31162 normpyth 31164 norm3dif 31169 norm3lemt 31171 norm3adifi 31172 normpar 31174 polid 31178 bcs 31200 pjoc1 31453 pjoc2 31458 h1de2ci 31575 spansn 31578 elspansn 31585 elspansn2 31586 h1datom 31601 spansnj 31666 spansncv 31672 pjch1 31689 pjadji 31704 pjaddi 31705 pjinormi 31706 pjsubi 31707 pjmuli 31708 pjcjt2 31711 pjch 31713 pjopyth 31739 pjnorm 31743 pjpyth 31744 pjnel 31745 eigre 31854 eigorth 31857 lnopeq0lem2 32025 lnopunii 32031 lnophmi 32037 pjss2coi 32183 pjssmi 32184 pjssge0i 32185 pjdifnormi 32186 |
| Copyright terms: Public domain | W3C validator |