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 𝑇 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( 𝐿 ‘ 𝑋 ) ) )