Metamath Proof Explorer

Theorem nmoval

Description: Value of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015) (Revised by AV, 26-Sep-2020)

Ref Expression
Hypotheses nmofval.1 ⊢N=SnormOpT
nmofval.2 ⊢V=BaseS
nmofval.3 ⊢L=norm⁡S
nmofval.4 ⊢M=norm⁡T
Assertion nmoval ⊢S∈NrmGrp∧T∈NrmGrp∧F∈SGrpHomT→N⁡F=supr∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡xℝ*<

Proof

Step Hyp Ref Expression
1 nmofval.1 ⊢N=SnormOpT
2 nmofval.2 ⊢V=BaseS
3 nmofval.3 ⊢L=norm⁡S
4 nmofval.4 ⊢M=norm⁡T
5 1 2 3 4 nmofval ⊢S∈NrmGrp∧T∈NrmGrp→N=f∈SGrpHomT⟼supr∈0+∞|∀x∈VM⁡f⁡x≤r⁢L⁡xℝ*<
6 5 fveq1d ⊢S∈NrmGrp∧T∈NrmGrp→N⁡F=f∈SGrpHomT⟼supr∈0+∞|∀x∈VM⁡f⁡x≤r⁢L⁡xℝ*<⁡F
7 fveq1 ⊢f=F→f⁡x=F⁡x
8 7 fveq2d ⊢f=F→M⁡f⁡x=M⁡F⁡x
9 8 breq1d ⊢f=F→M⁡f⁡x≤r⁢L⁡x↔M⁡F⁡x≤r⁢L⁡x
10 9 ralbidv ⊢f=F→∀x∈VM⁡f⁡x≤r⁢L⁡x↔∀x∈VM⁡F⁡x≤r⁢L⁡x
11 10 rabbidv ⊢f=F→r∈0+∞|∀x∈VM⁡f⁡x≤r⁢L⁡x=r∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡x
12 11 infeq1d ⊢f=F→supr∈0+∞|∀x∈VM⁡f⁡x≤r⁢L⁡xℝ*<=supr∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡xℝ*<
13 eqid ⊢f∈SGrpHomT⟼supr∈0+∞|∀x∈VM⁡f⁡x≤r⁢L⁡xℝ*<=f∈SGrpHomT⟼supr∈0+∞|∀x∈VM⁡f⁡x≤r⁢L⁡xℝ*<
14 xrltso ⊢<Orℝ*
15 14 infex ⊢supr∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡xℝ*<∈V
16 12 13 15 fvmpt ⊢F∈SGrpHomT→f∈SGrpHomT⟼supr∈0+∞|∀x∈VM⁡f⁡x≤r⁢L⁡xℝ*<⁡F=supr∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡xℝ*<
17 6 16 sylan9eq ⊢S∈NrmGrp∧T∈NrmGrp∧F∈SGrpHomT→N⁡F=supr∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡xℝ*<
18 17 3impa ⊢S∈NrmGrp∧T∈NrmGrp∧F∈SGrpHomT→N⁡F=supr∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡xℝ*<