Metamath Proof Explorer

Theorem isnmhm2

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

		Ref	Expression
	Hypothesis	isnmhm2.1	$⊢ N = S normOp T$
	Assertion	isnmhm2	$⊢ (S \in NrmMod \land T \in NrmMod \land F \in (S LMHom T)) \to (F \in (S NMHom T) \leftrightarrow N (F) \in ℝ)$

Proof

Step	Hyp	Ref	Expression
1		isnmhm2.1	$⊢ N = S normOp T$
2		isnmhm	$⊢ F \in (S NMHom T) \leftrightarrow ((S \in NrmMod \land T \in NrmMod) \land (F \in (S LMHom T) \land F \in (S NGHom T)))$
3	2	baib	$⊢ (S \in NrmMod \land T \in NrmMod) \to (F \in (S NMHom T) \leftrightarrow (F \in (S LMHom T) \land F \in (S NGHom T)))$
4	3	baibd	$⊢ ((S \in NrmMod \land T \in NrmMod) \land F \in (S LMHom T)) \to (F \in (S NMHom T) \leftrightarrow F \in (S NGHom T))$
5		lmghm	$⊢ F \in (S LMHom T) \to F \in (S GrpHom T)$
6		nlmngp	$⊢ S \in NrmMod \to S \in NrmGrp$
7		nlmngp	$⊢ T \in NrmMod \to T \in NrmGrp$
8	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 ℝ))$
9	8	baib	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to (F \in (S NGHom T) \leftrightarrow (F \in (S GrpHom T) \land N (F) \in ℝ))$
10	6 7 9	syl2an	$⊢ (S \in NrmMod \land T \in NrmMod) \to (F \in (S NGHom T) \leftrightarrow (F \in (S GrpHom T) \land N (F) \in ℝ))$
11	10	baibd	$⊢ ((S \in NrmMod \land T \in NrmMod) \land F \in (S GrpHom T)) \to (F \in (S NGHom T) \leftrightarrow N (F) \in ℝ)$
12	5 11	sylan2	$⊢ ((S \in NrmMod \land T \in NrmMod) \land F \in (S LMHom T)) \to (F \in (S NGHom T) \leftrightarrow N (F) \in ℝ)$
13	4 12	bitrd	$⊢ ((S \in NrmMod \land T \in NrmMod) \land F \in (S LMHom T)) \to (F \in (S NMHom T) \leftrightarrow N (F) \in ℝ)$
14	13	3impa	$⊢ (S \in NrmMod \land T \in NrmMod \land F \in (S LMHom T)) \to (F \in (S NMHom T) \leftrightarrow N (F) \in ℝ)$