Definition df-nmo

Description: Define the norm of an operator between two normed groups (usually vector spaces). This definition produces an operator norm function for each pair of groups <. s , t >. . Equivalent to the definition of linear operator norm in AkhiezerGlazman p. 39. (Contributed by Mario Carneiro, 18-Oct-2015) (Revised by AV, 25-Sep-2020)

	Ref	Expression
Assertion	df-nmo	⊢ normOp = ( 𝑠 ∈ NrmGrp , 𝑡 ∈ NrmGrp ↦ ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnmo	⊢ normOp
1		vs	⊢ 𝑠
2		cngp	⊢ NrmGrp
3		vt	⊢ 𝑡
4		vf	⊢ 𝑓
5	1	cv	⊢ 𝑠
6		cghm	⊢ GrpHom
7	3	cv	⊢ 𝑡
8	5 7 6	co	⊢ ( 𝑠 GrpHom 𝑡 )
9		vr	⊢ 𝑟
10		cc0	⊢ 0
11		cico	⊢ [,)
12		cpnf	⊢ +∞
13	10 12 11	co	⊢ ( 0 [,) +∞ )
14		vx	⊢ 𝑥
15		cbs	⊢ Base
16	5 15	cfv	⊢ ( Base ‘ 𝑠 )
17		cnm	⊢ norm
18	7 17	cfv	⊢ ( norm ‘ 𝑡 )
19	4	cv	⊢ 𝑓
20	14	cv	⊢ 𝑥
21	20 19	cfv	⊢ ( 𝑓 ‘ 𝑥 )
22	21 18	cfv	⊢ ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) )
23		cle	⊢ ≤
24	9	cv	⊢ 𝑟
25		cmul	⊢ ·
26	5 17	cfv	⊢ ( norm ‘ 𝑠 )
27	20 26	cfv	⊢ ( ( norm ‘ 𝑠 ) ‘ 𝑥 )
28	24 27 25	co	⊢ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) )
29	22 28 23	wbr	⊢ ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) )
30	29 14 16	wral	⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) )
31	30 9 13	crab	⊢ { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) }
32		cxr	⊢ ℝ*
33		clt	⊢ <
34	31 32 33	cinf	⊢ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < )
35	4 8 34	cmpt	⊢ ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) )
36	1 3 2 2 35	cmpo	⊢ ( 𝑠 ∈ NrmGrp , 𝑡 ∈ NrmGrp ↦ ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) )
37	0 36	wceq	⊢ normOp = ( 𝑠 ∈ NrmGrp , 𝑡 ∈ NrmGrp ↦ ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) )