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	$⊢ N = S normOp T$
	Assertion	isnghm	$⊢ F \in (S NGHom T) \leftrightarrow ((S \in NrmGrp \land T \in NrmGrp) \land (F \in (S GrpHom T) \land N (F) \in ℝ))$

Proof

Step	Hyp	Ref	Expression
1		nmofval.1	$⊢ N = S normOp T$
2	1	nghmfval	$⊢ S NGHom T = N^{-1} [ℝ]$
3	2	eleq2i	$⊢ F \in (S NGHom T) \leftrightarrow F \in N^{-1} [ℝ]$
4		n0i	$⊢ F \in N^{-1} [ℝ] \to \neg N^{-1} [ℝ] = \emptyset$
5		nmoffn	$⊢ normOp Fn (NrmGrp \times NrmGrp)$
6	5	fndmi	$⊢ dom normOp = NrmGrp \times NrmGrp$
7	6	ndmov	$⊢ \neg (S \in NrmGrp \land T \in NrmGrp) \to S normOp T = \emptyset$
8	1 7	eqtrid	$⊢ \neg (S \in NrmGrp \land T \in NrmGrp) \to N = \emptyset$
9	8	cnveqd	$⊢ \neg (S \in NrmGrp \land T \in NrmGrp) \to N^{-1} = \emptyset^{-1}$
10		cnv0	$⊢ \emptyset^{-1} = \emptyset$
11	9 10	eqtrdi	$⊢ \neg (S \in NrmGrp \land T \in NrmGrp) \to N^{-1} = \emptyset$
12	11	imaeq1d	$⊢ \neg (S \in NrmGrp \land T \in NrmGrp) \to N^{-1} [ℝ] = \emptyset [ℝ]$
13		0ima	$⊢ \emptyset [ℝ] = \emptyset$
14	12 13	eqtrdi	$⊢ \neg (S \in NrmGrp \land T \in NrmGrp) \to N^{-1} [ℝ] = \emptyset$
15	4 14	nsyl2	$⊢ F \in N^{-1} [ℝ] \to (S \in NrmGrp \land T \in NrmGrp)$
16	1	nmof	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to N : S GrpHom T ⟶ ℝ^{*}$
17		ffn	$⊢ N : S GrpHom T ⟶ ℝ^{*} \to N Fn (S GrpHom T)$
18		elpreima	$⊢ N Fn (S GrpHom T) \to (F \in N^{-1} [ℝ] \leftrightarrow (F \in (S GrpHom T) \land N (F) \in ℝ))$
19	16 17 18	3syl	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to (F \in N^{-1} [ℝ] \leftrightarrow (F \in (S GrpHom T) \land N (F) \in ℝ))$
20	15 19	biadanii	$⊢ F \in N^{-1} [ℝ] \leftrightarrow ((S \in NrmGrp \land T \in NrmGrp) \land (F \in (S GrpHom T) \land N (F) \in ℝ))$
21	3 20	bitri	$⊢ F \in (S NGHom T) \leftrightarrow ((S \in NrmGrp \land T \in NrmGrp) \land (F \in (S GrpHom T) \land N (F) \in ℝ))$

Metamath Proof Explorer

Theorem isnghm

Proof