Metamath Proof Explorer

Theorem nmoi

Description: The operator norm achieves the minimum of the set of upper bounds, if the operator is bounded. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Hypotheses nmofval.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
nmoi.2 ⊢ 𝑉 = ( Base ‘ 𝑆 )
nmoi.3 ⊢ 𝐿 = ( norm ‘ 𝑆 )
nmoi.4 ⊢ 𝑀 = ( norm ‘ 𝑇 )
Assertion nmoi ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( 𝐿 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2 nmoi.2 ⊢ 𝑉 = ( Base ‘ 𝑆 )
3 nmoi.3 ⊢ 𝐿 = ( norm ‘ 𝑆 )
4 nmoi.4 ⊢ 𝑀 = ( norm ‘ 𝑇 )
5 2fveq3 ⊢ ( 𝑋 = ( 0g ‘ 𝑆 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) )
6 fveq2 ⊢ ( 𝑋 = ( 0g ‘ 𝑆 ) → ( 𝐿 ‘ 𝑋 ) = ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) )
7 6 oveq2d ⊢ ( 𝑋 = ( 0g ‘ 𝑆 ) → ( ( 𝑁 ‘ 𝐹 ) · ( 𝐿 ‘ 𝑋 ) ) = ( ( 𝑁 ‘ 𝐹 ) · ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) ) )
8 5 7 breq12d ⊢ ( 𝑋 = ( 0g ‘ 𝑆 ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( 𝐿 ‘ 𝑋 ) ) ↔ ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) ) ) )
9 2fveq3 ⊢ ( 𝑥 = 𝑋 → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) )
10 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐿 ‘ 𝑥 ) = ( 𝐿 ‘ 𝑋 ) )
11 10 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) = ( 𝑟 · ( 𝐿 ‘ 𝑋 ) ) )
12 9 11 breq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) ↔ ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑋 ) ) ) )
13 12 rspcv ⊢ ( 𝑋 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑋 ) ) ) )
14 13 ad3antlr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑋 ) ) ) )
15 1 isnghm ⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ↔ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) ) )
16 15 simplbi ⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) )
17 16 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) )
18 17 simprd ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → 𝑇 ∈ NrmGrp )
19 15 simprbi ⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) )
20 19 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) )
21 20 simpld ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
22 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
23 2 22 ghmf ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
24 21 23 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
25 ffvelcdm ⊢ ( ( 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝑇 ) )
26 24 25 sylancom ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝑇 ) )
27 22 4 nmcl ⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝑇 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ )
28 18 26 27 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ )
29 28 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ )
30 29 adantr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ )
31 elrege0 ⊢ ( 𝑟 ∈ ( 0 [,) +∞ ) ↔ ( 𝑟 ∈ ℝ ∧ 0 ≤ 𝑟 ) )
32 31 simplbi ⊢ ( 𝑟 ∈ ( 0 [,) +∞ ) → 𝑟 ∈ ℝ )
33 32 adantl ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) → 𝑟 ∈ ℝ )
34 17 simpld ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → 𝑆 ∈ NrmGrp )
35 simpr ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
36 34 35 jca ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑆 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉 ) )
37 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
38 2 3 37 nmrpcl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( 𝐿 ‘ 𝑋 ) ∈ ℝ+ )
39 38 3expa ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( 𝐿 ‘ 𝑋 ) ∈ ℝ+ )
40 36 39 sylan ⊢ ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( 𝐿 ‘ 𝑋 ) ∈ ℝ+ )
41 40 rpregt0d ⊢ ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( ( 𝐿 ‘ 𝑋 ) ∈ ℝ ∧ 0 < ( 𝐿 ‘ 𝑋 ) ) )
42 41 adantr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) → ( ( 𝐿 ‘ 𝑋 ) ∈ ℝ ∧ 0 < ( 𝐿 ‘ 𝑋 ) ) )
43 ledivmul2 ⊢ ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ ∧ 𝑟 ∈ ℝ ∧ ( ( 𝐿 ‘ 𝑋 ) ∈ ℝ ∧ 0 < ( 𝐿 ‘ 𝑋 ) ) ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) ≤ 𝑟 ↔ ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑋 ) ) ) )
44 30 33 42 43 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) ≤ 𝑟 ↔ ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑋 ) ) ) )
45 14 44 sylibrd ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) ≤ 𝑟 ) )
46 45 ralrimiva ⊢ ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) ≤ 𝑟 ) )
47 34 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → 𝑆 ∈ NrmGrp )
48 18 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → 𝑇 ∈ NrmGrp )
49 21 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
50 29 40 rerpdivcld ⊢ ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) ∈ ℝ )
51 50 rexrd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) ∈ ℝ* )
52 1 2 3 4 nmogelb ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) ∈ ℝ* ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) ≤ ( 𝑁 ‘ 𝐹 ) ↔ ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) ≤ 𝑟 ) ) )
53 47 48 49 51 52 syl31anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) ≤ ( 𝑁 ‘ 𝐹 ) ↔ ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) ≤ 𝑟 ) ) )
54 46 53 mpbird ⊢ ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) ≤ ( 𝑁 ‘ 𝐹 ) )
55 20 simprd ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ )
56 55 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ )
57 29 56 40 ledivmul2d ⊢ ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) ≤ ( 𝑁 ‘ 𝐹 ) ↔ ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( 𝐿 ‘ 𝑋 ) ) ) )
58 54 57 mpbid ⊢ ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( 𝐿 ‘ 𝑋 ) ) )
59 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
60 37 59 ghmid ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
61 21 60 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
62 61 fveq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) = ( 𝑀 ‘ ( 0g ‘ 𝑇 ) ) )
63 4 59 nm0 ⊢ ( 𝑇 ∈ NrmGrp → ( 𝑀 ‘ ( 0g ‘ 𝑇 ) ) = 0 )
64 18 63 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 0g ‘ 𝑇 ) ) = 0 )
65 62 64 eqtrd ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) = 0 )
66 3 37 nm0 ⊢ ( 𝑆 ∈ NrmGrp → ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) = 0 )
67 34 66 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) = 0 )
68 0re ⊢ 0 ∈ ℝ
69 67 68 eqeltrdi ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) ∈ ℝ )
70 1 nmoge0 ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 0 ≤ ( 𝑁 ‘ 𝐹 ) )
71 34 18 21 70 syl3anc ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → 0 ≤ ( 𝑁 ‘ 𝐹 ) )
72 0le0 ⊢ 0 ≤ 0
73 72 67 breqtrrid ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → 0 ≤ ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) )
74 55 69 71 73 mulge0d ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → 0 ≤ ( ( 𝑁 ‘ 𝐹 ) · ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) ) )
75 65 74 eqbrtrd ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) ) )
76 8 58 75 pm2.61ne ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( 𝐿 ‘ 𝑋 ) ) )