Theorem hstoc

Description: Sum of a Hilbert-space-valued state of a lattice element and its orthocomplement. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hstoc	|- ( ( S e. CHStates /\ A e. CH ) -> ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) = ( S ` ~H ) )

Proof

Step	Hyp	Ref	Expression
1		choccl	|- ( A e. CH -> ( _|_ ` A ) e. CH )
2	1	adantl	|- ( ( S e. CHStates /\ A e. CH ) -> ( _|_ ` A ) e. CH )
3		chsh	|- ( A e. CH -> A e. SH )
4		shococss	|- ( A e. SH -> A C_ ( _|_ ` ( _|_ ` A ) ) )
5	3 4	syl	|- ( A e. CH -> A C_ ( _|_ ` ( _|_ ` A ) ) )
6	5	adantl	|- ( ( S e. CHStates /\ A e. CH ) -> A C_ ( _|_ ` ( _|_ ` A ) ) )
7	2 6	jca	|- ( ( S e. CHStates /\ A e. CH ) -> ( ( _|_ ` A ) e. CH /\ A C_ ( _|_ ` ( _|_ ` A ) ) ) )
8		hstosum	|- ( ( ( S e. CHStates /\ A e. CH ) /\ ( ( _|_ ` A ) e. CH /\ A C_ ( _|_ ` ( _|_ ` A ) ) ) ) -> ( S ` ( A vH ( _|_ ` A ) ) ) = ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) )
9	7 8	mpdan	|- ( ( S e. CHStates /\ A e. CH ) -> ( S ` ( A vH ( _|_ ` A ) ) ) = ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) )
10		chjo	|- ( A e. CH -> ( A vH ( _|_ ` A ) ) = ~H )
11	10	fveq2d	|- ( A e. CH -> ( S ` ( A vH ( _|_ ` A ) ) ) = ( S ` ~H ) )
12	11	adantl	|- ( ( S e. CHStates /\ A e. CH ) -> ( S ` ( A vH ( _|_ ` A ) ) ) = ( S ` ~H ) )
13	9 12	eqtr3d	|- ( ( S e. CHStates /\ A e. CH ) -> ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) = ( S ` ~H ) )