Theorem nghmco

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

	Ref	Expression
Assertion	nghmco	⊢ ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 NGHom 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		nghmrcl1	⊢ ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑆 ∈ NrmGrp )
2	1	adantl	⊢ ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → 𝑆 ∈ NrmGrp )
3		nghmrcl2	⊢ ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) → 𝑈 ∈ NrmGrp )
4	3	adantr	⊢ ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → 𝑈 ∈ NrmGrp )
5		nghmghm	⊢ ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) → 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) )
6		nghmghm	⊢ ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) )
7		ghmco	⊢ ( ( 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GrpHom 𝑈 ) )
8	5 6 7	syl2an	⊢ ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GrpHom 𝑈 ) )
9		eqid	⊢ ( 𝑇 normOp 𝑈 ) = ( 𝑇 normOp 𝑈 )
10	9	nghmcl	⊢ ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) → ( ( 𝑇 normOp 𝑈 ) ‘ 𝐹 ) ∈ ℝ )
11		eqid	⊢ ( 𝑆 normOp 𝑇 ) = ( 𝑆 normOp 𝑇 )
12	11	nghmcl	⊢ ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) → ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ∈ ℝ )
13		remulcl	⊢ ( ( ( ( 𝑇 normOp 𝑈 ) ‘ 𝐹 ) ∈ ℝ ∧ ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ∈ ℝ ) → ( ( ( 𝑇 normOp 𝑈 ) ‘ 𝐹 ) · ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ) ∈ ℝ )
14	10 12 13	syl2an	⊢ ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( ( ( 𝑇 normOp 𝑈 ) ‘ 𝐹 ) · ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ) ∈ ℝ )
15		eqid	⊢ ( 𝑆 normOp 𝑈 ) = ( 𝑆 normOp 𝑈 )
16	15 9 11	nmoco	⊢ ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( ( 𝑆 normOp 𝑈 ) ‘ ( 𝐹 ∘ 𝐺 ) ) ≤ ( ( ( 𝑇 normOp 𝑈 ) ‘ 𝐹 ) · ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ) )
17	15	bddnghm	⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑈 ∈ NrmGrp ∧ ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GrpHom 𝑈 ) ) ∧ ( ( ( ( 𝑇 normOp 𝑈 ) ‘ 𝐹 ) · ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ) ∈ ℝ ∧ ( ( 𝑆 normOp 𝑈 ) ‘ ( 𝐹 ∘ 𝐺 ) ) ≤ ( ( ( 𝑇 normOp 𝑈 ) ‘ 𝐹 ) · ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ) ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 NGHom 𝑈 ) )
18	2 4 8 14 16 17	syl32anc	⊢ ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 NGHom 𝑈 ) )