Definition df-nghm 22513

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 = ( s e. NrmGrp , t e. NrmGrp |-> ( `' ( s normOp t ) " RR ) )

Distinct variable group:   t, s

Detailed syntax breakdown of Definition df-nghm

Step	Hyp	Ref	Expression
1		cnghm 22510	. 2 class NGHom
2		vs	. . 3 setvar s
3		vt	. . 3 setvar t
4		cngp 22382	. . 3 class NrmGrp
5	2	cv 1482	. . . . . 6 class s
6	3	cv 1482	. . . . . 6 class t
7		cnmo 22509	. . . . . 6 class normOp
8	5, 6, 7	co 6650	. . . . 5 class ( s normOp t )
9	8	ccnv 5113	. . . 4 class `' ( s normOp t )
10		cr 9935	. . . 4 class RR
11	9, 10	cima 5117	. . 3 class ( `' ( s normOp t ) " RR )
12	2, 3, 4, 4, 11	cmpt2 6652	. 2 class ( s e. NrmGrp , t e. NrmGrp |-> ( `' ( s normOp t ) " RR ) )
13	1, 12	wceq 1483	1 wff NGHom = ( s e. NrmGrp , t e. NrmGrp |-> ( `' ( s normOp t ) " RR ) )

This definition is referenced by:  reldmnghm  22516  nghmfval  22526