Metamath Proof Explorer

Theorem kbpj

Description: If a vector A has norm 1, the outer product | A >. <. A | is the projector onto the subspace spanned by A . http://en.wikipedia.org/wiki/Bra-ket#Linear%5Foperators . (Contributed by NM, 30-May-2006) (New usage is discouraged.)

Ref Expression
Assertion kbpj 
|- ( ( A e. ~H /\ ( normh ` A ) = 1 ) -> ( A ketbra A ) = ( projh ` ( span ` { A } ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( ( normh ` A ) = 1 -> ( ( normh ` A ) ^ 2 ) = ( 1 ^ 2 ) )
2 sq1 
 |-  ( 1 ^ 2 ) = 1
3 1 2 eqtrdi 
 |-  ( ( normh ` A ) = 1 -> ( ( normh ` A ) ^ 2 ) = 1 )
4 3 oveq2d 
 |-  ( ( normh ` A ) = 1 -> ( ( x .ih A ) / ( ( normh ` A ) ^ 2 ) ) = ( ( x .ih A ) / 1 ) )
5 hicl 
 |-  ( ( x e. ~H /\ A e. ~H ) -> ( x .ih A ) e. CC )
6 5 ancoms 
 |-  ( ( A e. ~H /\ x e. ~H ) -> ( x .ih A ) e. CC )
7 6 div1d 
 |-  ( ( A e. ~H /\ x e. ~H ) -> ( ( x .ih A ) / 1 ) = ( x .ih A ) )
8 4 7 sylan9eqr 
 |-  ( ( ( A e. ~H /\ x e. ~H ) /\ ( normh ` A ) = 1 ) -> ( ( x .ih A ) / ( ( normh ` A ) ^ 2 ) ) = ( x .ih A ) )
9 8 an32s 
 |-  ( ( ( A e. ~H /\ ( normh ` A ) = 1 ) /\ x e. ~H ) -> ( ( x .ih A ) / ( ( normh ` A ) ^ 2 ) ) = ( x .ih A ) )
10 9 oveq1d 
 |-  ( ( ( A e. ~H /\ ( normh ` A ) = 1 ) /\ x e. ~H ) -> ( ( ( x .ih A ) / ( ( normh ` A ) ^ 2 ) ) .h A ) = ( ( x .ih A ) .h A ) )
11 simpll 
 |-  ( ( ( A e. ~H /\ ( normh ` A ) = 1 ) /\ x e. ~H ) -> A e. ~H )
12 simpr 
 |-  ( ( ( A e. ~H /\ ( normh ` A ) = 1 ) /\ x e. ~H ) -> x e. ~H )
13 ax-1ne0 
 |-  1 =/= 0
14 neeq1 
 |-  ( ( normh ` A ) = 1 -> ( ( normh ` A ) =/= 0 <-> 1 =/= 0 ) )
15 13 14 mpbiri 
 |-  ( ( normh ` A ) = 1 -> ( normh ` A ) =/= 0 )
16 normne0 
 |-  ( A e. ~H -> ( ( normh ` A ) =/= 0 <-> A =/= 0h ) )
17 15 16 syl5ib 
 |-  ( A e. ~H -> ( ( normh ` A ) = 1 -> A =/= 0h ) )
18 17 imp 
 |-  ( ( A e. ~H /\ ( normh ` A ) = 1 ) -> A =/= 0h )
19 18 adantr 
 |-  ( ( ( A e. ~H /\ ( normh ` A ) = 1 ) /\ x e. ~H ) -> A =/= 0h )
20 pjspansn 
 |-  ( ( A e. ~H /\ x e. ~H /\ A =/= 0h ) -> ( ( projh ` ( span ` { A } ) ) ` x ) = ( ( ( x .ih A ) / ( ( normh ` A ) ^ 2 ) ) .h A ) )
21 11 12 19 20 syl3anc 
 |-  ( ( ( A e. ~H /\ ( normh ` A ) = 1 ) /\ x e. ~H ) -> ( ( projh ` ( span ` { A } ) ) ` x ) = ( ( ( x .ih A ) / ( ( normh ` A ) ^ 2 ) ) .h A ) )
22 kbval 
 |-  ( ( A e. ~H /\ A e. ~H /\ x e. ~H ) -> ( ( A ketbra A ) ` x ) = ( ( x .ih A ) .h A ) )
23 22 3anidm12 
 |-  ( ( A e. ~H /\ x e. ~H ) -> ( ( A ketbra A ) ` x ) = ( ( x .ih A ) .h A ) )
24 23 adantlr 
 |-  ( ( ( A e. ~H /\ ( normh ` A ) = 1 ) /\ x e. ~H ) -> ( ( A ketbra A ) ` x ) = ( ( x .ih A ) .h A ) )
25 10 21 24 3eqtr4rd 
 |-  ( ( ( A e. ~H /\ ( normh ` A ) = 1 ) /\ x e. ~H ) -> ( ( A ketbra A ) ` x ) = ( ( projh ` ( span ` { A } ) ) ` x ) )
26 25 ralrimiva 
 |-  ( ( A e. ~H /\ ( normh ` A ) = 1 ) -> A. x e. ~H ( ( A ketbra A ) ` x ) = ( ( projh ` ( span ` { A } ) ) ` x ) )
27 kbop 
 |-  ( ( A e. ~H /\ A e. ~H ) -> ( A ketbra A ) : ~H --> ~H )
28 27 anidms 
 |-  ( A e. ~H -> ( A ketbra A ) : ~H --> ~H )
29 28 ffnd 
 |-  ( A e. ~H -> ( A ketbra A ) Fn ~H )
30 spansnch 
 |-  ( A e. ~H -> ( span ` { A } ) e. CH )
31 pjfn 
 |-  ( ( span ` { A } ) e. CH -> ( projh ` ( span ` { A } ) ) Fn ~H )
32 30 31 syl 
 |-  ( A e. ~H -> ( projh ` ( span ` { A } ) ) Fn ~H )
33 eqfnfv 
 |-  ( ( ( A ketbra A ) Fn ~H /\ ( projh ` ( span ` { A } ) ) Fn ~H ) -> ( ( A ketbra A ) = ( projh ` ( span ` { A } ) ) <-> A. x e. ~H ( ( A ketbra A ) ` x ) = ( ( projh ` ( span ` { A } ) ) ` x ) ) )
34 29 32 33 syl2anc 
 |-  ( A e. ~H -> ( ( A ketbra A ) = ( projh ` ( span ` { A } ) ) <-> A. x e. ~H ( ( A ketbra A ) ` x ) = ( ( projh ` ( span ` { A } ) ) ` x ) ) )
35 34 adantr 
 |-  ( ( A e. ~H /\ ( normh ` A ) = 1 ) -> ( ( A ketbra A ) = ( projh ` ( span ` { A } ) ) <-> A. x e. ~H ( ( A ketbra A ) ` x ) = ( ( projh ` ( span ` { A } ) ) ` x ) ) )
36 26 35 mpbird 
 |-  ( ( A e. ~H /\ ( normh ` A ) = 1 ) -> ( A ketbra A ) = ( projh ` ( span ` { A } ) ) )