Metamath Proof Explorer

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 ⊢ F ∈ T NGHom U ∧ G ∈ S NGHom T → F ∘ G ∈ S NGHom U

Proof

Step Hyp Ref Expression
1 nghmrcl1 ⊢ G ∈ S NGHom T → S ∈ NrmGrp
2 1 adantl ⊢ F ∈ T NGHom U ∧ G ∈ S NGHom T → S ∈ NrmGrp
3 nghmrcl2 ⊢ F ∈ T NGHom U → U ∈ NrmGrp
4 3 adantr ⊢ F ∈ T NGHom U ∧ G ∈ S NGHom T → U ∈ NrmGrp
5 nghmghm ⊢ F ∈ T NGHom U → F ∈ T GrpHom U
6 nghmghm ⊢ G ∈ S NGHom T → G ∈ S GrpHom T
7 ghmco ⊢ F ∈ T GrpHom U ∧ G ∈ S GrpHom T → F ∘ G ∈ S GrpHom U
8 5 6 7 syl2an ⊢ F ∈ T NGHom U ∧ G ∈ S NGHom T → F ∘ G ∈ S GrpHom U
9 eqid ⊢ T normOp U = T normOp U
10 9 nghmcl ⊢ F ∈ T NGHom U → T normOp U ⁡ F ∈ ℝ
11 eqid ⊢ S normOp T = S normOp T
12 11 nghmcl ⊢ G ∈ S NGHom T → S normOp T ⁡ G ∈ ℝ
13 remulcl ⊢ T normOp U ⁡ F ∈ ℝ ∧ S normOp T ⁡ G ∈ ℝ → T normOp U ⁡ F ⁢ S normOp T ⁡ G ∈ ℝ
14 10 12 13 syl2an ⊢ F ∈ T NGHom U ∧ G ∈ S NGHom T → T normOp U ⁡ F ⁢ S normOp T ⁡ G ∈ ℝ
15 eqid ⊢ S normOp U = S normOp U
16 15 9 11 nmoco ⊢ F ∈ T NGHom U ∧ G ∈ S NGHom T → S normOp U ⁡ F ∘ G ≤ T normOp U ⁡ F ⁢ S normOp T ⁡ G
17 15 bddnghm ⊢ S ∈ NrmGrp ∧ U ∈ NrmGrp ∧ F ∘ G ∈ S GrpHom U ∧ T normOp U ⁡ F ⁢ S normOp T ⁡ G ∈ ℝ ∧ S normOp U ⁡ F ∘ G ≤ T normOp U ⁡ F ⁢ S normOp T ⁡ G → F ∘ G ∈ S NGHom U
18 2 4 8 14 16 17 syl32anc ⊢ F ∈ T NGHom U ∧ G ∈ S NGHom T → F ∘ G ∈ S NGHom U