df-nghm

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)

		Ref	Expression
	Assertion	df-nghm	$⊢ NGHom = (s \in NrmGrp, t \in NrmGrp ⟼ {(s normOp t)}^{-1} [ℝ])$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnghm	$class NGHom$
1		vs	$setvar s$
2		cngp	$class NrmGrp$
3		vt	$setvar t$
4	1	cv	$setvar s$
5		cnmo	$class normOp$
6	3	cv	$setvar t$
7	4 6 5	co	$class (s normOp t)$
8	7	ccnv	$class {(s normOp t)}^{-1}$
9		cr	$class ℝ$
10	8 9	cima	$class {(s normOp t)}^{-1} [ℝ]$
11	1 3 2 2 10	cmpo	$class (s \in NrmGrp, t \in NrmGrp ⟼ {(s normOp t)}^{-1} [ℝ])$
12	0 11	wceq	$wff NGHom = (s \in NrmGrp, t \in NrmGrp ⟼ {(s normOp t)}^{-1} [ℝ])$

Metamath Proof Explorer

Definition df-nghm

Detailed syntax breakdown