This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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