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