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