This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isnghm3

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

Ref Expression
Hypothesis nmofval.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
Assertion isnghm3 ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ↔ ( 𝑁 ‘ 𝐹 ) < +∞ ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2 1 isnghm2 ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ↔ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) )
3 1 nmocl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ* )
4 1 nmoge0 ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 0 ≤ ( 𝑁 ‘ 𝐹 ) )
5 ge0gtmnf ⊢ ( ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ* ∧ 0 ≤ ( 𝑁 ‘ 𝐹 ) ) → -∞ < ( 𝑁 ‘ 𝐹 ) )
6 3 4 5 syl2anc ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → -∞ < ( 𝑁 ‘ 𝐹 ) )
7 xrrebnd ⊢ ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ* → ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ ↔ ( -∞ < ( 𝑁 ‘ 𝐹 ) ∧ ( 𝑁 ‘ 𝐹 ) < +∞ ) ) )
8 7 baibd ⊢ ( ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ* ∧ -∞ < ( 𝑁 ‘ 𝐹 ) ) → ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ ↔ ( 𝑁 ‘ 𝐹 ) < +∞ ) )
9 3 6 8 syl2anc ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ ↔ ( 𝑁 ‘ 𝐹 ) < +∞ ) )
10 2 9 bitrd ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ↔ ( 𝑁 ‘ 𝐹 ) < +∞ ) )