Theorem nmlnoubi

Description: An upper bound for the operator norm of a linear operator, using only the properties of nonzero arguments. (Contributed by NM, 1-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmlnoubi.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nmlnoubi.z	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
	nmlnoubi.k	⊢ 𝐾 = ( normCV ‘ 𝑈 )
	nmlnoubi.m	⊢ 𝑀 = ( normCV ‘ 𝑊 )
	nmlnoubi.3	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
	nmlnoubi.7	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
	nmlnoubi.u	⊢ 𝑈 ∈ NrmCVec
	nmlnoubi.w	⊢ 𝑊 ∈ NrmCVec
Assertion	nmlnoubi	⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nmlnoubi.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nmlnoubi.z	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
3		nmlnoubi.k	⊢ 𝐾 = ( normCV ‘ 𝑈 )
4		nmlnoubi.m	⊢ 𝑀 = ( normCV ‘ 𝑊 )
5		nmlnoubi.3	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
6		nmlnoubi.7	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
7		nmlnoubi.u	⊢ 𝑈 ∈ NrmCVec
8		nmlnoubi.w	⊢ 𝑊 ∈ NrmCVec
9		2fveq3	⊢ ( 𝑥 = 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) )
10		fveq2	⊢ ( 𝑥 = 𝑍 → ( 𝐾 ‘ 𝑥 ) = ( 𝐾 ‘ 𝑍 ) )
11	10	oveq2d	⊢ ( 𝑥 = 𝑍 → ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) = ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) )
12	9 11	breq12d	⊢ ( 𝑥 = 𝑍 → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ↔ ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) ) )
13		id	⊢ ( ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) → ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) )
14	13	imp	⊢ ( ( ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ∧ 𝑥 ≠ 𝑍 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) )
15	14	adantll	⊢ ( ( ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) ∧ ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ≠ 𝑍 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) )
16		0le0	⊢ 0 ≤ 0
17		eqid	⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
18		eqid	⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 )
19	1 17 2 18 6	lno0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ‘ 𝑍 ) = ( 0vec ‘ 𝑊 ) )
20	7 8 19	mp3an12	⊢ ( 𝑇 ∈ 𝐿 → ( 𝑇 ‘ 𝑍 ) = ( 0vec ‘ 𝑊 ) )
21	20	fveq2d	⊢ ( 𝑇 ∈ 𝐿 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) = ( 𝑀 ‘ ( 0vec ‘ 𝑊 ) ) )
22	18 4	nvz0	⊢ ( 𝑊 ∈ NrmCVec → ( 𝑀 ‘ ( 0vec ‘ 𝑊 ) ) = 0 )
23	8 22	ax-mp	⊢ ( 𝑀 ‘ ( 0vec ‘ 𝑊 ) ) = 0
24	21 23	eqtrdi	⊢ ( 𝑇 ∈ 𝐿 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) = 0 )
25	24	adantr	⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) = 0 )
26	2 3	nvz0	⊢ ( 𝑈 ∈ NrmCVec → ( 𝐾 ‘ 𝑍 ) = 0 )
27	7 26	ax-mp	⊢ ( 𝐾 ‘ 𝑍 ) = 0
28	27	oveq2i	⊢ ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) = ( 𝐴 · 0 )
29		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
30	29	mul01d	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) = 0 )
31	28 30	syl5eq	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) = 0 )
32	31	ad2antrl	⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) = 0 )
33	25 32	breq12d	⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) ↔ 0 ≤ 0 ) )
34	16 33	mpbiri	⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) )
35	34	adantr	⊢ ( ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) ∧ ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) )
36	12 15 35	pm2.61ne	⊢ ( ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) ∧ ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) )
37	36	ex	⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) )
38	37	ralimdv	⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) )
39	38	3impia	⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) )
40	1 17 6	lnof	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
41	7 8 40	mp3an12	⊢ ( 𝑇 ∈ 𝐿 → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
42	1 17 3 4 5 7 8	nmoub2i	⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 )
43	41 42	syl3an1	⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 )
44	39 43	syld3an3	⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 )