Metamath Proof Explorer

Theorem nmoffn

Description: The function producing operator norm functions is a function on normed groups. (Contributed by Mario Carneiro, 18-Oct-2015) (Proof shortened by AV, 26-Sep-2020)

Ref Expression
Assertion nmoffn ⊢ normOp Fn NrmGrp × NrmGrp

Proof

Step Hyp Ref Expression
1 df-nmo ⊢ normOp = s ∈ NrmGrp , t ∈ NrmGrp ⟼ f ∈ s GrpHom t ⟼ sup r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ℝ * <
2 eqid ⊢ f ∈ s GrpHom t ⟼ sup r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ℝ * < = f ∈ s GrpHom t ⟼ sup r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ℝ * <
3 ssrab2 ⊢ r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ⊆ 0 +∞
4 icossxr ⊢ 0 +∞ ⊆ ℝ *
5 3 4 sstri ⊢ r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ⊆ ℝ *
6 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 ℝ * < ∈ ℝ *
7 5 6 mp1i ⊢ f ∈ s GrpHom t → sup r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ℝ * < ∈ ℝ *
8 2 7 fmpti ⊢ f ∈ s GrpHom t ⟼ sup r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ℝ * < : s GrpHom t ⟶ ℝ *
9 ovex ⊢ s GrpHom t ∈ V
10 xrex ⊢ ℝ * ∈ V
11 fex2 ⊢ f ∈ s GrpHom t ⟼ sup r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ℝ * < : s GrpHom t ⟶ ℝ * ∧ s GrpHom t ∈ V ∧ ℝ * ∈ V → f ∈ s GrpHom t ⟼ sup r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ℝ * < ∈ V
12 8 9 10 11 mp3an ⊢ f ∈ s GrpHom t ⟼ sup r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ℝ * < ∈ V
13 1 12 fnmpoi ⊢ normOp Fn NrmGrp × NrmGrp