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 
|- S = ( x e. CH |-> ( ( projh ` x ) ` u ) )
Assertion hstrlem3a 
|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> S e. CHStates )

Proof

Step Hyp Ref Expression
1 hstrlem3a.1 
 |-  S = ( x e. CH |-> ( ( projh ` x ) ` u ) )
2 pjhcl 
 |-  ( ( x e. CH /\ u e. ~H ) -> ( ( projh ` x ) ` u ) e. ~H )
3 2 ancoms 
 |-  ( ( u e. ~H /\ x e. CH ) -> ( ( projh ` x ) ` u ) e. ~H )
4 3 adantlr 
 |-  ( ( ( u e. ~H /\ ( normh ` u ) = 1 ) /\ x e. CH ) -> ( ( projh ` x ) ` u ) e. ~H )
5 4 1 fmptd 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> S : CH --> ~H )
6 helch 
 |-  ~H e. CH
7 1 hstrlem2 
 |-  ( ~H e. CH -> ( S ` ~H ) = ( ( projh ` ~H ) ` u ) )
8 6 7 ax-mp 
 |-  ( S ` ~H ) = ( ( projh ` ~H ) ` u )
9 8 fveq2i 
 |-  ( normh ` ( S ` ~H ) ) = ( normh ` ( ( projh ` ~H ) ` u ) )
10 pjch1 
 |-  ( u e. ~H -> ( ( projh ` ~H ) ` u ) = u )
11 10 fveq2d 
 |-  ( u e. ~H -> ( normh ` ( ( projh ` ~H ) ` u ) ) = ( normh ` u ) )
12 id 
 |-  ( ( normh ` u ) = 1 -> ( normh ` u ) = 1 )
13 11 12 sylan9eq 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( normh ` ( ( projh ` ~H ) ` u ) ) = 1 )
14 9 13 eqtrid 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( normh ` ( S ` ~H ) ) = 1 )
15 1 hstrlem2 
 |-  ( z e. CH -> ( S ` z ) = ( ( projh ` z ) ` u ) )
16 1 hstrlem2 
 |-  ( w e. CH -> ( S ` w ) = ( ( projh ` w ) ` u ) )
17 15 16 oveqan12d 
 |-  ( ( z e. CH /\ w e. CH ) -> ( ( S ` z ) .ih ( S ` w ) ) = ( ( ( projh ` z ) ` u ) .ih ( ( projh ` w ) ` u ) ) )
18 17 3adant3 
 |-  ( ( z e. CH /\ w e. CH /\ u e. ~H ) -> ( ( S ` z ) .ih ( S ` w ) ) = ( ( ( projh ` z ) ` u ) .ih ( ( projh ` w ) ` u ) ) )
19 18 adantr 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( S ` z ) .ih ( S ` w ) ) = ( ( ( projh ` z ) ` u ) .ih ( ( projh ` w ) ` u ) ) )
20 pjoi0 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( ( projh ` z ) ` u ) .ih ( ( projh ` w ) ` u ) ) = 0 )
21 19 20 eqtrd 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( S ` z ) .ih ( S ` w ) ) = 0 )
22 pjcjt2 
 |-  ( ( z e. CH /\ w e. CH /\ u e. ~H ) -> ( z C_ ( _|_ ` w ) -> ( ( projh ` ( z vH w ) ) ` u ) = ( ( ( projh ` z ) ` u ) +h ( ( projh ` w ) ` u ) ) ) )
23 22 imp 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( projh ` ( z vH w ) ) ` u ) = ( ( ( projh ` z ) ` u ) +h ( ( projh ` w ) ` u ) ) )
24 chjcl 
 |-  ( ( z e. CH /\ w e. CH ) -> ( z vH w ) e. CH )
25 1 hstrlem2 
 |-  ( ( z vH w ) e. CH -> ( S ` ( z vH w ) ) = ( ( projh ` ( z vH w ) ) ` u ) )
26 24 25 syl 
 |-  ( ( z e. CH /\ w e. CH ) -> ( S ` ( z vH w ) ) = ( ( projh ` ( z vH w ) ) ` u ) )
27 26 3adant3 
 |-  ( ( z e. CH /\ w e. CH /\ u e. ~H ) -> ( S ` ( z vH w ) ) = ( ( projh ` ( z vH w ) ) ` u ) )
28 27 adantr 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( S ` ( z vH w ) ) = ( ( projh ` ( z vH w ) ) ` u ) )
29 15 16 oveqan12d 
 |-  ( ( z e. CH /\ w e. CH ) -> ( ( S ` z ) +h ( S ` w ) ) = ( ( ( projh ` z ) ` u ) +h ( ( projh ` w ) ` u ) ) )
30 29 3adant3 
 |-  ( ( z e. CH /\ w e. CH /\ u e. ~H ) -> ( ( S ` z ) +h ( S ` w ) ) = ( ( ( projh ` z ) ` u ) +h ( ( projh ` w ) ` u ) ) )
31 30 adantr 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( S ` z ) +h ( S ` w ) ) = ( ( ( projh ` z ) ` u ) +h ( ( projh ` w ) ` u ) ) )
32 23 28 31 3eqtr4d 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( S ` ( z vH w ) ) = ( ( S ` z ) +h ( S ` w ) ) )
33 21 32 jca 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( ( S ` z ) .ih ( S ` w ) ) = 0 /\ ( S ` ( z vH w ) ) = ( ( S ` z ) +h ( S ` w ) ) ) )
34 33 3exp1 
 |-  ( z e. CH -> ( w e. CH -> ( u e. ~H -> ( z C_ ( _|_ ` w ) -> ( ( ( S ` z ) .ih ( S ` w ) ) = 0 /\ ( S ` ( z vH w ) ) = ( ( S ` z ) +h ( S ` w ) ) ) ) ) ) )
35 34 com3r 
 |-  ( u e. ~H -> ( z e. CH -> ( w e. CH -> ( z C_ ( _|_ ` w ) -> ( ( ( S ` z ) .ih ( S ` w ) ) = 0 /\ ( S ` ( z vH w ) ) = ( ( S ` z ) +h ( S ` w ) ) ) ) ) ) )
36 35 adantr 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( z e. CH -> ( w e. CH -> ( z C_ ( _|_ ` w ) -> ( ( ( S ` z ) .ih ( S ` w ) ) = 0 /\ ( S ` ( z vH w ) ) = ( ( S ` z ) +h ( S ` w ) ) ) ) ) ) )
37 36 ralrimdv 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( z e. CH -> A. w e. CH ( z C_ ( _|_ ` w ) -> ( ( ( S ` z ) .ih ( S ` w ) ) = 0 /\ ( S ` ( z vH w ) ) = ( ( S ` z ) +h ( S ` w ) ) ) ) ) )
38 37 ralrimiv 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> A. z e. CH A. w e. CH ( z C_ ( _|_ ` w ) -> ( ( ( S ` z ) .ih ( S ` w ) ) = 0 /\ ( S ` ( z vH w ) ) = ( ( S ` z ) +h ( S ` w ) ) ) ) )
39 ishst 
 |-  ( S e. CHStates <-> ( S : CH --> ~H /\ ( normh ` ( S ` ~H ) ) = 1 /\ A. z e. CH A. w e. CH ( z C_ ( _|_ ` w ) -> ( ( ( S ` z ) .ih ( S ` w ) ) = 0 /\ ( S ` ( z vH w ) ) = ( ( S ` z ) +h ( S ` w ) ) ) ) ) )
40 5 14 38 39 syl3anbrc 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> S e. CHStates )