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

Metamath Proof Explorer

Theorem nmofval

Description: Value of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015) (Revised by AV, 26-Sep-2020)

Ref Expression
Hypotheses nmofval.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
nmofval.2 ⊢ 𝑉 = ( Base ‘ 𝑆 )
nmofval.3 ⊢ 𝐿 = ( norm ‘ 𝑆 )
nmofval.4 ⊢ 𝑀 = ( norm ‘ 𝑇 )
Assertion nmofval ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 𝑁 = ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2 nmofval.2 ⊢ 𝑉 = ( Base ‘ 𝑆 )
3 nmofval.3 ⊢ 𝐿 = ( norm ‘ 𝑆 )
4 nmofval.4 ⊢ 𝑀 = ( norm ‘ 𝑇 )
5 oveq12 ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑠 GrpHom 𝑡 ) = ( 𝑆 GrpHom 𝑇 ) )
6 simpl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → 𝑠 = 𝑆 )
7 6 fveq2d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
8 7 2 eqtr4di ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( Base ‘ 𝑠 ) = 𝑉 )
9 simpr ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → 𝑡 = 𝑇 )
10 9 fveq2d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( norm ‘ 𝑡 ) = ( norm ‘ 𝑇 ) )
11 10 4 eqtr4di ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( norm ‘ 𝑡 ) = 𝑀 )
12 11 fveq1d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) )
13 6 fveq2d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( norm ‘ 𝑠 ) = ( norm ‘ 𝑆 ) )
14 13 3 eqtr4di ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( norm ‘ 𝑠 ) = 𝐿 )
15 14 fveq1d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) = ( 𝐿 ‘ 𝑥 ) )
16 15 oveq2d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) = ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) )
17 12 16 breq12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) ↔ ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) ) )
18 8 17 raleqbidv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) ) )
19 18 rabbidv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } = { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } )
20 19 infeq1d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) = inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) )
21 5 20 mpteq12dv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) = ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ) )
22 df-nmo ⊢ normOp = ( 𝑠 ∈ NrmGrp , 𝑡 ∈ NrmGrp ↦ ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) )
23 eqid ⊢ ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ) = ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) )
24 ssrab2 ⊢ { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } ⊆ ( 0 [,) +∞ )
25 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
26 24 25 sstri ⊢ { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } ⊆ ℝ*
27 infxrcl ⊢ ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } ⊆ ℝ* → inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ∈ ℝ* )
28 26 27 mp1i ⊢ ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) → inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ∈ ℝ* )
29 23 28 fmpti ⊢ ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ) : ( 𝑆 GrpHom 𝑇 ) ⟶ ℝ*
30 ovex ⊢ ( 𝑆 GrpHom 𝑇 ) ∈ V
31 xrex ⊢ ℝ* ∈ V
32 fex2 ⊢ ( ( ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ) : ( 𝑆 GrpHom 𝑇 ) ⟶ ℝ* ∧ ( 𝑆 GrpHom 𝑇 ) ∈ V ∧ ℝ* ∈ V ) → ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ) ∈ V )
33 29 30 31 32 mp3an ⊢ ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ) ∈ V
34 21 22 33 ovmpoa ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑆 normOp 𝑇 ) = ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ) )
35 1 34 eqtrid ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 𝑁 = ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ) )