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	⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) )