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