Metamath Proof Explorer

Theorem nghmrcl1

Description: Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015)

		Ref	Expression
	Assertion	nghmrcl1	$⊢ F \in (S NGHom T) \to S \in NrmGrp$

Step	Hyp	Ref	Expression
1		eqid	$⊢ S normOp T = S normOp T$
2	1	isnghm	$⊢ F \in (S NGHom T) \leftrightarrow ((S \in NrmGrp \land T \in NrmGrp) \land (F \in (S GrpHom T) \land (S normOp T) (F) \in ℝ))$
3	2	simplbi	$⊢ F \in (S NGHom T) \to (S \in NrmGrp \land T \in NrmGrp)$
4	3	simpld	$⊢ F \in (S NGHom T) \to S \in NrmGrp$