This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐹 ∈ ( 𝑇 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 𝑈 ) )