Metamath Proof Explorer


Theorem kbass5

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

Proof

Step Hyp Ref Expression
1 kbval ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝐶 ketbra 𝐷 ) ‘ 𝑥 ) = ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) )
2 1 3expa ( ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐶 ketbra 𝐷 ) ‘ 𝑥 ) = ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) )
3 2 adantll ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐶 ketbra 𝐷 ) ‘ 𝑥 ) = ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) )
4 3 fveq2d ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ ( ( 𝐶 ketbra 𝐷 ) ‘ 𝑥 ) ) = ( ( 𝐴 ketbra 𝐵 ) ‘ ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) ) )
5 simplll ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → 𝐴 ∈ ℋ )
6 simpllr ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → 𝐵 ∈ ℋ )
7 simpr ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → 𝑥 ∈ ℋ )
8 simplrr ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → 𝐷 ∈ ℋ )
9 hicl ( ( 𝑥 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( 𝑥 ·ih 𝐷 ) ∈ ℂ )
10 7 8 9 syl2anc ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( 𝑥 ·ih 𝐷 ) ∈ ℂ )
11 simplrl ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → 𝐶 ∈ ℋ )
12 hvmulcl ( ( ( 𝑥 ·ih 𝐷 ) ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) ∈ ℋ )
13 10 11 12 syl2anc ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) ∈ ℋ )
14 kbval ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) ) = ( ( ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) ·ih 𝐵 ) · 𝐴 ) )
15 5 6 13 14 syl3anc ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) ) = ( ( ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) ·ih 𝐵 ) · 𝐴 ) )
16 4 15 eqtrd ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ ( ( 𝐶 ketbra 𝐷 ) ‘ 𝑥 ) ) = ( ( ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) ·ih 𝐵 ) · 𝐴 ) )
17 kbop ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( 𝐶 ketbra 𝐷 ) : ℋ ⟶ ℋ )
18 17 adantl ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐶 ketbra 𝐷 ) : ℋ ⟶ ℋ )
19 fvco3 ( ( ( 𝐶 ketbra 𝐷 ) : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ‘ 𝑥 ) = ( ( 𝐴 ketbra 𝐵 ) ‘ ( ( 𝐶 ketbra 𝐷 ) ‘ 𝑥 ) ) )
20 18 19 sylan ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ‘ 𝑥 ) = ( ( 𝐴 ketbra 𝐵 ) ‘ ( ( 𝐶 ketbra 𝐷 ) ‘ 𝑥 ) ) )
21 kbval ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) = ( ( 𝐶 ·ih 𝐵 ) · 𝐴 ) )
22 5 6 11 21 syl3anc ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) = ( ( 𝐶 ·ih 𝐵 ) · 𝐴 ) )
23 22 oveq2d ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐷 ) · ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ) = ( ( 𝑥 ·ih 𝐷 ) · ( ( 𝐶 ·ih 𝐵 ) · 𝐴 ) ) )
24 kbop ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ketbra 𝐵 ) : ℋ ⟶ ℋ )
25 24 ffvelrnda ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ∈ ℋ )
26 25 adantrr ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ∈ ℋ )
27 26 adantr ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ∈ ℋ )
28 kbval ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ∈ ℋ ∧ 𝐷 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ‘ 𝑥 ) = ( ( 𝑥 ·ih 𝐷 ) · ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ) )
29 27 8 7 28 syl3anc ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ‘ 𝑥 ) = ( ( 𝑥 ·ih 𝐷 ) · ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ) )
30 ax-his3 ( ( ( 𝑥 ·ih 𝐷 ) ∈ ℂ ∧ 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) ·ih 𝐵 ) = ( ( 𝑥 ·ih 𝐷 ) · ( 𝐶 ·ih 𝐵 ) ) )
31 10 11 6 30 syl3anc ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) ·ih 𝐵 ) = ( ( 𝑥 ·ih 𝐷 ) · ( 𝐶 ·ih 𝐵 ) ) )
32 31 oveq1d ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) ·ih 𝐵 ) · 𝐴 ) = ( ( ( 𝑥 ·ih 𝐷 ) · ( 𝐶 ·ih 𝐵 ) ) · 𝐴 ) )
33 hicl ( ( 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐶 ·ih 𝐵 ) ∈ ℂ )
34 11 6 33 syl2anc ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( 𝐶 ·ih 𝐵 ) ∈ ℂ )
35 ax-hvmulass ( ( ( 𝑥 ·ih 𝐷 ) ∈ ℂ ∧ ( 𝐶 ·ih 𝐵 ) ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( ( ( 𝑥 ·ih 𝐷 ) · ( 𝐶 ·ih 𝐵 ) ) · 𝐴 ) = ( ( 𝑥 ·ih 𝐷 ) · ( ( 𝐶 ·ih 𝐵 ) · 𝐴 ) ) )
36 10 34 5 35 syl3anc ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑥 ·ih 𝐷 ) · ( 𝐶 ·ih 𝐵 ) ) · 𝐴 ) = ( ( 𝑥 ·ih 𝐷 ) · ( ( 𝐶 ·ih 𝐵 ) · 𝐴 ) ) )
37 32 36 eqtrd ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) ·ih 𝐵 ) · 𝐴 ) = ( ( 𝑥 ·ih 𝐷 ) · ( ( 𝐶 ·ih 𝐵 ) · 𝐴 ) ) )
38 23 29 37 3eqtr4d ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ‘ 𝑥 ) = ( ( ( ( 𝑥 ·ih 𝐷 ) · 𝐶 ) ·ih 𝐵 ) · 𝐴 ) )
39 16 20 38 3eqtr4d ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ‘ 𝑥 ) = ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ‘ 𝑥 ) )
40 39 ralrimiva ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ∀ 𝑥 ∈ ℋ ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ‘ 𝑥 ) = ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ‘ 𝑥 ) )
41 fco ( ( ( 𝐴 ketbra 𝐵 ) : ℋ ⟶ ℋ ∧ ( 𝐶 ketbra 𝐷 ) : ℋ ⟶ ℋ ) → ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) : ℋ ⟶ ℋ )
42 24 17 41 syl2an ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) : ℋ ⟶ ℋ )
43 kbop ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) : ℋ ⟶ ℋ )
44 25 43 sylan ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐶 ∈ ℋ ) ∧ 𝐷 ∈ ℋ ) → ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) : ℋ ⟶ ℋ )
45 44 anasss ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) : ℋ ⟶ ℋ )
46 ffn ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) : ℋ ⟶ ℋ → ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) Fn ℋ )
47 ffn ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) : ℋ ⟶ ℋ → ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) Fn ℋ )
48 eqfnfv ( ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) Fn ℋ ∧ ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) Fn ℋ ) → ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) = ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ↔ ∀ 𝑥 ∈ ℋ ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ‘ 𝑥 ) = ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ‘ 𝑥 ) ) )
49 46 47 48 syl2an ( ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) : ℋ ⟶ ℋ ∧ ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) : ℋ ⟶ ℋ ) → ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) = ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ↔ ∀ 𝑥 ∈ ℋ ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ‘ 𝑥 ) = ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ‘ 𝑥 ) ) )
50 42 45 49 syl2anc ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) = ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ↔ ∀ 𝑥 ∈ ℋ ( ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) ‘ 𝑥 ) = ( ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) ‘ 𝑥 ) ) )
51 40 50 mpbird ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ketbra 𝐵 ) ∘ ( 𝐶 ketbra 𝐷 ) ) = ( ( ( 𝐴 ketbra 𝐵 ) ‘ 𝐶 ) ketbra 𝐷 ) )