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 ⊢normOpFnNrmGrp×NrmGrp

Proof

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