Metamath Proof Explorer

Theorem nmolb

Description: Any upper bound on the values of a linear operator translates to an upper bound on the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015) (Proof shortened by AV, 26-Sep-2020)

Ref Expression
Hypotheses nmofval.1 ⊢ N = S normOp T
nmofval.2 ⊢ V = Base S
nmofval.3 ⊢ L = norm ⁡ S
nmofval.4 ⊢ M = norm ⁡ T
Assertion nmolb ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T ∧ A ∈ ℝ ∧ 0 ≤ A → ∀ x ∈ V M ⁡ F ⁡ x ≤ A ⁢ L ⁡ x → N ⁡ F ≤ A

Proof

Step Hyp Ref Expression
1 nmofval.1 ⊢ N = S normOp T
2 nmofval.2 ⊢ V = Base S
3 nmofval.3 ⊢ L = norm ⁡ S
4 nmofval.4 ⊢ M = norm ⁡ T
5 elrege0 ⊢ A ∈ 0 +∞ ↔ A ∈ ℝ ∧ 0 ≤ A
6 1 2 3 4 nmoval ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T → N ⁡ F = sup r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ℝ * <
7 ssrab2 ⊢ r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ⊆ 0 +∞
8 icossxr ⊢ 0 +∞ ⊆ ℝ *
9 7 8 sstri ⊢ r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ⊆ ℝ *
10 infxrcl ⊢ r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ⊆ ℝ * → sup r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ℝ * < ∈ ℝ *
11 9 10 mp1i ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T → sup r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ℝ * < ∈ ℝ *
12 6 11 eqeltrd ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T → N ⁡ F ∈ ℝ *
13 12 xrleidd ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T → N ⁡ F ≤ N ⁡ F
14 1 2 3 4 nmogelb ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T ∧ N ⁡ F ∈ ℝ * → N ⁡ F ≤ N ⁡ F ↔ ∀ r ∈ 0 +∞ ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x → N ⁡ F ≤ r
15 12 14 mpdan ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T → N ⁡ F ≤ N ⁡ F ↔ ∀ r ∈ 0 +∞ ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x → N ⁡ F ≤ r
16 13 15 mpbid ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T → ∀ r ∈ 0 +∞ ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x → N ⁡ F ≤ r
17 oveq1 ⊢ r = A → r ⁢ L ⁡ x = A ⁢ L ⁡ x
18 17 breq2d ⊢ r = A → M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ↔ M ⁡ F ⁡ x ≤ A ⁢ L ⁡ x
19 18 ralbidv ⊢ r = A → ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ↔ ∀ x ∈ V M ⁡ F ⁡ x ≤ A ⁢ L ⁡ x
20 breq2 ⊢ r = A → N ⁡ F ≤ r ↔ N ⁡ F ≤ A
21 19 20 imbi12d ⊢ r = A → ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x → N ⁡ F ≤ r ↔ ∀ x ∈ V M ⁡ F ⁡ x ≤ A ⁢ L ⁡ x → N ⁡ F ≤ A
22 21 rspccv ⊢ ∀ r ∈ 0 +∞ ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x → N ⁡ F ≤ r → A ∈ 0 +∞ → ∀ x ∈ V M ⁡ F ⁡ x ≤ A ⁢ L ⁡ x → N ⁡ F ≤ A
23 16 22 syl ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T → A ∈ 0 +∞ → ∀ x ∈ V M ⁡ F ⁡ x ≤ A ⁢ L ⁡ x → N ⁡ F ≤ A
24 5 23 syl5bir ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T → A ∈ ℝ ∧ 0 ≤ A → ∀ x ∈ V M ⁡ F ⁡ x ≤ A ⁢ L ⁡ x → N ⁡ F ≤ A
25 24 3impib ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T ∧ A ∈ ℝ ∧ 0 ≤ A → ∀ x ∈ V M ⁡ F ⁡ x ≤ A ⁢ L ⁡ x → N ⁡ F ≤ A