Theorem kbass2

Description: Dirac bra-ket associative law ( <. A | B >. ) <. C | = <. A | ( | B >. <. C | ) , i.e., the juxtaposition of an inner product with a bra equals a ket juxtaposed with an outer product. (Contributed by NM, 23-May-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	kbass2	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ·fn ( bra ‘ 𝐶 ) ) = ( ( bra ‘ 𝐴 ) ∘ ( 𝐵 ketbra 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ovex	⊢ ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝑥 ) ) ∈ V
2		eqid	⊢ ( 𝑥 ∈ ℋ ↦ ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℋ ↦ ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝑥 ) ) )
3	1 2	fnmpti	⊢ ( 𝑥 ∈ ℋ ↦ ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝑥 ) ) ) Fn ℋ
4		bracl	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ∈ ℂ )
5		brafn	⊢ ( 𝐶 ∈ ℋ → ( bra ‘ 𝐶 ) : ℋ ⟶ ℂ )
6		hfmmval	⊢ ( ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ∈ ℂ ∧ ( bra ‘ 𝐶 ) : ℋ ⟶ ℂ ) → ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ·fn ( bra ‘ 𝐶 ) ) = ( 𝑥 ∈ ℋ ↦ ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝑥 ) ) ) )
7	4 5 6	syl2an	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐶 ∈ ℋ ) → ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ·fn ( bra ‘ 𝐶 ) ) = ( 𝑥 ∈ ℋ ↦ ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝑥 ) ) ) )
8	7	3impa	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ·fn ( bra ‘ 𝐶 ) ) = ( 𝑥 ∈ ℋ ↦ ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝑥 ) ) ) )
9	8	fneq1d	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ·fn ( bra ‘ 𝐶 ) ) Fn ℋ ↔ ( 𝑥 ∈ ℋ ↦ ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝑥 ) ) ) Fn ℋ ) )
10	3 9	mpbiri	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ·fn ( bra ‘ 𝐶 ) ) Fn ℋ )
11		brafn	⊢ ( 𝐴 ∈ ℋ → ( bra ‘ 𝐴 ) : ℋ ⟶ ℂ )
12		kbop	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ketbra 𝐶 ) : ℋ ⟶ ℋ )
13		fco	⊢ ( ( ( bra ‘ 𝐴 ) : ℋ ⟶ ℂ ∧ ( 𝐵 ketbra 𝐶 ) : ℋ ⟶ ℋ ) → ( ( bra ‘ 𝐴 ) ∘ ( 𝐵 ketbra 𝐶 ) ) : ℋ ⟶ ℂ )
14	11 12 13	syl2an	⊢ ( ( 𝐴 ∈ ℋ ∧ ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ) → ( ( bra ‘ 𝐴 ) ∘ ( 𝐵 ketbra 𝐶 ) ) : ℋ ⟶ ℂ )
15	14	3impb	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ∘ ( 𝐵 ketbra 𝐶 ) ) : ℋ ⟶ ℂ )
16	15	ffnd	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ∘ ( 𝐵 ketbra 𝐶 ) ) Fn ℋ )
17		simpl1	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → 𝐴 ∈ ℋ )
18		simpl2	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → 𝐵 ∈ ℋ )
19		braval	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) = ( 𝐵 ·ih 𝐴 ) )
20	17 18 19	syl2anc	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) = ( 𝐵 ·ih 𝐴 ) )
21		simpl3	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → 𝐶 ∈ ℋ )
22		simpr	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → 𝑥 ∈ ℋ )
23		braval	⊢ ( ( 𝐶 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( bra ‘ 𝐶 ) ‘ 𝑥 ) = ( 𝑥 ·ih 𝐶 ) )
24	21 22 23	syl2anc	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( bra ‘ 𝐶 ) ‘ 𝑥 ) = ( 𝑥 ·ih 𝐶 ) )
25	20 24	oveq12d	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( 𝐵 ·ih 𝐴 ) · ( 𝑥 ·ih 𝐶 ) ) )
26		hicl	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐵 ·ih 𝐴 ) ∈ ℂ )
27	18 17 26	syl2anc	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( 𝐵 ·ih 𝐴 ) ∈ ℂ )
28	20 27	eqeltrd	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ∈ ℂ )
29	21 5	syl	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( bra ‘ 𝐶 ) : ℋ ⟶ ℂ )
30		hfmval	⊢ ( ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ∈ ℂ ∧ ( bra ‘ 𝐶 ) : ℋ ⟶ ℂ ∧ 𝑥 ∈ ℋ ) → ( ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ·fn ( bra ‘ 𝐶 ) ) ‘ 𝑥 ) = ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝑥 ) ) )
31	28 29 22 30	syl3anc	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ·fn ( bra ‘ 𝐶 ) ) ‘ 𝑥 ) = ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) · ( ( bra ‘ 𝐶 ) ‘ 𝑥 ) ) )
32		hicl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝑥 ·ih 𝐶 ) ∈ ℂ )
33	22 21 32	syl2anc	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( 𝑥 ·ih 𝐶 ) ∈ ℂ )
34		ax-his3	⊢ ( ( ( 𝑥 ·ih 𝐶 ) ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( 𝑥 ·ih 𝐶 ) ·ℎ 𝐵 ) ·ih 𝐴 ) = ( ( 𝑥 ·ih 𝐶 ) · ( 𝐵 ·ih 𝐴 ) ) )
35	33 18 17 34	syl3anc	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑥 ·ih 𝐶 ) ·ℎ 𝐵 ) ·ih 𝐴 ) = ( ( 𝑥 ·ih 𝐶 ) · ( 𝐵 ·ih 𝐴 ) ) )
36	12	3adant1	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ketbra 𝐶 ) : ℋ ⟶ ℋ )
37		fvco3	⊢ ( ( ( 𝐵 ketbra 𝐶 ) : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( bra ‘ 𝐴 ) ∘ ( 𝐵 ketbra 𝐶 ) ) ‘ 𝑥 ) = ( ( bra ‘ 𝐴 ) ‘ ( ( 𝐵 ketbra 𝐶 ) ‘ 𝑥 ) ) )
38	36 37	sylan	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( bra ‘ 𝐴 ) ∘ ( 𝐵 ketbra 𝐶 ) ) ‘ 𝑥 ) = ( ( bra ‘ 𝐴 ) ‘ ( ( 𝐵 ketbra 𝐶 ) ‘ 𝑥 ) ) )
39		kbval	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝐵 ketbra 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ·ih 𝐶 ) ·ℎ 𝐵 ) )
40	18 21 22 39	syl3anc	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐵 ketbra 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ·ih 𝐶 ) ·ℎ 𝐵 ) )
41	40	fveq2d	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ ( ( 𝐵 ketbra 𝐶 ) ‘ 𝑥 ) ) = ( ( bra ‘ 𝐴 ) ‘ ( ( 𝑥 ·ih 𝐶 ) ·ℎ 𝐵 ) ) )
42		hvmulcl	⊢ ( ( ( 𝑥 ·ih 𝐶 ) ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐶 ) ·ℎ 𝐵 ) ∈ ℋ )
43	33 18 42	syl2anc	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐶 ) ·ℎ 𝐵 ) ∈ ℋ )
44		braval	⊢ ( ( 𝐴 ∈ ℋ ∧ ( ( 𝑥 ·ih 𝐶 ) ·ℎ 𝐵 ) ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ ( ( 𝑥 ·ih 𝐶 ) ·ℎ 𝐵 ) ) = ( ( ( 𝑥 ·ih 𝐶 ) ·ℎ 𝐵 ) ·ih 𝐴 ) )
45	17 43 44	syl2anc	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ ( ( 𝑥 ·ih 𝐶 ) ·ℎ 𝐵 ) ) = ( ( ( 𝑥 ·ih 𝐶 ) ·ℎ 𝐵 ) ·ih 𝐴 ) )
46	38 41 45	3eqtrd	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( bra ‘ 𝐴 ) ∘ ( 𝐵 ketbra 𝐶 ) ) ‘ 𝑥 ) = ( ( ( 𝑥 ·ih 𝐶 ) ·ℎ 𝐵 ) ·ih 𝐴 ) )
47	27 33	mulcomd	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝐵 ·ih 𝐴 ) · ( 𝑥 ·ih 𝐶 ) ) = ( ( 𝑥 ·ih 𝐶 ) · ( 𝐵 ·ih 𝐴 ) ) )
48	35 46 47	3eqtr4d	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( bra ‘ 𝐴 ) ∘ ( 𝐵 ketbra 𝐶 ) ) ‘ 𝑥 ) = ( ( 𝐵 ·ih 𝐴 ) · ( 𝑥 ·ih 𝐶 ) ) )
49	25 31 48	3eqtr4d	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ·fn ( bra ‘ 𝐶 ) ) ‘ 𝑥 ) = ( ( ( bra ‘ 𝐴 ) ∘ ( 𝐵 ketbra 𝐶 ) ) ‘ 𝑥 ) )
50	10 16 49	eqfnfvd	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ·fn ( bra ‘ 𝐶 ) ) = ( ( bra ‘ 𝐴 ) ∘ ( 𝐵 ketbra 𝐶 ) ) )