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 ∈ ℋ ∧ norm ℎ ⁡ A = 1 → A ketbra A = proj ℎ ⁡ span ⁡ A

Proof

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