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 eqtrdi 
 |-  ( ~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 eqtrdi 
 |-  ( ~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 ) ) )