# Metamath Proof Explorer

## Theorem nmopnegi

Description: Value of the norm of the negative of a Hilbert space operator. Unlike nmophmi , the operator does not have to be bounded. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmopneg.1 ${⊢}{T}:ℋ⟶ℋ$
Assertion nmopnegi ${⊢}{norm}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{T}\right)={norm}_{\mathrm{op}}\left({T}\right)$

### Proof

Step Hyp Ref Expression
1 nmopneg.1 ${⊢}{T}:ℋ⟶ℋ$
2 neg1cn ${⊢}-1\in ℂ$
3 homval ${⊢}\left(-1\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\to \left(-1{·}_{\mathrm{op}}{T}\right)\left({y}\right)=-1{\cdot }_{ℎ}{T}\left({y}\right)$
4 2 1 3 mp3an12 ${⊢}{y}\in ℋ\to \left(-1{·}_{\mathrm{op}}{T}\right)\left({y}\right)=-1{\cdot }_{ℎ}{T}\left({y}\right)$
5 4 fveq2d ${⊢}{y}\in ℋ\to {norm}_{ℎ}\left(\left(-1{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right)={norm}_{ℎ}\left(-1{\cdot }_{ℎ}{T}\left({y}\right)\right)$
6 1 ffvelrni ${⊢}{y}\in ℋ\to {T}\left({y}\right)\in ℋ$
7 normneg ${⊢}{T}\left({y}\right)\in ℋ\to {norm}_{ℎ}\left(-1{\cdot }_{ℎ}{T}\left({y}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)$
8 6 7 syl ${⊢}{y}\in ℋ\to {norm}_{ℎ}\left(-1{\cdot }_{ℎ}{T}\left({y}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)$
9 5 8 eqtrd ${⊢}{y}\in ℋ\to {norm}_{ℎ}\left(\left(-1{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)$
10 9 eqeq2d ${⊢}{y}\in ℋ\to \left({x}={norm}_{ℎ}\left(\left(-1{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right)↔{x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)$
11 10 anbi2d ${⊢}{y}\in ℋ\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left(\left(-1{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right)\right)↔\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right)$
12 11 rexbiia ${⊢}\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left(\left(-1{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right)\right)↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)$
13 12 abbii ${⊢}\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left(\left(-1{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right)\right)\right\}=\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\}$
14 13 supeq1i ${⊢}sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left(\left(-1{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)=sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
15 homulcl ${⊢}\left(-1\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to \left(-1{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
16 2 1 15 mp2an ${⊢}\left(-1{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
17 nmopval ${⊢}\left(-1{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\to {norm}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{T}\right)=sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left(\left(-1{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
18 16 17 ax-mp ${⊢}{norm}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{T}\right)=sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left(\left(-1{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
19 nmopval ${⊢}{T}:ℋ⟶ℋ\to {norm}_{\mathrm{op}}\left({T}\right)=sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
20 1 19 ax-mp ${⊢}{norm}_{\mathrm{op}}\left({T}\right)=sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
21 14 18 20 3eqtr4i ${⊢}{norm}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{T}\right)={norm}_{\mathrm{op}}\left({T}\right)$