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 𝐹 ∈ 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 mulid1i ( ( normop ‘ ( 𝐹op 𝑆 ) ) · 1 ) = ( normop ‘ ( 𝐹op 𝑆 ) )
88 85 87 syl6eq ( ℋ ≠ 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 mulid2i ( 1 · ( normop ‘ ( 𝐺op 𝑇 ) ) ) = ( normop ‘ ( 𝐺op 𝑇 ) )
94 91 93 syl6eq ( ℋ ≠ 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 𝑇 ) ) )