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 = S normOp T
nmofval.2 ⊢ V = Base S
nmofval.3 ⊢ L = norm ⁡ S
nmofval.4 ⊢ M = norm ⁡ T
Assertion nmogelb ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T ∧ A ∈ ℝ * → A ≤ N ⁡ F ↔ ∀ r ∈ 0 +∞ ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x → A ≤ r

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 1 2 3 4 nmoval ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T → N ⁡ F = inf r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ℝ * <
6 5 breq2d ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T → A ≤ N ⁡ F ↔ A ≤ inf 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 infxrgelb ⊢ r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ⊆ ℝ * ∧ A ∈ ℝ * → A ≤ inf r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ℝ * < ↔ ∀ s ∈ r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x A ≤ s
11 9 10 mpan ⊢ A ∈ ℝ * → A ≤ inf r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ℝ * < ↔ ∀ s ∈ r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x A ≤ s
12 breq2 ⊢ s = r → A ≤ s ↔ A ≤ r
13 12 ralrab2 ⊢ ∀ s ∈ r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x A ≤ s ↔ ∀ r ∈ 0 +∞ ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x → A ≤ r
14 11 13 bitrdi ⊢ A ∈ ℝ * → A ≤ inf r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ℝ * < ↔ ∀ r ∈ 0 +∞ ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x → A ≤ r
15 6 14 sylan9bb ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T ∧ A ∈ ℝ * → A ≤ N ⁡ F ↔ ∀ r ∈ 0 +∞ ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x → A ≤ r