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 CHStates A C norm S A 2 + norm S A 2 = 1

Proof

Step Hyp Ref Expression
1 hstoc S CHStates A C S A + S A = S
2 1 fveq2d S CHStates A C norm S A + S A = norm S
3 2 oveq1d S CHStates A C norm S A + S A 2 = norm S 2
4 hstcl S CHStates A C S A
5 choccl A C A C
6 hstcl S CHStates A C S A
7 5 6 sylan2 S CHStates A C S A
8 4 7 jca S CHStates A C S A S A
9 5 adantl S CHStates A C A C
10 chsh A C A S
11 shococss A S A A
12 10 11 syl A C A A
13 12 adantl S CHStates A C A A
14 9 13 jca S CHStates A C A C A A
15 hstorth S CHStates A C A C A A S A ih S A = 0
16 14 15 mpdan S CHStates A C S A ih S A = 0
17 normpyth S A S A S A ih S A = 0 norm S A + S A 2 = norm S A 2 + norm S A 2
18 8 16 17 sylc S CHStates A C norm S A + S A 2 = norm S A 2 + norm S A 2
19 hst1a S CHStates norm S = 1
20 19 oveq1d S CHStates norm S 2 = 1 2
21 sq1 1 2 = 1
22 20 21 syl6eq S CHStates norm S 2 = 1
23 22 adantr S CHStates A C norm S 2 = 1
24 3 18 23 3eqtr3d S CHStates A C norm S A 2 + norm S A 2 = 1