Theorem hstel2

Description: Properties of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hstel2	|- ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ ( _|_ ` B ) ) ) -> ( ( ( S ` A ) .ih ( S ` B ) ) = 0 /\ ( S ` ( A vH B ) ) = ( ( S ` A ) +h ( S ` B ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ishst	|- ( S e. CHStates <-> ( S : CH --> ~H /\ ( normh ` ( S ` ~H ) ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) ) )
2	1	simp3bi	|- ( S e. CHStates -> A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) )
3	2	ad2antrr	|- ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ ( _|_ ` B ) ) ) -> A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) )
4		sseq1	|- ( x = A -> ( x C_ ( _|_ ` y ) <-> A C_ ( _|_ ` y ) ) )
5		fveq2	|- ( x = A -> ( S ` x ) = ( S ` A ) )
6	5	oveq1d	|- ( x = A -> ( ( S ` x ) .ih ( S ` y ) ) = ( ( S ` A ) .ih ( S ` y ) ) )
7	6	eqeq1d	|- ( x = A -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 <-> ( ( S ` A ) .ih ( S ` y ) ) = 0 ) )
8		fvoveq1	|- ( x = A -> ( S ` ( x vH y ) ) = ( S ` ( A vH y ) ) )
9	5	oveq1d	|- ( x = A -> ( ( S ` x ) +h ( S ` y ) ) = ( ( S ` A ) +h ( S ` y ) ) )
10	8 9	eqeq12d	|- ( x = A -> ( ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) <-> ( S ` ( A vH y ) ) = ( ( S ` A ) +h ( S ` y ) ) ) )
11	7 10	anbi12d	|- ( x = A -> ( ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) <-> ( ( ( S ` A ) .ih ( S ` y ) ) = 0 /\ ( S ` ( A vH y ) ) = ( ( S ` A ) +h ( S ` y ) ) ) ) )
12	4 11	imbi12d	|- ( x = A -> ( ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) <-> ( A C_ ( _|_ ` y ) -> ( ( ( S ` A ) .ih ( S ` y ) ) = 0 /\ ( S ` ( A vH y ) ) = ( ( S ` A ) +h ( S ` y ) ) ) ) ) )
13		fveq2	|- ( y = B -> ( _|_ ` y ) = ( _|_ ` B ) )
14	13	sseq2d	|- ( y = B -> ( A C_ ( _|_ ` y ) <-> A C_ ( _|_ ` B ) ) )
15		fveq2	|- ( y = B -> ( S ` y ) = ( S ` B ) )
16	15	oveq2d	|- ( y = B -> ( ( S ` A ) .ih ( S ` y ) ) = ( ( S ` A ) .ih ( S ` B ) ) )
17	16	eqeq1d	|- ( y = B -> ( ( ( S ` A ) .ih ( S ` y ) ) = 0 <-> ( ( S ` A ) .ih ( S ` B ) ) = 0 ) )
18		oveq2	|- ( y = B -> ( A vH y ) = ( A vH B ) )
19	18	fveq2d	|- ( y = B -> ( S ` ( A vH y ) ) = ( S ` ( A vH B ) ) )
20	15	oveq2d	|- ( y = B -> ( ( S ` A ) +h ( S ` y ) ) = ( ( S ` A ) +h ( S ` B ) ) )
21	19 20	eqeq12d	|- ( y = B -> ( ( S ` ( A vH y ) ) = ( ( S ` A ) +h ( S ` y ) ) <-> ( S ` ( A vH B ) ) = ( ( S ` A ) +h ( S ` B ) ) ) )
22	17 21	anbi12d	|- ( y = B -> ( ( ( ( S ` A ) .ih ( S ` y ) ) = 0 /\ ( S ` ( A vH y ) ) = ( ( S ` A ) +h ( S ` y ) ) ) <-> ( ( ( S ` A ) .ih ( S ` B ) ) = 0 /\ ( S ` ( A vH B ) ) = ( ( S ` A ) +h ( S ` B ) ) ) ) )
23	14 22	imbi12d	|- ( y = B -> ( ( A C_ ( _|_ ` y ) -> ( ( ( S ` A ) .ih ( S ` y ) ) = 0 /\ ( S ` ( A vH y ) ) = ( ( S ` A ) +h ( S ` y ) ) ) ) <-> ( A C_ ( _|_ ` B ) -> ( ( ( S ` A ) .ih ( S ` B ) ) = 0 /\ ( S ` ( A vH B ) ) = ( ( S ` A ) +h ( S ` B ) ) ) ) ) )
24	12 23	rspc2v	|- ( ( A e. CH /\ B e. CH ) -> ( A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) -> ( A C_ ( _|_ ` B ) -> ( ( ( S ` A ) .ih ( S ` B ) ) = 0 /\ ( S ` ( A vH B ) ) = ( ( S ` A ) +h ( S ` B ) ) ) ) ) )
25	24	com23	|- ( ( A e. CH /\ B e. CH ) -> ( A C_ ( _|_ ` B ) -> ( A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) -> ( ( ( S ` A ) .ih ( S ` B ) ) = 0 /\ ( S ` ( A vH B ) ) = ( ( S ` A ) +h ( S ` B ) ) ) ) ) )
26	25	impr	|- ( ( A e. CH /\ ( B e. CH /\ A C_ ( _|_ ` B ) ) ) -> ( A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) -> ( ( ( S ` A ) .ih ( S ` B ) ) = 0 /\ ( S ` ( A vH B ) ) = ( ( S ` A ) +h ( S ` B ) ) ) ) )
27	26	adantll	|- ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ ( _|_ ` B ) ) ) -> ( A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( ( ( S ` x ) .ih ( S ` y ) ) = 0 /\ ( S ` ( x vH y ) ) = ( ( S ` x ) +h ( S ` y ) ) ) ) -> ( ( ( S ` A ) .ih ( S ` B ) ) = 0 /\ ( S ` ( A vH B ) ) = ( ( S ` A ) +h ( S ` B ) ) ) ) )
28	3 27	mpd	|- ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ ( _|_ ` B ) ) ) -> ( ( ( S ` A ) .ih ( S ` B ) ) = 0 /\ ( S ` ( A vH B ) ) = ( ( S ` A ) +h ( S ` B ) ) ) )