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 ‘ 𝑇 )
Assertion nmhmplusg ( ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NMHom 𝑇 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑆 NMHom 𝑇 ) )

Proof

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