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 ⊢ + ˙ = + T
Assertion nmhmplusg ⊢ F ∈ S NMHom T ∧ G ∈ S NMHom T → F + ˙ f G ∈ S NMHom T

Proof

Step Hyp Ref Expression
1 nmhmplusg.p ⊢ + ˙ = + T
2 nmhmrcl1 ⊢ F ∈ S NMHom T → S ∈ NrmMod
3 nmhmrcl2 ⊢ G ∈ S NMHom T → T ∈ NrmMod
4 2 3 anim12i ⊢ F ∈ S NMHom T ∧ G ∈ S NMHom T → S ∈ NrmMod ∧ T ∈ NrmMod
5 nmhmlmhm ⊢ F ∈ S NMHom T → F ∈ S LMHom T
6 nmhmlmhm ⊢ G ∈ S NMHom T → G ∈ S LMHom T
7 1 lmhmplusg ⊢ F ∈ S LMHom T ∧ G ∈ S LMHom T → F + ˙ f G ∈ S LMHom T
8 5 6 7 syl2an ⊢ F ∈ S NMHom T ∧ G ∈ S NMHom T → F + ˙ f G ∈ S LMHom T
9 nlmlmod ⊢ T ∈ NrmMod → T ∈ LMod
10 lmodabl ⊢ T ∈ LMod → T ∈ Abel
11 3 9 10 3syl ⊢ G ∈ S NMHom T → T ∈ Abel
12 11 adantl ⊢ F ∈ S NMHom T ∧ G ∈ S NMHom T → T ∈ Abel
13 nmhmnghm ⊢ F ∈ S NMHom T → F ∈ S NGHom T
14 13 adantr ⊢ F ∈ S NMHom T ∧ G ∈ S NMHom T → F ∈ S NGHom T
15 nmhmnghm ⊢ G ∈ S NMHom T → G ∈ S NGHom T
16 15 adantl ⊢ F ∈ S NMHom T ∧ G ∈ S NMHom T → G ∈ S NGHom T
17 1 nghmplusg ⊢ T ∈ Abel ∧ F ∈ S NGHom T ∧ G ∈ S NGHom T → F + ˙ f G ∈ S NGHom T
18 12 14 16 17 syl3anc ⊢ F ∈ S NMHom T ∧ G ∈ S NMHom T → F + ˙ f G ∈ S NGHom T
19 8 18 jca ⊢ F ∈ S NMHom T ∧ G ∈ S NMHom T → F + ˙ f G ∈ S LMHom T ∧ F + ˙ f G ∈ S NGHom T
20 isnmhm ⊢ F + ˙ f G ∈ S NMHom T ↔ S ∈ NrmMod ∧ T ∈ NrmMod ∧ F + ˙ f G ∈ S LMHom T ∧ F + ˙ f G ∈ S NGHom T
21 4 19 20 sylanbrc ⊢ F ∈ S NMHom T ∧ G ∈ S NMHom T → F + ˙ f G ∈ S NMHom T