![]() |
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 29994 | . 2 ⊢ 0ℎ ∈ ℋ | |
2 | 1 | elimel 4559 | 1 ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 ifcif 4490 ℋchba 29910 0ℎc0v 29915 |
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 2704 ax-hv0cl 29994 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-if 4491 |
This theorem is referenced by: hvsubsub4 30051 hvnegdi 30058 hvsubeq0 30059 hvaddcan 30061 hvsubadd 30068 normlem9at 30112 normsq 30125 normsub0 30127 norm-ii 30129 norm-iii 30131 normsub 30134 normpyth 30136 norm3dif 30141 norm3lemt 30143 norm3adifi 30144 normpar 30146 polid 30150 bcs 30172 pjoc1 30425 pjoc2 30430 h1de2ci 30547 spansn 30550 elspansn 30557 elspansn2 30558 h1datom 30573 spansnj 30638 spansncv 30644 pjch1 30661 pjadji 30676 pjaddi 30677 pjinormi 30678 pjsubi 30679 pjmuli 30680 pjcjt2 30683 pjch 30685 pjopyth 30711 pjnorm 30715 pjpyth 30716 pjnel 30717 eigre 30826 eigorth 30829 lnopeq0lem2 30997 lnopunii 31003 lnophmi 31009 pjss2coi 31155 pjssmi 31156 pjssge0i 31157 pjdifnormi 31158 |
Copyright terms: Public domain | W3C validator |