Theorem kbass2t 9962

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.

Assertion

Ref	Expression
kbass2t	|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> (((bra` A)` B) .fn (bra` C)) = ((bra` A) o. (B ketbra C)))

Proof of Theorem kbass2t

Step	Hyp	Ref	Expression
1		hfmmvalt 9432	. . . 4 |- ((((bra` A)` B) e. CC /\ (bra` C):H~-->CC) -> (((bra` A)` B) .fn (bra` C)) = {<.x, y>. | (x e. H~ /\ y = (((bra` A)` B) x. ((bra` C)` x)))})
2		braclt 9789	. . . 4 |- ((A e. H~ /\ B e. H~) -> ((bra` A)` B) e. CC)
3		brafnt 9787	. . . 4 |- (C e. H~ -> (bra` C):H~-->CC)
4	1, 2, 3	syl2an 454	. . 3 |- (((A e. H~ /\ B e. H~) /\ C e. H~) -> (((bra` A)` B) .fn (bra` C)) = {<.x, y>. | (x e. H~ /\ y = (((bra` A)` B) x. ((bra` C)` x)))})
5	4	3impa 826	. 2 |- ((A e. H~ /\ B e. H~ /\ C e. H~) -> (((bra` A)` B) .fn (bra` C)) = {<.x, y>. | (x e. H~ /\ y = (((bra` A)` B) x. ((bra` C)` x)))})
6		axmulcom 5248	. . . . . . . 8 |- (((B .ih A) e. CC /\ (x .ih C) e. CC) -> ((B .ih A) x. (x .ih C)) = ((x .ih C) x. (B .ih A)))
7		hiclt 8868	. . . . . . . . . . 11 |- ((B e. H~ /\ A e. H~) -> (B .ih A) e. CC)
8	7	ancoms 436	. . . . . . . . . 10 |- ((A e. H~ /\ B e. H~) -> (B .ih A) e. CC)
9	8	3adant3 797	. . . . . . . . 9 |- ((A e. H~ /\ B e. H~ /\ C e. H~) -> (B .ih A) e. CC)
10	9	adantr 389	. . . . . . . 8 |- (((A e. H~ /\ B e. H~ /\ C e. H~) /\ x e. H~) -> (B .ih A) e. CC)
11		hiclt 8868	. . . . . . . . . 10 |- ((x e. H~ /\ C e. H~) -> (x .ih C) e. CC)
12	11	ancoms 436	. . . . . . . . 9 |- ((C e. H~ /\ x e. H~) -> (x .ih C) e. CC)
13	12	3ad2antl3 809	. . . . . . . 8 |- (((A e. H~ /\ B e. H~ /\ C e. H~) /\ x e. H~) -> (x .ih C) e. CC)
14	6, 10, 13	sylanc 471	. . . . . . 7 |- (((A e. H~ /\ B e. H~ /\ C e. H~) /\ x e. H~) -> ((B .ih A) x. (x .ih C)) = ((x .ih C) x. (B .ih A)))
15		ax-his3 8872	. . . . . . . 8 |- (((x .ih C) e. CC /\ B e. H~ /\ A e. H~) -> (((x .ih C) .h B) .ih A) = ((x .ih C) x. (B .ih A)))
16		3simp2 787	. . . . . . . . 9 |- ((A e. H~ /\ B e. H~ /\ C e. H~) -> B e. H~)
17	16	adantr 389	. . . . . . . 8 |- (((A e. H~ /\ B e. H~ /\ C e. H~) /\ x e. H~) -> B e. H~)
18		3simp1 786	. . . . . . . . 9 |- ((A e. H~ /\ B e. H~ /\ C e. H~) -> A e. H~)
19	18	adantr 389	. . . . . . . 8 |- (((A e. H~ /\ B e. H~ /\ C e. H~) /\ x e. H~) -> A e. H~)
20	15, 13, 17, 19	syl3anc 856	. . . . . . 7 |- (((A e. H~ /\ B e. H~ /\ C e. H~) /\ x e. H~) -> (((x .ih C) .h B) .ih A) = ((x .ih C) x. (B .ih A)))
21	14, 20	eqtr4d 1502	. . . . . 6 |- (((A e. H~ /\ B e. H~ /\ C e. H~) /\ x e. H~) -> ((B .ih A) x. (x .ih C)) = (((x .ih C) .h B) .ih A))
22		bravalvalt 9784	. . . . . . . . 9 |- ((A e. H~ /\ B e. H~) -> ((bra` A)` B) = (B .ih A))
23	22	3adant3 797	. . . . . . . 8 |- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((bra` A)` B) = (B .ih A))
24	23	adantr 389	. . . . . . 7 |- (((A e. H~ /\ B e. H~ /\ C e. H~) /\ x e. H~) -> ((bra` A)` B) = (B .ih A))
25		bravalvalt 9784	. . . . . . . 8 |- ((C e. H~ /\ x e. H~) -> ((bra` C)` x) = (x .ih C))
26	25	3ad2antl3 809	. . . . . . 7 |- (((A e. H~ /\ B e. H~ /\ C e. H~) /\ x e. H~) -> ((bra` C)` x) = (x .ih C))
27	24, 26	opreq12d 3963	. . . . . 6 |- (((A e. H~ /\ B e. H~ /\ C e. H~) /\ x e. H~) -> (((bra` A)` B) x. ((bra` C)` x)) = ((B .ih A) x. (x .ih C)))
28		oprex 3968	. . . . . . . . 9 |- ((x .ih C) .h B) e. V
29		csbopr1g 3973	. . . . . . . . 9 |- (((x .ih C) .h B) e. V -> [_((x .ih C) .h B) / x]_(x .ih A) = ([_((x .ih C) .h B) / x]_x .ih A))
30	28, 29	ax-mp 7	. . . . . . . 8 |- [_((x .ih C) .h B) / x]_(x .ih A) = ([_((x .ih C) .h B) / x]_x .ih A)
31		csbvarg 2011	. . . . . . . . . 10 |- (((x .ih C) .h B) e. V -> [_((x .ih C) .h B) / x]_x = ((x .ih C) .h B))
32	28, 31	ax-mp 7	. . . . . . . . 9 |- [_((x .ih C) .h B) / x]_x = ((x .ih C) .h B)
33	32	opreq1i 3956	. . . . . . . 8 |- ([_((x .ih C) .h B) / x]_x .ih A) = (((x .ih C) .h B) .ih A)
34	30, 33	eqtr 1487	. . . . . . 7 |- [_((x .ih C) .h B) / x]_(x .ih A) = (((x .ih C) .h B) .ih A)
35	34	a1i 8	. . . . . 6 |- (((A e. H~ /\ B e. H~ /\ C e. H~) /\ x e. H~) -> [_((x .ih C) .h B) / x]_(x .ih A) = (((x .ih C) .h B) .ih A))
36	21, 27, 35	3eqtr4d 1509	. . . . 5 |- (((A e. H~ /\ B e. H~ /\ C e. H~) /\ x e. H~) -> (((bra` A)` B) x. ((bra` C)` x)) = [_((x .ih C) .h B) / x]_(x .ih A))
37	36	eqeq2d 1478	. . . 4 |- (((A e. H~ /\ B e. H~ /\ C e. H~) /\ x e. H~) -> (y = (((bra` A)` B) x. ((bra` C)` x)) <-> y = [_((x .ih C) .h B) / x]_(x .ih A)))
38	37	pm5.32da 647	. . 3 |- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((x e. H~ /\ y = (((bra` A)` B) x. ((bra` C)` x))) <-> (x e. H~ /\ y = [_((x .ih C) .h B) / x]_(x .ih A))))
39	38	opabbidv 2660	. 2 |- ((A e. H~ /\ B e. H~ /\ C e. H~) -> {<.x, y>. | (x e. H~ /\ y = (((bra` A)` B) x. ((bra` C)` x)))} = {<.x, y>. | (x e. H~ /\ y = [_((x .ih C) .h B) / x]_(x .ih A))})
40		bravalt 9783	. . . . . 6 |- (A e. H~ -> (bra` A) = {<.x, y>. | (x e. H~ /\ y = (x .ih A))})
41	40	coeq1d 3274	. . . . 5 |- (A e. H~ -> ((bra` A) o. (B ketbra C)) = ({<.x, y>. | (x e. H~ /\ y = (x .ih A))} o. (B ketbra C)))
42		kbvalt 9792	. . . . . 6 |- ((B e. H~ /\ C e. H~) -> (B ketbra C) = {<.x, y>. | (x e. H~ /\ y = ((x .ih C) .h B))})
43	42	coeq2d 3275	. . . . 5 |- ((B e. H~ /\ C e. H~) -> ({<.x, y>. | (x e. H~ /\ y = (x .ih A))} o. (B ketbra C)) = ({<.x, y>. | (x e. H~ /\ y = (x .ih A))} o. {<.x, y>. | (x e. H~ /\ y = ((x .ih C) .h B))}))
44	41, 43	sylan9eq 1519	. . . 4 |- ((A e. H~ /\ (B e. H~ /\ C e. H~)) -> ((bra` A) o. (B ketbra C)) = ({<.x, y>. | (x e. H~ /\ y = (x .ih A))} o. {<.x, y>. | (x e. H~ /\ y = ((x .ih C) .h B))}))
45	44	3impb 827	. . 3 |- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((bra` A) o. (B ketbra C)) = ({<.x, y>. | (x e. H~ /\ y = (x .ih A))} o. {<.x, y>. | (x e. H~ /\ y = ((x .ih C) .h B))}))
46		hvmulclt 8804	. . . . . . . . 9 |- (((x .ih C) e. CC /\ B e. H~) -> ((x .ih C) .h B) e. H~)
47	46, 11	sylan 448	. . . . . . . 8 |- (((x e. H~ /\ C e. H~) /\ B e. H~) -> ((x .ih C) .h B) e. H~)
48	47	ancom31s 490	. . . . . . 7 |- (((B e. H~ /\ C e. H~)