Metamath Proof Explorer

Theorem hstnmoc

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

Ref Expression
Assertion hstnmoc ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {{norm}_{ℎ}\left({S}\left({A}\right)\right)}^{2}+{{norm}_{ℎ}\left({S}\left(\perp \left({A}\right)\right)\right)}^{2}=1$

Proof

Step Hyp Ref Expression
1 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)$
2 1 fveq2d ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {norm}_{ℎ}\left({S}\left({A}\right){+}_{ℎ}{S}\left(\perp \left({A}\right)\right)\right)={norm}_{ℎ}\left({S}\left(ℋ\right)\right)$
3 2 oveq1d ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {{norm}_{ℎ}\left({S}\left({A}\right){+}_{ℎ}{S}\left(\perp \left({A}\right)\right)\right)}^{2}={{norm}_{ℎ}\left({S}\left(ℋ\right)\right)}^{2}$
4 hstcl ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {S}\left({A}\right)\in ℋ$
5 choccl ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \perp \left({A}\right)\in {\mathbf{C}}_{ℋ}$
6 hstcl ${⊢}\left({S}\in \mathrm{CHStates}\wedge \perp \left({A}\right)\in {\mathbf{C}}_{ℋ}\right)\to {S}\left(\perp \left({A}\right)\right)\in ℋ$
7 5 6 sylan2 ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {S}\left(\perp \left({A}\right)\right)\in ℋ$
8 4 7 jca ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to \left({S}\left({A}\right)\in ℋ\wedge {S}\left(\perp \left({A}\right)\right)\in ℋ\right)$
9 5 adantl ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left({A}\right)\in {\mathbf{C}}_{ℋ}$
10 chsh ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to {A}\in {\mathbf{S}}_{ℋ}$
11 shococss ${⊢}{A}\in {\mathbf{S}}_{ℋ}\to {A}\subseteq \perp \left(\perp \left({A}\right)\right)$
12 10 11 syl ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to {A}\subseteq \perp \left(\perp \left({A}\right)\right)$
13 12 adantl ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {A}\subseteq \perp \left(\perp \left({A}\right)\right)$
14 9 13 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)$
15 hstorth ${⊢}\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}\right){\cdot }_{\mathrm{ih}}{S}\left(\perp \left({A}\right)\right)=0$
16 14 15 mpdan ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {S}\left({A}\right){\cdot }_{\mathrm{ih}}{S}\left(\perp \left({A}\right)\right)=0$
17 normpyth ${⊢}\left({S}\left({A}\right)\in ℋ\wedge {S}\left(\perp \left({A}\right)\right)\in ℋ\right)\to \left({S}\left({A}\right){\cdot }_{\mathrm{ih}}{S}\left(\perp \left({A}\right)\right)=0\to {{norm}_{ℎ}\left({S}\left({A}\right){+}_{ℎ}{S}\left(\perp \left({A}\right)\right)\right)}^{2}={{norm}_{ℎ}\left({S}\left({A}\right)\right)}^{2}+{{norm}_{ℎ}\left({S}\left(\perp \left({A}\right)\right)\right)}^{2}\right)$
18 8 16 17 sylc ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {{norm}_{ℎ}\left({S}\left({A}\right){+}_{ℎ}{S}\left(\perp \left({A}\right)\right)\right)}^{2}={{norm}_{ℎ}\left({S}\left({A}\right)\right)}^{2}+{{norm}_{ℎ}\left({S}\left(\perp \left({A}\right)\right)\right)}^{2}$
19 hst1a ${⊢}{S}\in \mathrm{CHStates}\to {norm}_{ℎ}\left({S}\left(ℋ\right)\right)=1$
20 19 oveq1d ${⊢}{S}\in \mathrm{CHStates}\to {{norm}_{ℎ}\left({S}\left(ℋ\right)\right)}^{2}={1}^{2}$
21 sq1 ${⊢}{1}^{2}=1$
22 20 21 syl6eq ${⊢}{S}\in \mathrm{CHStates}\to {{norm}_{ℎ}\left({S}\left(ℋ\right)\right)}^{2}=1$
23 22 adantr ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {{norm}_{ℎ}\left({S}\left(ℋ\right)\right)}^{2}=1$
24 3 18 23 3eqtr3d ${⊢}\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {{norm}_{ℎ}\left({S}\left({A}\right)\right)}^{2}+{{norm}_{ℎ}\left({S}\left(\perp \left({A}\right)\right)\right)}^{2}=1$