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

Metamath Proof Explorer

Theorem kbass4

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 kbass4 ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) ) = ( ( bra ‘ 𝐴 ) ‘ ( ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) ·ℎ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 bracl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ∈ ℂ )
2 bracl ⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) ∈ ℂ )
3 mulcom ⊢ ( ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ∈ ℂ ∧ ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) ∈ ℂ ) → ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) ) = ( ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) · ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ) )
4 1 2 3 syl2an ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) ) = ( ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) · ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ) )
5 bralnfn ⊢ ( 𝐴 ∈ ℋ → ( bra ‘ 𝐴 ) ∈ LinFn )
6 5 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( bra ‘ 𝐴 ) ∈ LinFn )
7 2 adantl ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) ∈ ℂ )
8 simplr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → 𝐵 ∈ ℋ )
9 lnfnmul ⊢ ( ( ( bra ‘ 𝐴 ) ∈ LinFn ∧ ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ ( ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) ·ℎ 𝐵 ) ) = ( ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) · ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ) )
10 6 7 8 9 syl3anc ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( bra ‘ 𝐴 ) ‘ ( ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) ·ℎ 𝐵 ) ) = ( ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) · ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ) )
11 4 10 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) ) = ( ( bra ‘ 𝐴 ) ‘ ( ( ( bra ‘ 𝐶 ) ‘ 𝐷 ) ·ℎ 𝐵 ) ) )