Metamath Proof Explorer

Definition 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 ∈ NrmGrp , t ∈ 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 ∈ NrmGrp , t ∈ NrmGrp ⟼ s normOp t -1 ℝ
12 0 11 wceq wff NGHom = s ∈ NrmGrp , t ∈ NrmGrp ⟼ s normOp t -1 ℝ