This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )