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 = ( 𝑠 ∈ NrmGrp , 𝑡 ∈ NrmGrp ↦ ( ^◡ ( 𝑠 normOp 𝑡 ) “ ℝ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnghm	⊢ NGHom
1		vs	⊢ 𝑠
2		cngp	⊢ NrmGrp
3		vt	⊢ 𝑡
4	1	cv	⊢ 𝑠
5		cnmo	⊢ normOp
6	3	cv	⊢ 𝑡
7	4 6 5	co	⊢ ( 𝑠 normOp 𝑡 )
8	7	ccnv	⊢ ^◡ ( 𝑠 normOp 𝑡 )
9		cr	⊢ ℝ
10	8 9	cima	⊢ ( ^◡ ( 𝑠 normOp 𝑡 ) “ ℝ )
11	1 3 2 2 10	cmpo	⊢ ( 𝑠 ∈ NrmGrp , 𝑡 ∈ NrmGrp ↦ ( ^◡ ( 𝑠 normOp 𝑡 ) “ ℝ ) )
12	0 11	wceq	⊢ NGHom = ( 𝑠 ∈ NrmGrp , 𝑡 ∈ NrmGrp ↦ ( ^◡ ( 𝑠 normOp 𝑡 ) “ ℝ ) )

Metamath Proof Explorer

Definition df-nghm

Detailed syntax breakdown