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 ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ≤ 1 )

Proof

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