Metamath Proof Explorer


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 F UniOp
unierr.2 G UniOp
unierr.3 S UniOp
unierr.4 T UniOp
Assertion unierri norm op F G - op S T norm op F - op S + norm op G - op T

Proof

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