Metamath Proof Explorer


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 S CHStates S 0 = 0

Proof

Step Hyp Ref Expression
1 h0elch 0 C
2 helch C
3 2 choccli C
4 3 ch0lei 0
5 hstorth S CHStates 0 C C 0 S 0 ih S = 0
6 2 4 5 mpanr12 S CHStates 0 C S 0 ih S = 0
7 1 6 mpan2 S CHStates S 0 ih S = 0
8 hstoh S CHStates 0 C S 0 ih S = 0 S 0 = 0
9 1 8 mp3an2 S CHStates S 0 ih S = 0 S 0 = 0
10 7 9 mpdan S CHStates S 0 = 0