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 ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) ) = 1 )

Proof

Step Hyp Ref Expression
1 hstoc ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = ( 𝑆 ‘ ℋ ) )
2 1 fveq2d ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( normℎ ‘ ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ) = ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) )
3 2 oveq1d ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( normℎ ‘ ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ) ↑ 2 ) = ( ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) ↑ 2 ) )
4 hstcl ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( 𝑆 ‘ 𝐴 ) ∈ ℋ )
5 choccl ⊢ ( 𝐴 ∈ Cℋ → ( ⊥ ‘ 𝐴 ) ∈ Cℋ )
6 hstcl ⊢ ( ( 𝑆 ∈ CHStates ∧ ( ⊥ ‘ 𝐴 ) ∈ Cℋ ) → ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℋ )
7 5 6 sylan2 ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℋ )
8 4 7 jca ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( 𝑆 ‘ 𝐴 ) ∈ ℋ ∧ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℋ ) )
9 5 adantl ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ⊥ ‘ 𝐴 ) ∈ Cℋ )
10 chsh ⊢ ( 𝐴 ∈ Cℋ → 𝐴 ∈ Sℋ )
11 shococss ⊢ ( 𝐴 ∈ Sℋ → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
12 10 11 syl ⊢ ( 𝐴 ∈ Cℋ → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
13 12 adantl ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
14 9 13 jca ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ∧ 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) )
15 hstorth ⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ∧ 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) ) → ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = 0 )
16 14 15 mpdan ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = 0 )
17 normpyth ⊢ ( ( ( 𝑆 ‘ 𝐴 ) ∈ ℋ ∧ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℋ ) → ( ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = 0 → ( ( normℎ ‘ ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ) ↑ 2 ) = ( ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) ) ) )
18 8 16 17 sylc ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( normℎ ‘ ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ) ↑ 2 ) = ( ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) ) )
19 hst1a ⊢ ( 𝑆 ∈ CHStates → ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 )
20 19 oveq1d ⊢ ( 𝑆 ∈ CHStates → ( ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) ↑ 2 ) = ( 1 ↑ 2 ) )
21 sq1 ⊢ ( 1 ↑ 2 ) = 1
22 20 21 eqtrdi ⊢ ( 𝑆 ∈ CHStates → ( ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) ↑ 2 ) = 1 )
23 22 adantr ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) ↑ 2 ) = 1 )
24 3 18 23 3eqtr3d ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) ) = 1 )