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 𝑈 ) )