Metamath Proof Explorer

Theorem hst0

Description: A Hilbert-space-valued state is zero at the zero subspace. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hst0 
|- ( S e. CHStates -> ( S ` 0H ) = 0h )

Proof

Step Hyp Ref Expression
1 h0elch 
 |-  0H e. CH
2 helch 
 |-  ~H e. CH
3 2 choccli 
 |-  ( _|_ ` ~H ) e. CH
4 3 ch0lei 
 |-  0H C_ ( _|_ ` ~H )
5 hstorth 
 |-  ( ( ( S e. CHStates /\ 0H e. CH ) /\ ( ~H e. CH /\ 0H C_ ( _|_ ` ~H ) ) ) -> ( ( S ` 0H ) .ih ( S ` ~H ) ) = 0 )
6 2 4 5 mpanr12 
 |-  ( ( S e. CHStates /\ 0H e. CH ) -> ( ( S ` 0H ) .ih ( S ` ~H ) ) = 0 )
7 1 6 mpan2 
 |-  ( S e. CHStates -> ( ( S ` 0H ) .ih ( S ` ~H ) ) = 0 )
8 hstoh 
 |-  ( ( S e. CHStates /\ 0H e. CH /\ ( ( S ` 0H ) .ih ( S ` ~H ) ) = 0 ) -> ( S ` 0H ) = 0h )
9 1 8 mp3an2 
 |-  ( ( S e. CHStates /\ ( ( S ` 0H ) .ih ( S ` ~H ) ) = 0 ) -> ( S ` 0H ) = 0h )
10 7 9 mpdan 
 |-  ( S e. CHStates -> ( S ` 0H ) = 0h )