nmoi

Description: The operator norm achieves the minimum of the set of upper bounds, if the operator is bounded. (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)$
Assertion	nmoi	$⊢ (F \in (S NGHom T) \land X \in V) \to M (F (X)) \leq N (F) L (X)$

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		2fveq3	$⊢ X = 0_{S} \to M (F (X)) = M (F (0_{S}))$
6		fveq2	$⊢ X = 0_{S} \to L (X) = L (0_{S})$
7	6	oveq2d	$⊢ X = 0_{S} \to N (F) L (X) = N (F) L (0_{S})$
8	5 7	breq12d	$⊢ X = 0_{S} \to (M (F (X)) \leq N (F) L (X) \leftrightarrow M (F (0_{S})) \leq N (F) L (0_{S}))$
9		2fveq3	$⊢ x = X \to M (F (x)) = M (F (X))$
10		fveq2	$⊢ x = X \to L (x) = L (X)$
11	10	oveq2d	$⊢ x = X \to r L (x) = r L (X)$
12	9 11	breq12d	$⊢ x = X \to (M (F (x)) \leq r L (x) \leftrightarrow M (F (X)) \leq r L (X))$
13	12	rspcv	$⊢ X \in V \to (\forall x \in V M (F (x)) \leq r L (x) \to M (F (X)) \leq r L (X))$
14	13	ad3antlr	$⊢ (((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \land r \in [0, +∞)) \to (\forall x \in V M (F (x)) \leq r L (x) \to M (F (X)) \leq r L (X))$
15	1	isnghm	$⊢ F \in (S NGHom T) \leftrightarrow ((S \in NrmGrp \land T \in NrmGrp) \land (F \in (S GrpHom T) \land N (F) \in ℝ))$
16	15	simplbi	$⊢ F \in (S NGHom T) \to (S \in NrmGrp \land T \in NrmGrp)$
17	16	adantr	$⊢ (F \in (S NGHom T) \land X \in V) \to (S \in NrmGrp \land T \in NrmGrp)$
18	17	simprd	$⊢ (F \in (S NGHom T) \land X \in V) \to T \in NrmGrp$
19	15	simprbi	$⊢ F \in (S NGHom T) \to (F \in (S GrpHom T) \land N (F) \in ℝ)$
20	19	adantr	$⊢ (F \in (S NGHom T) \land X \in V) \to (F \in (S GrpHom T) \land N (F) \in ℝ)$
21	20	simpld	$⊢ (F \in (S NGHom T) \land X \in V) \to F \in (S GrpHom T)$
22		eqid	$⊢ {Base}_{T} = {Base}_{T}$
23	2 22	ghmf	$⊢ F \in (S GrpHom T) \to F : V ⟶ {Base}_{T}$
24	21 23	syl	$⊢ (F \in (S NGHom T) \land X \in V) \to F : V ⟶ {Base}_{T}$
25		ffvelcdm	$⊢ (F : V ⟶ {Base}_{T} \land X \in V) \to F (X) \in {Base}_{T}$
26	24 25	sylancom	$⊢ (F \in (S NGHom T) \land X \in V) \to F (X) \in {Base}_{T}$
27	22 4	nmcl	$⊢ (T \in NrmGrp \land F (X) \in {Base}_{T}) \to M (F (X)) \in ℝ$
28	18 26 27	syl2anc	$⊢ (F \in (S NGHom T) \land X \in V) \to M (F (X)) \in ℝ$
29	28	adantr	$⊢ ((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \to M (F (X)) \in ℝ$
30	29	adantr	$⊢ (((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \land r \in [0, +∞)) \to M (F (X)) \in ℝ$
31		elrege0	$⊢ r \in [0, +∞) \leftrightarrow (r \in ℝ \land 0 \leq r)$
32	31	simplbi	$⊢ r \in [0, +∞) \to r \in ℝ$
33	32	adantl	$⊢ (((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \land r \in [0, +∞)) \to r \in ℝ$
34	17	simpld	$⊢ (F \in (S NGHom T) \land X \in V) \to S \in NrmGrp$
35		simpr	$⊢ (F \in (S NGHom T) \land X \in V) \to X \in V$
36	34 35	jca	$⊢ (F \in (S NGHom T) \land X \in V) \to (S \in NrmGrp \land X \in V)$
37		eqid	$⊢ 0_{S} = 0_{S}$
38	2 3 37	nmrpcl	$⊢ (S \in NrmGrp \land X \in V \land X \neq 0_{S}) \to L (X) \in ℝ^{+}$
39	38	3expa	$⊢ ((S \in NrmGrp \land X \in V) \land X \neq 0_{S}) \to L (X) \in ℝ^{+}$
40	36 39	sylan	$⊢ ((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \to L (X) \in ℝ^{+}$
41	40	rpregt0d	$⊢ ((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \to (L (X) \in ℝ \land 0 < L (X))$
42	41	adantr	$⊢ (((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \land r \in [0, +∞)) \to (L (X) \in ℝ \land 0 < L (X))$
43		ledivmul2	$⊢ (M (F (X)) \in ℝ \land r \in ℝ \land (L (X) \in ℝ \land 0 < L (X))) \to (\frac{M (F (X))}{L (X)} \leq r \leftrightarrow M (F (X)) \leq r L (X))$
44	30 33 42 43	syl3anc	$⊢ (((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \land r \in [0, +∞)) \to (\frac{M (F (X))}{L (X)} \leq r \leftrightarrow M (F (X)) \leq r L (X))$
45	14 44	sylibrd	$⊢ (((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \land r \in [0, +∞)) \to (\forall x \in V M (F (x)) \leq r L (x) \to \frac{M (F (X))}{L (X)} \leq r)$
46	45	ralrimiva	$⊢ ((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \to \forall r \in [0, +∞) (\forall x \in V M (F (x)) \leq r L (x) \to \frac{M (F (X))}{L (X)} \leq r)$
47	34	adantr	$⊢ ((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \to S \in NrmGrp$
48	18	adantr	$⊢ ((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \to T \in NrmGrp$
49	21	adantr	$⊢ ((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \to F \in (S GrpHom T)$
50	29 40	rerpdivcld	$⊢ ((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \to \frac{M (F (X))}{L (X)} \in ℝ$
51	50	rexrd	$⊢ ((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \to \frac{M (F (X))}{L (X)} \in ℝ^{*}$
52	1 2 3 4	nmogelb	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land \frac{M (F (X))}{L (X)} \in ℝ^{*}) \to (\frac{M (F (X))}{L (X)} \leq N (F) \leftrightarrow \forall r \in [0, +∞) (\forall x \in V M (F (x)) \leq r L (x) \to \frac{M (F (X))}{L (X)} \leq r))$
53	47 48 49 51 52	syl31anc	$⊢ ((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \to (\frac{M (F (X))}{L (X)} \leq N (F) \leftrightarrow \forall r \in [0, +∞) (\forall x \in V M (F (x)) \leq r L (x) \to \frac{M (F (X))}{L (X)} \leq r))$
54	46 53	mpbird	$⊢ ((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \to \frac{M (F (X))}{L (X)} \leq N (F)$
55	20	simprd	$⊢ (F \in (S NGHom T) \land X \in V) \to N (F) \in ℝ$
56	55	adantr	$⊢ ((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \to N (F) \in ℝ$
57	29 56 40	ledivmul2d	$⊢ ((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \to (\frac{M (F (X))}{L (X)} \leq N (F) \leftrightarrow M (F (X)) \leq N (F) L (X))$
58	54 57	mpbid	$⊢ ((F \in (S NGHom T) \land X \in V) \land X \neq 0_{S}) \to M (F (X)) \leq N (F) L (X)$
59		eqid	$⊢ 0_{T} = 0_{T}$
60	37 59	ghmid	$⊢ F \in (S GrpHom T) \to F (0_{S}) = 0_{T}$
61	21 60	syl	$⊢ (F \in (S NGHom T) \land X \in V) \to F (0_{S}) = 0_{T}$
62	61	fveq2d	$⊢ (F \in (S NGHom T) \land X \in V) \to M (F (0_{S})) = M (0_{T})$
63	4 59	nm0	$⊢ T \in NrmGrp \to M (0_{T}) = 0$
64	18 63	syl	$⊢ (F \in (S NGHom T) \land X \in V) \to M (0_{T}) = 0$
65	62 64	eqtrd	$⊢ (F \in (S NGHom T) \land X \in V) \to M (F (0_{S})) = 0$
66	3 37	nm0	$⊢ S \in NrmGrp \to L (0_{S}) = 0$
67	34 66	syl	$⊢ (F \in (S NGHom T) \land X \in V) \to L (0_{S}) = 0$
68		0re	$⊢ 0 \in ℝ$
69	67 68	eqeltrdi	$⊢ (F \in (S NGHom T) \land X \in V) \to L (0_{S}) \in ℝ$
70	1	nmoge0	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to 0 \leq N (F)$
71	34 18 21 70	syl3anc	$⊢ (F \in (S NGHom T) \land X \in V) \to 0 \leq N (F)$
72		0le0	$⊢ 0 \leq 0$
73	72 67	breqtrrid	$⊢ (F \in (S NGHom T) \land X \in V) \to 0 \leq L (0_{S})$
74	55 69 71 73	mulge0d	$⊢ (F \in (S NGHom T) \land X \in V) \to 0 \leq N (F) L (0_{S})$
75	65 74	eqbrtrd	$⊢ (F \in (S NGHom T) \land X \in V) \to M (F (0_{S})) \leq N (F) L (0_{S})$
76	8 58 75	pm2.61ne	$⊢ (F \in (S NGHom T) \land X \in V) \to M (F (X)) \leq N (F) L (X)$

Metamath Proof Explorer

Theorem nmoi

Proof