nmoubi

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

	Ref	Expression
Hypotheses	nmoubi.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nmoubi.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	nmoubi.l	⊢ 𝐿 = ( norm_CV ‘ 𝑈 )
	nmoubi.m	⊢ 𝑀 = ( norm_CV ‘ 𝑊 )
	nmoubi.3	⊢ 𝑁 = ( 𝑈 normOp_OLD 𝑊 )
	nmoubi.u	⊢ 𝑈 ∈ NrmCVec
	nmoubi.w	⊢ 𝑊 ∈ NrmCVec
Assertion	nmoubi	⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ^* ) → ( ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmoubi.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nmoubi.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3		nmoubi.l	⊢ 𝐿 = ( norm_CV ‘ 𝑈 )
4		nmoubi.m	⊢ 𝑀 = ( norm_CV ‘ 𝑊 )
5		nmoubi.3	⊢ 𝑁 = ( 𝑈 normOp_OLD 𝑊 )
6		nmoubi.u	⊢ 𝑈 ∈ NrmCVec
7		nmoubi.w	⊢ 𝑊 ∈ NrmCVec
8	1 2 3 4 5	nmooval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑁 ‘ 𝑇 ) = sup ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ^* , < ) )
9	6 7 8	mp3an12	⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( 𝑁 ‘ 𝑇 ) = sup ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ^* , < ) )
10	9	breq1d	⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 ↔ sup ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ^* , < ) ≤ 𝐴 ) )
11	10	adantr	⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ^* ) → ( ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 ↔ sup ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ^* , < ) ≤ 𝐴 ) )
12	2 4	nmosetre	⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ⊆ ℝ )
13	7 12	mpan	⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ⊆ ℝ )
14		ressxr	⊢ ℝ ⊆ ℝ^*
15	13 14	sstrdi	⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ⊆ ℝ^* )
16		supxrleub	⊢ ( ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ⊆ ℝ^* ∧ 𝐴 ∈ ℝ^* ) → ( sup ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ^* , < ) ≤ 𝐴 ↔ ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑧 ≤ 𝐴 ) )
17	15 16	sylan	⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ^* ) → ( sup ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ^* , < ) ≤ 𝐴 ↔ ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑧 ≤ 𝐴 ) )
18	11 17	bitrd	⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ^* ) → ( ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 ↔ ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑧 ≤ 𝐴 ) )
19		eqeq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ↔ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
20	19	anbi2d	⊢ ( 𝑦 = 𝑧 → ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ↔ ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) )
21	20	rexbidv	⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ↔ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) )
22	21	ralab	⊢ ( ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑧 ≤ 𝐴 ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) )
23		ralcom4	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) ↔ ∀ 𝑧 ∀ 𝑥 ∈ 𝑋 ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) )
24		ancomst	⊢ ( ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) ↔ ( ( 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → 𝑧 ≤ 𝐴 ) )
25		impexp	⊢ ( ( ( 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → 𝑧 ≤ 𝐴 ) ↔ ( 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → 𝑧 ≤ 𝐴 ) ) )
26	24 25	bitri	⊢ ( ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) ↔ ( 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → 𝑧 ≤ 𝐴 ) ) )
27	26	albii	⊢ ( ∀ 𝑧 ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) ↔ ∀ 𝑧 ( 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → 𝑧 ≤ 𝐴 ) ) )
28		fvex	⊢ ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ V
29		breq1	⊢ ( 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( 𝑧 ≤ 𝐴 ↔ ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) )
30	29	imbi2d	⊢ ( 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → 𝑧 ≤ 𝐴 ) ↔ ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ) )
31	28 30	ceqsalv	⊢ ( ∀ 𝑧 ( 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → 𝑧 ≤ 𝐴 ) ) ↔ ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) )
32	27 31	bitri	⊢ ( ∀ 𝑧 ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) ↔ ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) )
33	32	ralbii	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) )
34		r19.23v	⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) ↔ ( ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) )
35	34	albii	⊢ ( ∀ 𝑧 ∀ 𝑥 ∈ 𝑋 ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) )
36	23 33 35	3bitr3i	⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) )
37	22 36	bitr4i	⊢ ( ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑧 ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) )
38	18 37	bitrdi	⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ^* ) → ( ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ) )

Metamath Proof Explorer

Theorem nmoubi

Proof