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