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

Metamath Proof Explorer

Theorem nghmghm

Description: A normed group homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015)

		Ref	Expression
	Assertion	nghmghm	$⊢ F \in (S NGHom T) \to F \in (S GrpHom T)$

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	simprbi	$⊢ F \in (S NGHom T) \to (F \in (S GrpHom T) \land (S normOp T) (F) \in ℝ)$
4	3	simpld	$⊢ F \in (S NGHom T) \to F \in (S GrpHom T)$