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