Theorem hst1a

Description: Unit value of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hst1a	⊢ ( 𝑆 ∈ CHStates → ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		ishst	⊢ ( 𝑆 ∈ CHStates ↔ ( 𝑆 : Cℋ ⟶ ℋ ∧ ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑆 ‘ 𝑥 ) ·ih ( 𝑆 ‘ 𝑦 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑦 ) ) ) ) ) )
2	1	simp2bi	⊢ ( 𝑆 ∈ CHStates → ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 )