Theorem hst0

Description: A Hilbert-space-valued state is zero at the zero subspace. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hst0	⊢ ( 𝑆 ∈ CHStates → ( 𝑆 ‘ 0ℋ ) = 0ℎ )

Proof

Step	Hyp	Ref	Expression
1		h0elch	⊢ 0ℋ ∈ Cℋ
2		helch	⊢ ℋ ∈ Cℋ
3	2	choccli	⊢ ( ⊥ ‘ ℋ ) ∈ Cℋ
4	3	ch0lei	⊢ 0ℋ ⊆ ( ⊥ ‘ ℋ )
5		hstorth	⊢ ( ( ( 𝑆 ∈ CHStates ∧ 0ℋ ∈ Cℋ ) ∧ ( ℋ ∈ Cℋ ∧ 0ℋ ⊆ ( ⊥ ‘ ℋ ) ) ) → ( ( 𝑆 ‘ 0ℋ ) ·ih ( 𝑆 ‘ ℋ ) ) = 0 )
6	2 4 5	mpanr12	⊢ ( ( 𝑆 ∈ CHStates ∧ 0ℋ ∈ Cℋ ) → ( ( 𝑆 ‘ 0ℋ ) ·ih ( 𝑆 ‘ ℋ ) ) = 0 )
7	1 6	mpan2	⊢ ( 𝑆 ∈ CHStates → ( ( 𝑆 ‘ 0ℋ ) ·ih ( 𝑆 ‘ ℋ ) ) = 0 )
8		hstoh	⊢ ( ( 𝑆 ∈ CHStates ∧ 0ℋ ∈ Cℋ ∧ ( ( 𝑆 ‘ 0ℋ ) ·ih ( 𝑆 ‘ ℋ ) ) = 0 ) → ( 𝑆 ‘ 0ℋ ) = 0ℎ )
9	1 8	mp3an2	⊢ ( ( 𝑆 ∈ CHStates ∧ ( ( 𝑆 ‘ 0ℋ ) ·ih ( 𝑆 ‘ ℋ ) ) = 0 ) → ( 𝑆 ‘ 0ℋ ) = 0ℎ )
10	7 9	mpdan	⊢ ( 𝑆 ∈ CHStates → ( 𝑆 ‘ 0ℋ ) = 0ℎ )