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

Metamath Proof Explorer

Theorem nghmplusg

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

Ref Expression
Hypothesis nghmplusg.p ⊢ + = ( +g ‘ 𝑇 )
Assertion nghmplusg ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑆 NGHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 nghmplusg.p ⊢ + = ( +g ‘ 𝑇 )
2 nghmrcl1 ⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑆 ∈ NrmGrp )
3 2 3ad2ant2 ⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → 𝑆 ∈ NrmGrp )
4 nghmrcl2 ⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑇 ∈ NrmGrp )
5 4 3ad2ant2 ⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → 𝑇 ∈ NrmGrp )
6 id ⊢ ( 𝑇 ∈ Abel → 𝑇 ∈ Abel )
7 nghmghm ⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
8 nghmghm ⊢ ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) )
9 1 ghmplusg ⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑆 GrpHom 𝑇 ) )
10 6 7 8 9 syl3an ⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑆 GrpHom 𝑇 ) )
11 eqid ⊢ ( 𝑆 normOp 𝑇 ) = ( 𝑆 normOp 𝑇 )
12 11 nghmcl ⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) ∈ ℝ )
13 12 3ad2ant2 ⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) ∈ ℝ )
14 11 nghmcl ⊢ ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) → ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ∈ ℝ )
15 14 3ad2ant3 ⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ∈ ℝ )
16 13 15 readdcld ⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ) ∈ ℝ )
17 11 1 nmotri ⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( ( 𝑆 normOp 𝑇 ) ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ) )
18 11 bddnghm ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ) ∈ ℝ ∧ ( ( 𝑆 normOp 𝑇 ) ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ) ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑆 NGHom 𝑇 ) )
19 3 5 10 16 17 18 syl32anc ⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑆 NGHom 𝑇 ) )