MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nghm Structured version   Visualization version   GIF version

Definition df-nghm 22507
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
StepHypRef Expression
1 cnghm 22504 . 2 class NGHom
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑡
4 cngp 22376 . . 3 class NrmGrp
52cv 1481 . . . . . 6 class 𝑠
63cv 1481 . . . . . 6 class 𝑡
7 cnmo 22503 . . . . . 6 class normOp
85, 6, 7co 6647 . . . . 5 class (𝑠 normOp 𝑡)
98ccnv 5111 . . . 4 class (𝑠 normOp 𝑡)
10 cr 9932 . . . 4 class
119, 10cima 5115 . . 3 class ((𝑠 normOp 𝑡) “ ℝ)
122, 3, 4, 4, 11cmpt2 6649 . 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ ((𝑠 normOp 𝑡) “ ℝ))
131, 12wceq 1482 1 wff NGHom = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ ((𝑠 normOp 𝑡) “ ℝ))
Colors of variables: wff setvar class
This definition is referenced by:  reldmnghm  22510  nghmfval  22520
  Copyright terms: Public domain W3C validator