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 ⊢ F ∈ T NMHom U ∧ G ∈ S NMHom T → F ∘ G ∈ S NMHom U

Proof

Step Hyp Ref Expression
1 nmhmrcl2 ⊢ F ∈ T NMHom U → U ∈ NrmMod
2 nmhmrcl1 ⊢ G ∈ S NMHom T → S ∈ NrmMod
3 1 2 anim12ci ⊢ F ∈ T NMHom U ∧ G ∈ S NMHom T → S ∈ NrmMod ∧ U ∈ NrmMod
4 nmhmlmhm ⊢ F ∈ T NMHom U → F ∈ T LMHom U
5 nmhmlmhm ⊢ G ∈ S NMHom T → G ∈ S LMHom T
6 lmhmco ⊢ F ∈ T LMHom U ∧ G ∈ S LMHom T → F ∘ G ∈ S LMHom U
7 4 5 6 syl2an ⊢ F ∈ T NMHom U ∧ G ∈ S NMHom T → F ∘ G ∈ S LMHom U
8 nmhmnghm ⊢ F ∈ T NMHom U → F ∈ T NGHom U
9 nmhmnghm ⊢ G ∈ S NMHom T → G ∈ S NGHom T
10 nghmco ⊢ F ∈ T NGHom U ∧ G ∈ S NGHom T → F ∘ G ∈ S NGHom U
11 8 9 10 syl2an ⊢ F ∈ T NMHom U ∧ G ∈ S NMHom T → F ∘ G ∈ S NGHom U
12 7 11 jca ⊢ F ∈ T NMHom U ∧ G ∈ S NMHom T → F ∘ G ∈ S LMHom U ∧ F ∘ G ∈ S NGHom U
13 isnmhm ⊢ F ∘ G ∈ S NMHom U ↔ S ∈ NrmMod ∧ U ∈ NrmMod ∧ F ∘ G ∈ S LMHom U ∧ F ∘ G ∈ S NGHom U
14 3 12 13 sylanbrc ⊢ F ∈ T NMHom U ∧ G ∈ S NMHom T → F ∘ G ∈ S NMHom U