# Metamath Proof Explorer

## Theorem hstoc

Description: Sum of a Hilbert-space-valued state of a lattice element and its orthocomplement. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hstoc
`|- ( ( S e. CHStates /\ A e. CH ) -> ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) = ( S ` ~H ) )`

### Proof

Step Hyp Ref Expression
1 choccl
` |-  ( A e. CH -> ( _|_ ` A ) e. CH )`
` |-  ( ( S e. CHStates /\ A e. CH ) -> ( _|_ ` A ) e. CH )`
3 chsh
` |-  ( A e. CH -> A e. SH )`
4 shococss
` |-  ( A e. SH -> A C_ ( _|_ ` ( _|_ ` A ) ) )`
5 3 4 syl
` |-  ( A e. CH -> A C_ ( _|_ ` ( _|_ ` A ) ) )`
` |-  ( ( S e. CHStates /\ A e. CH ) -> A C_ ( _|_ ` ( _|_ ` A ) ) )`
7 2 6 jca
` |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( _|_ ` A ) e. CH /\ A C_ ( _|_ ` ( _|_ ` A ) ) ) )`
8 hstosum
` |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( ( _|_ ` A ) e. CH /\ A C_ ( _|_ ` ( _|_ ` A ) ) ) ) -> ( S ` ( A vH ( _|_ ` A ) ) ) = ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) )`
9 7 8 mpdan
` |-  ( ( S e. CHStates /\ A e. CH ) -> ( S ` ( A vH ( _|_ ` A ) ) ) = ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) )`
10 chjo
` |-  ( A e. CH -> ( A vH ( _|_ ` A ) ) = ~H )`
11 10 fveq2d
` |-  ( A e. CH -> ( S ` ( A vH ( _|_ ` A ) ) ) = ( S ` ~H ) )`
` |-  ( ( S e. CHStates /\ A e. CH ) -> ( S ` ( A vH ( _|_ ` A ) ) ) = ( S ` ~H ) )`
` |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) = ( S ` ~H ) )`