nmoleub3

Description: The operator norm is the supremum of the value of a linear operator on the unit sphere. (Contributed by Mario Carneiro, 19-Oct-2015) (Proof shortened by AV, 29-Sep-2021)

	Ref	Expression
Hypotheses	nmoleub2.n	$⊢ N = S normOp T$
	nmoleub2.v	$⊢ V = {Base}_{S}$
	nmoleub2.l	$⊢ L = norm (S)$
	nmoleub2.m	$⊢ M = norm (T)$
	nmoleub2.g	$⊢ G = Scalar (S)$
	nmoleub2.w	$⊢ K = {Base}_{G}$
	nmoleub2.s	$⊢ φ \to S \in (NrmMod \cap CMod)$
	nmoleub2.t	$⊢ φ \to T \in (NrmMod \cap CMod)$
	nmoleub2.f	$⊢ φ \to F \in (S LMHom T)$
	nmoleub2.a	$⊢ φ \to A \in ℝ^{*}$
	nmoleub2.r	$⊢ φ \to R \in ℝ^{+}$
	nmoleub3.5	$⊢ φ \to 0 \leq A$
	nmoleub3.6	$⊢ φ \to ℝ \subseteq K$
Assertion	nmoleub3	$⊢ φ \to (N (F) \leq A \leftrightarrow \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A))$

Proof

