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	$⊢ N = S normOp T$
	Assertion	nghmfval	$⊢ S NGHom T = N^{-1} [ℝ]$

Step	Hyp	Ref	Expression
1		nmofval.1	$⊢ N = S normOp T$
2		oveq12	$⊢ (s = S \land t = T) \to s normOp t = S normOp T$
3	2 1	eqtr4di	$⊢ (s = S \land t = T) \to s normOp t = N$
4	3	cnveqd	$⊢ (s = S \land t = T) \to {(s normOp t)}^{-1} = N^{-1}$
5	4	imaeq1d	$⊢ (s = S \land t = T) \to {(s normOp t)}^{-1} [ℝ] = N^{-1} [ℝ]$
6		df-nghm	$⊢ NGHom = (s \in NrmGrp, t \in NrmGrp ⟼ {(s normOp t)}^{-1} [ℝ])$
7	1	ovexi	$⊢ N \in V$
8	7	cnvex	$⊢ N^{-1} \in V$
9	8	imaex	$⊢ N^{-1} [ℝ] \in V$
10	5 6 9	ovmpoa	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to S NGHom T = N^{-1} [ℝ]$
11	6	mpondm0	$⊢ \neg (S \in NrmGrp \land T \in NrmGrp) \to S NGHom T = \emptyset$
12		nmoffn	$⊢ normOp Fn (NrmGrp \times NrmGrp)$
13	12	fndmi	$⊢ dom normOp = NrmGrp \times NrmGrp$
14	13	ndmov	$⊢ \neg (S \in NrmGrp \land T \in NrmGrp) \to S normOp T = \emptyset$
15	1 14	syl5eq	$⊢ \neg (S \in NrmGrp \land T \in NrmGrp) \to N = \emptyset$
16	15	cnveqd	$⊢ \neg (S \in NrmGrp \land T \in NrmGrp) \to N^{-1} = \emptyset^{-1}$
17		cnv0	$⊢ \emptyset^{-1} = \emptyset$
18	16 17	eqtrdi	$⊢ \neg (S \in NrmGrp \land T \in NrmGrp) \to N^{-1} = \emptyset$
19	18	imaeq1d	$⊢ \neg (S \in NrmGrp \land T \in NrmGrp) \to N^{-1} [ℝ] = \emptyset [ℝ]$
20		0ima	$⊢ \emptyset [ℝ] = \emptyset$
21	19 20	eqtrdi	$⊢ \neg (S \in NrmGrp \land T \in NrmGrp) \to N^{-1} [ℝ] = \emptyset$
22	11 21	eqtr4d	$⊢ \neg (S \in NrmGrp \land T \in NrmGrp) \to S NGHom T = N^{-1} [ℝ]$
23	10 22	pm2.61i	$⊢ S NGHom T = N^{-1} [ℝ]$

Metamath Proof Explorer