Theorem st0

Description: The state of the zero subspace. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	st0	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 0ℋ ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		helch	⊢ ℋ ∈ Cℋ
2	1	sto2i	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ( ⊥ ‘ ℋ ) ) = ( 1 − ( 𝑆 ‘ ℋ ) ) )
3		sthil	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ℋ ) = 1 )
4	3	oveq2d	⊢ ( 𝑆 ∈ States → ( 1 − ( 𝑆 ‘ ℋ ) ) = ( 1 − 1 ) )
5	2 4	eqtrd	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ( ⊥ ‘ ℋ ) ) = ( 1 − 1 ) )
6		choc1	⊢ ( ⊥ ‘ ℋ ) = 0ℋ
7	6	fveq2i	⊢ ( 𝑆 ‘ ( ⊥ ‘ ℋ ) ) = ( 𝑆 ‘ 0ℋ )
8		1m1e0	⊢ ( 1 − 1 ) = 0
9	5 7 8	3eqtr3g	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 0ℋ ) = 0 )