isnghm2

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

		Ref	Expression
	Hypothesis	nmofval.1	$⊢ N = S normOp T$
	Assertion	isnghm2	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (F \in (S NGHom T) \leftrightarrow N (F) \in ℝ)$

Step	Hyp	Ref	Expression
1		nmofval.1	$⊢ N = 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 N (F) \in ℝ))$
3	2	baib	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to (F \in (S NGHom T) \leftrightarrow (F \in (S GrpHom T) \land N (F) \in ℝ))$
4	3	baibd	$⊢ ((S \in NrmGrp \land T \in NrmGrp) \land F \in (S GrpHom T)) \to (F \in (S NGHom T) \leftrightarrow N (F) \in ℝ)$
5	4	3impa	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (F \in (S NGHom T) \leftrightarrow N (F) \in ℝ)$

Metamath Proof Explorer