Metamath Proof Explorer


Theorem isnghm

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 isnghm ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ↔ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝑁𝐹 ) ∈ ℝ ) ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 𝑁 = ( 𝑆 normOp 𝑇 )
2 1 nghmfval ( 𝑆 NGHom 𝑇 ) = ( 𝑁 “ ℝ )
3 2 eleq2i ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑁 “ ℝ ) )
4 n0i ( 𝐹 ∈ ( 𝑁 “ ℝ ) → ¬ ( 𝑁 “ ℝ ) = ∅ )
5 nmoffn normOp Fn ( NrmGrp × NrmGrp )
6 5 fndmi dom normOp = ( NrmGrp × NrmGrp )
7 6 ndmov ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑆 normOp 𝑇 ) = ∅ )
8 1 7 syl5eq ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 𝑁 = ∅ )
9 8 cnveqd ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 𝑁 = ∅ )
10 cnv0 ∅ = ∅
11 9 10 eqtrdi ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 𝑁 = ∅ )
12 11 imaeq1d ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑁 “ ℝ ) = ( ∅ “ ℝ ) )
13 0ima ( ∅ “ ℝ ) = ∅
14 12 13 eqtrdi ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑁 “ ℝ ) = ∅ )
15 4 14 nsyl2 ( 𝐹 ∈ ( 𝑁 “ ℝ ) → ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) )
16 1 nmof ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 𝑁 : ( 𝑆 GrpHom 𝑇 ) ⟶ ℝ* )
17 ffn ( 𝑁 : ( 𝑆 GrpHom 𝑇 ) ⟶ ℝ*𝑁 Fn ( 𝑆 GrpHom 𝑇 ) )
18 elpreima ( 𝑁 Fn ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 ∈ ( 𝑁 “ ℝ ) ↔ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝑁𝐹 ) ∈ ℝ ) ) )
19 16 17 18 3syl ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝐹 ∈ ( 𝑁 “ ℝ ) ↔ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝑁𝐹 ) ∈ ℝ ) ) )
20 15 19 biadanii ( 𝐹 ∈ ( 𝑁 “ ℝ ) ↔ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝑁𝐹 ) ∈ ℝ ) ) )
21 3 20 bitri ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ↔ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝑁𝐹 ) ∈ ℝ ) ) )