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 syl5eq ( ( 𝑢 ∈ ℋ ∧ ( 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 )