Theorem nmoval

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	nmoval	⊢ ( ( 𝑆 ∈ 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	1 2 3 4	nmofval	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 𝑁 = ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ) )
6	5	fveq1d	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑁 ‘ 𝐹 ) = ( ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ) ‘ 𝐹 ) )
7		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
8	7	fveq2d	⊢ ( 𝑓 = 𝐹 → ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) )
9	8	breq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) ↔ ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) ) )
10	9	ralbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) ) )
11	10	rabbidv	⊢ ( 𝑓 = 𝐹 → { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } = { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } )
12	11	infeq1d	⊢ ( 𝑓 = 𝐹 → inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) = inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) )
13		eqid	⊢ ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ) = ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) )
14		xrltso	⊢ < Or ℝ*
15	14	infex	⊢ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ∈ V
16	12 13 15	fvmpt	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ) ‘ 𝐹 ) = inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) )
17	6 16	sylan9eq	⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁 ‘ 𝐹 ) = inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) )
18	17	3impa	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁 ‘ 𝐹 ) = inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) )