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

Proof

Step Hyp Ref Expression
1 simpr ( ( ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) ∧ ( 𝐵C𝐴𝐵 ) ) ∧ ( norm ‘ ( 𝑆𝐴 ) ) = 1 ) → ( norm ‘ ( 𝑆𝐴 ) ) = 1 )
2 hstle ( ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) ∧ ( 𝐵C𝐴𝐵 ) ) → ( norm ‘ ( 𝑆𝐴 ) ) ≤ ( norm ‘ ( 𝑆𝐵 ) ) )
3 2 adantr ( ( ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) ∧ ( 𝐵C𝐴𝐵 ) ) ∧ ( norm ‘ ( 𝑆𝐴 ) ) = 1 ) → ( norm ‘ ( 𝑆𝐴 ) ) ≤ ( norm ‘ ( 𝑆𝐵 ) ) )
4 1 3 eqbrtrrd ( ( ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) ∧ ( 𝐵C𝐴𝐵 ) ) ∧ ( norm ‘ ( 𝑆𝐴 ) ) = 1 ) → 1 ≤ ( norm ‘ ( 𝑆𝐵 ) ) )
5 4 ex ( ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) ∧ ( 𝐵C𝐴𝐵 ) ) → ( ( norm ‘ ( 𝑆𝐴 ) ) = 1 → 1 ≤ ( norm ‘ ( 𝑆𝐵 ) ) ) )
6 hstle1 ( ( 𝑆 ∈ CHStates ∧ 𝐵C ) → ( norm ‘ ( 𝑆𝐵 ) ) ≤ 1 )
7 6 ad2ant2r ( ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) ∧ ( 𝐵C𝐴𝐵 ) ) → ( norm ‘ ( 𝑆𝐵 ) ) ≤ 1 )
8 5 7 jctild ( ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) ∧ ( 𝐵C𝐴𝐵 ) ) → ( ( norm ‘ ( 𝑆𝐴 ) ) = 1 → ( ( norm ‘ ( 𝑆𝐵 ) ) ≤ 1 ∧ 1 ≤ ( norm ‘ ( 𝑆𝐵 ) ) ) ) )
9 hstcl ( ( 𝑆 ∈ CHStates ∧ 𝐵C ) → ( 𝑆𝐵 ) ∈ ℋ )
10 normcl ( ( 𝑆𝐵 ) ∈ ℋ → ( norm ‘ ( 𝑆𝐵 ) ) ∈ ℝ )
11 1re 1 ∈ ℝ
12 letri3 ( ( ( norm ‘ ( 𝑆𝐵 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( norm ‘ ( 𝑆𝐵 ) ) = 1 ↔ ( ( norm ‘ ( 𝑆𝐵 ) ) ≤ 1 ∧ 1 ≤ ( norm ‘ ( 𝑆𝐵 ) ) ) ) )
13 11 12 mpan2 ( ( norm ‘ ( 𝑆𝐵 ) ) ∈ ℝ → ( ( norm ‘ ( 𝑆𝐵 ) ) = 1 ↔ ( ( norm ‘ ( 𝑆𝐵 ) ) ≤ 1 ∧ 1 ≤ ( norm ‘ ( 𝑆𝐵 ) ) ) ) )
14 9 10 13 3syl ( ( 𝑆 ∈ CHStates ∧ 𝐵C ) → ( ( norm ‘ ( 𝑆𝐵 ) ) = 1 ↔ ( ( norm ‘ ( 𝑆𝐵 ) ) ≤ 1 ∧ 1 ≤ ( norm ‘ ( 𝑆𝐵 ) ) ) ) )
15 14 ad2ant2r ( ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) ∧ ( 𝐵C𝐴𝐵 ) ) → ( ( norm ‘ ( 𝑆𝐵 ) ) = 1 ↔ ( ( norm ‘ ( 𝑆𝐵 ) ) ≤ 1 ∧ 1 ≤ ( norm ‘ ( 𝑆𝐵 ) ) ) ) )
16 8 15 sylibrd ( ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) ∧ ( 𝐵C𝐴𝐵 ) ) → ( ( norm ‘ ( 𝑆𝐴 ) ) = 1 → ( norm ‘ ( 𝑆𝐵 ) ) = 1 ) )