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

Proof

Step Hyp Ref Expression
1 nghmplusg.p ⊢ + ˙ = + T
2 nghmrcl1 ⊢ F ∈ S NGHom T → S ∈ NrmGrp
3 2 3ad2ant2 ⊢ T ∈ Abel ∧ F ∈ S NGHom T ∧ G ∈ S NGHom T → S ∈ NrmGrp
4 nghmrcl2 ⊢ F ∈ S NGHom T → T ∈ NrmGrp
5 4 3ad2ant2 ⊢ T ∈ Abel ∧ F ∈ S NGHom T ∧ G ∈ S NGHom T → T ∈ NrmGrp
6 id ⊢ T ∈ Abel → T ∈ Abel
7 nghmghm ⊢ F ∈ S NGHom T → F ∈ S GrpHom T
8 nghmghm ⊢ G ∈ S NGHom T → G ∈ S GrpHom T
9 1 ghmplusg ⊢ T ∈ Abel ∧ F ∈ S GrpHom T ∧ G ∈ S GrpHom T → F + ˙ f G ∈ S GrpHom T
10 6 7 8 9 syl3an ⊢ T ∈ Abel ∧ F ∈ S NGHom T ∧ G ∈ S NGHom T → F + ˙ f G ∈ S GrpHom T
11 eqid ⊢ S normOp T = S normOp T
12 11 nghmcl ⊢ F ∈ S NGHom T → S normOp T ⁡ F ∈ ℝ
13 12 3ad2ant2 ⊢ T ∈ Abel ∧ F ∈ S NGHom T ∧ G ∈ S NGHom T → S normOp T ⁡ F ∈ ℝ
14 11 nghmcl ⊢ G ∈ S NGHom T → S normOp T ⁡ G ∈ ℝ
15 14 3ad2ant3 ⊢ T ∈ Abel ∧ F ∈ S NGHom T ∧ G ∈ S NGHom T → S normOp T ⁡ G ∈ ℝ
16 13 15 readdcld ⊢ T ∈ Abel ∧ F ∈ S NGHom T ∧ G ∈ S NGHom T → S normOp T ⁡ F + S normOp T ⁡ G ∈ ℝ
17 11 1 nmotri ⊢ T ∈ Abel ∧ F ∈ S NGHom T ∧ G ∈ S NGHom T → S normOp T ⁡ F + ˙ f G ≤ S normOp T ⁡ F + S normOp T ⁡ G
18 11 bddnghm ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ F + ˙ f G ∈ S GrpHom T ∧ S normOp T ⁡ F + S normOp T ⁡ G ∈ ℝ ∧ S normOp T ⁡ F + ˙ f G ≤ S normOp T ⁡ F + S normOp T ⁡ G → F + ˙ f G ∈ S NGHom T
19 3 5 10 16 17 18 syl32anc ⊢ T ∈ Abel ∧ F ∈ S NGHom T ∧ G ∈ S NGHom T → F + ˙ f G ∈ S NGHom T