This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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