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

Metamath Proof Explorer

Theorem nmhmco

Description: The composition of bounded linear operators is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015)

Ref Expression
Assertion nmhmco ( ( 𝐹 ∈ ( 𝑇 NMHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NMHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 NMHom 𝑈 ) )

Proof

Step Hyp Ref Expression
1 nmhmrcl2 ⊢ ( 𝐹 ∈ ( 𝑇 NMHom 𝑈 ) → 𝑈 ∈ NrmMod )
2 nmhmrcl1 ⊢ ( 𝐺 ∈ ( 𝑆 NMHom 𝑇 ) → 𝑆 ∈ NrmMod )
3 1 2 anim12ci ⊢ ( ( 𝐹 ∈ ( 𝑇 NMHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NMHom 𝑇 ) ) → ( 𝑆 ∈ NrmMod ∧ 𝑈 ∈ NrmMod ) )
4 nmhmlmhm ⊢ ( 𝐹 ∈ ( 𝑇 NMHom 𝑈 ) → 𝐹 ∈ ( 𝑇 LMHom 𝑈 ) )
5 nmhmlmhm ⊢ ( 𝐺 ∈ ( 𝑆 NMHom 𝑇 ) → 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) )
6 lmhmco ⊢ ( ( 𝐹 ∈ ( 𝑇 LMHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 LMHom 𝑈 ) )
7 4 5 6 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑇 NMHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NMHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 LMHom 𝑈 ) )
8 nmhmnghm ⊢ ( 𝐹 ∈ ( 𝑇 NMHom 𝑈 ) → 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) )
9 nmhmnghm ⊢ ( 𝐺 ∈ ( 𝑆 NMHom 𝑇 ) → 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) )
10 nghmco ⊢ ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 NGHom 𝑈 ) )
11 8 9 10 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑇 NMHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NMHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 NGHom 𝑈 ) )
12 7 11 jca ⊢ ( ( 𝐹 ∈ ( 𝑇 NMHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NMHom 𝑇 ) ) → ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 LMHom 𝑈 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 NGHom 𝑈 ) ) )
13 isnmhm ⊢ ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 NMHom 𝑈 ) ↔ ( ( 𝑆 ∈ NrmMod ∧ 𝑈 ∈ NrmMod ) ∧ ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 LMHom 𝑈 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 NGHom 𝑈 ) ) ) )
14 3 12 13 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑇 NMHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NMHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 NMHom 𝑈 ) )