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

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 = ( 𝑠 ∈ NrmGrp , 𝑡 ∈ NrmGrp ↦ ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) )
2 eqid ⊢ ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) = ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) )
3 ssrab2 ⊢ { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } ⊆ ( 0 [,) +∞ )
4 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
5 3 4 sstri ⊢ { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } ⊆ ℝ*
6 infxrcl ⊢ ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } ⊆ ℝ* → inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ∈ ℝ* )
7 5 6 mp1i ⊢ ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) → inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ∈ ℝ* )
8 2 7 fmpti ⊢ ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) : ( 𝑠 GrpHom 𝑡 ) ⟶ ℝ*
9 ovex ⊢ ( 𝑠 GrpHom 𝑡 ) ∈ V
10 xrex ⊢ ℝ* ∈ V
11 fex2 ⊢ ( ( ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) : ( 𝑠 GrpHom 𝑡 ) ⟶ ℝ* ∧ ( 𝑠 GrpHom 𝑡 ) ∈ V ∧ ℝ* ∈ V ) → ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) ∈ V )
12 8 9 10 11 mp3an ⊢ ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) ∈ V
13 1 12 fnmpoi ⊢ normOp Fn ( NrmGrp × NrmGrp )