Theorem sto1i

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

	Ref	Expression
Hypothesis	sto1.1	|- A e. CH
Assertion	sto1i	|- ( S e. States -> ( ( S ` A ) + ( S ` ( _|_ ` A ) ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		sto1.1	|- A e. CH
2	1	chjoi	|- ( A vH ( _|_ ` A ) ) = ~H
3	2	fveq2i	|- ( S ` ( A vH ( _|_ ` A ) ) ) = ( S ` ~H )
4	1	choccli	|- ( _|_ ` A ) e. CH
5	1 4	pm3.2i	|- ( A e. CH /\ ( _|_ ` A ) e. CH )
6	1	chshii	|- A e. SH
7		shococss	|- ( A e. SH -> A C_ ( _|_ ` ( _|_ ` A ) ) )
8	6 7	ax-mp	|- A C_ ( _|_ ` ( _|_ ` A ) )
9		stj	|- ( S e. States -> ( ( ( A e. CH /\ ( _|_ ` A ) e. CH ) /\ A C_ ( _|_ ` ( _|_ ` A ) ) ) -> ( S ` ( A vH ( _|_ ` A ) ) ) = ( ( S ` A ) + ( S ` ( _|_ ` A ) ) ) ) )
10	5 8 9	mp2ani	|- ( S e. States -> ( S ` ( A vH ( _|_ ` A ) ) ) = ( ( S ` A ) + ( S ` ( _|_ ` A ) ) ) )
11		sthil	|- ( S e. States -> ( S ` ~H ) = 1 )
12	3 10 11	3eqtr3a	|- ( S e. States -> ( ( S ` A ) + ( S ` ( _|_ ` A ) ) ) = 1 )