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

Metamath Proof Explorer

Theorem nghmfval

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 nghmfval ( 𝑆 NGHom 𝑇 ) = ( ◡ 𝑁 “ ℝ )

Proof

Step Hyp Ref Expression
1 nmofval.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2 oveq12 ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑠 normOp 𝑡 ) = ( 𝑆 normOp 𝑇 ) )
3 2 1 eqtr4di ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑠 normOp 𝑡 ) = 𝑁 )
4 3 cnveqd ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ◡ ( 𝑠 normOp 𝑡 ) = ◡ 𝑁 )
5 4 imaeq1d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ◡ ( 𝑠 normOp 𝑡 ) “ ℝ ) = ( ◡ 𝑁 “ ℝ ) )
6 df-nghm ⊢ NGHom = ( 𝑠 ∈ NrmGrp , 𝑡 ∈ NrmGrp ↦ ( ◡ ( 𝑠 normOp 𝑡 ) “ ℝ ) )
7 1 ovexi ⊢ 𝑁 ∈ V
8 7 cnvex ⊢ ◡ 𝑁 ∈ V
9 8 imaex ⊢ ( ◡ 𝑁 “ ℝ ) ∈ V
10 5 6 9 ovmpoa ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑆 NGHom 𝑇 ) = ( ◡ 𝑁 “ ℝ ) )
11 6 mpondm0 ⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑆 NGHom 𝑇 ) = ∅ )
12 nmoffn ⊢ normOp Fn ( NrmGrp × NrmGrp )
13 12 fndmi ⊢ dom normOp = ( NrmGrp × NrmGrp )
14 13 ndmov ⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑆 normOp 𝑇 ) = ∅ )
15 1 14 eqtrid ⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 𝑁 = ∅ )
16 15 cnveqd ⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ◡ 𝑁 = ◡ ∅ )
17 cnv0 ⊢ ◡ ∅ = ∅
18 16 17 eqtrdi ⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ◡ 𝑁 = ∅ )
19 18 imaeq1d ⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( ◡ 𝑁 “ ℝ ) = ( ∅ “ ℝ ) )
20 0ima ⊢ ( ∅ “ ℝ ) = ∅
21 19 20 eqtrdi ⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( ◡ 𝑁 “ ℝ ) = ∅ )
22 11 21 eqtr4d ⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑆 NGHom 𝑇 ) = ( ◡ 𝑁 “ ℝ ) )
23 10 22 pm2.61i ⊢ ( 𝑆 NGHom 𝑇 ) = ( ◡ 𝑁 “ ℝ )