Metamath Proof Explorer


Theorem hst0h

Description: The norm of a Hilbert-space-valued state equals zero iff the state value equals zero. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hst0h ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) → ( ( norm ‘ ( 𝑆𝐴 ) ) = 0 ↔ ( 𝑆𝐴 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 hstcl ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) → ( 𝑆𝐴 ) ∈ ℋ )
2 norm-i ( ( 𝑆𝐴 ) ∈ ℋ → ( ( norm ‘ ( 𝑆𝐴 ) ) = 0 ↔ ( 𝑆𝐴 ) = 0 ) )
3 1 2 syl ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) → ( ( norm ‘ ( 𝑆𝐴 ) ) = 0 ↔ ( 𝑆𝐴 ) = 0 ) )