This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reldmnghm

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

		Ref	Expression
	Assertion	reldmnghm	$⊢ Rel dom NGHom$

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