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 𝑇 ) ) → ( 𝑁 ‘ ( 𝐹𝐺 ) ) ≤ ( ( 𝐿𝐹 ) · ( 𝑀𝐺 ) ) )