Metamath Proof Explorer

Theorem hstle1

Description: The norm of the value of a Hilbert-space-valued state is less than or equal to one. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hstle1 ⊢ S ∈ CHStates ∧ A ∈ C ℋ → norm ℎ ⁡ S ⁡ A ≤ 1

Proof

Step Hyp Ref Expression
1 choccl ⊢ A ∈ C ℋ → ⊥ ⁡ A ∈ C ℋ
2 hstcl ⊢ S ∈ CHStates ∧ ⊥ ⁡ A ∈ C ℋ → S ⁡ ⊥ ⁡ A ∈ ℋ
3 1 2 sylan2 ⊢ S ∈ CHStates ∧ A ∈ C ℋ → S ⁡ ⊥ ⁡ A ∈ ℋ
4 normcl ⊢ S ⁡ ⊥ ⁡ A ∈ ℋ → norm ℎ ⁡ S ⁡ ⊥ ⁡ A ∈ ℝ
5 3 4 syl ⊢ S ∈ CHStates ∧ A ∈ C ℋ → norm ℎ ⁡ S ⁡ ⊥ ⁡ A ∈ ℝ
6 5 sqge0d ⊢ S ∈ CHStates ∧ A ∈ C ℋ → 0 ≤ norm ℎ ⁡ S ⁡ ⊥ ⁡ A 2
7 hstcl ⊢ S ∈ CHStates ∧ A ∈ C ℋ → S ⁡ A ∈ ℋ
8 normcl ⊢ S ⁡ A ∈ ℋ → norm ℎ ⁡ S ⁡ A ∈ ℝ
9 7 8 syl ⊢ S ∈ CHStates ∧ A ∈ C ℋ → norm ℎ ⁡ S ⁡ A ∈ ℝ
10 9 resqcld ⊢ S ∈ CHStates ∧ A ∈ C ℋ → norm ℎ ⁡ S ⁡ A 2 ∈ ℝ
11 5 resqcld ⊢ S ∈ CHStates ∧ A ∈ C ℋ → norm ℎ ⁡ S ⁡ ⊥ ⁡ A 2 ∈ ℝ
12 10 11 addge01d ⊢ S ∈ CHStates ∧ A ∈ C ℋ → 0 ≤ norm ℎ ⁡ S ⁡ ⊥ ⁡ A 2 ↔ norm ℎ ⁡ S ⁡ A 2 ≤ norm ℎ ⁡ S ⁡ A 2 + norm ℎ ⁡ S ⁡ ⊥ ⁡ A 2
13 6 12 mpbid ⊢ S ∈ CHStates ∧ A ∈ C ℋ → norm ℎ ⁡ S ⁡ A 2 ≤ norm ℎ ⁡ S ⁡ A 2 + norm ℎ ⁡ S ⁡ ⊥ ⁡ A 2
14 hstnmoc ⊢ S ∈ CHStates ∧ A ∈ C ℋ → norm ℎ ⁡ S ⁡ A 2 + norm ℎ ⁡ S ⁡ ⊥ ⁡ A 2 = 1
15 sq1 ⊢ 1 2 = 1
16 14 15 eqtr4di ⊢ S ∈ CHStates ∧ A ∈ C ℋ → norm ℎ ⁡ S ⁡ A 2 + norm ℎ ⁡ S ⁡ ⊥ ⁡ A 2 = 1 2
17 13 16 breqtrd ⊢ S ∈ CHStates ∧ A ∈ C ℋ → norm ℎ ⁡ S ⁡ A 2 ≤ 1 2
18 normge0 ⊢ S ⁡ A ∈ ℋ → 0 ≤ norm ℎ ⁡ S ⁡ A
19 7 18 syl ⊢ S ∈ CHStates ∧ A ∈ C ℋ → 0 ≤ norm ℎ ⁡ S ⁡ A
20 1re ⊢ 1 ∈ ℝ
21 0le1 ⊢ 0 ≤ 1
22 le2sq ⊢ norm ℎ ⁡ S ⁡ A ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ S ⁡ A ∧ 1 ∈ ℝ ∧ 0 ≤ 1 → norm ℎ ⁡ S ⁡ A ≤ 1 ↔ norm ℎ ⁡ S ⁡ A 2 ≤ 1 2
23 20 21 22 mpanr12 ⊢ norm ℎ ⁡ S ⁡ A ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ S ⁡ A → norm ℎ ⁡ S ⁡ A ≤ 1 ↔ norm ℎ ⁡ S ⁡ A 2 ≤ 1 2
24 9 19 23 syl2anc ⊢ S ∈ CHStates ∧ A ∈ C ℋ → norm ℎ ⁡ S ⁡ A ≤ 1 ↔ norm ℎ ⁡ S ⁡ A 2 ≤ 1 2
25 17 24 mpbird ⊢ S ∈ CHStates ∧ A ∈ C ℋ → norm ℎ ⁡ S ⁡ A ≤ 1