# Metamath Proof Explorer

## Theorem ishst

Description: Property of a complex Hilbert-space-valued state. Definition of CH-states in Mayet3 p. 9. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion ishst ${⊢}{S}\in \mathrm{CHStates}↔\left({S}:{\mathbf{C}}_{ℋ}⟶ℋ\wedge {norm}_{ℎ}\left({S}\left(ℋ\right)\right)=1\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to \left({S}\left({x}\right){\cdot }_{\mathrm{ih}}{S}\left({y}\right)=0\wedge {S}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}\right){+}_{ℎ}{S}\left({y}\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 ax-hilex ${⊢}ℋ\in \mathrm{V}$
2 chex ${⊢}{\mathbf{C}}_{ℋ}\in \mathrm{V}$
3 1 2 elmap ${⊢}{S}\in \left({ℋ}^{{\mathbf{C}}_{ℋ}}\right)↔{S}:{\mathbf{C}}_{ℋ}⟶ℋ$
4 3 anbi1i ${⊢}\left({S}\in \left({ℋ}^{{\mathbf{C}}_{ℋ}}\right)\wedge \left({norm}_{ℎ}\left({S}\left(ℋ\right)\right)=1\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to \left({S}\left({x}\right){\cdot }_{\mathrm{ih}}{S}\left({y}\right)=0\wedge {S}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}\right){+}_{ℎ}{S}\left({y}\right)\right)\right)\right)\right)↔\left({S}:{\mathbf{C}}_{ℋ}⟶ℋ\wedge \left({norm}_{ℎ}\left({S}\left(ℋ\right)\right)=1\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to \left({S}\left({x}\right){\cdot }_{\mathrm{ih}}{S}\left({y}\right)=0\wedge {S}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}\right){+}_{ℎ}{S}\left({y}\right)\right)\right)\right)\right)$
5 fveq1 ${⊢}{f}={S}\to {f}\left(ℋ\right)={S}\left(ℋ\right)$
6 5 fveqeq2d ${⊢}{f}={S}\to \left({norm}_{ℎ}\left({f}\left(ℋ\right)\right)=1↔{norm}_{ℎ}\left({S}\left(ℋ\right)\right)=1\right)$
7 fveq1 ${⊢}{f}={S}\to {f}\left({x}\right)={S}\left({x}\right)$
8 fveq1 ${⊢}{f}={S}\to {f}\left({y}\right)={S}\left({y}\right)$
9 7 8 oveq12d ${⊢}{f}={S}\to {f}\left({x}\right){\cdot }_{\mathrm{ih}}{f}\left({y}\right)={S}\left({x}\right){\cdot }_{\mathrm{ih}}{S}\left({y}\right)$
10 9 eqeq1d ${⊢}{f}={S}\to \left({f}\left({x}\right){\cdot }_{\mathrm{ih}}{f}\left({y}\right)=0↔{S}\left({x}\right){\cdot }_{\mathrm{ih}}{S}\left({y}\right)=0\right)$
11 fveq1 ${⊢}{f}={S}\to {f}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}{\vee }_{ℋ}{y}\right)$
12 7 8 oveq12d ${⊢}{f}={S}\to {f}\left({x}\right){+}_{ℎ}{f}\left({y}\right)={S}\left({x}\right){+}_{ℎ}{S}\left({y}\right)$
13 11 12 eqeq12d ${⊢}{f}={S}\to \left({f}\left({x}{\vee }_{ℋ}{y}\right)={f}\left({x}\right){+}_{ℎ}{f}\left({y}\right)↔{S}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}\right){+}_{ℎ}{S}\left({y}\right)\right)$
14 10 13 anbi12d ${⊢}{f}={S}\to \left(\left({f}\left({x}\right){\cdot }_{\mathrm{ih}}{f}\left({y}\right)=0\wedge {f}\left({x}{\vee }_{ℋ}{y}\right)={f}\left({x}\right){+}_{ℎ}{f}\left({y}\right)\right)↔\left({S}\left({x}\right){\cdot }_{\mathrm{ih}}{S}\left({y}\right)=0\wedge {S}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}\right){+}_{ℎ}{S}\left({y}\right)\right)\right)$
15 14 imbi2d ${⊢}{f}={S}\to \left(\left({x}\subseteq \perp \left({y}\right)\to \left({f}\left({x}\right){\cdot }_{\mathrm{ih}}{f}\left({y}\right)=0\wedge {f}\left({x}{\vee }_{ℋ}{y}\right)={f}\left({x}\right){+}_{ℎ}{f}\left({y}\right)\right)\right)↔\left({x}\subseteq \perp \left({y}\right)\to \left({S}\left({x}\right){\cdot }_{\mathrm{ih}}{S}\left({y}\right)=0\wedge {S}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}\right){+}_{ℎ}{S}\left({y}\right)\right)\right)\right)$
16 15 2ralbidv ${⊢}{f}={S}\to \left(\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to \left({f}\left({x}\right){\cdot }_{\mathrm{ih}}{f}\left({y}\right)=0\wedge {f}\left({x}{\vee }_{ℋ}{y}\right)={f}\left({x}\right){+}_{ℎ}{f}\left({y}\right)\right)\right)↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to \left({S}\left({x}\right){\cdot }_{\mathrm{ih}}{S}\left({y}\right)=0\wedge {S}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}\right){+}_{ℎ}{S}\left({y}\right)\right)\right)\right)$
17 6 16 anbi12d ${⊢}{f}={S}\to \left(\left({norm}_{ℎ}\left({f}\left(ℋ\right)\right)=1\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to \left({f}\left({x}\right){\cdot }_{\mathrm{ih}}{f}\left({y}\right)=0\wedge {f}\left({x}{\vee }_{ℋ}{y}\right)={f}\left({x}\right){+}_{ℎ}{f}\left({y}\right)\right)\right)\right)↔\left({norm}_{ℎ}\left({S}\left(ℋ\right)\right)=1\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to \left({S}\left({x}\right){\cdot }_{\mathrm{ih}}{S}\left({y}\right)=0\wedge {S}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}\right){+}_{ℎ}{S}\left({y}\right)\right)\right)\right)\right)$
18 df-hst ${⊢}\mathrm{CHStates}=\left\{{f}\in \left({ℋ}^{{\mathbf{C}}_{ℋ}}\right)|\left({norm}_{ℎ}\left({f}\left(ℋ\right)\right)=1\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to \left({f}\left({x}\right){\cdot }_{\mathrm{ih}}{f}\left({y}\right)=0\wedge {f}\left({x}{\vee }_{ℋ}{y}\right)={f}\left({x}\right){+}_{ℎ}{f}\left({y}\right)\right)\right)\right)\right\}$
19 17 18 elrab2 ${⊢}{S}\in \mathrm{CHStates}↔\left({S}\in \left({ℋ}^{{\mathbf{C}}_{ℋ}}\right)\wedge \left({norm}_{ℎ}\left({S}\left(ℋ\right)\right)=1\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to \left({S}\left({x}\right){\cdot }_{\mathrm{ih}}{S}\left({y}\right)=0\wedge {S}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}\right){+}_{ℎ}{S}\left({y}\right)\right)\right)\right)\right)$
20 3anass ${⊢}\left({S}:{\mathbf{C}}_{ℋ}⟶ℋ\wedge {norm}_{ℎ}\left({S}\left(ℋ\right)\right)=1\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to \left({S}\left({x}\right){\cdot }_{\mathrm{ih}}{S}\left({y}\right)=0\wedge {S}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}\right){+}_{ℎ}{S}\left({y}\right)\right)\right)\right)↔\left({S}:{\mathbf{C}}_{ℋ}⟶ℋ\wedge \left({norm}_{ℎ}\left({S}\left(ℋ\right)\right)=1\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to \left({S}\left({x}\right){\cdot }_{\mathrm{ih}}{S}\left({y}\right)=0\wedge {S}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}\right){+}_{ℎ}{S}\left({y}\right)\right)\right)\right)\right)$
21 4 19 20 3bitr4i ${⊢}{S}\in \mathrm{CHStates}↔\left({S}:{\mathbf{C}}_{ℋ}⟶ℋ\wedge {norm}_{ℎ}\left({S}\left(ℋ\right)\right)=1\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to \left({S}\left({x}\right){\cdot }_{\mathrm{ih}}{S}\left({y}\right)=0\wedge {S}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}\right){+}_{ℎ}{S}\left({y}\right)\right)\right)\right)$