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 one. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hst1h ⊢ S ∈ CHStates ∧ A ∈ C ℋ → norm ℎ ⁡ S ⁡ A = 1 ↔ S ⁡ A = S ⁡ ℋ

Proof

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