Theorem nmcfnex

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

	Ref	Expression
Assertion	nmcfnex	⊢ ( ( 𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ) → ( normfn ‘ 𝑇 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) ↔ ( 𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ) )
2		fveq2	⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( normfn ‘ 𝑇 ) = ( normfn ‘ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ) )
3	2	eleq1d	⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ( normfn ‘ 𝑇 ) ∈ ℝ ↔ ( normfn ‘ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ) ∈ ℝ ) )
4		0lnfn	⊢ ( ℋ × { 0 } ) ∈ LinFn
5		0cnfn	⊢ ( ℋ × { 0 } ) ∈ ContFn
6		elin	⊢ ( ( ℋ × { 0 } ) ∈ ( LinFn ∩ ContFn ) ↔ ( ( ℋ × { 0 } ) ∈ LinFn ∧ ( ℋ × { 0 } ) ∈ ContFn ) )
7	4 5 6	mpbir2an	⊢ ( ℋ × { 0 } ) ∈ ( LinFn ∩ ContFn )
8	7	elimel	⊢ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ( LinFn ∩ ContFn )
9		elin	⊢ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ( LinFn ∩ ContFn ) ↔ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn ∧ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ContFn ) )
10	8 9	mpbi	⊢ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn ∧ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ContFn )
11	10	simpli	⊢ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn
12	10	simpri	⊢ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ContFn
13	11 12	nmcfnexi	⊢ ( normfn ‘ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ) ∈ ℝ
14	3 13	dedth	⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( normfn ‘ 𝑇 ) ∈ ℝ )
15	1 14	sylbir	⊢ ( ( 𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ) → ( normfn ‘ 𝑇 ) ∈ ℝ )