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 28950 | . 2 ⊢ 0ℎ ∈ ℋ | |
2 | 1 | elimel 4493 | 1 ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2114 ifcif 4424 ℋchba 28866 0ℎc0v 28871 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 ax-hv0cl 28950 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-if 4425 |
This theorem is referenced by: hvsubsub4 29007 hvnegdi 29014 hvsubeq0 29015 hvaddcan 29017 hvsubadd 29024 normlem9at 29068 normsq 29081 normsub0 29083 norm-ii 29085 norm-iii 29087 normsub 29090 normpyth 29092 norm3dif 29097 norm3lemt 29099 norm3adifi 29100 normpar 29102 polid 29106 bcs 29128 pjoc1 29381 pjoc2 29386 h1de2ci 29503 spansn 29506 elspansn 29513 elspansn2 29514 h1datom 29529 spansnj 29594 spansncv 29600 pjch1 29617 pjadji 29632 pjaddi 29633 pjinormi 29634 pjsubi 29635 pjmuli 29636 pjcjt2 29639 pjch 29641 pjopyth 29667 pjnorm 29671 pjpyth 29672 pjnel 29673 eigre 29782 eigorth 29785 lnopeq0lem2 29953 lnopunii 29959 lnophmi 29965 pjss2coi 30111 pjssmi 30112 pjssge0i 30113 pjdifnormi 30114 |
Copyright terms: Public domain | W3C validator |