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	syl5eq	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 𝑁 = ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ) )