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

Metamath Proof Explorer

Theorem kbass6

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 kbass6 ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) = ( 𝐴 ketbra ( ◡ bra ‘ ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 kbass5 ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) = ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) )
2 kbval ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) = ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) )
3 2 3expa ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) = ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) )
4 3 adantrr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) = ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) )
5 4 oveq1d ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) = ( ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ketbra 𝐷 ) )
6 hicl ⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐶 ·ih 𝐵 ) ∈ ℂ )
7 kbmul ⊢ ( ( ( 𝐶 ·ih 𝐵 ) ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ketbra 𝐷 ) = ( 𝐴 ketbra ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) )
8 6 7 syl3an1 ⊢ ( ( ( 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐴 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ketbra 𝐷 ) = ( 𝐴 ketbra ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) )
9 8 3exp ⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ∈ ℋ → ( 𝐷 ∈ ℋ → ( ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ketbra 𝐷 ) = ( 𝐴 ketbra ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) ) ) )
10 9 ex ⊢ ( 𝐶 ∈ ℋ → ( 𝐵 ∈ ℋ → ( 𝐴 ∈ ℋ → ( 𝐷 ∈ ℋ → ( ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ketbra 𝐷 ) = ( 𝐴 ketbra ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) ) ) ) )
11 10 com13 ⊢ ( 𝐴 ∈ ℋ → ( 𝐵 ∈ ℋ → ( 𝐶 ∈ ℋ → ( 𝐷 ∈ ℋ → ( ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ketbra 𝐷 ) = ( 𝐴 ketbra ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) ) ) ) )
12 11 imp43 ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ketbra 𝐷 ) = ( 𝐴 ketbra ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) )
13 bracl ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ∈ ℂ )
14 bracnln ⊢ ( 𝐷 ∈ ℋ → ( bra ‘ 𝐷 ) ∈ ( LinFn ∩ ContFn ) )
15 cnvbramul ⊢ ( ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ∈ ℂ ∧ ( bra ‘ 𝐷 ) ∈ ( LinFn ∩ ContFn ) ) → ( ◡ bra ‘ ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·fn ( bra ‘ 𝐷 ) ) ) = ( ( ∗ ‘ ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ) ·ℎ ( ◡ bra ‘ ( bra ‘ 𝐷 ) ) ) )
16 13 14 15 syl2an ⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝐷 ∈ ℋ ) → ( ◡ bra ‘ ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·fn ( bra ‘ 𝐷 ) ) ) = ( ( ∗ ‘ ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ) ·ℎ ( ◡ bra ‘ ( bra ‘ 𝐷 ) ) ) )
17 braval ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) = ( 𝐶 ·ih 𝐵 ) )
18 17 fveq2d ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ∗ ‘ ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ) = ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) )
19 cnvbrabra ⊢ ( 𝐷 ∈ ℋ → ( ◡ bra ‘ ( bra ‘ 𝐷 ) ) = 𝐷 )
20 18 19 oveqan12d ⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝐷 ∈ ℋ ) → ( ( ∗ ‘ ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ) ·ℎ ( ◡ bra ‘ ( bra ‘ 𝐷 ) ) ) = ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) )
21 16 20 eqtr2d ⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝐷 ∈ ℋ ) → ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) = ( ◡ bra ‘ ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·fn ( bra ‘ 𝐷 ) ) ) )
22 21 anasss ⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) = ( ◡ bra ‘ ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·fn ( bra ‘ 𝐷 ) ) ) )
23 kbass2 ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·fn ( bra ‘ 𝐷 ) ) = ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) )
24 23 3expb ⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·fn ( bra ‘ 𝐷 ) ) = ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) )
25 24 fveq2d ⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ◡ bra ‘ ( ( ( bra ‘ 𝐵 ) ‘ 𝐶 ) ·fn ( bra ‘ 𝐷 ) ) ) = ( ◡ bra ‘ ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ) )
26 22 25 eqtr2d ⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ◡ bra ‘ ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ) = ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) )
27 26 adantll ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ◡ bra ‘ ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ) = ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) )
28 27 oveq2d ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐴 ketbra ( ◡ bra ‘ ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ) ) = ( 𝐴 ketbra ( ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ·ℎ 𝐷 ) ) )
29 12 28 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( 𝐶 ·ih 𝐵 ) ·ℎ 𝐴 ) ketbra 𝐷 ) = ( 𝐴 ketbra ( ◡ bra ‘ ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ) ) )
30 1 5 29 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) = ( 𝐴 ketbra ( ◡ bra ‘ ( ( bra ‘ 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ) ) )