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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1 | |
|
2 | sq1 | |
|
3 | 1 2 | eqtrdi | |
4 | 3 | oveq2d | |
5 | hicl | |
|
6 | 5 | ancoms | |
7 | 6 | div1d | |
8 | 4 7 | sylan9eqr | |
9 | 8 | an32s | |
10 | 9 | oveq1d | |
11 | simpll | |
|
12 | simpr | |
|
13 | ax-1ne0 | |
|
14 | neeq1 | |
|
15 | 13 14 | mpbiri | |
16 | normne0 | |
|
17 | 15 16 | syl5ib | |
18 | 17 | imp | |
19 | 18 | adantr | |
20 | pjspansn | |
|
21 | 11 12 19 20 | syl3anc | |
22 | kbval | |
|
23 | 22 | 3anidm12 | |
24 | 23 | adantlr | |
25 | 10 21 24 | 3eqtr4rd | |
26 | 25 | ralrimiva | |
27 | kbop | |
|
28 | 27 | anidms | |
29 | 28 | ffnd | |
30 | spansnch | |
|
31 | pjfn | |
|
32 | 30 31 | syl | |
33 | eqfnfv | |
|
34 | 29 32 33 | syl2anc | |
35 | 34 | adantr | |
36 | 26 35 | mpbird | |