Theorem st0

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

	Ref	Expression
Assertion	st0	|- ( S e. States -> ( S ` 0H ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		helch	|- ~H e. CH
2	1	sto2i	|- ( S e. States -> ( S ` ( _|_ ` ~H ) ) = ( 1 - ( S ` ~H ) ) )
3		sthil	|- ( S e. States -> ( S ` ~H ) = 1 )
4	3	oveq2d	|- ( S e. States -> ( 1 - ( S ` ~H ) ) = ( 1 - 1 ) )
5	2 4	eqtrd	|- ( S e. States -> ( S ` ( _|_ ` ~H ) ) = ( 1 - 1 ) )
6		choc1	|- ( _|_ ` ~H ) = 0H
7	6	fveq2i	|- ( S ` ( _|_ ` ~H ) ) = ( S ` 0H )
8		1m1e0	|- ( 1 - 1 ) = 0
9	5 7 8	3eqtr3g	|- ( S e. States -> ( S ` 0H ) = 0 )