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

Proof

Step Hyp Ref Expression
1 df-nghm 
 |-  NGHom = ( s e. NrmGrp , t e. NrmGrp |-> ( `' ( s normOp t ) " RR ) )
2 1 reldmmpo 
 |-  Rel dom NGHom