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	imbitrid	⊢ ( 𝐴 ∈ ℋ → ( ( 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 ‘ { 𝐴 } ) ) )