Metamath Proof Explorer

Theorem hst1h

Description: The norm of a Hilbert-space-valued state equals one iff the state value equals the state value of the lattice unit. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hst1h ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 ↔ ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ ℋ ) ) )

Proof

Step Hyp Ref Expression
1 hstcl ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( 𝑆 ‘ 𝐴 ) ∈ ℋ )
2 ax-hvaddid ⊢ ( ( 𝑆 ‘ 𝐴 ) ∈ ℋ → ( ( 𝑆 ‘ 𝐴 ) +ℎ 0ℎ ) = ( 𝑆 ‘ 𝐴 ) )
3 1 2 syl ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( 𝑆 ‘ 𝐴 ) +ℎ 0ℎ ) = ( 𝑆 ‘ 𝐴 ) )
4 3 adantr ⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 ) → ( ( 𝑆 ‘ 𝐴 ) +ℎ 0ℎ ) = ( 𝑆 ‘ 𝐴 ) )
5 ax-1cn ⊢ 1 ∈ ℂ
6 choccl ⊢ ( 𝐴 ∈ Cℋ → ( ⊥ ‘ 𝐴 ) ∈ Cℋ )
7 hstcl ⊢ ( ( 𝑆 ∈ CHStates ∧ ( ⊥ ‘ 𝐴 ) ∈ Cℋ ) → ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℋ )
8 6 7 sylan2 ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℋ )
9 normcl ⊢ ( ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℋ → ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ∈ ℝ )
10 8 9 syl ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ∈ ℝ )
11 10 resqcld ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) ∈ ℝ )
12 11 recnd ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) ∈ ℂ )
13 pncan2 ⊢ ( ( 1 ∈ ℂ ∧ ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) ∈ ℂ ) → ( ( 1 + ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) ) − 1 ) = ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) )
14 5 12 13 sylancr ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( 1 + ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) ) − 1 ) = ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) )
15 14 adantr ⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 ) → ( ( 1 + ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) ) − 1 ) = ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) )
16 oveq1 ⊢ ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 → ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) = ( 1 ↑ 2 ) )
17 sq1 ⊢ ( 1 ↑ 2 ) = 1
18 16 17 eqtr2di ⊢ ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 → 1 = ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) )
19 18 oveq1d ⊢ ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 → ( 1 + ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) ) = ( ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) ) )
20 hstnmoc ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) ) = 1 )
21 19 20 sylan9eqr ⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 ) → ( 1 + ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) ) = 1 )
22 21 oveq1d ⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 ) → ( ( 1 + ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) ) − 1 ) = ( 1 − 1 ) )
23 15 22 eqtr3d ⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 ) → ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) = ( 1 − 1 ) )
24 1m1e0 ⊢ ( 1 − 1 ) = 0
25 23 24 eqtrdi ⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 ) → ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) = 0 )
26 25 ex ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 → ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) = 0 ) )
27 10 recnd ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ∈ ℂ )
28 sqeq0 ⊢ ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ∈ ℂ → ( ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) = 0 ↔ ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = 0 ) )
29 27 28 syl ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) = 0 ↔ ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = 0 ) )
30 norm-i ⊢ ( ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℋ → ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = 0 ↔ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) = 0ℎ ) )
31 8 30 syl ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = 0 ↔ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) = 0ℎ ) )
32 29 31 bitrd ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( ( normℎ ‘ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ↑ 2 ) = 0 ↔ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) = 0ℎ ) )
33 26 32 sylibd ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 → ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) = 0ℎ ) )
34 33 imp ⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 ) → ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) = 0ℎ )
35 34 oveq2d ⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 ) → ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = ( ( 𝑆 ‘ 𝐴 ) +ℎ 0ℎ ) )
36 hstoc ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = ( 𝑆 ‘ ℋ ) )
37 36 adantr ⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 ) → ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = ( 𝑆 ‘ ℋ ) )
38 35 37 eqtr3d ⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 ) → ( ( 𝑆 ‘ 𝐴 ) +ℎ 0ℎ ) = ( 𝑆 ‘ ℋ ) )
39 4 38 eqtr3d ⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 ) → ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ ℋ ) )
40 fveq2 ⊢ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ ℋ ) → ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) )
41 hst1a ⊢ ( 𝑆 ∈ CHStates → ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 )
42 41 adantr ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 )
43 40 42 sylan9eqr ⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ ℋ ) ) → ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 )
44 39 43 impbida ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 ↔ ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ ℋ ) ) )