Metamath Proof Explorer

Theorem nmogelb

Description: Property of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015) (Proof shortened 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 nmogelb ⊢S∈NrmGrp∧T∈NrmGrp∧F∈SGrpHomT∧A∈ℝ*→A≤N⁡F↔∀r∈0+∞∀x∈VM⁡F⁡x≤r⁢L⁡x→A≤r

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 nmoval ⊢S∈NrmGrp∧T∈NrmGrp∧F∈SGrpHomT→N⁡F=supr∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡xℝ*<
6 5 breq2d ⊢S∈NrmGrp∧T∈NrmGrp∧F∈SGrpHomT→A≤N⁡F↔A≤supr∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡xℝ*<
7 ssrab2 ⊢r∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡x⊆0+∞
8 icossxr ⊢0+∞⊆ℝ*
9 7 8 sstri ⊢r∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡x⊆ℝ*
10 infxrgelb ⊢r∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡x⊆ℝ*∧A∈ℝ*→A≤supr∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡xℝ*<↔∀s∈r∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡xA≤s
11 9 10 mpan ⊢A∈ℝ*→A≤supr∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡xℝ*<↔∀s∈r∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡xA≤s
12 breq2 ⊢s=r→A≤s↔A≤r
13 12 ralrab2 ⊢∀s∈r∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡xA≤s↔∀r∈0+∞∀x∈VM⁡F⁡x≤r⁢L⁡x→A≤r
14 11 13 bitrdi ⊢A∈ℝ*→A≤supr∈0+∞|∀x∈VM⁡F⁡x≤r⁢L⁡xℝ*<↔∀r∈0+∞∀x∈VM⁡F⁡x≤r⁢L⁡x→A≤r
15 6 14 sylan9bb ⊢S∈NrmGrp∧T∈NrmGrp∧F∈SGrpHomT∧A∈ℝ*→A≤N⁡F↔∀r∈0+∞∀x∈VM⁡F⁡x≤r⁢L⁡x→A≤r