Metamath Proof Explorer


Theorem ho0val

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.)

Ref Expression
Assertion ho0val ( 𝐴 ∈ ℋ → ( 0hop𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 choc1 ( ⊥ ‘ ℋ ) = 0
2 1 fveq2i ( proj ‘ ( ⊥ ‘ ℋ ) ) = ( proj ‘ 0 )
3 df-h0op 0hop = ( proj ‘ 0 )
4 2 3 eqtr4i ( proj ‘ ( ⊥ ‘ ℋ ) ) = 0hop
5 4 fveq1i ( ( proj ‘ ( ⊥ ‘ ℋ ) ) ‘ 𝐴 ) = ( 0hop𝐴 )
6 helch ℋ ∈ C
7 pjo ( ( ℋ ∈ C𝐴 ∈ ℋ ) → ( ( proj ‘ ( ⊥ ‘ ℋ ) ) ‘ 𝐴 ) = ( ( ( proj ‘ ℋ ) ‘ 𝐴 ) − ( ( proj ‘ ℋ ) ‘ 𝐴 ) ) )
8 6 7 mpan ( 𝐴 ∈ ℋ → ( ( proj ‘ ( ⊥ ‘ ℋ ) ) ‘ 𝐴 ) = ( ( ( proj ‘ ℋ ) ‘ 𝐴 ) − ( ( proj ‘ ℋ ) ‘ 𝐴 ) ) )
9 5 8 eqtr3id ( 𝐴 ∈ ℋ → ( 0hop𝐴 ) = ( ( ( proj ‘ ℋ ) ‘ 𝐴 ) − ( ( proj ‘ ℋ ) ‘ 𝐴 ) ) )
10 6 pjhcli ( 𝐴 ∈ ℋ → ( ( proj ‘ ℋ ) ‘ 𝐴 ) ∈ ℋ )
11 hvsubid ( ( ( proj ‘ ℋ ) ‘ 𝐴 ) ∈ ℋ → ( ( ( proj ‘ ℋ ) ‘ 𝐴 ) − ( ( proj ‘ ℋ ) ‘ 𝐴 ) ) = 0 )
12 10 11 syl ( 𝐴 ∈ ℋ → ( ( ( proj ‘ ℋ ) ‘ 𝐴 ) − ( ( proj ‘ ℋ ) ‘ 𝐴 ) ) = 0 )
13 9 12 eqtrd ( 𝐴 ∈ ℋ → ( 0hop𝐴 ) = 0 )