Theorem nmoub3i

Description: An upper bound for an operator norm. (Contributed by NM, 12-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmoubi.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nmoubi.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	nmoubi.l	⊢ 𝐿 = ( normCV ‘ 𝑈 )
	nmoubi.m	⊢ 𝑀 = ( normCV ‘ 𝑊 )
	nmoubi.3	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
	nmoubi.u	⊢ 𝑈 ∈ NrmCVec
	nmoubi.w	⊢ 𝑊 ∈ NrmCVec
Assertion	nmoub3i	⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ ( abs ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		nmoubi.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nmoubi.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3		nmoubi.l	⊢ 𝐿 = ( normCV ‘ 𝑈 )
4		nmoubi.m	⊢ 𝑀 = ( normCV ‘ 𝑊 )
5		nmoubi.3	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
6		nmoubi.u	⊢ 𝑈 ∈ NrmCVec
7		nmoubi.w	⊢ 𝑊 ∈ NrmCVec
8	1 3	nvcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) → ( 𝐿 ‘ 𝑥 ) ∈ ℝ )
9	6 8	mpan	⊢ ( 𝑥 ∈ 𝑋 → ( 𝐿 ‘ 𝑥 ) ∈ ℝ )
10		remulcl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐿 ‘ 𝑥 ) ∈ ℝ ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ )
11	9 10	sylan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ )
12	11	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ )
13		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
14	13	abscld	⊢ ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) ∈ ℝ )
15		remulcl	⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ ( 𝐿 ‘ 𝑥 ) ∈ ℝ ) → ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ )
16	14 9 15	syl2an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ )
17	16	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ )
18	14	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
19		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
20	14	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
21	1 3	nvge0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( 𝐿 ‘ 𝑥 ) )
22	6 21	mpan	⊢ ( 𝑥 ∈ 𝑋 → 0 ≤ ( 𝐿 ‘ 𝑥 ) )
23	9 22	jca	⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐿 ‘ 𝑥 ) ) )
24	23	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐿 ‘ 𝑥 ) ) )
25		leabs	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ ( abs ‘ 𝐴 ) )
26	25	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ≤ ( abs ‘ 𝐴 ) )
27		lemul1a	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( abs ‘ 𝐴 ) ∈ ℝ ∧ ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐿 ‘ 𝑥 ) ) ) ∧ 𝐴 ≤ ( abs ‘ 𝐴 ) ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ≤ ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) )
28	19 20 24 26 27	syl31anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ≤ ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) )
29	28	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ≤ ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) )
30	9	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → ( 𝐿 ‘ 𝑥 ) ∈ ℝ )
31		1red	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → 1 ∈ ℝ )
32	13	absge0d	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( abs ‘ 𝐴 ) )
33	32	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( abs ‘ 𝐴 ) )
34	20 33	jca	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) )
35	30 31 34	3jca	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) ) )
36		lemul2a	⊢ ( ( ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) ≤ ( ( abs ‘ 𝐴 ) · 1 ) )
37	35 36	sylan	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) ≤ ( ( abs ‘ 𝐴 ) · 1 ) )
38	14	recnd	⊢ ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) ∈ ℂ )
39	38	mulridd	⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ 𝐴 ) · 1 ) = ( abs ‘ 𝐴 ) )
40	39	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( ( abs ‘ 𝐴 ) · 1 ) = ( abs ‘ 𝐴 ) )
41	37 40	breqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) )
42	12 17 18 29 41	letrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) )
43	42	adantlll	⊢ ( ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) )
44		ffvelcdm	⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑇 ‘ 𝑥 ) ∈ 𝑌 )
45	2 4	nvcl	⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝑥 ) ∈ 𝑌 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
46	7 44 45	sylancr	⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
47	46	adantlr	⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
48	11	adantll	⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ )
49	14	ad2antlr	⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
50		letr	⊢ ( ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ ∧ ( abs ‘ 𝐴 ) ∈ ℝ ) → ( ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ∧ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) )
51	47 48 49 50	syl3anc	⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ∧ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) )
52	51	adantr	⊢ ( ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ∧ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) )
53	43 52	mpan2d	⊢ ( ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) )
54	53	ex	⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) ) )
55	54	com23	⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) ) )
56	55	ralimdva	⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) ) )
57	56	imp	⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) )
58	14	rexrd	⊢ ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) ∈ ℝ* )
59	1 2 3 4 5 6 7	nmoubi	⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ( abs ‘ 𝐴 ) ∈ ℝ* ) → ( ( 𝑁 ‘ 𝑇 ) ≤ ( abs ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) ) )
60	58 59	sylan2	⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) → ( ( 𝑁 ‘ 𝑇 ) ≤ ( abs ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) ) )
61	60	biimpar	⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ ( abs ‘ 𝐴 ) )
62	57 61	syldan	⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ ( abs ‘ 𝐴 ) )
63	62	3impa	⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ ( abs ‘ 𝐴 ) )