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	\|- ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) = 0 <-> ( S ` A ) = 0h ) )

Proof

Step	Hyp	Ref	Expression
1		hstcl	\|- ( ( S e. CHStates /\ A e. CH ) -> ( S ` A ) e. ~H )
2		norm-i	\|- ( ( S ` A ) e. ~H -> ( ( normh ` ( S ` A ) ) = 0 <-> ( S ` A ) = 0h ) )
3	1 2	syl	\|- ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) = 0 <-> ( S ` A ) = 0h ) )

Step

Hyp

Ref

Expression

hstcl

 |-  ( ( S e. CHStates /\ A e. CH ) -> ( S ` A ) e. ~H )

norm-i

 |-  ( ( S ` A ) e. ~H -> ( ( normh ` ( S ` A ) ) = 0 <-> ( S ` A ) = 0h ) )

1 2

syl

 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` A ) ) = 0 <-> ( S ` A ) = 0h ) )