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 ⊢S∈CHStates∧A∈Cℋ→normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡A2=1

Proof

Step Hyp Ref Expression
1 hstoc ⊢S∈CHStates∧A∈Cℋ→S⁡A+ℎS⁡⊥⁡A=S⁡ℋ
2 1 fveq2d ⊢S∈CHStates∧A∈Cℋ→normℎ⁡S⁡A+ℎS⁡⊥⁡A=normℎ⁡S⁡ℋ
3 2 oveq1d ⊢S∈CHStates∧A∈Cℋ→normℎ⁡S⁡A+ℎS⁡⊥⁡A2=normℎ⁡S⁡ℋ2
4 hstcl ⊢S∈CHStates∧A∈Cℋ→S⁡A∈ℋ
5 choccl ⊢A∈Cℋ→⊥⁡A∈Cℋ
6 hstcl ⊢S∈CHStates∧⊥⁡A∈Cℋ→S⁡⊥⁡A∈ℋ
7 5 6 sylan2 ⊢S∈CHStates∧A∈Cℋ→S⁡⊥⁡A∈ℋ
8 4 7 jca ⊢S∈CHStates∧A∈Cℋ→S⁡A∈ℋ∧S⁡⊥⁡A∈ℋ
9 5 adantl ⊢S∈CHStates∧A∈Cℋ→⊥⁡A∈Cℋ
10 chsh ⊢A∈Cℋ→A∈Sℋ
11 shococss ⊢A∈Sℋ→A⊆⊥⁡⊥⁡A
12 10 11 syl ⊢A∈Cℋ→A⊆⊥⁡⊥⁡A
13 12 adantl ⊢S∈CHStates∧A∈Cℋ→A⊆⊥⁡⊥⁡A
14 9 13 jca ⊢S∈CHStates∧A∈Cℋ→⊥⁡A∈Cℋ∧A⊆⊥⁡⊥⁡A
15 hstorth ⊢S∈CHStates∧A∈Cℋ∧⊥⁡A∈Cℋ∧A⊆⊥⁡⊥⁡A→S⁡A⋅ihS⁡⊥⁡A=0
16 14 15 mpdan ⊢S∈CHStates∧A∈Cℋ→S⁡A⋅ihS⁡⊥⁡A=0
17 normpyth ⊢S⁡A∈ℋ∧S⁡⊥⁡A∈ℋ→S⁡A⋅ihS⁡⊥⁡A=0→normℎ⁡S⁡A+ℎS⁡⊥⁡A2=normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡A2
18 8 16 17 sylc ⊢S∈CHStates∧A∈Cℋ→normℎ⁡S⁡A+ℎS⁡⊥⁡A2=normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡A2
19 hst1a ⊢S∈CHStates→normℎ⁡S⁡ℋ=1
20 19 oveq1d ⊢S∈CHStates→normℎ⁡S⁡ℋ2=12
21 sq1 ⊢12=1
22 20 21 eqtrdi ⊢S∈CHStates→normℎ⁡S⁡ℋ2=1
23 22 adantr ⊢S∈CHStates∧A∈Cℋ→normℎ⁡S⁡ℋ2=1
24 3 18 23 3eqtr3d ⊢S∈CHStates∧A∈Cℋ→normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡A2=1