Metamath Proof Explorer


Theorem nmhmplusg

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

Ref Expression
Hypothesis nmhmplusg.p
|- .+ = ( +g ` T )
Assertion nmhmplusg
|- ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> ( F oF .+ G ) e. ( S NMHom T ) )

Proof

Step Hyp Ref Expression
1 nmhmplusg.p
 |-  .+ = ( +g ` T )
2 nmhmrcl1
 |-  ( F e. ( S NMHom T ) -> S e. NrmMod )
3 nmhmrcl2
 |-  ( G e. ( S NMHom T ) -> T e. NrmMod )
4 2 3 anim12i
 |-  ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> ( S e. NrmMod /\ T e. NrmMod ) )
5 nmhmlmhm
 |-  ( F e. ( S NMHom T ) -> F e. ( S LMHom T ) )
6 nmhmlmhm
 |-  ( G e. ( S NMHom T ) -> G e. ( S LMHom T ) )
7 1 lmhmplusg
 |-  ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) -> ( F oF .+ G ) e. ( S LMHom T ) )
8 5 6 7 syl2an
 |-  ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> ( F oF .+ G ) e. ( S LMHom T ) )
9 nlmlmod
 |-  ( T e. NrmMod -> T e. LMod )
10 lmodabl
 |-  ( T e. LMod -> T e. Abel )
11 3 9 10 3syl
 |-  ( G e. ( S NMHom T ) -> T e. Abel )
12 11 adantl
 |-  ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> T e. Abel )
13 nmhmnghm
 |-  ( F e. ( S NMHom T ) -> F e. ( S NGHom T ) )
14 13 adantr
 |-  ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> F e. ( S NGHom T ) )
15 nmhmnghm
 |-  ( G e. ( S NMHom T ) -> G e. ( S NGHom T ) )
16 15 adantl
 |-  ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> G e. ( S NGHom T ) )
17 1 nghmplusg
 |-  ( ( T e. Abel /\ F e. ( S NGHom T ) /\ G e. ( S NGHom T ) ) -> ( F oF .+ G ) e. ( S NGHom T ) )
18 12 14 16 17 syl3anc
 |-  ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> ( F oF .+ G ) e. ( S NGHom T ) )
19 8 18 jca
 |-  ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> ( ( F oF .+ G ) e. ( S LMHom T ) /\ ( F oF .+ G ) e. ( S NGHom T ) ) )
20 isnmhm
 |-  ( ( F oF .+ G ) e. ( S NMHom T ) <-> ( ( S e. NrmMod /\ T e. NrmMod ) /\ ( ( F oF .+ G ) e. ( S LMHom T ) /\ ( F oF .+ G ) e. ( S NGHom T ) ) ) )
21 4 19 20 sylanbrc
 |-  ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> ( F oF .+ G ) e. ( S NMHom T ) )