Definition df-nghm 24919

Description: Define the set of normed group homomorphisms between two normed groups. A normed group homomorphism is a group homomorphism which additionally bounds the increase of norm by a fixed real operator. In vector spaces these are also known as bounded linear operators. (Contributed by Mario Carneiro, 18-Oct-2015.)

Assertion

Ref	Expression
df-nghm	⊢ NGHom = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (◡(𝑠 normOp 𝑡) “ ℝ))

Distinct variable group:   𝑡,𝑠

Detailed syntax breakdown of Definition df-nghm

Step	Hyp	Ref	Expression
1		cnghm 24916	. 2 class NGHom
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24787	. . 3 class NrmGrp
5	2	cv 1569	. . . . . 6 class 𝑠
6	3	cv 1569	. . . . . 6 class 𝑡
7		cnmo 24915	. . . . . 6 class normOp
8	5, 6, 7	co 7419	. . . . 5 class (𝑠 normOp 𝑡)
9	8	ccnv 5662	. . . 4 class ◡(𝑠 normOp 𝑡)
10		cr 11116	. . . 4 class ℝ
11	9, 10	cima 5666	. . 3 class (◡(𝑠 normOp 𝑡) “ ℝ)
12	2, 3, 4, 4, 11	cmpo 7421	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (◡(𝑠 normOp 𝑡) “ ℝ))
13	1, 12	wceq 1570	1 wff NGHom = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (◡(𝑠 normOp 𝑡) “ ℝ))

This definition is used by:  reldmnghm  24922  nghmfval  24932