Metamath Proof Explorer

Theorem hstoh

Description: A Hilbert-space-valued state orthogonal to the state of the lattice unit is zero. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hstoh ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ∧ ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ℋ ) ) = 0 ) → ( 𝑆 ‘ 𝐴 ) = 0ℎ )

Proof

Step Hyp Ref Expression
1 hstcl ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( 𝑆 ‘ 𝐴 ) ∈ ℋ )
2 choccl ⊢ ( 𝐴 ∈ Cℋ → ( ⊥ ‘ 𝐴 ) ∈ Cℋ )
3 hstcl ⊢ ( ( 𝑆 ∈ CHStates ∧ ( ⊥ ‘ 𝐴 ) ∈ Cℋ ) → ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℋ )
4 2 3 sylan2 ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℋ )
5 his7 ⊢ ( ( ( 𝑆 ‘ 𝐴 ) ∈ ℋ ∧ ( 𝑆 ‘ 𝐴 ) ∈ ℋ ∧ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℋ ) → ( ( 𝑆 ‘ 𝐴 ) ·ih ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ) = ( ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ 𝐴 ) ) + ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ) )
6 1 1 4 5 syl3anc ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( 𝑆 ‘ 𝐴 ) ·ih ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ) = ( ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ 𝐴 ) ) + ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ) )
7 normsq ⊢ ( ( 𝑆 ‘ 𝐴 ) ∈ ℋ → ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) = ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ 𝐴 ) ) )
8 1 7 syl ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) = ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ 𝐴 ) ) )
9 8 eqcomd ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ 𝐴 ) ) = ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) )
10 ococ ⊢ ( 𝐴 ∈ Cℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴 )
11 eqimss2 ⊢ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴 → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
12 10 11 syl ⊢ ( 𝐴 ∈ Cℋ → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
13 2 12 jca ⊢ ( 𝐴 ∈ Cℋ → ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ∧ 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) )
14 13 adantl ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ∧ 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) )
15 hstorth ⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ∧ 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) ) → ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = 0 )
16 14 15 mpdan ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = 0 )
17 9 16 oveq12d ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ 𝐴 ) ) + ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ) = ( ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) + 0 ) )
18 normcl ⊢ ( ( 𝑆 ‘ 𝐴 ) ∈ ℋ → ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ∈ ℝ )
19 1 18 syl ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ∈ ℝ )
20 19 resqcld ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) ∈ ℝ )
21 20 recnd ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) ∈ ℂ )
22 21 addid1d ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) + 0 ) = ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) )
23 6 17 22 3eqtrrd ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) = ( ( 𝑆 ‘ 𝐴 ) ·ih ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ) )
24 hstoc ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = ( 𝑆 ‘ ℋ ) )
25 24 oveq2d ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( 𝑆 ‘ 𝐴 ) ·ih ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ) = ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ℋ ) ) )
26 23 25 eqtrd ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) = ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ℋ ) ) )
27 id ⊢ ( ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ℋ ) ) = 0 → ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ℋ ) ) = 0 )
28 26 27 sylan9eq ⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ℋ ) ) = 0 ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) = 0 )
29 28 3impa ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ∧ ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ℋ ) ) = 0 ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) = 0 )
30 19 recnd ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ∈ ℂ )
31 sqeq0 ⊢ ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ∈ ℂ → ( ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) = 0 ↔ ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 0 ) )
32 30 31 syl ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) = 0 ↔ ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 0 ) )
33 32 3adant3 ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ∧ ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ℋ ) ) = 0 ) → ( ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) ↑ 2 ) = 0 ↔ ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 0 ) )
34 29 33 mpbid ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ∧ ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ℋ ) ) = 0 ) → ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 0 )
35 hst0h ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 0 ↔ ( 𝑆 ‘ 𝐴 ) = 0ℎ ) )
36 35 3adant3 ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ∧ ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ℋ ) ) = 0 ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 0 ↔ ( 𝑆 ‘ 𝐴 ) = 0ℎ ) )
37 34 36 mpbid ⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ∧ ( ( 𝑆 ‘ 𝐴 ) ·ih ( 𝑆 ‘ ℋ ) ) = 0 ) → ( 𝑆 ‘ 𝐴 ) = 0ℎ )