# 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 ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 )`
` |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( normh ` ( S ` ~H ) ) ^ 2 ) = 1 )`
` |-  ( ( S e. CHStates /\ A e. CH ) -> ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` ( _|_ ` A ) ) ) ^ 2 ) ) = 1 )`