# 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 ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {S}\left({A}\right){+}_{ℎ}{S}\left(\perp \left({A}\right)\right)={S}\left(ℋ\right)$

### Proof

Step Hyp Ref Expression
1 choccl ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \perp \left({A}\right)\in {\mathbf{C}}_{ℋ}$
2 1 adantl ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left({A}\right)\in {\mathbf{C}}_{ℋ}$
3 chsh ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to {A}\in {\mathbf{S}}_{ℋ}$
4 shococss ${⊢}{A}\in {\mathbf{S}}_{ℋ}\to {A}\subseteq \perp \left(\perp \left({A}\right)\right)$
5 3 4 syl ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to {A}\subseteq \perp \left(\perp \left({A}\right)\right)$
6 5 adantl ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {A}\subseteq \perp \left(\perp \left({A}\right)\right)$
7 2 6 jca ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to \left(\perp \left({A}\right)\in {\mathbf{C}}_{ℋ}\wedge {A}\subseteq \perp \left(\perp \left({A}\right)\right)\right)$
8 hstosum ${⊢}\left(\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\wedge \left(\perp \left({A}\right)\in {\mathbf{C}}_{ℋ}\wedge {A}\subseteq \perp \left(\perp \left({A}\right)\right)\right)\right)\to {S}\left({A}{\vee }_{ℋ}\perp \left({A}\right)\right)={S}\left({A}\right){+}_{ℎ}{S}\left(\perp \left({A}\right)\right)$
9 7 8 mpdan ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {S}\left({A}{\vee }_{ℋ}\perp \left({A}\right)\right)={S}\left({A}\right){+}_{ℎ}{S}\left(\perp \left({A}\right)\right)$
10 chjo ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to {A}{\vee }_{ℋ}\perp \left({A}\right)=ℋ$
11 10 fveq2d ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to {S}\left({A}{\vee }_{ℋ}\perp \left({A}\right)\right)={S}\left(ℋ\right)$
12 11 adantl ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {S}\left({A}{\vee }_{ℋ}\perp \left({A}\right)\right)={S}\left(ℋ\right)$
13 9 12 eqtr3d ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {S}\left({A}\right){+}_{ℎ}{S}\left(\perp \left({A}\right)\right)={S}\left(ℋ\right)$