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

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 ffvelcdmda ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 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 𝐷 ) )