Theorem reldmnghm

Description: Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015)

	Ref	Expression
Assertion	reldmnghm	⊢ Rel dom NGHom

Proof

Step	Hyp	Ref	Expression
1		df-nghm	⊢ NGHom = ( 𝑠 ∈ NrmGrp , 𝑡 ∈ NrmGrp ↦ ( ◡ ( 𝑠 normOp 𝑡 ) “ ℝ ) )
2	1	reldmmpo	⊢ Rel dom NGHom