Theorem reldmnghm

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

	Ref	Expression
Assertion	reldmnghm	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{NGHom}$$

Proof

Step	Hyp	Ref	Expression
1		df-nghm	$$⊢\mathrm{NGHom}=\left(s\in \mathrm{NrmGrp},t\in \mathrm{NrmGrp}⟼{\left(s\mathrm{normOp}t\right)}^{-1}\left[ℝ\right]\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{NGHom}$$