Step	Hyp	Ref	Expression
1		nmoleub2.n	$⊢ N = S normOp T$
2		nmoleub2.v	$⊢ V = {Base}_{S}$
3		nmoleub2.l	$⊢ L = norm (S)$
4		nmoleub2.m	$⊢ M = norm (T)$
5		nmoleub2.g	$⊢ G = Scalar (S)$
6		nmoleub2.w	$⊢ K = {Base}_{G}$
7		nmoleub2.s	$⊢ φ \to S \in (NrmMod \cap CMod)$
8		nmoleub2.t	$⊢ φ \to T \in (NrmMod \cap CMod)$
9		nmoleub2.f	$⊢ φ \to F \in (S LMHom T)$
10		nmoleub2.a	$⊢ φ \to A \in ℝ^{*}$
11		nmoleub2.r	$⊢ φ \to R \in ℝ^{+}$
12		nmoleub3.5	$⊢ φ \to 0 \leq A$
13		nmoleub3.6	$⊢ φ \to ℝ \subseteq K$
14	12	adantr	$⊢ (φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \to 0 \leq A$
15	9	ad3antrrr	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to F \in (S LMHom T)$
16	13	ad3antrrr	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to ℝ \subseteq K$
17	11	ad3antrrr	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to R \in ℝ^{+}$
18	7	elin1d	$⊢ φ \to S \in NrmMod$
19	18	ad3antrrr	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to S \in NrmMod$
20		nlmngp	$⊢ S \in NrmMod \to S \in NrmGrp$
21	19 20	syl	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to S \in NrmGrp$
22		simprl	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to y \in V$
23		simprr	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to y \neq 0_{S}$
24		eqid	$⊢ 0_{S} = 0_{S}$
25	2 3 24	nmrpcl	$⊢ (S \in NrmGrp \land y \in V \land y \neq 0_{S}) \to L (y) \in ℝ^{+}$
26	21 22 23 25	syl3anc	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to L (y) \in ℝ^{+}$
27	17 26	rpdivcld	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to \frac{R}{L (y)} \in ℝ^{+}$
28	27	rpred	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to \frac{R}{L (y)} \in ℝ$
29	16 28	sseldd	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to \frac{R}{L (y)} \in K$
30		eqid	$⊢ \cdot_{S} = \cdot_{S}$
31		eqid	$⊢ \cdot_{T} = \cdot_{T}$
32	5 6 2 30 31	lmhmlin	$⊢ (F \in (S LMHom T) \land \frac{R}{L (y)} \in K \land y \in V) \to F ((\frac{R}{L (y)}) \cdot_{S} y) = (\frac{R}{L (y)}) \cdot_{T} F (y)$
33	15 29 22 32	syl3anc	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to F ((\frac{R}{L (y)}) \cdot_{S} y) = (\frac{R}{L (y)}) \cdot_{T} F (y)$
34	33	fveq2d	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to M (F ((\frac{R}{L (y)}) \cdot_{S} y)) = M ((\frac{R}{L (y)}) \cdot_{T} F (y))$
35	8	elin1d	$⊢ φ \to T \in NrmMod$
36	35	ad3antrrr	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to T \in NrmMod$
37		eqid	$⊢ Scalar (T) = Scalar (T)$
38	5 37	lmhmsca	$⊢ F \in (S LMHom T) \to Scalar (T) = G$
39	15 38	syl	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to Scalar (T) = G$
40	39	fveq2d	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to {Base}_{Scalar (T)} = {Base}_{G}$
41	40 6	eqtr4di	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to {Base}_{Scalar (T)} = K$
42	29 41	eleqtrrd	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to \frac{R}{L (y)} \in {Base}_{Scalar (T)}$
43		eqid	$⊢ {Base}_{T} = {Base}_{T}$
44	2 43	lmhmf	$⊢ F \in (S LMHom T) \to F : V ⟶ {Base}_{T}$
45	15 44	syl	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to F : V ⟶ {Base}_{T}$
46	45 22	ffvelcdmd	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to F (y) \in {Base}_{T}$
47		eqid	$⊢ {Base}_{Scalar (T)} = {Base}_{Scalar (T)}$
48		eqid	$⊢ norm (Scalar (T)) = norm (Scalar (T))$
49	43 4 31 37 47 48	nmvs	$⊢ (T \in NrmMod \land \frac{R}{L (y)} \in {Base}_{Scalar (T)} \land F (y) \in {Base}_{T}) \to M ((\frac{R}{L (y)}) \cdot_{T} F (y)) = norm (Scalar (T)) (\frac{R}{L (y)}) M (F (y))$
50	36 42 46 49	syl3anc	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to M ((\frac{R}{L (y)}) \cdot_{T} F (y)) = norm (Scalar (T)) (\frac{R}{L (y)}) M (F (y))$
51	39	fveq2d	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to norm (Scalar (T)) = norm (G)$
52	51	fveq1d	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to norm (Scalar (T)) (\frac{R}{L (y)}) = norm (G) (\frac{R}{L (y)})$
53	7	elin2d	$⊢ φ \to S \in CMod$
54	53	ad3antrrr	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to S \in CMod$
55	5 6	clmabs	$⊢ (S \in CMod \land \frac{R}{L (y)} \in K) \to \|\frac{R}{L (y)}\| = norm (G) (\frac{R}{L (y)})$
56	54 29 55	syl2anc	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to \|\frac{R}{L (y)}\| = norm (G) (\frac{R}{L (y)})$
57	27	rpge0d	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to 0 \leq \frac{R}{L (y)}$
58	28 57	absidd	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to \|\frac{R}{L (y)}\| = \frac{R}{L (y)}$
59	56 58	eqtr3d	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to norm (G) (\frac{R}{L (y)}) = \frac{R}{L (y)}$
60	52 59	eqtrd	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to norm (Scalar (T)) (\frac{R}{L (y)}) = \frac{R}{L (y)}$
61	60	oveq1d	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to norm (Scalar (T)) (\frac{R}{L (y)}) M (F (y)) = (\frac{R}{L (y)}) M (F (y))$
62	34 50 61	3eqtrd	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to M (F ((\frac{R}{L (y)}) \cdot_{S} y)) = (\frac{R}{L (y)}) M (F (y))$
63	62	oveq1d	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to \frac{M (F ((\frac{R}{L (y)}) \cdot_{S} y))}{R} = \frac{(\frac{R}{L (y)}) M (F (y))}{R}$
64	27	rpcnd	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to \frac{R}{L (y)} \in ℂ$
65		nlmngp	$⊢ T \in NrmMod \to T \in NrmGrp$
66	36 65	syl	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to T \in NrmGrp$
67	43 4	nmcl	$⊢ (T \in NrmGrp \land F (y) \in {Base}_{T}) \to M (F (y)) \in ℝ$
68	66 46 67	syl2anc	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to M (F (y)) \in ℝ$
69	68	recnd	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to M (F (y)) \in ℂ$
70	17	rpcnd	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to R \in ℂ$
71	17	rpne0d	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to R \neq 0$
72	64 69 70 71	divassd	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to \frac{(\frac{R}{L (y)}) M (F (y))}{R} = (\frac{R}{L (y)}) (\frac{M (F (y))}{R})$
73	26	rpcnd	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to L (y) \in ℂ$
74	26	rpne0d	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to L (y) \neq 0$
75	69 70 73 71 74	dmdcand	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to (\frac{R}{L (y)}) (\frac{M (F (y))}{R}) = \frac{M (F (y))}{L (y)}$
76	63 72 75	3eqtrd	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to \frac{M (F ((\frac{R}{L (y)}) \cdot_{S} y))}{R} = \frac{M (F (y))}{L (y)}$
77		eqid	$⊢ norm (G) = norm (G)$
78	2 3 30 5 6 77	nmvs	$⊢ (S \in NrmMod \land \frac{R}{L (y)} \in K \land y \in V) \to L ((\frac{R}{L (y)}) \cdot_{S} y) = norm (G) (\frac{R}{L (y)}) L (y)$
79	19 29 22 78	syl3anc	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to L ((\frac{R}{L (y)}) \cdot_{S} y) = norm (G) (\frac{R}{L (y)}) L (y)$
80	59	oveq1d	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to norm (G) (\frac{R}{L (y)}) L (y) = (\frac{R}{L (y)}) L (y)$
81	70 73 74	divcan1d	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to (\frac{R}{L (y)}) L (y) = R$
82	79 80 81	3eqtrd	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to L ((\frac{R}{L (y)}) \cdot_{S} y) = R$
83		fveqeq2	$⊢ x = (\frac{R}{L (y)}) \cdot_{S} y \to (L (x) = R \leftrightarrow L ((\frac{R}{L (y)}) \cdot_{S} y) = R)$
84		2fveq3	$⊢ x = (\frac{R}{L (y)}) \cdot_{S} y \to M (F (x)) = M (F ((\frac{R}{L (y)}) \cdot_{S} y))$
85	84	oveq1d	$⊢ x = (\frac{R}{L (y)}) \cdot_{S} y \to \frac{M (F (x))}{R} = \frac{M (F ((\frac{R}{L (y)}) \cdot_{S} y))}{R}$
86	85	breq1d	$⊢ x = (\frac{R}{L (y)}) \cdot_{S} y \to (\frac{M (F (x))}{R} \leq A \leftrightarrow \frac{M (F ((\frac{R}{L (y)}) \cdot_{S} y))}{R} \leq A)$
87	83 86	imbi12d	$⊢ x = (\frac{R}{L (y)}) \cdot_{S} y \to ((L (x) = R \to \frac{M (F (x))}{R} \leq A) \leftrightarrow (L ((\frac{R}{L (y)}) \cdot_{S} y) = R \to \frac{M (F ((\frac{R}{L (y)}) \cdot_{S} y))}{R} \leq A))$
88		simpllr	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)$
89	2 5 30 6	clmvscl	$⊢ (S \in CMod \land \frac{R}{L (y)} \in K \land y \in V) \to (\frac{R}{L (y)}) \cdot_{S} y \in V$
90	54 29 22 89	syl3anc	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to (\frac{R}{L (y)}) \cdot_{S} y \in V$
91	87 88 90	rspcdva	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to (L ((\frac{R}{L (y)}) \cdot_{S} y) = R \to \frac{M (F ((\frac{R}{L (y)}) \cdot_{S} y))}{R} \leq A)$
92	82 91	mpd	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to \frac{M (F ((\frac{R}{L (y)}) \cdot_{S} y))}{R} \leq A$
93	76 92	eqbrtrrd	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to \frac{M (F (y))}{L (y)} \leq A$
94		simplr	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to A \in ℝ$
95	68 94 26	ledivmul2d	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to (\frac{M (F (y))}{L (y)} \leq A \leftrightarrow M (F (y)) \leq A L (y))$
96	93 95	mpbid	$⊢ (((φ \land \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \land (y \in V \land y \neq 0_{S})) \to M (F (y)) \leq A L (y)$
97	11	adantr	$⊢ (φ \land x \in V) \to R \in ℝ^{+}$
98	97	rpred	$⊢ (φ \land x \in V) \to R \in ℝ$
99	98	leidd	$⊢ (φ \land x \in V) \to R \leq R$
100		breq1	$⊢ L (x) = R \to (L (x) \leq R \leftrightarrow R \leq R)$
101	99 100	syl5ibrcom	$⊢ (φ \land x \in V) \to (L (x) = R \to L (x) \leq R)$
102	1 2 3 4 5 6 7 8 9 10 11 14 96 101	nmoleub2lem	$⊢ φ \to (N (F) \leq A \leftrightarrow \forall x \in V (L (x) = R \to \frac{M (F (x))}{R} \leq A))$

Metamath Proof Explorer

Theorem nmoleub3

Proof