Metamath Proof Explorer

Theorem nmcoplb

Description: A lower bound for the norm of a continuous linear Hilbert space operator. Theorem 3.5(ii) of Beran p. 99. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmcoplb ( ( 𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ∧ 𝐴 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝑇 ∈ ( LinOp ∩ ContOp ) ↔ ( 𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ) )
2 fveq1 ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) → ( 𝑇 ‘ 𝐴 ) = ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝐴 ) )
3 2 fveq2d ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) = ( normℎ ‘ ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝐴 ) ) )
4 fveq2 ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) → ( normop ‘ 𝑇 ) = ( normop ‘ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ) )
5 4 oveq1d ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) = ( ( normop ‘ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ) · ( normℎ ‘ 𝐴 ) ) )
6 3 5 breq12d ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ↔ ( normℎ ‘ ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝐴 ) ) ≤ ( ( normop ‘ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ) · ( normℎ ‘ 𝐴 ) ) ) )
7 6 imbi2d ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ) ↔ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝐴 ) ) ≤ ( ( normop ‘ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ) · ( normℎ ‘ 𝐴 ) ) ) ) )
8 idlnop ⊢ ( I ↾ ℋ ) ∈ LinOp
9 idcnop ⊢ ( I ↾ ℋ ) ∈ ContOp
10 elin ⊢ ( ( I ↾ ℋ ) ∈ ( LinOp ∩ ContOp ) ↔ ( ( I ↾ ℋ ) ∈ LinOp ∧ ( I ↾ ℋ ) ∈ ContOp ) )
11 8 9 10 mpbir2an ⊢ ( I ↾ ℋ ) ∈ ( LinOp ∩ ContOp )
12 11 elimel ⊢ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ∈ ( LinOp ∩ ContOp )
13 elin ⊢ ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ∈ ( LinOp ∩ ContOp ) ↔ ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp ∧ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ∈ ContOp ) )
14 12 13 mpbi ⊢ ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp ∧ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ∈ ContOp )
15 14 simpli ⊢ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp
16 14 simpri ⊢ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ∈ ContOp
17 15 16 nmcoplbi ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝐴 ) ) ≤ ( ( normop ‘ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ) · ( normℎ ‘ 𝐴 ) ) )
18 7 17 dedth ⊢ ( 𝑇 ∈ ( LinOp ∩ ContOp ) → ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ) )
19 18 imp ⊢ ( ( 𝑇 ∈ ( LinOp ∩ ContOp ) ∧ 𝐴 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )
20 1 19 sylanbr ⊢ ( ( ( 𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ) ∧ 𝐴 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )
21 20 3impa ⊢ ( ( 𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ∧ 𝐴 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )