Theorem pjbdlni

Description: A projector is a bounded linear operator. (Contributed by NM, 3-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjhmop.1	⊢ 𝐻 ∈ Cℋ
Assertion	pjbdlni	⊢ ( projℎ ‘ 𝐻 ) ∈ BndLinOp

Proof

Step	Hyp	Ref	Expression
1		pjhmop.1	⊢ 𝐻 ∈ Cℋ
2	1	pjlnopi	⊢ ( projℎ ‘ 𝐻 ) ∈ LinOp
3		2fveq3	⊢ ( 𝐻 = 0ℋ → ( normop ‘ ( projℎ ‘ 𝐻 ) ) = ( normop ‘ ( projℎ ‘ 0ℋ ) ) )
4	3	eleq1d	⊢ ( 𝐻 = 0ℋ → ( ( normop ‘ ( projℎ ‘ 𝐻 ) ) ∈ ℝ ↔ ( normop ‘ ( projℎ ‘ 0ℋ ) ) ∈ ℝ ) )
5	1	pjnmopi	⊢ ( 𝐻 ≠ 0ℋ → ( normop ‘ ( projℎ ‘ 𝐻 ) ) = 1 )
6		1re	⊢ 1 ∈ ℝ
7	5 6	eqeltrdi	⊢ ( 𝐻 ≠ 0ℋ → ( normop ‘ ( projℎ ‘ 𝐻 ) ) ∈ ℝ )
8	7	adantl	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐻 ≠ 0ℋ ) → ( normop ‘ ( projℎ ‘ 𝐻 ) ) ∈ ℝ )
9		df-h0op	⊢ 0hop = ( projℎ ‘ 0ℋ )
10	9	fveq2i	⊢ ( normop ‘ 0hop ) = ( normop ‘ ( projℎ ‘ 0ℋ ) )
11		nmop0	⊢ ( normop ‘ 0hop ) = 0
12	10 11	eqtr3i	⊢ ( normop ‘ ( projℎ ‘ 0ℋ ) ) = 0
13		0re	⊢ 0 ∈ ℝ
14	12 13	eqeltri	⊢ ( normop ‘ ( projℎ ‘ 0ℋ ) ) ∈ ℝ
15	14	a1i	⊢ ( 𝐻 ∈ Cℋ → ( normop ‘ ( projℎ ‘ 0ℋ ) ) ∈ ℝ )
16	4 8 15	pm2.61ne	⊢ ( 𝐻 ∈ Cℋ → ( normop ‘ ( projℎ ‘ 𝐻 ) ) ∈ ℝ )
17	1 16	ax-mp	⊢ ( normop ‘ ( projℎ ‘ 𝐻 ) ) ∈ ℝ
18		elbdop2	⊢ ( ( projℎ ‘ 𝐻 ) ∈ BndLinOp ↔ ( ( projℎ ‘ 𝐻 ) ∈ LinOp ∧ ( normop ‘ ( projℎ ‘ 𝐻 ) ) ∈ ℝ ) )
19	2 17 18	mpbir2an	⊢ ( projℎ ‘ 𝐻 ) ∈ BndLinOp