Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  ho0val Structured version   Visualization version   GIF version

Theorem ho0val 29521
 Description: Value of the zero Hilbert space operator (null projector). Remark in [Beran] p. 111. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression
ho0val (𝐴 ∈ ℋ → ( 0hop𝐴) = 0)

Proof of Theorem ho0val
StepHypRef Expression
1 choc1 29098 . . . . . 6 (⊥‘ ℋ) = 0
21fveq2i 6668 . . . . 5 (proj‘(⊥‘ ℋ)) = (proj‘0)
3 df-h0op 29519 . . . . 5 0hop = (proj‘0)
42, 3eqtr4i 2847 . . . 4 (proj‘(⊥‘ ℋ)) = 0hop
54fveq1i 6666 . . 3 ((proj‘(⊥‘ ℋ))‘𝐴) = ( 0hop𝐴)
6 helch 29014 . . . 4 ℋ ∈ C
7 pjo 29442 . . . 4 (( ℋ ∈ C𝐴 ∈ ℋ) → ((proj‘(⊥‘ ℋ))‘𝐴) = (((proj‘ ℋ)‘𝐴) − ((proj‘ ℋ)‘𝐴)))
86, 7mpan 688 . . 3 (𝐴 ∈ ℋ → ((proj‘(⊥‘ ℋ))‘𝐴) = (((proj‘ ℋ)‘𝐴) − ((proj‘ ℋ)‘𝐴)))
95, 8syl5eqr 2870 . 2 (𝐴 ∈ ℋ → ( 0hop𝐴) = (((proj‘ ℋ)‘𝐴) − ((proj‘ ℋ)‘𝐴)))
106pjhcli 29189 . . 3 (𝐴 ∈ ℋ → ((proj‘ ℋ)‘𝐴) ∈ ℋ)
11 hvsubid 28797 . . 3 (((proj‘ ℋ)‘𝐴) ∈ ℋ → (((proj‘ ℋ)‘𝐴) − ((proj‘ ℋ)‘𝐴)) = 0)
1210, 11syl 17 . 2 (𝐴 ∈ ℋ → (((proj‘ ℋ)‘𝐴) − ((proj‘ ℋ)‘𝐴)) = 0)
139, 12eqtrd 2856 1 (𝐴 ∈ ℋ → ( 0hop𝐴) = 0)