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
|- ( A e. ~H -> ( 0hop ` A ) = 0h )

Proof

Step Hyp Ref Expression
1 choc1
 |-  ( _|_ ` ~H ) = 0H
2 1 fveq2i
 |-  ( projh ` ( _|_ ` ~H ) ) = ( projh ` 0H )
3 df-h0op
 |-  0hop = ( projh ` 0H )
4 2 3 eqtr4i
 |-  ( projh ` ( _|_ ` ~H ) ) = 0hop
5 4 fveq1i
 |-  ( ( projh ` ( _|_ ` ~H ) ) ` A ) = ( 0hop ` A )
6 helch
 |-  ~H e. CH
7 pjo
 |-  ( ( ~H e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` ~H ) ) ` A ) = ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` ~H ) ` A ) ) )
8 6 7 mpan
 |-  ( A e. ~H -> ( ( projh ` ( _|_ ` ~H ) ) ` A ) = ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` ~H ) ` A ) ) )
9 5 8 eqtr3id
 |-  ( A e. ~H -> ( 0hop ` A ) = ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` ~H ) ` A ) ) )
10 6 pjhcli
 |-  ( A e. ~H -> ( ( projh ` ~H ) ` A ) e. ~H )
11 hvsubid
 |-  ( ( ( projh ` ~H ) ` A ) e. ~H -> ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` ~H ) ` A ) ) = 0h )
12 10 11 syl
 |-  ( A e. ~H -> ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` ~H ) ` A ) ) = 0h )
13 9 12 eqtrd
 |-  ( A e. ~H -> ( 0hop ` A ) = 0h )