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 ⁡ A 2 + norm ℎ ⁡ S ⁡ ⊥ ⁡ A 2 = 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 ⁡ ⊥ ⁡ A 2 = 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 ⋅ ih S ⁡ ⊥ ⁡ A = 0
16 14 15 mpdan ⊢ S ∈ CHStates ∧ A ∈ C ℋ → S ⁡ A ⋅ ih S ⁡ ⊥ ⁡ A = 0
17 normpyth ⊢ S ⁡ A ∈ ℋ ∧ S ⁡ ⊥ ⁡ A ∈ ℋ → S ⁡ A ⋅ ih S ⁡ ⊥ ⁡ A = 0 → norm ℎ ⁡ S ⁡ A + ℎ S ⁡ ⊥ ⁡ A 2 = norm ℎ ⁡ S ⁡ A 2 + norm ℎ ⁡ S ⁡ ⊥ ⁡ A 2
18 8 16 17 sylc ⊢ S ∈ CHStates ∧ A ∈ C ℋ → norm ℎ ⁡ S ⁡ A + ℎ S ⁡ ⊥ ⁡ A 2 = norm ℎ ⁡ S ⁡ A 2 + norm ℎ ⁡ S ⁡ ⊥ ⁡ A 2
19 hst1a ⊢ S ∈ CHStates → norm ℎ ⁡ S ⁡ ℋ = 1
20 19 oveq1d ⊢ S ∈ CHStates → norm ℎ ⁡ S ⁡ ℋ 2 = 1 2
21 sq1 ⊢ 1 2 = 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 ⁡ A 2 + norm ℎ ⁡ S ⁡ ⊥ ⁡ A 2 = 1