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 )