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 𝐷 ) )