Metamath Proof Explorer

Theorem hstrlem3a

Description: Lemma for strong set of CH states theorem: the function S , that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypothesis hstrlem3a.1 ⊢ 𝑆 = ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) )
Assertion hstrlem3a ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → 𝑆 ∈ CHStates )

Proof

Step Hyp Ref Expression
1 hstrlem3a.1 ⊢ 𝑆 = ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) )
2 pjhcl ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) → ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ∈ ℋ )
3 2 ancoms ⊢ ( ( 𝑢 ∈ ℋ ∧ 𝑥 ∈ Cℋ ) → ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ∈ ℋ )
4 3 adantlr ⊢ ( ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) ∧ 𝑥 ∈ Cℋ ) → ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ∈ ℋ )
5 4 1 fmptd ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → 𝑆 : Cℋ ⟶ ℋ )
6 helch ⊢ ℋ ∈ Cℋ
7 1 hstrlem2 ⊢ ( ℋ ∈ Cℋ → ( 𝑆 ‘ ℋ ) = ( ( projℎ ‘ ℋ ) ‘ 𝑢 ) )
8 6 7 ax-mp ⊢ ( 𝑆 ‘ ℋ ) = ( ( projℎ ‘ ℋ ) ‘ 𝑢 )
9 8 fveq2i ⊢ ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = ( normℎ ‘ ( ( projℎ ‘ ℋ ) ‘ 𝑢 ) )
10 pjch1 ⊢ ( 𝑢 ∈ ℋ → ( ( projℎ ‘ ℋ ) ‘ 𝑢 ) = 𝑢 )
11 10 fveq2d ⊢ ( 𝑢 ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ ℋ ) ‘ 𝑢 ) ) = ( normℎ ‘ 𝑢 ) )
12 id ⊢ ( ( normℎ ‘ 𝑢 ) = 1 → ( normℎ ‘ 𝑢 ) = 1 )
13 11 12 sylan9eq ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( normℎ ‘ ( ( projℎ ‘ ℋ ) ‘ 𝑢 ) ) = 1 )
14 9 13 eqtrid ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 )
15 1 hstrlem2 ⊢ ( 𝑧 ∈ Cℋ → ( 𝑆 ‘ 𝑧 ) = ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) )
16 1 hstrlem2 ⊢ ( 𝑤 ∈ Cℋ → ( 𝑆 ‘ 𝑤 ) = ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) )
17 15 16 oveqan12d ⊢ ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ) → ( ( 𝑆 ‘ 𝑧 ) ·ih ( 𝑆 ‘ 𝑤 ) ) = ( ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) ·ih ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) )
18 17 3adant3 ⊢ ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) → ( ( 𝑆 ‘ 𝑧 ) ·ih ( 𝑆 ‘ 𝑤 ) ) = ( ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) ·ih ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) )
19 18 adantr ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( ( 𝑆 ‘ 𝑧 ) ·ih ( 𝑆 ‘ 𝑤 ) ) = ( ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) ·ih ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) )
20 pjoi0 ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) ·ih ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) = 0 )
21 19 20 eqtrd ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( ( 𝑆 ‘ 𝑧 ) ·ih ( 𝑆 ‘ 𝑤 ) ) = 0 )
22 pjcjt2 ⊢ ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) → ( 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) → ( ( projℎ ‘ ( 𝑧 ∨ℋ 𝑤 ) ) ‘ 𝑢 ) = ( ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) +ℎ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) ) )
23 22 imp ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( ( projℎ ‘ ( 𝑧 ∨ℋ 𝑤 ) ) ‘ 𝑢 ) = ( ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) +ℎ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) )
24 chjcl ⊢ ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ) → ( 𝑧 ∨ℋ 𝑤 ) ∈ Cℋ )
25 1 hstrlem2 ⊢ ( ( 𝑧 ∨ℋ 𝑤 ) ∈ Cℋ → ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( projℎ ‘ ( 𝑧 ∨ℋ 𝑤 ) ) ‘ 𝑢 ) )
26 24 25 syl ⊢ ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ) → ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( projℎ ‘ ( 𝑧 ∨ℋ 𝑤 ) ) ‘ 𝑢 ) )
27 26 3adant3 ⊢ ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) → ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( projℎ ‘ ( 𝑧 ∨ℋ 𝑤 ) ) ‘ 𝑢 ) )
28 27 adantr ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( projℎ ‘ ( 𝑧 ∨ℋ 𝑤 ) ) ‘ 𝑢 ) )
29 15 16 oveqan12d ⊢ ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ) → ( ( 𝑆 ‘ 𝑧 ) +ℎ ( 𝑆 ‘ 𝑤 ) ) = ( ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) +ℎ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) )
30 29 3adant3 ⊢ ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) → ( ( 𝑆 ‘ 𝑧 ) +ℎ ( 𝑆 ‘ 𝑤 ) ) = ( ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) +ℎ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) )
31 30 adantr ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( ( 𝑆 ‘ 𝑧 ) +ℎ ( 𝑆 ‘ 𝑤 ) ) = ( ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) +ℎ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) )
32 23 28 31 3eqtr4d ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( 𝑆 ‘ 𝑧 ) +ℎ ( 𝑆 ‘ 𝑤 ) ) )
33 21 32 jca ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( ( ( 𝑆 ‘ 𝑧 ) ·ih ( 𝑆 ‘ 𝑤 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( 𝑆 ‘ 𝑧 ) +ℎ ( 𝑆 ‘ 𝑤 ) ) ) )
34 33 3exp1 ⊢ ( 𝑧 ∈ Cℋ → ( 𝑤 ∈ Cℋ → ( 𝑢 ∈ ℋ → ( 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) → ( ( ( 𝑆 ‘ 𝑧 ) ·ih ( 𝑆 ‘ 𝑤 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( 𝑆 ‘ 𝑧 ) +ℎ ( 𝑆 ‘ 𝑤 ) ) ) ) ) ) )
35 34 com3r ⊢ ( 𝑢 ∈ ℋ → ( 𝑧 ∈ Cℋ → ( 𝑤 ∈ Cℋ → ( 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) → ( ( ( 𝑆 ‘ 𝑧 ) ·ih ( 𝑆 ‘ 𝑤 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( 𝑆 ‘ 𝑧 ) +ℎ ( 𝑆 ‘ 𝑤 ) ) ) ) ) ) )
36 35 adantr ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( 𝑧 ∈ Cℋ → ( 𝑤 ∈ Cℋ → ( 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) → ( ( ( 𝑆 ‘ 𝑧 ) ·ih ( 𝑆 ‘ 𝑤 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( 𝑆 ‘ 𝑧 ) +ℎ ( 𝑆 ‘ 𝑤 ) ) ) ) ) ) )
37 36 ralrimdv ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( 𝑧 ∈ Cℋ → ∀ 𝑤 ∈ Cℋ ( 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) → ( ( ( 𝑆 ‘ 𝑧 ) ·ih ( 𝑆 ‘ 𝑤 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( 𝑆 ‘ 𝑧 ) +ℎ ( 𝑆 ‘ 𝑤 ) ) ) ) ) )
38 37 ralrimiv ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ∀ 𝑧 ∈ Cℋ ∀ 𝑤 ∈ Cℋ ( 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) → ( ( ( 𝑆 ‘ 𝑧 ) ·ih ( 𝑆 ‘ 𝑤 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( 𝑆 ‘ 𝑧 ) +ℎ ( 𝑆 ‘ 𝑤 ) ) ) ) )
39 ishst ⊢ ( 𝑆 ∈ CHStates ↔ ( 𝑆 : Cℋ ⟶ ℋ ∧ ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 ∧ ∀ 𝑧 ∈ Cℋ ∀ 𝑤 ∈ Cℋ ( 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) → ( ( ( 𝑆 ‘ 𝑧 ) ·ih ( 𝑆 ‘ 𝑤 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( 𝑆 ‘ 𝑧 ) +ℎ ( 𝑆 ‘ 𝑤 ) ) ) ) ) )
40 5 14 38 39 syl3anbrc ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → 𝑆 ∈ CHStates )