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 ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ 𝐴 ) = 1 ) → ( 𝐴 ketbra 𝐴 ) = ( projℎ ‘ ( span ‘ { 𝐴 } ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( ( normℎ ‘ 𝐴 ) = 1 → ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( 1 ↑ 2 ) )
2 sq1 ⊢ ( 1 ↑ 2 ) = 1
3 1 2 eqtrdi ⊢ ( ( normℎ ‘ 𝐴 ) = 1 → ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = 1 )
4 3 oveq2d ⊢ ( ( normℎ ‘ 𝐴 ) = 1 → ( ( 𝑥 ·ih 𝐴 ) / ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ) = ( ( 𝑥 ·ih 𝐴 ) / 1 ) )
5 hicl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝑥 ·ih 𝐴 ) ∈ ℂ )
6 5 ancoms ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑥 ·ih 𝐴 ) ∈ ℂ )
7 6 div1d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐴 ) / 1 ) = ( 𝑥 ·ih 𝐴 ) )
8 4 7 sylan9eqr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( normℎ ‘ 𝐴 ) = 1 ) → ( ( 𝑥 ·ih 𝐴 ) / ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ) = ( 𝑥 ·ih 𝐴 ) )
9 8 an32s ⊢ ( ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ 𝐴 ) = 1 ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐴 ) / ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ) = ( 𝑥 ·ih 𝐴 ) )
10 9 oveq1d ⊢ ( ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ 𝐴 ) = 1 ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑥 ·ih 𝐴 ) / ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ) ·ℎ 𝐴 ) = ( ( 𝑥 ·ih 𝐴 ) ·ℎ 𝐴 ) )
11 simpll ⊢ ( ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ 𝐴 ) = 1 ) ∧ 𝑥 ∈ ℋ ) → 𝐴 ∈ ℋ )
12 simpr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ 𝐴 ) = 1 ) ∧ 𝑥 ∈ ℋ ) → 𝑥 ∈ ℋ )
13 ax-1ne0 ⊢ 1 ≠ 0
14 neeq1 ⊢ ( ( normℎ ‘ 𝐴 ) = 1 → ( ( normℎ ‘ 𝐴 ) ≠ 0 ↔ 1 ≠ 0 ) )
15 13 14 mpbiri ⊢ ( ( normℎ ‘ 𝐴 ) = 1 → ( normℎ ‘ 𝐴 ) ≠ 0 )
16 normne0 ⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ 0ℎ ) )
17 15 16 syl5ib ⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ 𝐴 ) = 1 → 𝐴 ≠ 0ℎ ) )
18 17 imp ⊢ ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ 𝐴 ) = 1 ) → 𝐴 ≠ 0ℎ )
19 18 adantr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ 𝐴 ) = 1 ) ∧ 𝑥 ∈ ℋ ) → 𝐴 ≠ 0ℎ )
20 pjspansn ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ( projℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝑥 ) = ( ( ( 𝑥 ·ih 𝐴 ) / ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ) ·ℎ 𝐴 ) )
21 11 12 19 20 syl3anc ⊢ ( ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ 𝐴 ) = 1 ) ∧ 𝑥 ∈ ℋ ) → ( ( projℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝑥 ) = ( ( ( 𝑥 ·ih 𝐴 ) / ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ) ·ℎ 𝐴 ) )
22 kbval ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐴 ) ‘ 𝑥 ) = ( ( 𝑥 ·ih 𝐴 ) ·ℎ 𝐴 ) )
23 22 3anidm12 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐴 ) ‘ 𝑥 ) = ( ( 𝑥 ·ih 𝐴 ) ·ℎ 𝐴 ) )
24 23 adantlr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ 𝐴 ) = 1 ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐴 ) ‘ 𝑥 ) = ( ( 𝑥 ·ih 𝐴 ) ·ℎ 𝐴 ) )
25 10 21 24 3eqtr4rd ⊢ ( ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ 𝐴 ) = 1 ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐴 ) ‘ 𝑥 ) = ( ( projℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝑥 ) )
26 25 ralrimiva ⊢ ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ 𝐴 ) = 1 ) → ∀ 𝑥 ∈ ℋ ( ( 𝐴 ketbra 𝐴 ) ‘ 𝑥 ) = ( ( projℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝑥 ) )
27 kbop ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 ketbra 𝐴 ) : ℋ ⟶ ℋ )
28 27 anidms ⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ketbra 𝐴 ) : ℋ ⟶ ℋ )
29 28 ffnd ⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ketbra 𝐴 ) Fn ℋ )
30 spansnch ⊢ ( 𝐴 ∈ ℋ → ( span ‘ { 𝐴 } ) ∈ Cℋ )
31 pjfn ⊢ ( ( span ‘ { 𝐴 } ) ∈ Cℋ → ( projℎ ‘ ( span ‘ { 𝐴 } ) ) Fn ℋ )
32 30 31 syl ⊢ ( 𝐴 ∈ ℋ → ( projℎ ‘ ( span ‘ { 𝐴 } ) ) Fn ℋ )
33 eqfnfv ⊢ ( ( ( 𝐴 ketbra 𝐴 ) Fn ℋ ∧ ( projℎ ‘ ( span ‘ { 𝐴 } ) ) Fn ℋ ) → ( ( 𝐴 ketbra 𝐴 ) = ( projℎ ‘ ( span ‘ { 𝐴 } ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( 𝐴 ketbra 𝐴 ) ‘ 𝑥 ) = ( ( projℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝑥 ) ) )
34 29 32 33 syl2anc ⊢ ( 𝐴 ∈ ℋ → ( ( 𝐴 ketbra 𝐴 ) = ( projℎ ‘ ( span ‘ { 𝐴 } ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( 𝐴 ketbra 𝐴 ) ‘ 𝑥 ) = ( ( projℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝑥 ) ) )
35 34 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ 𝐴 ) = 1 ) → ( ( 𝐴 ketbra 𝐴 ) = ( projℎ ‘ ( span ‘ { 𝐴 } ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( 𝐴 ketbra 𝐴 ) ‘ 𝑥 ) = ( ( projℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝑥 ) ) )
36 26 35 mpbird ⊢ ( ( 𝐴 ∈ ℋ ∧ ( normℎ ‘ 𝐴 ) = 1 ) → ( 𝐴 ketbra 𝐴 ) = ( projℎ ‘ ( span ‘ { 𝐴 } ) ) )