This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem kbass3

Description: Dirac bra-ket associative law <. A | B >. <. C | D >. = ( <. A | B >. <. C | ) | D >. . (Contributed by NM, 30-May-2006) (New usage is discouraged.)

Ref Expression
Assertion kbass3 ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) ) = ( ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ·fn ( bra ‘ 𝐶 ) ) ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 bracl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ∈ ℂ )
2 1 adantr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ∈ ℂ )
3 brafn ⊢ ( 𝐶 ∈ ℋ → ( bra ‘ 𝐶 ) : ℋ ⟶ ℂ )
4 3 ad2antrl ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( bra ‘ 𝐶 ) : ℋ ⟶ ℂ )
5 simprr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → 𝐷 ∈ ℋ )
6 hfmval ⊢ ( ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ∈ ℂ ∧ ( bra ‘ 𝐶 ) : ℋ ⟶ ℂ ∧ 𝐷 ∈ ℋ ) → ( ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ·fn ( bra ‘ 𝐶 ) ) ‘ 𝐷 ) = ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) ) )
7 2 4 5 6 syl3anc ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ·fn ( bra ‘ 𝐶 ) ) ‘ 𝐷 ) = ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) ) )
8 7 eqcomd ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) ) = ( ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ·fn ( bra ‘ 𝐶 ) ) ‘ 𝐷 ) )