nghmco

Description: The composition of normed group homomorphisms is a normed group homomorphism. (Contributed by Mario Carneiro, 20-Oct-2015)

		Ref	Expression
	Assertion	nghmco	$⊢ (F \in (T NGHom U) \land G \in (S NGHom T)) \to F \circ G \in (S NGHom U)$

Step	Hyp	Ref	Expression
1		nghmrcl1	$⊢ G \in (S NGHom T) \to S \in NrmGrp$
2	1	adantl	$⊢ (F \in (T NGHom U) \land G \in (S NGHom T)) \to S \in NrmGrp$
3		nghmrcl2	$⊢ F \in (T NGHom U) \to U \in NrmGrp$
4	3	adantr	$⊢ (F \in (T NGHom U) \land G \in (S NGHom T)) \to U \in NrmGrp$
5		nghmghm	$⊢ F \in (T NGHom U) \to F \in (T GrpHom U)$
6		nghmghm	$⊢ G \in (S NGHom T) \to G \in (S GrpHom T)$
7		ghmco	$⊢ (F \in (T GrpHom U) \land G \in (S GrpHom T)) \to F \circ G \in (S GrpHom U)$
8	5 6 7	syl2an	$⊢ (F \in (T NGHom U) \land G \in (S NGHom T)) \to F \circ G \in (S GrpHom U)$
9		eqid	$⊢ T normOp U = T normOp U$
10	9	nghmcl	$⊢ F \in (T NGHom U) \to (T normOp U) (F) \in ℝ$
11		eqid	$⊢ S normOp T = S normOp T$
12	11	nghmcl	$⊢ G \in (S NGHom T) \to (S normOp T) (G) \in ℝ$
13		remulcl	$⊢ ((T normOp U) (F) \in ℝ \land (S normOp T) (G) \in ℝ) \to (T normOp U) (F) (S normOp T) (G) \in ℝ$
14	10 12 13	syl2an	$⊢ (F \in (T NGHom U) \land G \in (S NGHom T)) \to (T normOp U) (F) (S normOp T) (G) \in ℝ$
15		eqid	$⊢ S normOp U = S normOp U$
16	15 9 11	nmoco	$⊢ (F \in (T NGHom U) \land G \in (S NGHom T)) \to (S normOp U) (F \circ G) \leq (T normOp U) (F) (S normOp T) (G)$
17	15	bddnghm	$⊢ ((S \in NrmGrp \land U \in NrmGrp \land F \circ G \in (S GrpHom U)) \land ((T normOp U) (F) (S normOp T) (G) \in ℝ \land (S normOp U) (F \circ G) \leq (T normOp U) (F) (S normOp T) (G))) \to F \circ G \in (S NGHom U)$
18	2 4 8 14 16 17	syl32anc	$⊢ (F \in (T NGHom U) \land G \in (S NGHom T)) \to F \circ G \in (S NGHom U)$

Metamath Proof Explorer