Metamath Proof Explorer

Theorem nmoix

Description: The operator norm is a bound on the size of an operator, even when it is infinite (using extended real multiplication). (Contributed by Mario Carneiro, 18-Oct-2015)

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

Proof

Step Hyp Ref Expression
1 nmofval.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2 nmoi.2 ⊢ 𝑉 = ( Base ‘ 𝑆 )
3 nmoi.3 ⊢ 𝐿 = ( norm ‘ 𝑆 )
4 nmoi.4 ⊢ 𝑀 = ( norm ‘ 𝑇 )
5 1 isnghm2 ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ↔ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) )
6 5 biimpar ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) → 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) )
7 1 2 3 4 nmoi ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( 𝐿 ‘ 𝑋 ) ) )
8 6 7 sylan ⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( 𝐿 ‘ 𝑋 ) ) )
9 8 an32s ⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( 𝐿 ‘ 𝑋 ) ) )
10 id ⊢ ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ → ( 𝑁 ‘ 𝐹 ) ∈ ℝ )
11 2 3 nmcl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉 ) → ( 𝐿 ‘ 𝑋 ) ∈ ℝ )
12 11 3ad2antl1 ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐿 ‘ 𝑋 ) ∈ ℝ )
13 rexmul ⊢ ( ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ ∧ ( 𝐿 ‘ 𝑋 ) ∈ ℝ ) → ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑋 ) ) = ( ( 𝑁 ‘ 𝐹 ) · ( 𝐿 ‘ 𝑋 ) ) )
14 10 12 13 syl2anr ⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) → ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑋 ) ) = ( ( 𝑁 ‘ 𝐹 ) · ( 𝐿 ‘ 𝑋 ) ) )
15 9 14 breqtrrd ⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑋 ) ) )
16 fveq2 ⊢ ( 𝑋 = ( 0g ‘ 𝑆 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) )
17 16 fveq2d ⊢ ( 𝑋 = ( 0g ‘ 𝑆 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) )
18 fveq2 ⊢ ( 𝑋 = ( 0g ‘ 𝑆 ) → ( 𝐿 ‘ 𝑋 ) = ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) )
19 18 oveq2d ⊢ ( 𝑋 = ( 0g ‘ 𝑆 ) → ( +∞ ·e ( 𝐿 ‘ 𝑋 ) ) = ( +∞ ·e ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) ) )
20 17 19 breq12d ⊢ ( 𝑋 = ( 0g ‘ 𝑆 ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( +∞ ·e ( 𝐿 ‘ 𝑋 ) ) ↔ ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) ≤ ( +∞ ·e ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) ) ) )
21 simpl2 ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → 𝑇 ∈ NrmGrp )
22 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
23 2 22 ghmf ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
24 23 ffvelcdmda ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝑇 ) )
25 24 3ad2antl3 ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝑇 ) )
26 22 4 nmcl ⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝑇 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ )
27 21 25 26 syl2anc ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ )
28 27 adantr ⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ )
29 28 rexrd ⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ* )
30 pnfge ⊢ ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ* → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ +∞ )
31 29 30 syl ⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ +∞ )
32 simp1 ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 𝑆 ∈ NrmGrp )
33 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
34 2 3 33 nmrpcl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( 𝐿 ‘ 𝑋 ) ∈ ℝ+ )
35 34 3expa ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( 𝐿 ‘ 𝑋 ) ∈ ℝ+ )
36 32 35 sylanl1 ⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( 𝐿 ‘ 𝑋 ) ∈ ℝ+ )
37 rpxr ⊢ ( ( 𝐿 ‘ 𝑋 ) ∈ ℝ+ → ( 𝐿 ‘ 𝑋 ) ∈ ℝ* )
38 rpgt0 ⊢ ( ( 𝐿 ‘ 𝑋 ) ∈ ℝ+ → 0 < ( 𝐿 ‘ 𝑋 ) )
39 xmulpnf2 ⊢ ( ( ( 𝐿 ‘ 𝑋 ) ∈ ℝ* ∧ 0 < ( 𝐿 ‘ 𝑋 ) ) → ( +∞ ·e ( 𝐿 ‘ 𝑋 ) ) = +∞ )
40 37 38 39 syl2anc ⊢ ( ( 𝐿 ‘ 𝑋 ) ∈ ℝ+ → ( +∞ ·e ( 𝐿 ‘ 𝑋 ) ) = +∞ )
41 36 40 syl ⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( +∞ ·e ( 𝐿 ‘ 𝑋 ) ) = +∞ )
42 31 41 breqtrrd ⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( +∞ ·e ( 𝐿 ‘ 𝑋 ) ) )
43 0le0 ⊢ 0 ≤ 0
44 simpl3 ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
45 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
46 33 45 ghmid ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
47 44 46 syl ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
48 47 fveq2d ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) = ( 𝑀 ‘ ( 0g ‘ 𝑇 ) ) )
49 4 45 nm0 ⊢ ( 𝑇 ∈ NrmGrp → ( 𝑀 ‘ ( 0g ‘ 𝑇 ) ) = 0 )
50 21 49 syl ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 0g ‘ 𝑇 ) ) = 0 )
51 48 50 eqtrd ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) = 0 )
52 simpl1 ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → 𝑆 ∈ NrmGrp )
53 3 33 nm0 ⊢ ( 𝑆 ∈ NrmGrp → ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) = 0 )
54 52 53 syl ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) = 0 )
55 54 oveq2d ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( +∞ ·e ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) ) = ( +∞ ·e 0 ) )
56 pnfxr ⊢ +∞ ∈ ℝ*
57 xmul01 ⊢ ( +∞ ∈ ℝ* → ( +∞ ·e 0 ) = 0 )
58 56 57 ax-mp ⊢ ( +∞ ·e 0 ) = 0
59 55 58 eqtrdi ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( +∞ ·e ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) ) = 0 )
60 51 59 breq12d ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) ≤ ( +∞ ·e ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) ) ↔ 0 ≤ 0 ) )
61 43 60 mpbiri ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) ≤ ( +∞ ·e ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) ) )
62 20 42 61 pm2.61ne ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( +∞ ·e ( 𝐿 ‘ 𝑋 ) ) )
63 62 adantr ⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ‘ 𝐹 ) = +∞ ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( +∞ ·e ( 𝐿 ‘ 𝑋 ) ) )
64 simpr ⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ‘ 𝐹 ) = +∞ ) → ( 𝑁 ‘ 𝐹 ) = +∞ )
65 64 oveq1d ⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ‘ 𝐹 ) = +∞ ) → ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑋 ) ) = ( +∞ ·e ( 𝐿 ‘ 𝑋 ) ) )
66 63 65 breqtrrd ⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ‘ 𝐹 ) = +∞ ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑋 ) ) )
67 1 nmocl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ* )
68 1 nmoge0 ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 0 ≤ ( 𝑁 ‘ 𝐹 ) )
69 ge0nemnf ⊢ ( ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ* ∧ 0 ≤ ( 𝑁 ‘ 𝐹 ) ) → ( 𝑁 ‘ 𝐹 ) ≠ -∞ )
70 67 68 69 syl2anc ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁 ‘ 𝐹 ) ≠ -∞ )
71 67 70 jca ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ* ∧ ( 𝑁 ‘ 𝐹 ) ≠ -∞ ) )
72 xrnemnf ⊢ ( ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ* ∧ ( 𝑁 ‘ 𝐹 ) ≠ -∞ ) ↔ ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ ∨ ( 𝑁 ‘ 𝐹 ) = +∞ ) )
73 71 72 sylib ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ ∨ ( 𝑁 ‘ 𝐹 ) = +∞ ) )
74 73 adantr ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ ∨ ( 𝑁 ‘ 𝐹 ) = +∞ ) )
75 15 66 74 mpjaodan ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑋 ) ) )