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}\in \mathrm{UniOp}$
unierr.2 ${⊢}{G}\in \mathrm{UniOp}$
unierr.3 ${⊢}{S}\in \mathrm{UniOp}$
unierr.4 ${⊢}{T}\in \mathrm{UniOp}$
Assertion unierri ${⊢}{norm}_{\mathrm{op}}\left(\left({F}\circ {G}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)\right)\le {norm}_{\mathrm{op}}\left({F}{-}_{\mathrm{op}}{S}\right)+{norm}_{\mathrm{op}}\left({G}{-}_{\mathrm{op}}{T}\right)$

Proof

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