Metamath Proof Explorer

Theorem nmof

Description: The operator norm is a function into the extended reals. (Contributed by Mario Carneiro, 18-Oct-2015) (Proof shortened by AV, 26-Sep-2020)

Ref Expression
Hypothesis nmofval.1 ⊢ N = S normOp T
Assertion nmof ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp → N : S GrpHom T ⟶ ℝ *

Proof

Step Hyp Ref Expression
1 nmofval.1 ⊢ N = S normOp T
2 eqid ⊢ Base S = Base S
3 eqid ⊢ norm ⁡ S = norm ⁡ S
4 eqid ⊢ norm ⁡ T = norm ⁡ T
5 1 2 3 4 nmofval ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp → N = f ∈ S GrpHom T ⟼ sup r ∈ 0 +∞ | ∀ x ∈ Base S norm ⁡ T ⁡ f ⁡ x ≤ r ⁢ norm ⁡ S ⁡ x ℝ * <
6 ssrab2 ⊢ r ∈ 0 +∞ | ∀ x ∈ Base S norm ⁡ T ⁡ f ⁡ x ≤ r ⁢ norm ⁡ S ⁡ x ⊆ 0 +∞
7 icossxr ⊢ 0 +∞ ⊆ ℝ *
8 6 7 sstri ⊢ r ∈ 0 +∞ | ∀ x ∈ Base S norm ⁡ T ⁡ f ⁡ x ≤ r ⁢ norm ⁡ S ⁡ x ⊆ ℝ *
9 infxrcl ⊢ r ∈ 0 +∞ | ∀ x ∈ Base S norm ⁡ T ⁡ f ⁡ x ≤ r ⁢ norm ⁡ S ⁡ x ⊆ ℝ * → sup r ∈ 0 +∞ | ∀ x ∈ Base S norm ⁡ T ⁡ f ⁡ x ≤ r ⁢ norm ⁡ S ⁡ x ℝ * < ∈ ℝ *
10 8 9 mp1i ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ f ∈ S GrpHom T → sup r ∈ 0 +∞ | ∀ x ∈ Base S norm ⁡ T ⁡ f ⁡ x ≤ r ⁢ norm ⁡ S ⁡ x ℝ * < ∈ ℝ *
11 5 10 fmpt3d ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp → N : S GrpHom T ⟶ ℝ *