Metamath Proof Explorer

Theorem nmcopex

Description: The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of Beran p. 99. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmcopex ( ( 𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ) → ( normop ‘ 𝑇 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝑇 ∈ ( LinOp ∩ ContOp ) ↔ ( 𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ) )
2 fveq2 ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) → ( normop ‘ 𝑇 ) = ( normop ‘ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ) )
3 2 eleq1d ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( normop ‘ 𝑇 ) ∈ ℝ ↔ ( normop ‘ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ) ∈ ℝ ) )
4 idlnop ⊢ ( I ↾ ℋ ) ∈ LinOp
5 idcnop ⊢ ( I ↾ ℋ ) ∈ ContOp
6 elin ⊢ ( ( I ↾ ℋ ) ∈ ( LinOp ∩ ContOp ) ↔ ( ( I ↾ ℋ ) ∈ LinOp ∧ ( I ↾ ℋ ) ∈ ContOp ) )
7 4 5 6 mpbir2an ⊢ ( I ↾ ℋ ) ∈ ( LinOp ∩ ContOp )
8 7 elimel ⊢ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ∈ ( LinOp ∩ ContOp )
9 elin ⊢ ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ∈ ( LinOp ∩ ContOp ) ↔ ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp ∧ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ∈ ContOp ) )
10 8 9 mpbi ⊢ ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp ∧ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ∈ ContOp )
11 10 simpli ⊢ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp
12 10 simpri ⊢ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ∈ ContOp
13 11 12 nmcopexi ⊢ ( normop ‘ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , ( I ↾ ℋ ) ) ) ∈ ℝ
14 3 13 dedth ⊢ ( 𝑇 ∈ ( LinOp ∩ ContOp ) → ( normop ‘ 𝑇 ) ∈ ℝ )
15 1 14 sylbir ⊢ ( ( 𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ) → ( normop ‘ 𝑇 ) ∈ ℝ )