# 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 ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) → ( ( 𝑆𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = ( 𝑆 ‘ ℋ ) )

### Proof

Step Hyp Ref Expression
1 choccl ( 𝐴C → ( ⊥ ‘ 𝐴 ) ∈ C )
2 1 adantl ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) → ( ⊥ ‘ 𝐴 ) ∈ C )
3 chsh ( 𝐴C𝐴S )
4 shococss ( 𝐴S𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
5 3 4 syl ( 𝐴C𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
6 5 adantl ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
7 2 6 jca ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) → ( ( ⊥ ‘ 𝐴 ) ∈ C𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) )
8 hstosum ( ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) ∧ ( ( ⊥ ‘ 𝐴 ) ∈ C𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) ) → ( 𝑆 ‘ ( 𝐴 ( ⊥ ‘ 𝐴 ) ) ) = ( ( 𝑆𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) )
9 7 8 mpdan ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) → ( 𝑆 ‘ ( 𝐴 ( ⊥ ‘ 𝐴 ) ) ) = ( ( 𝑆𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) )
10 chjo ( 𝐴C → ( 𝐴 ( ⊥ ‘ 𝐴 ) ) = ℋ )
11 10 fveq2d ( 𝐴C → ( 𝑆 ‘ ( 𝐴 ( ⊥ ‘ 𝐴 ) ) ) = ( 𝑆 ‘ ℋ ) )
12 11 adantl ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) → ( 𝑆 ‘ ( 𝐴 ( ⊥ ‘ 𝐴 ) ) ) = ( 𝑆 ‘ ℋ ) )
13 9 12 eqtr3d ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) → ( ( 𝑆𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = ( 𝑆 ‘ ℋ ) )