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

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 eqtrid ⊢ ( ¬ ( 𝑆 ∈ 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 𝑇 ) ∧ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) ) )