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 e. ( T NMHom U ) /\ G e. ( S NMHom T ) ) -> ( F o. G ) e. ( S NMHom U ) )

Proof

Step Hyp Ref Expression
1 nmhmrcl2
 |-  ( F e. ( T NMHom U ) -> U e. NrmMod )
2 nmhmrcl1
 |-  ( G e. ( S NMHom T ) -> S e. NrmMod )
3 1 2 anim12ci
 |-  ( ( F e. ( T NMHom U ) /\ G e. ( S NMHom T ) ) -> ( S e. NrmMod /\ U e. NrmMod ) )
4 nmhmlmhm
 |-  ( F e. ( T NMHom U ) -> F e. ( T LMHom U ) )
5 nmhmlmhm
 |-  ( G e. ( S NMHom T ) -> G e. ( S LMHom T ) )
6 lmhmco
 |-  ( ( F e. ( T LMHom U ) /\ G e. ( S LMHom T ) ) -> ( F o. G ) e. ( S LMHom U ) )
7 4 5 6 syl2an
 |-  ( ( F e. ( T NMHom U ) /\ G e. ( S NMHom T ) ) -> ( F o. G ) e. ( S LMHom U ) )
8 nmhmnghm
 |-  ( F e. ( T NMHom U ) -> F e. ( T NGHom U ) )
9 nmhmnghm
 |-  ( G e. ( S NMHom T ) -> G e. ( S NGHom T ) )
10 nghmco
 |-  ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> ( F o. G ) e. ( S NGHom U ) )
11 8 9 10 syl2an
 |-  ( ( F e. ( T NMHom U ) /\ G e. ( S NMHom T ) ) -> ( F o. G ) e. ( S NGHom U ) )
12 7 11 jca
 |-  ( ( F e. ( T NMHom U ) /\ G e. ( S NMHom T ) ) -> ( ( F o. G ) e. ( S LMHom U ) /\ ( F o. G ) e. ( S NGHom U ) ) )
13 isnmhm
 |-  ( ( F o. G ) e. ( S NMHom U ) <-> ( ( S e. NrmMod /\ U e. NrmMod ) /\ ( ( F o. G ) e. ( S LMHom U ) /\ ( F o. G ) e. ( S NGHom U ) ) ) )
14 3 12 13 sylanbrc
 |-  ( ( F e. ( T NMHom U ) /\ G e. ( S NMHom T ) ) -> ( F o. G ) e. ( S NMHom U ) )