Theorem unierr 9975

Description: If we approximate a chain of unitary transformations (quantum computer gates) F, G by other unitary transformations S, T, the error increases at most additively. Equation 4.73 of [NielsenChuang] p. 195.

Hypotheses

Ref	Expression
unierr.1	|- F e. UniOp
unierr.2	|- G e. UniOp
unierr.3	|- S e. UniOp
unierr.4	|- T e. UniOp

Assertion

Ref	Expression
unierr	|- (normop` ((F o. G) -op (S o. T))) <_ ((normop` (F -op S)) + (normop` (G -op T)))

Proof of Theorem unierr

Step	Hyp	Ref	Expression
1		unierr.1	. . . . . . . 8 |- F e. UniOp
2		unopbdt 9878	. . . . . . . 8 |- (F e. UniOp -> F e. BndLinOp)
3	1, 2	ax-mp 7	. . . . . . 7 |- F e. BndLinOp
4		bdopft 9729	. . . . . . 7 |- (F e. BndLinOp -> F:H~-->H~)
5	3, 4	ax-mp 7	. . . . . 6 |- F:H~-->H~
6		unierr.2	. . . . . . . 8 |- G e. UniOp
7		unopbdt 9878	. . . . . . . 8 |- (G e. UniOp -> G e. BndLinOp)
8	6, 7	ax-mp 7	. . . . . . 7 |- G e. BndLinOp
9		bdopft 9729	. . . . . . 7 |- (G e. BndLinOp -> G:H~-->H~)
10	8, 9	ax-mp 7	. . . . . 6 |- G:H~-->H~
11	5, 10	hocof 9632	. . . . 5 |- (F o. G):H~-->H~
12		unierr.3	. . . . . . . 8 |- S e. UniOp
13		unopbdt 9878	. . . . . . . 8 |- (S e. UniOp -> S e. BndLinOp)
14	12, 13	ax-mp 7	. . . . . . 7 |- S e. BndLinOp
15		bdopft 9729	. . . . . . 7 |- (S e. BndLinOp -> S:H~-->H~)
16	14, 15	ax-mp 7	. . . . . 6 |- S:H~-->H~
17		unierr.4	. . . . . . . 8 |- T e. UniOp
18		unopbdt 9878	. . . . . . . 8 |- (T e. UniOp -> T e. BndLinOp)
19	17, 18	ax-mp 7	. . . . . . 7 |- T e. BndLinOp
20		bdopft 9729	. . . . . . 7 |- (T e. BndLinOp -> T:H~-->H~)
21	19, 20	ax-mp 7	. . . . . 6 |- T:H~-->H~
22	16, 21	hocof 9632	. . . . 5 |- (S o. T):H~-->H~
23	11, 22	hosubcl 9635	. . . 4 |- ((F o. G) -op (S o. T)):H~-->H~
24		nmop0h 9854	. . . 4 |- ((H~ = 0H /\ ((F o. G) -op (S o. T)):H~-->H~) -> (normop` ((F o. G) -op (S o. T))) = 0)
25	23, 24	mpan2 695	. . 3 |- (H~ = 0H -> (normop` ((F o. G) -op (S o. T))) = 0)
26	5, 16	hosubcl 9635	. . . . . 6 |- (F -op S):H~-->H~
27		nmop0h 9854	. . . . . 6 |- ((H~ = 0H /\ (F -op S):H~-->H~) -> (normop` (F -op S)) = 0)
28	26, 27	mpan2 695	. . . . 5 |- (H~ = 0H -> (normop` (F -op S)) = 0)
29	10, 21	hosubcl 9635	. . . . . 6 |- (G -op T):H~-->H~
30		nmop0h 9854	. . . . . 6 |- ((H~ = 0H /\ (G -op T):H~-->H~) -> (normop` (G -op T)) = 0)
31	29, 30	mpan2 695	. . . . 5 |- (H~ = 0H -> (normop` (G -op T)) = 0)
32	28, 31	opreq12d 3969	. . . 4 |- (H~ = 0H -> ((normop` (F -op S)) + (normop` (G -op T))) = (0 + 0))
33		0re 5420	. . . . . 6 |- 0 e. RR
34	33	leid 5592	. . . . 5 |- 0 <_ 0
35		0cn 5308	. . . . . 6 |- 0 e. CC
36	35	addid1 5310	. . . . 5 |- (0 + 0) = 0
37	34, 36	breqtrr 2635	. . . 4 |- 0 <_ (0 + 0)
38	32, 37	syl5breqr 2646	. . 3 |- (H~ = 0H -> 0 <_ ((normop` (F -op S)) + (normop` (G -op T))))
39	25, 38	eqbrtrd 2630	. 2 |- (H~ = 0H -> (normop` ((F o. G) -op (S o. T))) <_ ((normop` (F -op S)) + (normop` (G -op T))))
40		nmopunt 9877	. . . . . . 7 |- ((H~ =/= 0H /\ G e. UniOp) -> (normop` G) = 1)
41	6, 40	mpan2 695	. . . . . 6 |- (H~ =/= 0H -> (normop` G) = 1)
42	41	opreq2d 3967	. . . . 5 |- (H~ =/= 0H -> ((normop` (F -op S)) x. (normop` G)) = ((normop` (F -op S)) x. 1))
43	3, 14	bdophd 9968	. . . . . . . 8 |- (F -op S) e. BndLinOp
44		nmopret 9737	. . . . . . . 8 |- ((F -op S) e. BndLinOp -> (normop` (F -op S)) e. RR)
45	43, 44	ax-mp 7	. . . . . . 7 |- (normop` (F -op S)) e. RR
46	45	recn 5294	. . . . . 6 |- (normop` (F -op S)) e. CC
47	46	mulid1 5312	. . . . 5 |- ((normop` (F -op S)) x. 1) = (normop` (F -op S))
48	42, 47	syl6eq 1520	. . . 4 |- (H~ =/= 0H -> ((normop` (F -op S)) x. (normop` G)) = (normop` (F -op S)))
49		nmopunt 9877	. . . . . . 7 |- ((H~ =/= 0H /\ S e. UniOp) -> (normop` S) = 1)
50	12, 49	mpan2 695	. . . . . 6 |- (H~ =/= 0H -> (normop` S) = 1)
51	50	opreq1d 3966	. . . . 5 |- (H~ =/= 0H -> ((normop` S) x. (normop` (G -op T))) = (1 x. (normop` (G -op T))))
52	8, 19	bdophd 9968	. . . . . . . 8 |- (G -op T) e. BndLinOp
53		nmopret 9737	. . . . . . . 8 |- ((G -op T) e. BndLinOp -> (normop` (G -op T)) e. RR)
54	52, 53	ax-mp 7	. . . . . . 7 |- (normop` (G -op T)) e. RR
55	54	recn 5294	. . . . . 6 |- (normop` (G -op T)) e. CC
56	55	mulid2 5313	. . . . 5 |- (1 x. (normop` (G -op T))) = (normop` (G -op T))
57	51, 56	syl6eq 1520	. . . 4 |- (H~ =/= 0H -> ((normop` S) x. (normop` (G -op T))) = (normop` (G -op T)))
58	48, 57	opreq12d 3969	. . 3 |- (H~ =/= 0H -> (((normop` (F -op S)) x. (normop` G)) + ((normop` S) x. (normop` (G -op T)))) = ((normop` (F -op S)) + (normop` (G -op T))))
59	16, 10	hocof 9632	. . . . . 6 |- (S o. G):H~-->H~
60	11, 59, 22	honpncan 9693	. . . . 5 |- (((F o. G) -op (S o. G)) +op ((S o. G) -op (S o. T))) = ((F o. G) -op (S o. T))
61	60	fveq2i 3718	. . . 4 |- (normop` (((F o. G) -op (S o. G)) +op ((S o. G) -op (S o. T)))) = (normop` ((F o. G) -op (S o. T)))
62	3, 8	bdopco 9969	. . . . . . 7 |- (F o. G) e. BndLinOp
63	14, 8	bdopco 9969	. . . . . . 7 |- (S o. G) e. BndLinOp
64	62, 63	bdophd 9968	. . . . . 6 |- ((F o. G) -op (S o. G)) e. BndLinOp
65	14, 19	bdopco 9969	. . . . . . 7 |- (S o. T) e. BndLinOp
66	63, 65	bdophd 9968	. . . . . 6 |- ((S o. G) -op (S o. T)) e. BndLinOp
67	64, 66	nmoptri 9965	. . . . 5 |- (normop` (((F o. G) -op (S o. G)) +op ((S o. G) -op (S o. T)))) <_ ((normop` ((F o. G) -op (S o. G))) + (normop` ((S o. G) -op (S o. T))))
68	5, 16, 10	hocsubdir 9646	. . . . . . . 8 |- ((F -op S) o. G) = ((F o. G) -op (S o. G))
69	68	fveq2i 3718	. . . . . . 7 |- (normop` ((F -op S) o. G)) = (normop` ((F o. G) -op (S o. G)))
70	43, 8	nmopco 9966	. . . . . . 7 |- (normop` ((F -op S) o. G)) <_ ((normop` (F -op S)) x. (normop` G))
71	69, 70	eqbrtrr 2631	. . . . . 6 |- (normop` ((F o. G) -op (S o. G))) <_ ((normop` (F -op S)) x. (normop` G))
72		bdoplnt 9728	. . . . . . . . . 10 |- (S e. BndLinOp -> S e. LinOp)
73	14, 72	ax-mp 7	. . . . . . . . 9 |- S e. LinOp
74	73, 10, 21	hoddi 9852	. . . . . . . 8 |- (S o. (G -op T)) = ((S o. G) -op (S o. T))
75	74	fveq2i 3718	. . . . . . 7 |- (normop` (S o. (G -op T))) = (normop` ((S o. G) -op (S o. T)))
76	14, 52	nmopco 9966	. . . . . . 7 |- (normop` (S o. (G -op T))) <_ ((normop` S) x. (normop` (G -op T)))
77	75, 76	eqbrtrr 2631	. . . . . 6 |- (normop` ((S o. G) -op (S o. T))) <_ ((normop` S) x. (normop` (G -op T)))
78		nmopret 9737	. . . . . . . 8 |- (((F o. G) -op (S o. G)) e. BndLinOp -> (normop` ((F o. G) -op (S o. G))) e. RR)
79	64, 78	ax-mp 7	. . . . . . 7 |- (normop` ((F o. G) -op (S o. G))) e. RR
80		nmopret 9737	. . . . . . . 8 |- (((S o. G) -op (S o. T)) e. BndLinOp -> (normop` ((S o. G) -op (S o. T))) e. RR)
81	66, 80	ax-mp 7	. . . . . . 7 |- (normop` ((S o. G) -op (S o. T))) e. RR
82		nmopret 9737	. . . . . . . . 9 |- (G e. BndLinOp -> (normop` G) e. RR)
83	8, 82	ax-mp 7	. . . . . . . 8 |- (normop` G) e. RR
84	45, 83	remulcl 5315	. . . . . . 7 |- ((normop` (F -op S)) x. (normop` G)) e. RR
85		nmopret 9737	. . . . . . . . 9 |- (S e. BndLinOp -> (normop` S) e. RR)
86	14, 85	ax-mp 7	. . . . . . . 8 |- (normop` S) e. RR
87	86, 54	remulcl 5315	. . . . . . 7 |- ((normop` S) x. (normop` (G -op T))) e. RR
88	79, 81, 84, 87	le2add 5579	. . . . . 6 |- (((normop` ((F o. G) -op (S o. G))) <_ ((normop` (F -op S)) x. (normop` G)) /\ (normop` ((S o. G) -op (S o. T))) <_ ((normop` S) x. (normop` (G -op T)))) -> ((normop` ((F o. G) -op (S o. G))) + (normop` ((S o. G) -op (S o. T)))) <_ (((normop` (F -op S)) x. (normop` G)) + ((normop` S) x. (normop` (G -op T)))))
89	71, 77, 88	mp2an 696	. . . . 5 |- ((normop` ((F o. G) -op (S o. G))) + (normop` ((S o. G) -op (S o. T)))) <_ (((normop` (F -op S)) x. (normop` G)) + ((normop` S) x. (normop` (G -op T))))
90	64, 66	bdophs 9967	. . . . . . 7 |- (((F o. G) -op (S o. G)) +op ((S o. G) -op (S o. T))) e. BndLinOp
91		nmopret 9737	. . . . . . 7 |- ((((F o. G) -op (S o. G)) +op ((S o.