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 syl5eq ( ¬ ( 𝑆 ∈ 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 𝑇 ) = ( 𝑁 “ ℝ )