# Metamath Proof Explorer

## Theorem isnghm2

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}\mathrm{normOp}{T}$
Assertion isnghm2 ${⊢}\left({S}\in \mathrm{NrmGrp}\wedge {T}\in \mathrm{NrmGrp}\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)$

### Proof

Step Hyp Ref Expression
1 nmofval.1 ${⊢}{N}={S}\mathrm{normOp}{T}$
2 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)$
3 2 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)$
4 3 baibd ${⊢}\left(\left({S}\in \mathrm{NrmGrp}\wedge {T}\in \mathrm{NrmGrp}\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)$
5 4 3impa ${⊢}\left({S}\in \mathrm{NrmGrp}\wedge {T}\in \mathrm{NrmGrp}\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)$