# 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}\mathrm{normOp}{T}$
Assertion isnmhm2 ${⊢}\left({S}\in \mathrm{NrmMod}\wedge {T}\in \mathrm{NrmMod}\wedge {F}\in \left({S}\mathrm{LMHom}{T}\right)\right)\to \left({F}\in \left({S}\mathrm{NMHom}{T}\right)↔{N}\left({F}\right)\in ℝ\right)$

### Proof

Step Hyp Ref Expression
1 isnmhm2.1 ${⊢}{N}={S}\mathrm{normOp}{T}$
2 isnmhm ${⊢}{F}\in \left({S}\mathrm{NMHom}{T}\right)↔\left(\left({S}\in \mathrm{NrmMod}\wedge {T}\in \mathrm{NrmMod}\right)\wedge \left({F}\in \left({S}\mathrm{LMHom}{T}\right)\wedge {F}\in \left({S}\mathrm{NGHom}{T}\right)\right)\right)$
3 2 baib ${⊢}\left({S}\in \mathrm{NrmMod}\wedge {T}\in \mathrm{NrmMod}\right)\to \left({F}\in \left({S}\mathrm{NMHom}{T}\right)↔\left({F}\in \left({S}\mathrm{LMHom}{T}\right)\wedge {F}\in \left({S}\mathrm{NGHom}{T}\right)\right)\right)$
4 3 baibd ${⊢}\left(\left({S}\in \mathrm{NrmMod}\wedge {T}\in \mathrm{NrmMod}\right)\wedge {F}\in \left({S}\mathrm{LMHom}{T}\right)\right)\to \left({F}\in \left({S}\mathrm{NMHom}{T}\right)↔{F}\in \left({S}\mathrm{NGHom}{T}\right)\right)$
5 lmghm ${⊢}{F}\in \left({S}\mathrm{LMHom}{T}\right)\to {F}\in \left({S}\mathrm{GrpHom}{T}\right)$
6 nlmngp ${⊢}{S}\in \mathrm{NrmMod}\to {S}\in \mathrm{NrmGrp}$
7 nlmngp ${⊢}{T}\in \mathrm{NrmMod}\to {T}\in \mathrm{NrmGrp}$
8 1 isnghm ${⊢}{F}\in \left({S}\mathrm{NGHom}{T}\right)↔\left(\left({S}\in \mathrm{NrmGrp}\wedge {T}\in \mathrm{NrmGrp}\right)\wedge \left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {N}\left({F}\right)\in ℝ\right)\right)$
9 8 baib ${⊢}\left({S}\in \mathrm{NrmGrp}\wedge {T}\in \mathrm{NrmGrp}\right)\to \left({F}\in \left({S}\mathrm{NGHom}{T}\right)↔\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {N}\left({F}\right)\in ℝ\right)\right)$
10 6 7 9 syl2an ${⊢}\left({S}\in \mathrm{NrmMod}\wedge {T}\in \mathrm{NrmMod}\right)\to \left({F}\in \left({S}\mathrm{NGHom}{T}\right)↔\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {N}\left({F}\right)\in ℝ\right)\right)$
11 10 baibd ${⊢}\left(\left({S}\in \mathrm{NrmMod}\wedge {T}\in \mathrm{NrmMod}\right)\wedge {F}\in \left({S}\mathrm{GrpHom}{T}\right)\right)\to \left({F}\in \left({S}\mathrm{NGHom}{T}\right)↔{N}\left({F}\right)\in ℝ\right)$
12 5 11 sylan2 ${⊢}\left(\left({S}\in \mathrm{NrmMod}\wedge {T}\in \mathrm{NrmMod}\right)\wedge {F}\in \left({S}\mathrm{LMHom}{T}\right)\right)\to \left({F}\in \left({S}\mathrm{NGHom}{T}\right)↔{N}\left({F}\right)\in ℝ\right)$
13 4 12 bitrd ${⊢}\left(\left({S}\in \mathrm{NrmMod}\wedge {T}\in \mathrm{NrmMod}\right)\wedge {F}\in \left({S}\mathrm{LMHom}{T}\right)\right)\to \left({F}\in \left({S}\mathrm{NMHom}{T}\right)↔{N}\left({F}\right)\in ℝ\right)$
14 13 3impa ${⊢}\left({S}\in \mathrm{NrmMod}\wedge {T}\in \mathrm{NrmMod}\wedge {F}\in \left({S}\mathrm{LMHom}{T}\right)\right)\to \left({F}\in \left({S}\mathrm{NMHom}{T}\right)↔{N}\left({F}\right)\in ℝ\right)$