Metamath Proof Explorer

Theorem nmblolbi

Description: A lower bound for the norm of a bounded linear operator. (Contributed by NM, 10-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmblolbi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nmblolbi.4 ⊢ 𝐿 = ( normCV ‘ 𝑈 )
nmblolbi.5 ⊢ 𝑀 = ( normCV ‘ 𝑊 )
nmblolbi.6 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
nmblolbi.7 ⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
nmblolbi.u ⊢ 𝑈 ∈ NrmCVec
nmblolbi.w ⊢ 𝑊 ∈ NrmCVec
Assertion nmblolbi ( ( 𝑇 ∈ 𝐵 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 nmblolbi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nmblolbi.4 ⊢ 𝐿 = ( normCV ‘ 𝑈 )
3 nmblolbi.5 ⊢ 𝑀 = ( normCV ‘ 𝑊 )
4 nmblolbi.6 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
5 nmblolbi.7 ⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
6 nmblolbi.u ⊢ 𝑈 ∈ NrmCVec
7 nmblolbi.w ⊢ 𝑊 ∈ NrmCVec
8 fveq1 ⊢ ( 𝑇 = if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) → ( 𝑇 ‘ 𝐴 ) = ( if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ‘ 𝐴 ) )
9 8 fveq2d ⊢ ( 𝑇 = if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ‘ 𝐴 ) ) )
10 fveq2 ⊢ ( 𝑇 = if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) → ( 𝑁 ‘ 𝑇 ) = ( 𝑁 ‘ if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ) )
11 10 oveq1d ⊢ ( 𝑇 = if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) → ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) = ( ( 𝑁 ‘ if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ) · ( 𝐿 ‘ 𝐴 ) ) )
12 9 11 breq12d ⊢ ( 𝑇 = if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) ↔ ( 𝑀 ‘ ( if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ) · ( 𝐿 ‘ 𝐴 ) ) ) )
13 12 imbi2d ⊢ ( 𝑇 = if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) → ( ( 𝐴 ∈ 𝑋 → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) ) ↔ ( 𝐴 ∈ 𝑋 → ( 𝑀 ‘ ( if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ) · ( 𝐿 ‘ 𝐴 ) ) ) ) )
14 eqid ⊢ ( 𝑈 0op 𝑊 ) = ( 𝑈 0op 𝑊 )
15 14 5 0blo ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑈 0op 𝑊 ) ∈ 𝐵 )
16 6 7 15 mp2an ⊢ ( 𝑈 0op 𝑊 ) ∈ 𝐵
17 16 elimel ⊢ if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ∈ 𝐵
18 1 2 3 4 5 6 7 17 nmblolbii ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑀 ‘ ( if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ if ( 𝑇 ∈ 𝐵 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ) · ( 𝐿 ‘ 𝐴 ) ) )
19 13 18 dedth ⊢ ( 𝑇 ∈ 𝐵 → ( 𝐴 ∈ 𝑋 → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) ) )
20 19 imp ⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) )