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	$⊢ \underset{˙}{+} = +_{T}$
	Assertion	nghmplusg	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to F {\underset{˙}{+}}_{f} G \in (S NGHom T)$

Proof

Step	Hyp	Ref	Expression
1		nghmplusg.p	$⊢ \underset{˙}{+} = +_{T}$
2		nghmrcl1	$⊢ F \in (S NGHom T) \to S \in NrmGrp$
3	2	3ad2ant2	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to S \in NrmGrp$
4		nghmrcl2	$⊢ F \in (S NGHom T) \to T \in NrmGrp$
5	4	3ad2ant2	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to T \in NrmGrp$
6		id	$⊢ T \in Abel \to T \in Abel$
7		nghmghm	$⊢ F \in (S NGHom T) \to F \in (S GrpHom T)$
8		nghmghm	$⊢ G \in (S NGHom T) \to G \in (S GrpHom T)$
9	1	ghmplusg	$⊢ (T \in Abel \land F \in (S GrpHom T) \land G \in (S GrpHom T)) \to F {\underset{˙}{+}}_{f} G \in (S GrpHom T)$
10	6 7 8 9	syl3an	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to F {\underset{˙}{+}}_{f} G \in (S GrpHom T)$
11		eqid	$⊢ S normOp T = S normOp T$
12	11	nghmcl	$⊢ F \in (S NGHom T) \to (S normOp T) (F) \in ℝ$
13	12	3ad2ant2	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to (S normOp T) (F) \in ℝ$
14	11	nghmcl	$⊢ G \in (S NGHom T) \to (S normOp T) (G) \in ℝ$
15	14	3ad2ant3	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to (S normOp T) (G) \in ℝ$
16	13 15	readdcld	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to (S normOp T) (F) + (S normOp T) (G) \in ℝ$
17	11 1	nmotri	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to (S normOp T) (F {\underset{˙}{+}}_{f} G) \leq (S normOp T) (F) + (S normOp T) (G)$
18	11	bddnghm	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F {\underset{˙}{+}}_{f} G \in (S GrpHom T)) \land ((S normOp T) (F) + (S normOp T) (G) \in ℝ \land (S normOp T) (F {\underset{˙}{+}}_{f} G) \leq (S normOp T) (F) + (S normOp T) (G))) \to F {\underset{˙}{+}}_{f} G \in (S NGHom T)$
19	3 5 10 16 17 18	syl32anc	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to F {\underset{˙}{+}}_{f} G \in (S NGHom T)$