Theorem kbass5t 9991

Description: Dirac bra-ket associative law ( | A>. <.B | )( | C>. <.D | ) = (( | A>. <.B | ) | C>.)<.D |.

Assertion

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

Proof of Theorem kbass5t

Step	Hyp	Ref	Expression
1		kbvalt 9815	. . . . . . 7 |- ((C e. H~ /\ D e. H~) -> (C ketbra D) = {<.x, y>. | (x e. H~ /\ y = ((x .ih D) .h C))})
2	1	rneqd 3336	. . . . . 6 |- ((C e. H~ /\ D e. H~) -> ran ( C ketbra D) = ran {<.x, y>. | (x e. H~ /\ y = ((x .ih D) .h C))})
3		kbopt 9816	. . . . . . 7 |- ((C e. H~ /\ D e. H~) -> (C ketbra D):H~-->H~)
4		frn 3624	. . . . . . 7 |- ((C ketbra D):H~-->H~ -> ran ( C ketbra D) (_ H~)
5	3, 4	syl 10	. . . . . 6 |- ((C e. H~ /\ D e. H~) -> ran ( C ketbra D) (_ H~)
6	2, 5	eqsstr3d 2092	. . . . 5 |- ((C e. H~ /\ D e. H~) -> ran {<.x, y>. | (x e. H~ /\ y = ((x .ih D) .h C))} (_ H~)
7	6	adantl 388	. . . 4 |- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> ran {<.x, y>. | (x e. H~ /\ y = ((x .ih D) .h C))} (_ H~)
8		oprex 3974	. . . . 5 |- ((x .ih B) .h A) e. V
9		oprex 3974	. . . . 5 |- ((x .ih D) .h C) e. V
10		eqid 1473	. . . . 5 |- {<.x, y>. | (x e. H~ /\ y = ((x .ih B) .h A))} = {<.x, y>. | (x e. H~ /\ y = ((x .ih B) .h A))}
11		eqid 1473	. . . . 5 |- {<.x, y>. | (x e. H~ /\ y = ((x .ih D) .h C))} = {<.x, y>. | (x e. H~ /\ y = ((x .ih D) .h C))}
12	8, 9, 10, 11	fopabcos 3824	. . . 4 |- (ran {<.x, y>. | (x e. H~ /\ y = ((x .ih D) .h C))} (_ H~ -> ({<.x, y>. | (x e. H~ /\ y = ((x .ih B) .h A))} o. {<.x, y>. | (x e. H~ /\ y = ((x .ih D) .h C))}) = {<.x, y>. | (x e. H~ /\ y = [_((x .ih D) .h C) / x]_((x .ih B) .h A))})
13	7, 12	syl 10	. . 3 |- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> ({<.x, y>. | (x e. H~ /\ y = ((x .ih B) .h A))} o. {<.x, y>. | (x e. H~ /\ y = ((x .ih D) .h C))}) = {<.x, y>. | (x e. H~ /\ y = [_((x .ih D) .h C) / x]_((x .ih B) .h A))})
14		ax-his3 8890	. . . . . . . . . . 11 |- (((x .ih D) e. CC /\ C e. H~ /\ B e. H~) -> (((x .ih D) .h C) .ih B) = ((x .ih D) x. (C .ih B)))
15		hiclt 8886	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ D e. H~) -> (x .ih D) e. CC)
16	15	ancoms 436	. . . . . . . . . . . . 13 |- ((D e. H~ /\ x e. H~) -> (x .ih D) e. CC)
17	16	adantll 392	. . . . . . . . . . . 12 |- (((C e. H~ /\ D e. H~) /\ x e. H~) -> (x .ih D) e. CC)
18	17	adantll 392	. . . . . . . . . . 11 |- (((B e. H~ /\ (C e. H~ /\ D e. H~)) /\ x e. H~) -> (x .ih D) e. CC)
19		pm3.26 319	. . . . . . . . . . . 12 |- ((C e. H~ /\ D e. H~) -> C e. H~)
20	19	ad2antlr 405	. . . . . . . . . . 11 |- (((B e. H~ /\ (C e. H~ /\ D e. H~)) /\ x e. H~) -> C e. H~)
21		simpll 412	. . . . . . . . . . 11 |- (((B e. H~ /\ (C e. H~ /\ D e. H~)) /\ x e. H~) -> B e. H~)
22	14, 18, 20, 21	syl3anc 857	. . . . . . . . . 10 |- (((B e. H~ /\ (C e. H~ /\ D e. H~)) /\ x e. H~) -> (((x .ih D) .h C) .ih B) = ((x .ih D) x. (C .ih B)))
23	22	adantlll 396	. . . . . . . . 9 |- ((((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) /\ x e. H~) -> (((x .ih D) .h C) .ih B) = ((x .ih D) x. (C .ih B)))
24	23	opreq1d 3966	. . . . . . . 8 |- ((((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) /\ x e. H~) -> ((((x .ih D) .h C) .ih B) .h A) = (((x .ih D) x. (C .ih B)) .h A))
25		ax-hvmulass 8816	. . . . . . . . 9 |- (((x .ih D) e. CC /\ (C .ih B) e. CC /\ A e. H~) -> (((x .ih D) x. (C .ih B)) .h A) = ((x .ih D) .h ((C .ih B) .h A)))
26	17	adantll 392	. . . . . . . . 9 |- ((((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) /\ x e. H~) -> (x .ih D) e. CC)
27		hiclt 8886	. . . . . . . . . . . 12 |- ((C e. H~ /\ B e. H~) -> (C .ih B) e. CC)
28	27	ancoms 436	. . . . . . . . . . 11 |- ((B e. H~ /\ C e. H~) -> (C .ih B) e. CC)
29	28	ad2ant2lr 410	. . . . . . . . . 10 |- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> (C .ih B) e. CC)
30	29	adantr 389	. . . . . . . . 9 |- ((((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) /\ x e. H~) -> (C .ih B) e. CC)
31		pm3.26 319	. . . . . . . . . 10 |- ((A e. H~ /\ B e. H~) -> A e. H~)
32	31	ad2antrr 404	. . . . . . . . 9 |- ((((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) /\ x e. H~) -> A e. H~)
33	25, 26, 30, 32	syl3anc 857	. . . . . . . 8 |- ((((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) /\ x e. H~) -> (((x .ih D) x. (C .ih B)) .h A) = ((x .ih D) .h ((C .ih B) .h A)))
34	24, 33	eqtrd 1504	. . . . . . 7 |- ((((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) /\ x e. H~) -> ((((x .ih D) .h C) .ih B) .h A) = ((x .ih D) .h ((C .ih B) .h A)))
35		csbopr1g 3979	. . . . . . . . 9 |- (((x .ih D) .h C) e. V -> [_((x .ih D) .h C) / x]_((x .ih B) .h A) = ([_((x .ih D) .h C) / x]_(x .ih B) .h A))
36	9, 35	ax-mp 7	. . . . . . . 8 |- [_((x .ih D) .h C) / x]_((x .ih B) .h A) = ([_((x .ih D) .h C) / x]_(x .ih B) .h A)
37		csbopr1g 3979	. . . . . . . . . . 11 |- (((x .ih D) .h C) e. V -> [_((x .ih D) .h C) / x]_(x .ih B) = ([_((x .ih D) .h C) / x]_x .ih B))
38	9, 37	ax-mp 7	. . . . . . . . . 10 |- [_((x .ih D) .h C) / x]_(x .ih B) = ([_((x .ih D) .h C) / x]_x .ih B)
39		csbvarg 2017	. . . . . . . . . . . 12 |- (((x .ih D) .h C) e. V -> [_((x .ih D) .h C) / x]_x = ((x .ih D) .h C))
40	9, 39	ax-mp 7	. . . . . . . . . . 11 |- [_((x .ih D) .h C) / x]_x = ((x .ih D) .h C)
41	40	opreq1i 3962	. . . . . . . . . 10 |- ([_((x .ih D) .h C) / x]_x .ih B) = (((x .ih D) .h C) .ih B)
42	38, 41	eqtr 1492	. . . . . . . . 9 |- [_((x .ih D) .h C) / x]_(x .ih B) = (((x .ih D) .h C) .ih B)
43	42	opreq1i 3962	. . . . . . . 8 |- ([_((x .ih D) .h C) / x]_(x .ih B) .h A) = ((((x .ih D) .h C) .ih B) .h A)
44	36, 43	eqtr 1492	. . . . . . 7 |- [_((x .ih D) .h C) / x]_((x .ih B) .h A) = ((((x .ih D) .h C) .ih B) .h A)
45	34, 44	syl5eq 1516	. . . . . 6 |- ((((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) /\ x e. H~) -> [_((x .ih D) .h C) / x]_((x .ih B) .h A) = ((x .ih D) .h ((C .ih B) .h A)))
46	45	eqeq2d 1483	. . . . 5 |- ((((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) /\ x e. H~) -> (y = [_((x .ih D) .h C) / x]_((x .ih B) .h A) <-> y = ((x .ih D) .h ((C .ih B) .h A))))
47	46	pm5.32da 648	. . . 4 |- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> (