# Metamath Proof Explorer

## Theorem nmopun

Description: Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopun ${⊢}\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\to {norm}_{\mathrm{op}}\left({T}\right)=1$

### Proof

Step Hyp Ref Expression
1 unoplin ${⊢}{T}\in \mathrm{UniOp}\to {T}\in \mathrm{LinOp}$
2 lnopf ${⊢}{T}\in \mathrm{LinOp}\to {T}:ℋ⟶ℋ$
3 1 2 syl ${⊢}{T}\in \mathrm{UniOp}\to {T}:ℋ⟶ℋ$
4 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)$
5 3 4 syl ${⊢}{T}\in \mathrm{UniOp}\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)$
6 5 adantl ${⊢}\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\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)$
7 nmopsetretHIL ${⊢}{T}:ℋ⟶ℋ\to \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\}\subseteq ℝ$
8 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
9 7 8 sstrdi ${⊢}{T}:ℋ⟶ℋ\to \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\}\subseteq {ℝ}^{*}$
10 3 9 syl ${⊢}{T}\in \mathrm{UniOp}\to \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\}\subseteq {ℝ}^{*}$
11 10 adantl ${⊢}\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\to \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\}\subseteq {ℝ}^{*}$
12 1xr ${⊢}1\in {ℝ}^{*}$
13 11 12 jctir ${⊢}\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\to \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\}\subseteq {ℝ}^{*}\wedge 1\in {ℝ}^{*}\right)$
14 vex ${⊢}{z}\in \mathrm{V}$
15 eqeq1 ${⊢}{x}={z}\to \left({x}={norm}_{ℎ}\left({T}\left({y}\right)\right)↔{z}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)$
16 15 anbi2d ${⊢}{x}={z}\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)↔\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {z}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right)$
17 16 rexbidv ${⊢}{x}={z}\to \left(\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {z}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right)$
18 14 17 elab ${⊢}{z}\in \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\}↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {z}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)$
19 unopnorm ${⊢}\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\right)\to {norm}_{ℎ}\left({T}\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)$
20 19 eqeq2d ${⊢}\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\right)\to \left({z}={norm}_{ℎ}\left({T}\left({y}\right)\right)↔{z}={norm}_{ℎ}\left({y}\right)\right)$
21 20 anbi2d ${⊢}\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\right)\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {z}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)↔\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {z}={norm}_{ℎ}\left({y}\right)\right)\right)$
22 breq1 ${⊢}{z}={norm}_{ℎ}\left({y}\right)\to \left({z}\le 1↔{norm}_{ℎ}\left({y}\right)\le 1\right)$
23 22 biimparc ${⊢}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {z}={norm}_{ℎ}\left({y}\right)\right)\to {z}\le 1$
24 21 23 syl6bi ${⊢}\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\right)\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {z}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\to {z}\le 1\right)$
25 24 rexlimdva ${⊢}{T}\in \mathrm{UniOp}\to \left(\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {z}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\to {z}\le 1\right)$
26 25 imp ${⊢}\left({T}\in \mathrm{UniOp}\wedge \exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {z}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right)\to {z}\le 1$
27 18 26 sylan2b ${⊢}\left({T}\in \mathrm{UniOp}\wedge {z}\in \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)\to {z}\le 1$
28 27 ralrimiva ${⊢}{T}\in \mathrm{UniOp}\to \forall {z}\in \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\}\phantom{\rule{.4em}{0ex}}{z}\le 1$
29 28 adantl ${⊢}\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\to \forall {z}\in \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\}\phantom{\rule{.4em}{0ex}}{z}\le 1$
30 hne0 ${⊢}ℋ\ne {0}_{ℋ}↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}\ne {0}_{ℎ}$
31 norm1hex ${⊢}\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}\ne {0}_{ℎ}↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({y}\right)=1$
32 30 31 sylbb ${⊢}ℋ\ne {0}_{ℋ}\to \exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({y}\right)=1$
33 32 adantr ${⊢}\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\to \exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({y}\right)=1$
34 1le1 ${⊢}1\le 1$
35 breq1 ${⊢}{norm}_{ℎ}\left({y}\right)=1\to \left({norm}_{ℎ}\left({y}\right)\le 1↔1\le 1\right)$
36 34 35 mpbiri ${⊢}{norm}_{ℎ}\left({y}\right)=1\to {norm}_{ℎ}\left({y}\right)\le 1$
37 36 a1i ${⊢}\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\right)\to \left({norm}_{ℎ}\left({y}\right)=1\to {norm}_{ℎ}\left({y}\right)\le 1\right)$
38 19 adantr ${⊢}\left(\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\right)\wedge {norm}_{ℎ}\left({y}\right)=1\right)\to {norm}_{ℎ}\left({T}\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)$
39 eqeq2 ${⊢}{norm}_{ℎ}\left({y}\right)=1\to \left({norm}_{ℎ}\left({T}\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)↔{norm}_{ℎ}\left({T}\left({y}\right)\right)=1\right)$
40 39 adantl ${⊢}\left(\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\right)\wedge {norm}_{ℎ}\left({y}\right)=1\right)\to \left({norm}_{ℎ}\left({T}\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)↔{norm}_{ℎ}\left({T}\left({y}\right)\right)=1\right)$
41 38 40 mpbid ${⊢}\left(\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\right)\wedge {norm}_{ℎ}\left({y}\right)=1\right)\to {norm}_{ℎ}\left({T}\left({y}\right)\right)=1$
42 41 eqcomd ${⊢}\left(\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\right)\wedge {norm}_{ℎ}\left({y}\right)=1\right)\to 1={norm}_{ℎ}\left({T}\left({y}\right)\right)$
43 42 ex ${⊢}\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\right)\to \left({norm}_{ℎ}\left({y}\right)=1\to 1={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)$
44 37 43 jcad ${⊢}\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\right)\to \left({norm}_{ℎ}\left({y}\right)=1\to \left({norm}_{ℎ}\left({y}\right)\le 1\wedge 1={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right)$
45 44 adantll ${⊢}\left(\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\wedge {y}\in ℋ\right)\to \left({norm}_{ℎ}\left({y}\right)=1\to \left({norm}_{ℎ}\left({y}\right)\le 1\wedge 1={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right)$
46 45 reximdva ${⊢}\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\to \left(\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({y}\right)=1\to \exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge 1={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right)$
47 33 46 mpd ${⊢}\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\to \exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge 1={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)$
48 1ex ${⊢}1\in \mathrm{V}$
49 eqeq1 ${⊢}{x}=1\to \left({x}={norm}_{ℎ}\left({T}\left({y}\right)\right)↔1={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)$
50 49 anbi2d ${⊢}{x}=1\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)↔\left({norm}_{ℎ}\left({y}\right)\le 1\wedge 1={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right)$
51 50 rexbidv ${⊢}{x}=1\to \left(\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge 1={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right)$
52 48 51 elab ${⊢}1\in \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\}↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge 1={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)$
53 47 52 sylibr ${⊢}\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\to 1\in \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\}$
54 53 adantr ${⊢}\left(\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\wedge {z}\in ℝ\right)\to 1\in \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\}$
55 breq2 ${⊢}{w}=1\to \left({z}<{w}↔{z}<1\right)$
56 55 rspcev ${⊢}\left(1\in \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\}\wedge {z}<1\right)\to \exists {w}\in \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\}\phantom{\rule{.4em}{0ex}}{z}<{w}$
57 54 56 sylan ${⊢}\left(\left(\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\wedge {z}\in ℝ\right)\wedge {z}<1\right)\to \exists {w}\in \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\}\phantom{\rule{.4em}{0ex}}{z}<{w}$
58 57 ex ${⊢}\left(\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\wedge {z}\in ℝ\right)\to \left({z}<1\to \exists {w}\in \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\}\phantom{\rule{.4em}{0ex}}{z}<{w}\right)$
59 58 ralrimiva ${⊢}\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\to \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<1\to \exists {w}\in \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\}\phantom{\rule{.4em}{0ex}}{z}<{w}\right)$
60 supxr2 ${⊢}\left(\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\}\subseteq {ℝ}^{*}\wedge 1\in {ℝ}^{*}\right)\wedge \left(\forall {z}\in \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\}\phantom{\rule{.4em}{0ex}}{z}\le 1\wedge \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<1\to \exists {w}\in \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\}\phantom{\rule{.4em}{0ex}}{z}<{w}\right)\right)\right)\to 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)=1$
61 13 29 59 60 syl12anc ${⊢}\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\to 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)=1$
62 6 61 eqtrd ${⊢}\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\to {norm}_{\mathrm{op}}\left({T}\right)=1$