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