nmoleub

Description: The operator norm, defined as an infimum of upper bounds, can also be defined as a supremum of norms of F ( x ) away from zero. (Contributed by Mario Carneiro, 18-Oct-2015)

	Ref	Expression
Hypotheses	nmofval.1	$⊢ N = S normOp T$
	nmoi.2	$⊢ V = {Base}_{S}$
	nmoi.3	$⊢ L = norm (S)$
	nmoi.4	$⊢ M = norm (T)$
	nmoi2.z	$⊢ \underset{˙}{0} = 0_{S}$
	nmoleub.1	$⊢ φ \to S \in NrmGrp$
	nmoleub.2	$⊢ φ \to T \in NrmGrp$
	nmoleub.3	$⊢ φ \to F \in (S GrpHom T)$
	nmoleub.4	$⊢ φ \to A \in ℝ^{*}$
	nmoleub.5	$⊢ φ \to 0 \leq A$
Assertion	nmoleub	$⊢ φ \to (N (F) \leq A \leftrightarrow \forall x \in V (x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A))$

Proof

Step	Hyp	Ref	Expression
1		nmofval.1	$⊢ N = S normOp T$
2		nmoi.2	$⊢ V = {Base}_{S}$
3		nmoi.3	$⊢ L = norm (S)$
4		nmoi.4	$⊢ M = norm (T)$
5		nmoi2.z	$⊢ \underset{˙}{0} = 0_{S}$
6		nmoleub.1	$⊢ φ \to S \in NrmGrp$
7		nmoleub.2	$⊢ φ \to T \in NrmGrp$
8		nmoleub.3	$⊢ φ \to F \in (S GrpHom T)$
9		nmoleub.4	$⊢ φ \to A \in ℝ^{*}$
10		nmoleub.5	$⊢ φ \to 0 \leq A$
11	7	ad2antrr	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land x \neq \underset{˙}{0})) \to T \in NrmGrp$
12		eqid	$⊢ {Base}_{T} = {Base}_{T}$
13	2 12	ghmf	$⊢ F \in (S GrpHom T) \to F : V ⟶ {Base}_{T}$
14	8 13	syl	$⊢ φ \to F : V ⟶ {Base}_{T}$
15	14	ad2antrr	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land x \neq \underset{˙}{0})) \to F : V ⟶ {Base}_{T}$
16		simprl	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land x \neq \underset{˙}{0})) \to x \in V$
17		ffvelcdm	$⊢ (F : V ⟶ {Base}_{T} \land x \in V) \to F (x) \in {Base}_{T}$
18	15 16 17	syl2anc	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land x \neq \underset{˙}{0})) \to F (x) \in {Base}_{T}$
19	12 4	nmcl	$⊢ (T \in NrmGrp \land F (x) \in {Base}_{T}) \to M (F (x)) \in ℝ$
20	11 18 19	syl2anc	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land x \neq \underset{˙}{0})) \to M (F (x)) \in ℝ$
21	6	adantr	$⊢ (φ \land N (F) \leq A) \to S \in NrmGrp$
22	2 3 5	nmrpcl	$⊢ (S \in NrmGrp \land x \in V \land x \neq \underset{˙}{0}) \to L (x) \in ℝ^{+}$
23	22	3expb	$⊢ (S \in NrmGrp \land (x \in V \land x \neq \underset{˙}{0})) \to L (x) \in ℝ^{+}$
24	21 23	sylan	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land x \neq \underset{˙}{0})) \to L (x) \in ℝ^{+}$
25	20 24	rerpdivcld	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land x \neq \underset{˙}{0})) \to \frac{M (F (x))}{L (x)} \in ℝ$
26	25	rexrd	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land x \neq \underset{˙}{0})) \to \frac{M (F (x))}{L (x)} \in ℝ^{*}$
27	1	nmocl	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to N (F) \in ℝ^{*}$
28	6 7 8 27	syl3anc	$⊢ φ \to N (F) \in ℝ^{*}$
29	28	ad2antrr	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land x \neq \underset{˙}{0})) \to N (F) \in ℝ^{*}$
30	9	ad2antrr	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land x \neq \underset{˙}{0})) \to A \in ℝ^{*}$
31	6 7 8	3jca	$⊢ φ \to (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T))$
32	31	adantr	$⊢ (φ \land N (F) \leq A) \to (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T))$
33	1 2 3 4 5	nmoi2	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (x \in V \land x \neq \underset{˙}{0})) \to \frac{M (F (x))}{L (x)} \leq N (F)$
34	32 33	sylan	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land x \neq \underset{˙}{0})) \to \frac{M (F (x))}{L (x)} \leq N (F)$
35		simplr	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land x \neq \underset{˙}{0})) \to N (F) \leq A$
36	26 29 30 34 35	xrletrd	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land x \neq \underset{˙}{0})) \to \frac{M (F (x))}{L (x)} \leq A$
37	36	expr	$⊢ ((φ \land N (F) \leq A) \land x \in V) \to (x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A)$
38	37	ralrimiva	$⊢ (φ \land N (F) \leq A) \to \forall x \in V (x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A)$
39		0le0	$⊢ 0 \leq 0$
40		simpllr	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x = \underset{˙}{0}) \to A \in ℝ$
41	40	recnd	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x = \underset{˙}{0}) \to A \in ℂ$
42	41	mul01d	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x = \underset{˙}{0}) \to A \cdot 0 = 0$
43	39 42	breqtrrid	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x = \underset{˙}{0}) \to 0 \leq A \cdot 0$
44		fveq2	$⊢ x = \underset{˙}{0} \to F (x) = F (\underset{˙}{0})$
45	8	ad2antrr	$⊢ ((φ \land A \in ℝ) \land x \in V) \to F \in (S GrpHom T)$
46		eqid	$⊢ 0_{T} = 0_{T}$
47	5 46	ghmid	$⊢ F \in (S GrpHom T) \to F (\underset{˙}{0}) = 0_{T}$
48	45 47	syl	$⊢ ((φ \land A \in ℝ) \land x \in V) \to F (\underset{˙}{0}) = 0_{T}$
49	44 48	sylan9eqr	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x = \underset{˙}{0}) \to F (x) = 0_{T}$
50	49	fveq2d	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x = \underset{˙}{0}) \to M (F (x)) = M (0_{T})$
51	7	ad3antrrr	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x = \underset{˙}{0}) \to T \in NrmGrp$
52	4 46	nm0	$⊢ T \in NrmGrp \to M (0_{T}) = 0$
53	51 52	syl	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x = \underset{˙}{0}) \to M (0_{T}) = 0$
54	50 53	eqtrd	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x = \underset{˙}{0}) \to M (F (x)) = 0$
55		fveq2	$⊢ x = \underset{˙}{0} \to L (x) = L (\underset{˙}{0})$
56	6	ad2antrr	$⊢ ((φ \land A \in ℝ) \land x \in V) \to S \in NrmGrp$
57	3 5	nm0	$⊢ S \in NrmGrp \to L (\underset{˙}{0}) = 0$
58	56 57	syl	$⊢ ((φ \land A \in ℝ) \land x \in V) \to L (\underset{˙}{0}) = 0$
59	55 58	sylan9eqr	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x = \underset{˙}{0}) \to L (x) = 0$
60	59	oveq2d	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x = \underset{˙}{0}) \to A L (x) = A \cdot 0$
61	43 54 60	3brtr4d	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x = \underset{˙}{0}) \to M (F (x)) \leq A L (x)$
62	61	a1d	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x = \underset{˙}{0}) \to ((x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A) \to M (F (x)) \leq A L (x))$
63		simpr	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x \neq \underset{˙}{0}) \to x \neq \underset{˙}{0}$
64	7	ad2antrr	$⊢ ((φ \land A \in ℝ) \land x \in V) \to T \in NrmGrp$
65	14	adantr	$⊢ (φ \land A \in ℝ) \to F : V ⟶ {Base}_{T}$
66	65 17	sylan	$⊢ ((φ \land A \in ℝ) \land x \in V) \to F (x) \in {Base}_{T}$
67	64 66 19	syl2anc	$⊢ ((φ \land A \in ℝ) \land x \in V) \to M (F (x)) \in ℝ$
68	67	adantr	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x \neq \underset{˙}{0}) \to M (F (x)) \in ℝ$
69		simpllr	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x \neq \underset{˙}{0}) \to A \in ℝ$
70	6	adantr	$⊢ (φ \land A \in ℝ) \to S \in NrmGrp$
71	22	3expa	$⊢ ((S \in NrmGrp \land x \in V) \land x \neq \underset{˙}{0}) \to L (x) \in ℝ^{+}$
72	70 71	sylanl1	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x \neq \underset{˙}{0}) \to L (x) \in ℝ^{+}$
73	68 69 72	ledivmul2d	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x \neq \underset{˙}{0}) \to (\frac{M (F (x))}{L (x)} \leq A \leftrightarrow M (F (x)) \leq A L (x))$
74	73	biimpd	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x \neq \underset{˙}{0}) \to (\frac{M (F (x))}{L (x)} \leq A \to M (F (x)) \leq A L (x))$
75	63 74	embantd	$⊢ (((φ \land A \in ℝ) \land x \in V) \land x \neq \underset{˙}{0}) \to ((x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A) \to M (F (x)) \leq A L (x))$
76	62 75	pm2.61dane	$⊢ ((φ \land A \in ℝ) \land x \in V) \to ((x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A) \to M (F (x)) \leq A L (x))$
77	76	ralimdva	$⊢ (φ \land A \in ℝ) \to (\forall x \in V (x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A) \to \forall x \in V M (F (x)) \leq A L (x))$
78	7	adantr	$⊢ (φ \land A \in ℝ) \to T \in NrmGrp$
79	8	adantr	$⊢ (φ \land A \in ℝ) \to F \in (S GrpHom T)$
80		simpr	$⊢ (φ \land A \in ℝ) \to A \in ℝ$
81	10	adantr	$⊢ (φ \land A \in ℝ) \to 0 \leq A$
82	1 2 3 4	nmolb	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land A \in ℝ \land 0 \leq A) \to (\forall x \in V M (F (x)) \leq A L (x) \to N (F) \leq A)$
83	70 78 79 80 81 82	syl311anc	$⊢ (φ \land A \in ℝ) \to (\forall x \in V M (F (x)) \leq A L (x) \to N (F) \leq A)$
84	77 83	syld	$⊢ (φ \land A \in ℝ) \to (\forall x \in V (x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A) \to N (F) \leq A)$
85	84	imp	$⊢ ((φ \land A \in ℝ) \land \forall x \in V (x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A)) \to N (F) \leq A$
86	85	an32s	$⊢ ((φ \land \forall x \in V (x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A)) \land A \in ℝ) \to N (F) \leq A$
87	28	ad2antrr	$⊢ ((φ \land \forall x \in V (x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A)) \land A = +∞) \to N (F) \in ℝ^{*}$
88		pnfge	$⊢ N (F) \in ℝ^{*} \to N (F) \leq +∞$
89	87 88	syl	$⊢ ((φ \land \forall x \in V (x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A)) \land A = +∞) \to N (F) \leq +∞$
90		simpr	$⊢ ((φ \land \forall x \in V (x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A)) \land A = +∞) \to A = +∞$
91	89 90	breqtrrd	$⊢ ((φ \land \forall x \in V (x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A)) \land A = +∞) \to N (F) \leq A$
92		ge0nemnf	$⊢ (A \in ℝ^{*} \land 0 \leq A) \to A \neq −∞$
93	9 10 92	syl2anc	$⊢ φ \to A \neq −∞$
94	9 93	jca	$⊢ φ \to (A \in ℝ^{*} \land A \neq −∞)$
95		xrnemnf	$⊢ (A \in ℝ^{*} \land A \neq −∞) \leftrightarrow (A \in ℝ \lor A = +∞)$
96	94 95	sylib	$⊢ φ \to (A \in ℝ \lor A = +∞)$
97	96	adantr	$⊢ (φ \land \forall x \in V (x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A)) \to (A \in ℝ \lor A = +∞)$
98	86 91 97	mpjaodan	$⊢ (φ \land \forall x \in V (x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A)) \to N (F) \leq A$
99	38 98	impbida	$⊢ φ \to (N (F) \leq A \leftrightarrow \forall x \in V (x \neq \underset{˙}{0} \to \frac{M (F (x))}{L (x)} \leq A))$

Metamath Proof Explorer

Theorem nmoleub

Proof