Theorem lnopco0i

Description: The composition of a linear operator with one whose norm is zero. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lnopco.1	⊢ 𝑆 ∈ LinOp
	lnopco.2	⊢ 𝑇 ∈ LinOp
Assertion	lnopco0i	⊢ ( ( normop ‘ 𝑇 ) = 0 → ( normop ‘ ( 𝑆 ∘ 𝑇 ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		lnopco.1	⊢ 𝑆 ∈ LinOp
2		lnopco.2	⊢ 𝑇 ∈ LinOp
3		coeq2	⊢ ( 𝑇 = 0hop → ( 𝑆 ∘ 𝑇 ) = ( 𝑆 ∘ 0hop ) )
4		0lnop	⊢ 0hop ∈ LinOp
5	1 4	lnopcoi	⊢ ( 𝑆 ∘ 0hop ) ∈ LinOp
6	5	lnopfi	⊢ ( 𝑆 ∘ 0hop ) : ℋ ⟶ ℋ
7		ffn	⊢ ( ( 𝑆 ∘ 0hop ) : ℋ ⟶ ℋ → ( 𝑆 ∘ 0hop ) Fn ℋ )
8	6 7	ax-mp	⊢ ( 𝑆 ∘ 0hop ) Fn ℋ
9		ho0f	⊢ 0hop : ℋ ⟶ ℋ
10		ffn	⊢ ( 0hop : ℋ ⟶ ℋ → 0hop Fn ℋ )
11	9 10	ax-mp	⊢ 0hop Fn ℋ
12		eqfnfv	⊢ ( ( ( 𝑆 ∘ 0hop ) Fn ℋ ∧ 0hop Fn ℋ ) → ( ( 𝑆 ∘ 0hop ) = 0hop ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑆 ∘ 0hop ) ‘ 𝑥 ) = ( 0hop ‘ 𝑥 ) ) )
13	8 11 12	mp2an	⊢ ( ( 𝑆 ∘ 0hop ) = 0hop ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑆 ∘ 0hop ) ‘ 𝑥 ) = ( 0hop ‘ 𝑥 ) )
14		ho0val	⊢ ( 𝑥 ∈ ℋ → ( 0hop ‘ 𝑥 ) = 0ℎ )
15	14	fveq2d	⊢ ( 𝑥 ∈ ℋ → ( 𝑆 ‘ ( 0hop ‘ 𝑥 ) ) = ( 𝑆 ‘ 0ℎ ) )
16	1	lnop0i	⊢ ( 𝑆 ‘ 0ℎ ) = 0ℎ
17	15 16	eqtrdi	⊢ ( 𝑥 ∈ ℋ → ( 𝑆 ‘ ( 0hop ‘ 𝑥 ) ) = 0ℎ )
18	1	lnopfi	⊢ 𝑆 : ℋ ⟶ ℋ
19	18 9	hocoi	⊢ ( 𝑥 ∈ ℋ → ( ( 𝑆 ∘ 0hop ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 0hop ‘ 𝑥 ) ) )
20	17 19 14	3eqtr4d	⊢ ( 𝑥 ∈ ℋ → ( ( 𝑆 ∘ 0hop ) ‘ 𝑥 ) = ( 0hop ‘ 𝑥 ) )
21	13 20	mprgbir	⊢ ( 𝑆 ∘ 0hop ) = 0hop
22	3 21	eqtrdi	⊢ ( 𝑇 = 0hop → ( 𝑆 ∘ 𝑇 ) = 0hop )
23	2	nmlnop0iHIL	⊢ ( ( normop ‘ 𝑇 ) = 0 ↔ 𝑇 = 0hop )
24	1 2	lnopcoi	⊢ ( 𝑆 ∘ 𝑇 ) ∈ LinOp
25	24	nmlnop0iHIL	⊢ ( ( normop ‘ ( 𝑆 ∘ 𝑇 ) ) = 0 ↔ ( 𝑆 ∘ 𝑇 ) = 0hop )
26	22 23 25	3imtr4i	⊢ ( ( normop ‘ 𝑇 ) = 0 → ( normop ‘ ( 𝑆 ∘ 𝑇 ) ) = 0 )