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 AnormA=1AketbraA=projspanA

Proof

Step Hyp Ref Expression
1 oveq1 normA=1normA2=12
2 sq1 12=1
3 1 2 eqtrdi normA=1normA2=1
4 3 oveq2d normA=1xihAnormA2=xihA1
5 hicl xAxihA
6 5 ancoms AxxihA
7 6 div1d AxxihA1=xihA
8 4 7 sylan9eqr AxnormA=1xihAnormA2=xihA
9 8 an32s AnormA=1xxihAnormA2=xihA
10 9 oveq1d AnormA=1xxihAnormA2A=xihAA
11 simpll AnormA=1xA
12 simpr AnormA=1xx
13 ax-1ne0 10
14 neeq1 normA=1normA010
15 13 14 mpbiri normA=1normA0
16 normne0 AnormA0A0
17 15 16 syl5ib AnormA=1A0
18 17 imp AnormA=1A0
19 18 adantr AnormA=1xA0
20 pjspansn AxA0projspanAx=xihAnormA2A
21 11 12 19 20 syl3anc AnormA=1xprojspanAx=xihAnormA2A
22 kbval AAxAketbraAx=xihAA
23 22 3anidm12 AxAketbraAx=xihAA
24 23 adantlr AnormA=1xAketbraAx=xihAA
25 10 21 24 3eqtr4rd AnormA=1xAketbraAx=projspanAx
26 25 ralrimiva AnormA=1xAketbraAx=projspanAx
27 kbop AAAketbraA:
28 27 anidms AAketbraA:
29 28 ffnd AAketbraAFn
30 spansnch AspanAC
31 pjfn spanACprojspanAFn
32 30 31 syl AprojspanAFn
33 eqfnfv AketbraAFnprojspanAFnAketbraA=projspanAxAketbraAx=projspanAx
34 29 32 33 syl2anc AAketbraA=projspanAxAketbraAx=projspanAx
35 34 adantr AnormA=1AketbraA=projspanAxAketbraAx=projspanAx
36 26 35 mpbird AnormA=1AketbraA=projspanA