# 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`
` |-  ( ( normop ` ( ( F o. G ) -op ( S o. G ) ) ) + ( normop ` ( ( S o. G ) -op ( S o. T ) ) ) ) e. RR`
` |-  ( ( ( 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 ) ) )`