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 ∈ NrmMod ∧ T ∈ NrmMod ∧ F ∈ S LMHom T → F ∈ S NMHom T ↔ N ⁡ F ∈ ℝ

Proof

Step Hyp Ref Expression
1 isnmhm2.1 ⊢ N = S normOp T
2 isnmhm ⊢ F ∈ S NMHom T ↔ S ∈ NrmMod ∧ T ∈ NrmMod ∧ F ∈ S LMHom T ∧ F ∈ S NGHom T
3 2 baib ⊢ S ∈ NrmMod ∧ T ∈ NrmMod → F ∈ S NMHom T ↔ F ∈ S LMHom T ∧ F ∈ S NGHom T
4 3 baibd ⊢ S ∈ NrmMod ∧ T ∈ NrmMod ∧ F ∈ S LMHom T → F ∈ S NMHom T ↔ F ∈ S NGHom T
5 lmghm ⊢ F ∈ S LMHom T → F ∈ S GrpHom T
6 nlmngp ⊢ S ∈ NrmMod → S ∈ NrmGrp
7 nlmngp ⊢ T ∈ NrmMod → T ∈ NrmGrp
8 1 isnghm ⊢ F ∈ S NGHom T ↔ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F ∈ S GrpHom T ∧ N ⁡ F ∈ ℝ
9 8 baib ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp → F ∈ S NGHom T ↔ F ∈ S GrpHom T ∧ N ⁡ F ∈ ℝ
10 6 7 9 syl2an ⊢ S ∈ NrmMod ∧ T ∈ NrmMod → F ∈ S NGHom T ↔ F ∈ S GrpHom T ∧ N ⁡ F ∈ ℝ
11 10 baibd ⊢ S ∈ NrmMod ∧ T ∈ NrmMod ∧ F ∈ S GrpHom T → F ∈ S NGHom T ↔ N ⁡ F ∈ ℝ
12 5 11 sylan2 ⊢ S ∈ NrmMod ∧ T ∈ NrmMod ∧ F ∈ S LMHom T → F ∈ S NGHom T ↔ N ⁡ F ∈ ℝ
13 4 12 bitrd ⊢ S ∈ NrmMod ∧ T ∈ NrmMod ∧ F ∈ S LMHom T → F ∈ S NMHom T ↔ N ⁡ F ∈ ℝ
14 13 3impa ⊢ S ∈ NrmMod ∧ T ∈ NrmMod ∧ F ∈ S LMHom T → F ∈ S NMHom T ↔ N ⁡ F ∈ ℝ