bddnghm

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

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

Step	Hyp	Ref	Expression
1		nmofval.1	$⊢ N = S normOp T$
2	1	nmocl	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to N (F) \in ℝ^{*}$
3	1	nmoge0	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to 0 \leq N (F)$
4	2 3	jca	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (N (F) \in ℝ^{*} \land 0 \leq N (F))$
5		xrrege0	$⊢ ((N (F) \in ℝ^{*} \land A \in ℝ) \land (0 \leq N (F) \land N (F) \leq A)) \to N (F) \in ℝ$
6	5	an4s	$⊢ ((N (F) \in ℝ^{*} \land 0 \leq N (F)) \land (A \in ℝ \land N (F) \leq A)) \to N (F) \in ℝ$
7	4 6	sylan	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (A \in ℝ \land N (F) \leq A)) \to N (F) \in ℝ$
8	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 ℝ)$
9	8	adantr	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (A \in ℝ \land N (F) \leq A)) \to (F \in (S NGHom T) \leftrightarrow N (F) \in ℝ)$
10	7 9	mpbird	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (A \in ℝ \land N (F) \leq A)) \to F \in (S NGHom T)$

Metamath Proof Explorer