Metamath Proof Explorer

Theorem nmoco

Description: An upper bound on the operator norm of a composition. (Contributed by Mario Carneiro, 20-Oct-2015)

Ref Expression
Hypotheses nmoco.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑈 )
nmoco.2 ⊢ 𝐿 = ( 𝑇 normOp 𝑈 )
nmoco.3 ⊢ 𝑀 = ( 𝑆 normOp 𝑇 )
Assertion nmoco ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝑁 ‘ ( 𝐹 ∘ 𝐺 ) ) ≤ ( ( 𝐿 ‘ 𝐹 ) · ( 𝑀 ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 nmoco.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑈 )
2 nmoco.2 ⊢ 𝐿 = ( 𝑇 normOp 𝑈 )
3 nmoco.3 ⊢ 𝑀 = ( 𝑆 normOp 𝑇 )
4 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
5 eqid ⊢ ( norm ‘ 𝑆 ) = ( norm ‘ 𝑆 )
6 eqid ⊢ ( norm ‘ 𝑈 ) = ( norm ‘ 𝑈 )
7 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
8 nghmrcl1 ⊢ ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑆 ∈ NrmGrp )
9 8 adantl ⊢ ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → 𝑆 ∈ NrmGrp )
10 nghmrcl2 ⊢ ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) → 𝑈 ∈ NrmGrp )
11 10 adantr ⊢ ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → 𝑈 ∈ NrmGrp )
12 nghmghm ⊢ ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) → 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) )
13 nghmghm ⊢ ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) )
14 ghmco ⊢ ( ( 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GrpHom 𝑈 ) )
15 12 13 14 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GrpHom 𝑈 ) )
16 2 nghmcl ⊢ ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) → ( 𝐿 ‘ 𝐹 ) ∈ ℝ )
17 3 nghmcl ⊢ ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) → ( 𝑀 ‘ 𝐺 ) ∈ ℝ )
18 remulcl ⊢ ( ( ( 𝐿 ‘ 𝐹 ) ∈ ℝ ∧ ( 𝑀 ‘ 𝐺 ) ∈ ℝ ) → ( ( 𝐿 ‘ 𝐹 ) · ( 𝑀 ‘ 𝐺 ) ) ∈ ℝ )
19 16 17 18 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( ( 𝐿 ‘ 𝐹 ) · ( 𝑀 ‘ 𝐺 ) ) ∈ ℝ )
20 nghmrcl1 ⊢ ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) → 𝑇 ∈ NrmGrp )
21 2 nmoge0 ⊢ ( ( 𝑇 ∈ NrmGrp ∧ 𝑈 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) ) → 0 ≤ ( 𝐿 ‘ 𝐹 ) )
22 20 10 12 21 syl3anc ⊢ ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) → 0 ≤ ( 𝐿 ‘ 𝐹 ) )
23 16 22 jca ⊢ ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) → ( ( 𝐿 ‘ 𝐹 ) ∈ ℝ ∧ 0 ≤ ( 𝐿 ‘ 𝐹 ) ) )
24 nghmrcl2 ⊢ ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑇 ∈ NrmGrp )
25 3 nmoge0 ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 0 ≤ ( 𝑀 ‘ 𝐺 ) )
26 8 24 13 25 syl3anc ⊢ ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) → 0 ≤ ( 𝑀 ‘ 𝐺 ) )
27 17 26 jca ⊢ ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) → ( ( 𝑀 ‘ 𝐺 ) ∈ ℝ ∧ 0 ≤ ( 𝑀 ‘ 𝐺 ) ) )
28 mulge0 ⊢ ( ( ( ( 𝐿 ‘ 𝐹 ) ∈ ℝ ∧ 0 ≤ ( 𝐿 ‘ 𝐹 ) ) ∧ ( ( 𝑀 ‘ 𝐺 ) ∈ ℝ ∧ 0 ≤ ( 𝑀 ‘ 𝐺 ) ) ) → 0 ≤ ( ( 𝐿 ‘ 𝐹 ) · ( 𝑀 ‘ 𝐺 ) ) )
29 23 27 28 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → 0 ≤ ( ( 𝐿 ‘ 𝐹 ) · ( 𝑀 ‘ 𝐺 ) ) )
30 10 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝑈 ∈ NrmGrp )
31 12 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) )
32 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
33 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
34 32 33 ghmf ⊢ ( 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) → 𝐹 : ( Base ‘ 𝑇 ) ⟶ ( Base ‘ 𝑈 ) )
35 31 34 syl ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝐹 : ( Base ‘ 𝑇 ) ⟶ ( Base ‘ 𝑈 ) )
36 13 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) )
37 4 32 ghmf ⊢ ( 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
38 36 37 syl ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
39 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
40 38 39 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) )
41 35 40 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑈 ) )
42 33 6 nmcl ⊢ ( ( 𝑈 ∈ NrmGrp ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑈 ) ) → ( ( norm ‘ 𝑈 ) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℝ )
43 30 41 42 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑈 ) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℝ )
44 16 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝐿 ‘ 𝐹 ) ∈ ℝ )
45 20 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝑇 ∈ NrmGrp )
46 eqid ⊢ ( norm ‘ 𝑇 ) = ( norm ‘ 𝑇 )
47 32 46 nmcl ⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ )
48 45 40 47 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ )
49 44 48 remulcld ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝐿 ‘ 𝐹 ) · ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℝ )
50 17 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑀 ‘ 𝐺 ) ∈ ℝ )
51 4 5 nmcl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℝ )
52 8 51 sylan ⊢ ( ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℝ )
53 52 ad2ant2lr ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℝ )
54 50 53 remulcld ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝑀 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ∈ ℝ )
55 44 54 remulcld ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝐿 ‘ 𝐹 ) · ( ( 𝑀 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ) ∈ ℝ )
56 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) )
57 2 32 46 6 nmoi ⊢ ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) ) → ( ( norm ‘ 𝑈 ) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( ( 𝐿 ‘ 𝐹 ) · ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
58 56 40 57 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑈 ) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( ( 𝐿 ‘ 𝐹 ) · ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
59 23 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝐿 ‘ 𝐹 ) ∈ ℝ ∧ 0 ≤ ( 𝐿 ‘ 𝐹 ) ) )
60 3 4 5 46 nmoi ⊢ ( ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ ( ( 𝑀 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
61 60 ad2ant2lr ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ ( ( 𝑀 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
62 lemul2a ⊢ ( ( ( ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ ∧ ( ( 𝑀 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ∈ ℝ ∧ ( ( 𝐿 ‘ 𝐹 ) ∈ ℝ ∧ 0 ≤ ( 𝐿 ‘ 𝐹 ) ) ) ∧ ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ ( ( 𝑀 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ) → ( ( 𝐿 ‘ 𝐹 ) · ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( ( 𝐿 ‘ 𝐹 ) · ( ( 𝑀 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ) )
63 48 54 59 61 62 syl31anc ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝐿 ‘ 𝐹 ) · ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( ( 𝐿 ‘ 𝐹 ) · ( ( 𝑀 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ) )
64 43 49 55 58 63 letrd ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑈 ) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( ( 𝐿 ‘ 𝐹 ) · ( ( 𝑀 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ) )
65 fvco3 ⊢ ( ( 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) )
66 38 39 65 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) )
67 66 fveq2d ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑈 ) ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ) = ( ( norm ‘ 𝑈 ) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
68 44 recnd ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝐿 ‘ 𝐹 ) ∈ ℂ )
69 50 recnd ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑀 ‘ 𝐺 ) ∈ ℂ )
70 53 recnd ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℂ )
71 68 69 70 mulassd ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( ( 𝐿 ‘ 𝐹 ) · ( 𝑀 ‘ 𝐺 ) ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) = ( ( 𝐿 ‘ 𝐹 ) · ( ( 𝑀 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ) )
72 64 67 71 3brtr4d ⊢ ( ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑈 ) ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( ( ( 𝐿 ‘ 𝐹 ) · ( 𝑀 ‘ 𝐺 ) ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
73 1 4 5 6 7 9 11 15 19 29 72 nmolb2d ⊢ ( ( 𝐹 ∈ ( 𝑇 NGHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝑁 ‘ ( 𝐹 ∘ 𝐺 ) ) ≤ ( ( 𝐿 ‘ 𝐹 ) · ( 𝑀 ‘ 𝐺 ) ) )