nmofval

Description: Value of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015) (Revised by AV, 26-Sep-2020)

	Ref	Expression
Hypotheses	nmofval.1	$⊢ N = S normOp T$
	nmofval.2	$⊢ V = {Base}_{S}$
	nmofval.3	$⊢ L = norm (S)$
	nmofval.4	$⊢ M = norm (T)$
Assertion	nmofval	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to N = (f \in (S GrpHom T) ⟼ sup (\{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\} ℝ^{*} <))$

Proof

Step	Hyp	Ref	Expression
1		nmofval.1	$⊢ N = S normOp T$
2		nmofval.2	$⊢ V = {Base}_{S}$
3		nmofval.3	$⊢ L = norm (S)$
4		nmofval.4	$⊢ M = norm (T)$
5		oveq12	$⊢ (s = S \land t = T) \to s GrpHom t = S GrpHom T$
6		simpl	$⊢ (s = S \land t = T) \to s = S$
7	6	fveq2d	$⊢ (s = S \land t = T) \to {Base}_{s} = {Base}_{S}$
8	7 2	eqtr4di	$⊢ (s = S \land t = T) \to {Base}_{s} = V$
9		simpr	$⊢ (s = S \land t = T) \to t = T$
10	9	fveq2d	$⊢ (s = S \land t = T) \to norm (t) = norm (T)$
11	10 4	eqtr4di	$⊢ (s = S \land t = T) \to norm (t) = M$
12	11	fveq1d	$⊢ (s = S \land t = T) \to norm (t) (f (x)) = M (f (x))$
13	6	fveq2d	$⊢ (s = S \land t = T) \to norm (s) = norm (S)$
14	13 3	eqtr4di	$⊢ (s = S \land t = T) \to norm (s) = L$
15	14	fveq1d	$⊢ (s = S \land t = T) \to norm (s) (x) = L (x)$
16	15	oveq2d	$⊢ (s = S \land t = T) \to r norm (s) (x) = r L (x)$
17	12 16	breq12d	$⊢ (s = S \land t = T) \to (norm (t) (f (x)) \leq r norm (s) (x) \leftrightarrow M (f (x)) \leq r L (x))$
18	8 17	raleqbidv	$⊢ (s = S \land t = T) \to (\forall x \in {Base}_{s} norm (t) (f (x)) \leq r norm (s) (x) \leftrightarrow \forall x \in V M (f (x)) \leq r L (x))$
19	18	rabbidv	$⊢ (s = S \land t = T) \to \{r \in [0, +∞) \| \forall x \in {Base}_{s} norm (t) (f (x)) \leq r norm (s) (x)\} = \{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\}$
20	19	infeq1d	$⊢ (s = S \land t = T) \to sup (\{r \in [0, +∞) \| \forall x \in {Base}_{s} norm (t) (f (x)) \leq r norm (s) (x)\} ℝ^{} <) = sup (\{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\} ℝ^{} <)$
21	5 20	mpteq12dv	$⊢ (s = S \land t = T) \to (f \in (s GrpHom t) ⟼ sup (\{r \in [0, +∞) \| \forall x \in {Base}_{s} norm (t) (f (x)) \leq r norm (s) (x)\} ℝ^{} <)) = (f \in (S GrpHom T) ⟼ sup (\{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\} ℝ^{} <))$
22		df-nmo	$⊢ normOp = (s \in NrmGrp, t \in NrmGrp ⟼ (f \in (s GrpHom t) ⟼ sup (\{r \in [0, +∞) \| \forall x \in {Base}_{s} norm (t) (f (x)) \leq r norm (s) (x)\} ℝ^{*} <)))$
23		eqid	$⊢ (f \in (S GrpHom T) ⟼ sup (\{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\} ℝ^{} <)) = (f \in (S GrpHom T) ⟼ sup (\{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\} ℝ^{} <))$
24		ssrab2	$⊢ \{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\} \subseteq [0, +∞)$
25		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
26	24 25	sstri	$⊢ \{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\} \subseteq ℝ^{*}$
27		infxrcl	$⊢ \{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\} \subseteq ℝ^{} \to sup (\{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\} ℝ^{} <) \in ℝ^{*}$
28	26 27	mp1i	$⊢ f \in (S GrpHom T) \to sup (\{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\} ℝ^{} <) \in ℝ^{}$
29	23 28	fmpti	$⊢ (f \in (S GrpHom T) ⟼ sup (\{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\} ℝ^{} <)) : S GrpHom T ⟶ ℝ^{}$
30		ovex	$⊢ S GrpHom T \in V$
31		xrex	$⊢ ℝ^{*} \in V$
32		fex2	$⊢ ((f \in (S GrpHom T) ⟼ sup (\{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\} ℝ^{} <)) : S GrpHom T ⟶ ℝ^{} \land S GrpHom T \in V \land ℝ^{} \in V) \to (f \in (S GrpHom T) ⟼ sup (\{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\} ℝ^{} <)) \in V$
33	29 30 31 32	mp3an	$⊢ (f \in (S GrpHom T) ⟼ sup (\{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\} ℝ^{*} <)) \in V$
34	21 22 33	ovmpoa	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to S normOp T = (f \in (S GrpHom T) ⟼ sup (\{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\} ℝ^{*} <))$
35	1 34	eqtrid	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to N = (f \in (S GrpHom T) ⟼ sup (\{r \in [0, +∞) \| \forall x \in V M (f (x)) \leq r L (x)\} ℝ^{*} <))$

Metamath Proof Explorer

Theorem nmofval

Proof