Metamath Proof Explorer

Theorem bddnghm

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

Ref Expression
Hypothesis nmofval.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
Assertion bddnghm ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝐴 ∈ ℝ ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ) → 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2 1 nmocl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ* )
3 1 nmoge0 ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 0 ≤ ( 𝑁 ‘ 𝐹 ) )
4 2 3 jca ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ* ∧ 0 ≤ ( 𝑁 ‘ 𝐹 ) ) )
5 xrrege0 ⊢ ( ( ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ* ∧ 𝐴 ∈ ℝ ) ∧ ( 0 ≤ ( 𝑁 ‘ 𝐹 ) ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ )
6 5 an4s ⊢ ( ( ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ* ∧ 0 ≤ ( 𝑁 ‘ 𝐹 ) ) ∧ ( 𝐴 ∈ ℝ ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ )
7 4 6 sylan ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝐴 ∈ ℝ ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ )
8 1 isnghm2 ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ↔ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) )
9 8 adantr ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝐴 ∈ ℝ ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ) → ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ↔ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) )
10 7 9 mpbird ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝐴 ∈ ℝ ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ) → 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) )