isnghm3

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	isnghm3	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (F \in (S NGHom T) \leftrightarrow N (F) < +∞)$

Step	Hyp	Ref	Expression
1		nmofval.1	$⊢ N = S normOp T$
2	1	isnghm2	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (F \in (S NGHom T) \leftrightarrow N (F) \in ℝ)$
3	1	nmocl	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to N (F) \in ℝ^{*}$
4	1	nmoge0	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to 0 \leq N (F)$
5		ge0gtmnf	$⊢ (N (F) \in ℝ^{*} \land 0 \leq N (F)) \to −∞ < N (F)$
6	3 4 5	syl2anc	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to −∞ < N (F)$
7		xrrebnd	$⊢ N (F) \in ℝ^{*} \to (N (F) \in ℝ \leftrightarrow (−∞ < N (F) \land N (F) < +∞))$
8	7	baibd	$⊢ (N (F) \in ℝ^{*} \land −∞ < N (F)) \to (N (F) \in ℝ \leftrightarrow N (F) < +∞)$
9	3 6 8	syl2anc	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (N (F) \in ℝ \leftrightarrow N (F) < +∞)$
10	2 9	bitrd	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (F \in (S NGHom T) \leftrightarrow N (F) < +∞)$

Metamath Proof Explorer