Metamath Proof Explorer

Theorem hstles

Description: Ordering property of a Hilbert-space-valued state. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hstles ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ B → norm ℎ ⁡ S ⁡ A = 1 → norm ℎ ⁡ S ⁡ B = 1

Proof

Step Hyp Ref Expression
1 simpr ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ B ∧ norm ℎ ⁡ S ⁡ A = 1 → norm ℎ ⁡ S ⁡ A = 1
2 hstle ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ B → norm ℎ ⁡ S ⁡ A ≤ norm ℎ ⁡ S ⁡ B
3 2 adantr ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ B ∧ norm ℎ ⁡ S ⁡ A = 1 → norm ℎ ⁡ S ⁡ A ≤ norm ℎ ⁡ S ⁡ B
4 1 3 eqbrtrrd ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ B ∧ norm ℎ ⁡ S ⁡ A = 1 → 1 ≤ norm ℎ ⁡ S ⁡ B
5 4 ex ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ B → norm ℎ ⁡ S ⁡ A = 1 → 1 ≤ norm ℎ ⁡ S ⁡ B
6 hstle1 ⊢ S ∈ CHStates ∧ B ∈ C ℋ → norm ℎ ⁡ S ⁡ B ≤ 1
7 6 ad2ant2r ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ B → norm ℎ ⁡ S ⁡ B ≤ 1
8 5 7 jctild ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ B → norm ℎ ⁡ S ⁡ A = 1 → norm ℎ ⁡ S ⁡ B ≤ 1 ∧ 1 ≤ norm ℎ ⁡ S ⁡ B
9 hstcl ⊢ S ∈ CHStates ∧ B ∈ C ℋ → S ⁡ B ∈ ℋ
10 normcl ⊢ S ⁡ B ∈ ℋ → norm ℎ ⁡ S ⁡ B ∈ ℝ
11 1re ⊢ 1 ∈ ℝ
12 letri3 ⊢ norm ℎ ⁡ S ⁡ B ∈ ℝ ∧ 1 ∈ ℝ → norm ℎ ⁡ S ⁡ B = 1 ↔ norm ℎ ⁡ S ⁡ B ≤ 1 ∧ 1 ≤ norm ℎ ⁡ S ⁡ B
13 11 12 mpan2 ⊢ norm ℎ ⁡ S ⁡ B ∈ ℝ → norm ℎ ⁡ S ⁡ B = 1 ↔ norm ℎ ⁡ S ⁡ B ≤ 1 ∧ 1 ≤ norm ℎ ⁡ S ⁡ B
14 9 10 13 3syl ⊢ S ∈ CHStates ∧ B ∈ C ℋ → norm ℎ ⁡ S ⁡ B = 1 ↔ norm ℎ ⁡ S ⁡ B ≤ 1 ∧ 1 ≤ norm ℎ ⁡ S ⁡ B
15 14 ad2ant2r ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ B → norm ℎ ⁡ S ⁡ B = 1 ↔ norm ℎ ⁡ S ⁡ B ≤ 1 ∧ 1 ≤ norm ℎ ⁡ S ⁡ B
16 8 15 sylibrd ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ B → norm ℎ ⁡ S ⁡ A = 1 → norm ℎ ⁡ S ⁡ B = 1