kbass1

Description: Dirac bra-ket associative law ( | A >. <. B | ) | C >. = | A >. ( <. B | C >. ) , i.e., the juxtaposition of an outer product with a ket equals a bra juxtaposed with an inner product. Since <. B | C >. is a complex number, it is the first argument in the inner product .h that it is mapped to, although in Dirac notation it is placed after the ket. (Contributed by NM, 15-May-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	kbass1	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) = ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·_ℎ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		kbval	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) = ( ( 𝐶 ·_ih 𝐵 ) ·_ℎ 𝐴 ) )
2		braval	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) = ( 𝐶 ·_ih 𝐵 ) )
3	2	3adant1	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) = ( 𝐶 ·_ih 𝐵 ) )
4	3	oveq1d	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·_ℎ 𝐴 ) = ( ( 𝐶 ·_ih 𝐵 ) ·_ℎ 𝐴 ) )
5	1 4	eqtr4d	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) = ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·_ℎ 𝐴 ) )

Metamath Proof Explorer

Theorem kbass1

Proof