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 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ketbra B ∘ C ketbra D = A ketbra B ⁡ C ketbra D

Proof

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