Metamath Proof Explorer

Theorem nmoolb

Description: A lower bound for an operator norm. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoolb.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nmoolb.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
nmoolb.l ⊢ 𝐿 = ( normCV ‘ 𝑈 )
nmoolb.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
nmoolb.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
Assertion nmoolb ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ ( 𝐿 ‘ 𝐴 ) ≤ 1 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( 𝑁 ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 nmoolb.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nmoolb.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3 nmoolb.l ⊢ 𝐿 = ( normCV ‘ 𝑈 )
4 nmoolb.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
5 nmoolb.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
6 2 4 nmosetre ⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ )
7 ressxr ⊢ ℝ ⊆ ℝ*
8 6 7 sstrdi ⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ* )
9 8 3adant1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ* )
10 fveq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐿 ‘ 𝑦 ) = ( 𝐿 ‘ 𝐴 ) )
11 10 breq1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ↔ ( 𝐿 ‘ 𝐴 ) ≤ 1 ) )
12 2fveq3 ⊢ ( 𝑦 = 𝐴 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) )
13 12 eqeq2d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ↔ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
14 11 13 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ↔ ( ( 𝐿 ‘ 𝐴 ) ≤ 1 ∧ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ) ) )
15 eqid ⊢ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) )
16 15 biantru ⊢ ( ( 𝐿 ‘ 𝐴 ) ≤ 1 ↔ ( ( 𝐿 ‘ 𝐴 ) ≤ 1 ∧ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
17 14 16 bitr4di ⊢ ( 𝑦 = 𝐴 → ( ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ↔ ( 𝐿 ‘ 𝐴 ) ≤ 1 ) )
18 17 rspcev ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝐿 ‘ 𝐴 ) ≤ 1 ) → ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
19 fvex ⊢ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ V
20 eqeq1 ⊢ ( 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) → ( 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ↔ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
21 20 anbi2d ⊢ ( 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) → ( ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ↔ ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) )
22 21 rexbidv ⊢ ( 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) → ( ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ↔ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) )
23 19 22 elab ⊢ ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ↔ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
24 18 23 sylibr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝐿 ‘ 𝐴 ) ≤ 1 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) } )
25 supxrub ⊢ ( ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ* ∧ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) )
26 9 24 25 syl2an ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ ( 𝐿 ‘ 𝐴 ) ≤ 1 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) )
27 1 2 3 4 5 nmooval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑁 ‘ 𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) )
28 27 adantr ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ ( 𝐿 ‘ 𝐴 ) ≤ 1 ) ) → ( 𝑁 ‘ 𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) )
29 26 28 breqtrrd ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ ( 𝐿 ‘ 𝐴 ) ≤ 1 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( 𝑁 ‘ 𝑇 ) )