This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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 nmofval ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp → N = f ∈ S GrpHom T ⟼ inf r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * <
6 5 fveq1d ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp → N ⁡ F = f ∈ S GrpHom T ⟼ inf r ∈ 0 +∞ | ∀ x ∈ V M ⁡ 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 ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ↔ ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x
11 10 rabbidv ⊢ f = F → r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x = r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x
12 11 infeq1d ⊢ f = F → inf r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * < = inf r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ℝ * <
13 eqid ⊢ f ∈ S GrpHom T ⟼ inf r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * < = f ∈ S GrpHom T ⟼ inf r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * <
14 xrltso ⊢ < Or ℝ *
15 14 infex ⊢ inf r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ℝ * < ∈ V
16 12 13 15 fvmpt ⊢ F ∈ S GrpHom T → f ∈ S GrpHom T ⟼ inf r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * < ⁡ F = inf r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ℝ * <
17 6 16 sylan9eq ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T → N ⁡ F = inf r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ℝ * <
18 17 3impa ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T → N ⁡ F = inf r ∈ 0 +∞ | ∀ x ∈ V M ⁡ F ⁡ x ≤ r ⁢ L ⁡ x ℝ * <