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∈ℋ→AketbraB∘CketbraD=AketbraB⁡CketbraD

Proof

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