Theorem unierri

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. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	unierr.1	⊢ 𝐹 ∈ UniOp
	unierr.2	⊢ 𝐺 ∈ UniOp
	unierr.3	⊢ 𝑆 ∈ UniOp
	unierr.4	⊢ 𝑇 ∈ UniOp
Assertion	unierri	⊢ ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ≤ ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) + ( normop ‘ ( 𝐺 −op 𝑇 ) ) )

Proof

Step	Hyp	Ref	Expression
1		unierr.1	⊢ 𝐹 ∈ UniOp
2		unierr.2	⊢ 𝐺 ∈ UniOp
3		unierr.3	⊢ 𝑆 ∈ UniOp
4		unierr.4	⊢ 𝑇 ∈ UniOp
5		unopbd	⊢ ( 𝐹 ∈ UniOp → 𝐹 ∈ BndLinOp )
6	1 5	ax-mp	⊢ 𝐹 ∈ BndLinOp
7		bdopf	⊢ ( 𝐹 ∈ BndLinOp → 𝐹 : ℋ ⟶ ℋ )
8	6 7	ax-mp	⊢ 𝐹 : ℋ ⟶ ℋ
9		unopbd	⊢ ( 𝐺 ∈ UniOp → 𝐺 ∈ BndLinOp )
10	2 9	ax-mp	⊢ 𝐺 ∈ BndLinOp
11		bdopf	⊢ ( 𝐺 ∈ BndLinOp → 𝐺 : ℋ ⟶ ℋ )
12	10 11	ax-mp	⊢ 𝐺 : ℋ ⟶ ℋ
13	8 12	hocofi	⊢ ( 𝐹 ∘ 𝐺 ) : ℋ ⟶ ℋ
14		unopbd	⊢ ( 𝑆 ∈ UniOp → 𝑆 ∈ BndLinOp )
15	3 14	ax-mp	⊢ 𝑆 ∈ BndLinOp
16		bdopf	⊢ ( 𝑆 ∈ BndLinOp → 𝑆 : ℋ ⟶ ℋ )
17	15 16	ax-mp	⊢ 𝑆 : ℋ ⟶ ℋ
18		unopbd	⊢ ( 𝑇 ∈ UniOp → 𝑇 ∈ BndLinOp )
19	4 18	ax-mp	⊢ 𝑇 ∈ BndLinOp
20		bdopf	⊢ ( 𝑇 ∈ BndLinOp → 𝑇 : ℋ ⟶ ℋ )
21	19 20	ax-mp	⊢ 𝑇 : ℋ ⟶ ℋ
22	17 21	hocofi	⊢ ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ ℋ
23	13 22	hosubcli	⊢ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) : ℋ ⟶ ℋ
24		nmop0h	⊢ ( ( ℋ = 0ℋ ∧ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) : ℋ ⟶ ℋ ) → ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) = 0 )
25	23 24	mpan2	⊢ ( ℋ = 0ℋ → ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) = 0 )
26		0le0	⊢ 0 ≤ 0
27		00id	⊢ ( 0 + 0 ) = 0
28	26 27	breqtrri	⊢ 0 ≤ ( 0 + 0 )
29	8 17	hosubcli	⊢ ( 𝐹 −op 𝑆 ) : ℋ ⟶ ℋ
30		nmop0h	⊢ ( ( ℋ = 0ℋ ∧ ( 𝐹 −op 𝑆 ) : ℋ ⟶ ℋ ) → ( normop ‘ ( 𝐹 −op 𝑆 ) ) = 0 )
31	29 30	mpan2	⊢ ( ℋ = 0ℋ → ( normop ‘ ( 𝐹 −op 𝑆 ) ) = 0 )
32	12 21	hosubcli	⊢ ( 𝐺 −op 𝑇 ) : ℋ ⟶ ℋ
33		nmop0h	⊢ ( ( ℋ = 0ℋ ∧ ( 𝐺 −op 𝑇 ) : ℋ ⟶ ℋ ) → ( normop ‘ ( 𝐺 −op 𝑇 ) ) = 0 )
34	32 33	mpan2	⊢ ( ℋ = 0ℋ → ( normop ‘ ( 𝐺 −op 𝑇 ) ) = 0 )
35	31 34	oveq12d	⊢ ( ℋ = 0ℋ → ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) + ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) = ( 0 + 0 ) )
36	28 35	breqtrrid	⊢ ( ℋ = 0ℋ → 0 ≤ ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) + ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) )
37	25 36	eqbrtrd	⊢ ( ℋ = 0ℋ → ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ≤ ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) + ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) )
38	17 12	hocofi	⊢ ( 𝑆 ∘ 𝐺 ) : ℋ ⟶ ℋ
39	13 38 22	honpncani	⊢ ( ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) +op ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) = ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) )
40	39	fveq2i	⊢ ( normop ‘ ( ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) +op ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ) = ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) )
41	6 10	bdopcoi	⊢ ( 𝐹 ∘ 𝐺 ) ∈ BndLinOp
42	15 10	bdopcoi	⊢ ( 𝑆 ∘ 𝐺 ) ∈ BndLinOp
43	41 42	bdophdi	⊢ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) ∈ BndLinOp
44	15 19	bdopcoi	⊢ ( 𝑆 ∘ 𝑇 ) ∈ BndLinOp
45	42 44	bdophdi	⊢ ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ∈ BndLinOp
46	43 45	nmoptrii	⊢ ( normop ‘ ( ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) +op ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ) ≤ ( ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) ) + ( normop ‘ ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) )
47	8 17 12	hocsubdiri	⊢ ( ( 𝐹 −op 𝑆 ) ∘ 𝐺 ) = ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) )
48	47	fveq2i	⊢ ( normop ‘ ( ( 𝐹 −op 𝑆 ) ∘ 𝐺 ) ) = ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) )
49	6 15	bdophdi	⊢ ( 𝐹 −op 𝑆 ) ∈ BndLinOp
50	49 10	nmopcoi	⊢ ( normop ‘ ( ( 𝐹 −op 𝑆 ) ∘ 𝐺 ) ) ≤ ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) · ( normop ‘ 𝐺 ) )
51	48 50	eqbrtrri	⊢ ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) ) ≤ ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) · ( normop ‘ 𝐺 ) )
52		bdopln	⊢ ( 𝑆 ∈ BndLinOp → 𝑆 ∈ LinOp )
53	15 52	ax-mp	⊢ 𝑆 ∈ LinOp
54	53 12 21	hoddii	⊢ ( 𝑆 ∘ ( 𝐺 −op 𝑇 ) ) = ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) )
55	54	fveq2i	⊢ ( normop ‘ ( 𝑆 ∘ ( 𝐺 −op 𝑇 ) ) ) = ( normop ‘ ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) )
56	10 19	bdophdi	⊢ ( 𝐺 −op 𝑇 ) ∈ BndLinOp
57	15 56	nmopcoi	⊢ ( normop ‘ ( 𝑆 ∘ ( 𝐺 −op 𝑇 ) ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ ( 𝐺 −op 𝑇 ) ) )
58	55 57	eqbrtrri	⊢ ( normop ‘ ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ ( 𝐺 −op 𝑇 ) ) )
59		nmopre	⊢ ( ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) ∈ BndLinOp → ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) ) ∈ ℝ )
60	43 59	ax-mp	⊢ ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) ) ∈ ℝ
61		nmopre	⊢ ( ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ∈ BndLinOp → ( normop ‘ ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ∈ ℝ )
62	45 61	ax-mp	⊢ ( normop ‘ ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ∈ ℝ
63		nmopre	⊢ ( ( 𝐹 −op 𝑆 ) ∈ BndLinOp → ( normop ‘ ( 𝐹 −op 𝑆 ) ) ∈ ℝ )
64	49 63	ax-mp	⊢ ( normop ‘ ( 𝐹 −op 𝑆 ) ) ∈ ℝ
65		nmopre	⊢ ( 𝐺 ∈ BndLinOp → ( normop ‘ 𝐺 ) ∈ ℝ )
66	10 65	ax-mp	⊢ ( normop ‘ 𝐺 ) ∈ ℝ
67	64 66	remulcli	⊢ ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) · ( normop ‘ 𝐺 ) ) ∈ ℝ
68		nmopre	⊢ ( 𝑆 ∈ BndLinOp → ( normop ‘ 𝑆 ) ∈ ℝ )
69	15 68	ax-mp	⊢ ( normop ‘ 𝑆 ) ∈ ℝ
70		nmopre	⊢ ( ( 𝐺 −op 𝑇 ) ∈ BndLinOp → ( normop ‘ ( 𝐺 −op 𝑇 ) ) ∈ ℝ )
71	56 70	ax-mp	⊢ ( normop ‘ ( 𝐺 −op 𝑇 ) ) ∈ ℝ
72	69 71	remulcli	⊢ ( ( normop ‘ 𝑆 ) · ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) ∈ ℝ
73	60 62 67 72	le2addi	⊢ ( ( ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) ) ≤ ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) · ( normop ‘ 𝐺 ) ) ∧ ( normop ‘ ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) ) → ( ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) ) + ( normop ‘ ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ) ≤ ( ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) · ( normop ‘ 𝐺 ) ) + ( ( normop ‘ 𝑆 ) · ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) ) )
74	51 58 73	mp2an	⊢ ( ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) ) + ( normop ‘ ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ) ≤ ( ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) · ( normop ‘ 𝐺 ) ) + ( ( normop ‘ 𝑆 ) · ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) )
75	43 45	bdophsi	⊢ ( ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) +op ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ∈ BndLinOp
76		nmopre	⊢ ( ( ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) +op ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ∈ BndLinOp → ( normop ‘ ( ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) +op ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ) ∈ ℝ )
77	75 76	ax-mp	⊢ ( normop ‘ ( ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) +op ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ) ∈ ℝ
78	60 62	readdcli	⊢ ( ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) ) + ( normop ‘ ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ) ∈ ℝ
79	67 72	readdcli	⊢ ( ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) · ( normop ‘ 𝐺 ) ) + ( ( normop ‘ 𝑆 ) · ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) ) ∈ ℝ
80	77 78 79	letri	⊢ ( ( ( normop ‘ ( ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) +op ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ) ≤ ( ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) ) + ( normop ‘ ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ) ∧ ( ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) ) + ( normop ‘ ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ) ≤ ( ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) · ( normop ‘ 𝐺 ) ) + ( ( normop ‘ 𝑆 ) · ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) ) ) → ( normop ‘ ( ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) +op ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ) ≤ ( ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) · ( normop ‘ 𝐺 ) ) + ( ( normop ‘ 𝑆 ) · ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) ) )
81	46 74 80	mp2an	⊢ ( normop ‘ ( ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝐺 ) ) +op ( ( 𝑆 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ) ≤ ( ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) · ( normop ‘ 𝐺 ) ) + ( ( normop ‘ 𝑆 ) · ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) )
82	40 81	eqbrtrri	⊢ ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ≤ ( ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) · ( normop ‘ 𝐺 ) ) + ( ( normop ‘ 𝑆 ) · ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) )
83		nmopun	⊢ ( ( ℋ ≠ 0ℋ ∧ 𝐺 ∈ UniOp ) → ( normop ‘ 𝐺 ) = 1 )
84	2 83	mpan2	⊢ ( ℋ ≠ 0ℋ → ( normop ‘ 𝐺 ) = 1 )
85	84	oveq2d	⊢ ( ℋ ≠ 0ℋ → ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) · ( normop ‘ 𝐺 ) ) = ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) · 1 ) )
86	64	recni	⊢ ( normop ‘ ( 𝐹 −op 𝑆 ) ) ∈ ℂ
87	86	mulridi	⊢ ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) · 1 ) = ( normop ‘ ( 𝐹 −op 𝑆 ) )
88	85 87	eqtrdi	⊢ ( ℋ ≠ 0ℋ → ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) · ( normop ‘ 𝐺 ) ) = ( normop ‘ ( 𝐹 −op 𝑆 ) ) )
89		nmopun	⊢ ( ( ℋ ≠ 0ℋ ∧ 𝑆 ∈ UniOp ) → ( normop ‘ 𝑆 ) = 1 )
90	3 89	mpan2	⊢ ( ℋ ≠ 0ℋ → ( normop ‘ 𝑆 ) = 1 )
91	90	oveq1d	⊢ ( ℋ ≠ 0ℋ → ( ( normop ‘ 𝑆 ) · ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) = ( 1 · ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) )
92	71	recni	⊢ ( normop ‘ ( 𝐺 −op 𝑇 ) ) ∈ ℂ
93	92	mullidi	⊢ ( 1 · ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) = ( normop ‘ ( 𝐺 −op 𝑇 ) )
94	91 93	eqtrdi	⊢ ( ℋ ≠ 0ℋ → ( ( normop ‘ 𝑆 ) · ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) = ( normop ‘ ( 𝐺 −op 𝑇 ) ) )
95	88 94	oveq12d	⊢ ( ℋ ≠ 0ℋ → ( ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) · ( normop ‘ 𝐺 ) ) + ( ( normop ‘ 𝑆 ) · ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) ) = ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) + ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) )
96	82 95	breqtrid	⊢ ( ℋ ≠ 0ℋ → ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ≤ ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) + ( normop ‘ ( 𝐺 −op 𝑇 ) ) ) )
97	37 96	pm2.61ine	⊢ ( normop ‘ ( ( 𝐹 ∘ 𝐺 ) −op ( 𝑆 ∘ 𝑇 ) ) ) ≤ ( ( normop ‘ ( 𝐹 −op 𝑆 ) ) + ( normop ‘ ( 𝐺 −op 𝑇 ) ) )