Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  kbpj Structured version   Unicode version

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

Proof of Theorem kbpj
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 oveq1 6090 . . . . . . . . 9
2 sq1 11478 . . . . . . . . 9
31, 2syl6eq 2486 . . . . . . . 8
43oveq2d 6099 . . . . . . 7
5 hicl 22584 . . . . . . . . 9
65ancoms 441 . . . . . . . 8
76div1d 9784 . . . . . . 7
84, 7sylan9eqr 2492 . . . . . 6
98an32s 781 . . . . 5
109oveq1d 6098 . . . 4
11 simpll 732 . . . . 5
12 simpr 449 . . . . 5
13 ax-1ne0 9061 . . . . . . . . 9
14 neeq1 2611 . . . . . . . . 9
1513, 14mpbiri 226 . . . . . . . 8
16 normne0 22634 . . . . . . . 8
1715, 16syl5ib 212 . . . . . . 7
1817imp 420 . . . . . 6
1918adantr 453 . . . . 5
20 pjspansn 23081 . . . . 5
2111, 12, 19, 20syl3anc 1185 . . . 4
22 kbval 23459 . . . . . 6
23223anidm12 1242 . . . . 5
2423adantlr 697 . . . 4
2510, 21, 243eqtr4rd 2481 . . 3
2625ralrimiva 2791 . 2
27 kbop 23458 . . . . . 6
2827anidms 628 . . . . 5
29 ffn 5593 . . . . 5
3028, 29syl 16 . . . 4
31 spansnch 23064 . . . . 5
32 pjfn 23213 . . . . 5
3331, 32syl 16 . . . 4
34 eqfnfv 5829 . . . 4
3530, 33, 34syl2anc 644 . . 3