Theorem nmblolbii

Description: A lower bound for the norm of a bounded linear operator. (Contributed by NM, 7-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmblolbi.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nmblolbi.4	⊢ 𝐿 = ( normCV ‘ 𝑈 )
	nmblolbi.5	⊢ 𝑀 = ( normCV ‘ 𝑊 )
	nmblolbi.6	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
	nmblolbi.7	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
	nmblolbi.u	⊢ 𝑈 ∈ NrmCVec
	nmblolbi.w	⊢ 𝑊 ∈ NrmCVec
	nmblolbii.b	⊢ 𝑇 ∈ 𝐵
Assertion	nmblolbii	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmblolbi.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nmblolbi.4	⊢ 𝐿 = ( normCV ‘ 𝑈 )
3		nmblolbi.5	⊢ 𝑀 = ( normCV ‘ 𝑊 )
4		nmblolbi.6	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
5		nmblolbi.7	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
6		nmblolbi.u	⊢ 𝑈 ∈ NrmCVec
7		nmblolbi.w	⊢ 𝑊 ∈ NrmCVec
8		nmblolbii.b	⊢ 𝑇 ∈ 𝐵
9		fveq2	⊢ ( 𝐴 = ( 0vec ‘ 𝑈 ) → ( 𝑇 ‘ 𝐴 ) = ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) )
10	9	fveq2d	⊢ ( 𝐴 = ( 0vec ‘ 𝑈 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) )
11		fveq2	⊢ ( 𝐴 = ( 0vec ‘ 𝑈 ) → ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) )
12	11	oveq2d	⊢ ( 𝐴 = ( 0vec ‘ 𝑈 ) → ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) = ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) ) )
13	10 12	breq12d	⊢ ( 𝐴 = ( 0vec ‘ 𝑈 ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) ↔ ( 𝑀 ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) ) ) )
14	1 2	nvcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐿 ‘ 𝐴 ) ∈ ℝ )
15	6 14	mpan	⊢ ( 𝐴 ∈ 𝑋 → ( 𝐿 ‘ 𝐴 ) ∈ ℝ )
16	15	adantr	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐴 ) ∈ ℝ )
17		eqid	⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
18	1 17 2	nvz	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐿 ‘ 𝐴 ) = 0 ↔ 𝐴 = ( 0vec ‘ 𝑈 ) ) )
19	6 18	mpan	⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝐿 ‘ 𝐴 ) = 0 ↔ 𝐴 = ( 0vec ‘ 𝑈 ) ) )
20	19	necon3bid	⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝐿 ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) )
21	20	biimpar	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐴 ) ≠ 0 )
22	16 21	rereccld	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℝ )
23	1 17 2	nvgt0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ≠ ( 0vec ‘ 𝑈 ) ↔ 0 < ( 𝐿 ‘ 𝐴 ) ) )
24	6 23	mpan	⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ≠ ( 0vec ‘ 𝑈 ) ↔ 0 < ( 𝐿 ‘ 𝐴 ) ) )
25	24	biimpa	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → 0 < ( 𝐿 ‘ 𝐴 ) )
26	16 25	recgt0d	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → 0 < ( 1 / ( 𝐿 ‘ 𝐴 ) ) )
27		0re	⊢ 0 ∈ ℝ
28		ltle	⊢ ( ( 0 ∈ ℝ ∧ ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℝ ) → ( 0 < ( 1 / ( 𝐿 ‘ 𝐴 ) ) → 0 ≤ ( 1 / ( 𝐿 ‘ 𝐴 ) ) ) )
29	27 22 28	sylancr	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 0 < ( 1 / ( 𝐿 ‘ 𝐴 ) ) → 0 ≤ ( 1 / ( 𝐿 ‘ 𝐴 ) ) ) )
30	26 29	mpd	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → 0 ≤ ( 1 / ( 𝐿 ‘ 𝐴 ) ) )
31		eqid	⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
32	1 31 5	blof	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
33	6 7 8 32	mp3an	⊢ 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 )
34	33	ffvelcdmi	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑇 ‘ 𝐴 ) ∈ ( BaseSet ‘ 𝑊 ) )
35	34	adantr	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑇 ‘ 𝐴 ) ∈ ( BaseSet ‘ 𝑊 ) )
36		eqid	⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
37	31 36 3	nvsge0	⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 1 / ( 𝐿 ‘ 𝐴 ) ) ) ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑀 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) ) = ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) · ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
38	7 37	mp3an1	⊢ ( ( ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 1 / ( 𝐿 ‘ 𝐴 ) ) ) ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑀 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) ) = ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) · ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
39	22 30 35 38	syl21anc	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑀 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) ) = ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) · ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
40	22	recnd	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℂ )
41		simpl	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → 𝐴 ∈ 𝑋 )
42		eqid	⊢ ( 𝑈 LnOp 𝑊 ) = ( 𝑈 LnOp 𝑊 )
43	42 5	bloln	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) )
44	6 7 8 43	mp3an	⊢ 𝑇 ∈ ( 𝑈 LnOp 𝑊 )
45	6 7 44	3pm3.2i	⊢ ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) )
46		eqid	⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
47	1 46 36 42	lnomul	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) ) ∧ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) )
48	45 47	mpan	⊢ ( ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑇 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) )
49	40 41 48	syl2anc	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑇 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) )
50	49	fveq2d	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) = ( 𝑀 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) ) )
51	31 3	nvcl	⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ )
52	7 34 51	sylancr	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ )
53	52	adantr	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ )
54	53	recnd	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℂ )
55	16	recnd	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐴 ) ∈ ℂ )
56	54 55 21	divrec2d	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) / ( 𝐿 ‘ 𝐴 ) ) = ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) · ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
57	39 50 56	3eqtr4rd	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) / ( 𝐿 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) )
58	1 46	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 )
59	6 58	mp3an1	⊢ ( ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 )
60	59	ancoms	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℂ ) → ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 )
61	40 60	syldan	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 )
62	1 2	nvcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 ) → ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ∈ ℝ )
63	6 61 62	sylancr	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ∈ ℝ )
64	1 46 17 2	nv1	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = 1 )
65	6 64	mp3an1	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = 1 )
66		eqle	⊢ ( ( ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ∈ ℝ ∧ ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = 1 ) → ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ≤ 1 )
67	63 65 66	syl2anc	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ≤ 1 )
68	6 7 33	3pm3.2i	⊢ ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
69	1 31 2 3 4	nmoolb	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ) ∧ ( ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 ∧ ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ≤ 1 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ≤ ( 𝑁 ‘ 𝑇 ) )
70	68 69	mpan	⊢ ( ( ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 ∧ ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ≤ 1 ) → ( 𝑀 ‘ ( 𝑇 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ≤ ( 𝑁 ‘ 𝑇 ) )
71	61 67 70	syl2anc	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ≤ ( 𝑁 ‘ 𝑇 ) )
72	57 71	eqbrtrd	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) / ( 𝐿 ‘ 𝐴 ) ) ≤ ( 𝑁 ‘ 𝑇 ) )
73	1 31 4 5	nmblore	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ )
74	6 7 8 73	mp3an	⊢ ( 𝑁 ‘ 𝑇 ) ∈ ℝ
75	74	a1i	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ )
76		ledivmul2	⊢ ( ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝑁 ‘ 𝑇 ) ∈ ℝ ∧ ( ( 𝐿 ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( 𝐿 ‘ 𝐴 ) ) ) → ( ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) / ( 𝐿 ‘ 𝐴 ) ) ≤ ( 𝑁 ‘ 𝑇 ) ↔ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) ) )
77	53 75 16 25 76	syl112anc	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) / ( 𝐿 ‘ 𝐴 ) ) ≤ ( 𝑁 ‘ 𝑇 ) ↔ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) ) )
78	72 77	mpbid	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) )
79		0le0	⊢ 0 ≤ 0
80		eqid	⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 )
81	1 31 17 80 42	lno0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) ) → ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) = ( 0vec ‘ 𝑊 ) )
82	6 7 44 81	mp3an	⊢ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) = ( 0vec ‘ 𝑊 )
83	82	fveq2i	⊢ ( 𝑀 ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) = ( 𝑀 ‘ ( 0vec ‘ 𝑊 ) )
84	80 3	nvz0	⊢ ( 𝑊 ∈ NrmCVec → ( 𝑀 ‘ ( 0vec ‘ 𝑊 ) ) = 0 )
85	7 84	ax-mp	⊢ ( 𝑀 ‘ ( 0vec ‘ 𝑊 ) ) = 0
86	83 85	eqtri	⊢ ( 𝑀 ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) = 0
87	17 2	nvz0	⊢ ( 𝑈 ∈ NrmCVec → ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) = 0 )
88	6 87	ax-mp	⊢ ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) = 0
89	88	oveq2i	⊢ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) ) = ( ( 𝑁 ‘ 𝑇 ) · 0 )
90	74	recni	⊢ ( 𝑁 ‘ 𝑇 ) ∈ ℂ
91	90	mul01i	⊢ ( ( 𝑁 ‘ 𝑇 ) · 0 ) = 0
92	89 91	eqtri	⊢ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) ) = 0
93	79 86 92	3brtr4i	⊢ ( 𝑀 ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) )
94	93	a1i	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑀 ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) ) )
95	13 78 94	pm2.61ne	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) )