Metamath Proof Explorer

Theorem hstnmoc

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

Ref Expression
Assertion hstnmoc 
|- ( ( S e. CHStates /\ A e. CH ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) = 1 )

Proof

Step Hyp Ref Expression
1 hstoc 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) = ( S ` ~H ) )
2 1 fveq2d 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( normh ` ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) ) = ( normh ` ( S ` ~H ) ) )
3 2 oveq1d 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) ) ^ 2 ) = ( ( normh ` ( S ` ~H ) ) ^ 2 ) )
4 hstcl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( S ` A ) e. ~H )
5 choccl 
 |-  ( A e. CH -> ( _|_ ` A ) e. CH )
6 hstcl 
 |-  ( ( S e. CHStates /\ ( _|_ ` A ) e. CH ) -> ( S ` ( _|_ ` A ) ) e. ~H )
7 5 6 sylan2 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( S ` ( _|_ ` A ) ) e. ~H )
8 4 7 jca 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( S ` A ) e. ~H /\ ( S ` ( _|_ ` A ) ) e. ~H ) )
9 5 adantl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( _|_ ` A ) e. CH )
10 chsh 
 |-  ( A e. CH -> A e. SH )
11 shococss 
 |-  ( A e. SH -> A C_ ( _|_ ` ( _|_ ` A ) ) )
12 10 11 syl 
 |-  ( A e. CH -> A C_ ( _|_ ` ( _|_ ` A ) ) )
13 12 adantl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> A C_ ( _|_ ` ( _|_ ` A ) ) )
14 9 13 jca 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( _|_ ` A ) e. CH /\ A C_ ( _|_ ` ( _|_ ` A ) ) ) )
15 hstorth 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( ( _|_ ` A ) e. CH /\ A C_ ( _|_ ` ( _|_ ` A ) ) ) ) -> ( ( S ` A ) .ih ( S ` ( _|_ ` A ) ) ) = 0 )
16 14 15 mpdan 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( S ` A ) .ih ( S ` ( _|_ ` A ) ) ) = 0 )
17 normpyth 
 |-  ( ( ( S ` A ) e. ~H /\ ( S ` ( _|_ ` A ) ) e. ~H ) -> ( ( ( S ` A ) .ih ( S ` ( _|_ ` A ) ) ) = 0 -> ( ( normh ` ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) ) ^ 2 ) = ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) ) )
18 8 16 17 sylc 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( ( S ` A ) +h ( S ` ( _|_ ` A ) ) ) ) ^ 2 ) = ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) )
19 hst1a 
 |-  ( S e. CHStates -> ( normh ` ( S ` ~H ) ) = 1 )
20 19 oveq1d 
 |-  ( S e. CHStates -> ( ( normh ` ( S ` ~H ) ) ^ 2 ) = ( 1 ^ 2 ) )
21 sq1 
 |-  ( 1 ^ 2 ) = 1
22 20 21 eqtrdi 
 |-  ( S e. CHStates -> ( ( normh ` ( S ` ~H ) ) ^ 2 ) = 1 )
23 22 adantr 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` ~H ) ) ^ 2 ) = 1 )
24 3 18 23 3eqtr3d 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) = 1 )