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 e. UniOp
unierr.2
|- G e. UniOp
unierr.3
|- S e. UniOp
unierr.4
|- T e. UniOp
Assertion unierri
|- ( normop ` ( ( F o. G ) -op ( S o. T ) ) ) <_ ( ( normop ` ( F -op S ) ) + ( normop ` ( G -op T ) ) )

Proof

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