Proof of Theorem nmblolbii
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6905 | . . . 4
⊢ (𝐴 = (0vec‘𝑈) → (𝑇‘𝐴) = (𝑇‘(0vec‘𝑈))) | 
| 2 | 1 | fveq2d 6909 | . . 3
⊢ (𝐴 = (0vec‘𝑈) → (𝑀‘(𝑇‘𝐴)) = (𝑀‘(𝑇‘(0vec‘𝑈)))) | 
| 3 |  | fveq2 6905 | . . . 4
⊢ (𝐴 = (0vec‘𝑈) → (𝐿‘𝐴) = (𝐿‘(0vec‘𝑈))) | 
| 4 | 3 | oveq2d 7448 | . . 3
⊢ (𝐴 = (0vec‘𝑈) → ((𝑁‘𝑇) · (𝐿‘𝐴)) = ((𝑁‘𝑇) · (𝐿‘(0vec‘𝑈)))) | 
| 5 | 2, 4 | breq12d 5155 | . 2
⊢ (𝐴 = (0vec‘𝑈) → ((𝑀‘(𝑇‘𝐴)) ≤ ((𝑁‘𝑇) · (𝐿‘𝐴)) ↔ (𝑀‘(𝑇‘(0vec‘𝑈))) ≤ ((𝑁‘𝑇) · (𝐿‘(0vec‘𝑈))))) | 
| 6 |  | nmblolbi.u | . . . . . . . . 9
⊢ 𝑈 ∈ NrmCVec | 
| 7 |  | nmblolbi.1 | . . . . . . . . . 10
⊢ 𝑋 = (BaseSet‘𝑈) | 
| 8 |  | nmblolbi.4 | . . . . . . . . . 10
⊢ 𝐿 =
(normCV‘𝑈) | 
| 9 | 7, 8 | nvcl 30681 | . . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐿‘𝐴) ∈ ℝ) | 
| 10 | 6, 9 | mpan 690 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑋 → (𝐿‘𝐴) ∈ ℝ) | 
| 11 | 10 | adantr 480 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (𝐿‘𝐴) ∈ ℝ) | 
| 12 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(0vec‘𝑈) = (0vec‘𝑈) | 
| 13 | 7, 12, 8 | nvz 30689 | . . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((𝐿‘𝐴) = 0 ↔ 𝐴 = (0vec‘𝑈))) | 
| 14 | 6, 13 | mpan 690 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝑋 → ((𝐿‘𝐴) = 0 ↔ 𝐴 = (0vec‘𝑈))) | 
| 15 | 14 | necon3bid 2984 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑋 → ((𝐿‘𝐴) ≠ 0 ↔ 𝐴 ≠ (0vec‘𝑈))) | 
| 16 | 15 | biimpar 477 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (𝐿‘𝐴) ≠ 0) | 
| 17 | 11, 16 | rereccld 12095 | . . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (1 / (𝐿‘𝐴)) ∈ ℝ) | 
| 18 | 7, 12, 8 | nvgt0 30694 | . . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴 ≠ (0vec‘𝑈) ↔ 0 < (𝐿‘𝐴))) | 
| 19 | 6, 18 | mpan 690 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝑋 → (𝐴 ≠ (0vec‘𝑈) ↔ 0 < (𝐿‘𝐴))) | 
| 20 | 19 | biimpa 476 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → 0 < (𝐿‘𝐴)) | 
| 21 | 11, 20 | recgt0d 12203 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → 0 < (1 / (𝐿‘𝐴))) | 
| 22 |  | 0re 11264 | . . . . . . . 8
⊢ 0 ∈
ℝ | 
| 23 |  | ltle 11350 | . . . . . . . 8
⊢ ((0
∈ ℝ ∧ (1 / (𝐿‘𝐴)) ∈ ℝ) → (0 < (1 /
(𝐿‘𝐴)) → 0 ≤ (1 / (𝐿‘𝐴)))) | 
| 24 | 22, 17, 23 | sylancr 587 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (0 < (1 / (𝐿‘𝐴)) → 0 ≤ (1 / (𝐿‘𝐴)))) | 
| 25 | 21, 24 | mpd 15 | . . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → 0 ≤ (1 / (𝐿‘𝐴))) | 
| 26 |  | nmblolbi.w | . . . . . . . . 9
⊢ 𝑊 ∈ NrmCVec | 
| 27 |  | nmblolbii.b | . . . . . . . . 9
⊢ 𝑇 ∈ 𝐵 | 
| 28 |  | eqid 2736 | . . . . . . . . . 10
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) | 
| 29 |  | nmblolbi.7 | . . . . . . . . . 10
⊢ 𝐵 = (𝑈 BLnOp 𝑊) | 
| 30 | 7, 28, 29 | blof 30805 | . . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → 𝑇:𝑋⟶(BaseSet‘𝑊)) | 
| 31 | 6, 26, 27, 30 | mp3an 1462 | . . . . . . . 8
⊢ 𝑇:𝑋⟶(BaseSet‘𝑊) | 
| 32 | 31 | ffvelcdmi 7102 | . . . . . . 7
⊢ (𝐴 ∈ 𝑋 → (𝑇‘𝐴) ∈ (BaseSet‘𝑊)) | 
| 33 | 32 | adantr 480 | . . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (𝑇‘𝐴) ∈ (BaseSet‘𝑊)) | 
| 34 |  | eqid 2736 | . . . . . . . 8
⊢ (
·𝑠OLD ‘𝑊) = ( ·𝑠OLD
‘𝑊) | 
| 35 |  | nmblolbi.5 | . . . . . . . 8
⊢ 𝑀 =
(normCV‘𝑊) | 
| 36 | 28, 34, 35 | nvsge0 30684 | . . . . . . 7
⊢ ((𝑊 ∈ NrmCVec ∧ ((1 /
(𝐿‘𝐴)) ∈ ℝ ∧ 0 ≤ (1 / (𝐿‘𝐴))) ∧ (𝑇‘𝐴) ∈ (BaseSet‘𝑊)) → (𝑀‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑊)(𝑇‘𝐴))) = ((1 / (𝐿‘𝐴)) · (𝑀‘(𝑇‘𝐴)))) | 
| 37 | 26, 36 | mp3an1 1449 | . . . . . 6
⊢ ((((1 /
(𝐿‘𝐴)) ∈ ℝ ∧ 0 ≤ (1 / (𝐿‘𝐴))) ∧ (𝑇‘𝐴) ∈ (BaseSet‘𝑊)) → (𝑀‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑊)(𝑇‘𝐴))) = ((1 / (𝐿‘𝐴)) · (𝑀‘(𝑇‘𝐴)))) | 
| 38 | 17, 25, 33, 37 | syl21anc 837 | . . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (𝑀‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑊)(𝑇‘𝐴))) = ((1 / (𝐿‘𝐴)) · (𝑀‘(𝑇‘𝐴)))) | 
| 39 | 17 | recnd 11290 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (1 / (𝐿‘𝐴)) ∈ ℂ) | 
| 40 |  | simpl 482 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → 𝐴 ∈ 𝑋) | 
| 41 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (𝑈 LnOp 𝑊) = (𝑈 LnOp 𝑊) | 
| 42 | 41, 29 | bloln 30804 | . . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → 𝑇 ∈ (𝑈 LnOp 𝑊)) | 
| 43 | 6, 26, 27, 42 | mp3an 1462 | . . . . . . . . 9
⊢ 𝑇 ∈ (𝑈 LnOp 𝑊) | 
| 44 | 6, 26, 43 | 3pm3.2i 1339 | . . . . . . . 8
⊢ (𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ (𝑈 LnOp 𝑊)) | 
| 45 |  | eqid 2736 | . . . . . . . . 9
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) | 
| 46 | 7, 45, 34, 41 | lnomul 30780 | . . . . . . . 8
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ (𝑈 LnOp 𝑊)) ∧ ((1 / (𝐿‘𝐴)) ∈ ℂ ∧ 𝐴 ∈ 𝑋)) → (𝑇‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴)) = ((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑊)(𝑇‘𝐴))) | 
| 47 | 44, 46 | mpan 690 | . . . . . . 7
⊢ (((1 /
(𝐿‘𝐴)) ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (𝑇‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴)) = ((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑊)(𝑇‘𝐴))) | 
| 48 | 39, 40, 47 | syl2anc 584 | . . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (𝑇‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴)) = ((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑊)(𝑇‘𝐴))) | 
| 49 | 48 | fveq2d 6909 | . . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (𝑀‘(𝑇‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴))) = (𝑀‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑊)(𝑇‘𝐴)))) | 
| 50 | 28, 35 | nvcl 30681 | . . . . . . . . 9
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝐴) ∈ (BaseSet‘𝑊)) → (𝑀‘(𝑇‘𝐴)) ∈ ℝ) | 
| 51 | 26, 32, 50 | sylancr 587 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑋 → (𝑀‘(𝑇‘𝐴)) ∈ ℝ) | 
| 52 | 51 | adantr 480 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (𝑀‘(𝑇‘𝐴)) ∈ ℝ) | 
| 53 | 52 | recnd 11290 | . . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (𝑀‘(𝑇‘𝐴)) ∈ ℂ) | 
| 54 | 11 | recnd 11290 | . . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (𝐿‘𝐴) ∈ ℂ) | 
| 55 | 53, 54, 16 | divrec2d 12048 | . . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → ((𝑀‘(𝑇‘𝐴)) / (𝐿‘𝐴)) = ((1 / (𝐿‘𝐴)) · (𝑀‘(𝑇‘𝐴)))) | 
| 56 | 38, 49, 55 | 3eqtr4rd 2787 | . . . 4
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → ((𝑀‘(𝑇‘𝐴)) / (𝐿‘𝐴)) = (𝑀‘(𝑇‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴)))) | 
| 57 | 7, 45 | nvscl 30646 | . . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ (1 /
(𝐿‘𝐴)) ∈ ℂ ∧ 𝐴 ∈ 𝑋) → ((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴) ∈ 𝑋) | 
| 58 | 6, 57 | mp3an1 1449 | . . . . . . 7
⊢ (((1 /
(𝐿‘𝐴)) ∈ ℂ ∧ 𝐴 ∈ 𝑋) → ((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴) ∈ 𝑋) | 
| 59 | 58 | ancoms 458 | . . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ (1 / (𝐿‘𝐴)) ∈ ℂ) → ((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴) ∈ 𝑋) | 
| 60 | 39, 59 | syldan 591 | . . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → ((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴) ∈ 𝑋) | 
| 61 | 7, 8 | nvcl 30681 | . . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ ((1 /
(𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴) ∈ 𝑋) → (𝐿‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴)) ∈ ℝ) | 
| 62 | 6, 60, 61 | sylancr 587 | . . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (𝐿‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴)) ∈ ℝ) | 
| 63 | 7, 45, 12, 8 | nv1 30695 | . . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (𝐿‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴)) = 1) | 
| 64 | 6, 63 | mp3an1 1449 | . . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (𝐿‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴)) = 1) | 
| 65 |  | eqle 11364 | . . . . . 6
⊢ (((𝐿‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴)) ∈ ℝ ∧ (𝐿‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴)) = 1) → (𝐿‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴)) ≤ 1) | 
| 66 | 62, 64, 65 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (𝐿‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴)) ≤ 1) | 
| 67 | 6, 26, 31 | 3pm3.2i 1339 | . . . . . 6
⊢ (𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶(BaseSet‘𝑊)) | 
| 68 |  | nmblolbi.6 | . . . . . . 7
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) | 
| 69 | 7, 28, 8, 35, 68 | nmoolb 30791 | . . . . . 6
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶(BaseSet‘𝑊)) ∧ (((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴) ∈ 𝑋 ∧ (𝐿‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴)) ≤ 1)) → (𝑀‘(𝑇‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴))) ≤ (𝑁‘𝑇)) | 
| 70 | 67, 69 | mpan 690 | . . . . 5
⊢ ((((1 /
(𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴) ∈ 𝑋 ∧ (𝐿‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴)) ≤ 1) → (𝑀‘(𝑇‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴))) ≤ (𝑁‘𝑇)) | 
| 71 | 60, 66, 70 | syl2anc 584 | . . . 4
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (𝑀‘(𝑇‘((1 / (𝐿‘𝐴))( ·𝑠OLD
‘𝑈)𝐴))) ≤ (𝑁‘𝑇)) | 
| 72 | 56, 71 | eqbrtrd 5164 | . . 3
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → ((𝑀‘(𝑇‘𝐴)) / (𝐿‘𝐴)) ≤ (𝑁‘𝑇)) | 
| 73 | 7, 28, 68, 29 | nmblore 30806 | . . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → (𝑁‘𝑇) ∈ ℝ) | 
| 74 | 6, 26, 27, 73 | mp3an 1462 | . . . . 5
⊢ (𝑁‘𝑇) ∈ ℝ | 
| 75 | 74 | a1i 11 | . . . 4
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (𝑁‘𝑇) ∈ ℝ) | 
| 76 |  | ledivmul2 12148 | . . . 4
⊢ (((𝑀‘(𝑇‘𝐴)) ∈ ℝ ∧ (𝑁‘𝑇) ∈ ℝ ∧ ((𝐿‘𝐴) ∈ ℝ ∧ 0 < (𝐿‘𝐴))) → (((𝑀‘(𝑇‘𝐴)) / (𝐿‘𝐴)) ≤ (𝑁‘𝑇) ↔ (𝑀‘(𝑇‘𝐴)) ≤ ((𝑁‘𝑇) · (𝐿‘𝐴)))) | 
| 77 | 52, 75, 11, 20, 76 | syl112anc 1375 | . . 3
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (((𝑀‘(𝑇‘𝐴)) / (𝐿‘𝐴)) ≤ (𝑁‘𝑇) ↔ (𝑀‘(𝑇‘𝐴)) ≤ ((𝑁‘𝑇) · (𝐿‘𝐴)))) | 
| 78 | 72, 77 | mpbid 232 | . 2
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0vec‘𝑈)) → (𝑀‘(𝑇‘𝐴)) ≤ ((𝑁‘𝑇) · (𝐿‘𝐴))) | 
| 79 |  | 0le0 12368 | . . . 4
⊢ 0 ≤
0 | 
| 80 |  | eqid 2736 | . . . . . . . 8
⊢
(0vec‘𝑊) = (0vec‘𝑊) | 
| 81 | 7, 28, 12, 80, 41 | lno0 30776 | . . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ (𝑈 LnOp 𝑊)) → (𝑇‘(0vec‘𝑈)) =
(0vec‘𝑊)) | 
| 82 | 6, 26, 43, 81 | mp3an 1462 | . . . . . 6
⊢ (𝑇‘(0vec‘𝑈)) =
(0vec‘𝑊) | 
| 83 | 82 | fveq2i 6908 | . . . . 5
⊢ (𝑀‘(𝑇‘(0vec‘𝑈))) = (𝑀‘(0vec‘𝑊)) | 
| 84 | 80, 35 | nvz0 30688 | . . . . . 6
⊢ (𝑊 ∈ NrmCVec → (𝑀‘(0vec‘𝑊)) = 0) | 
| 85 | 26, 84 | ax-mp 5 | . . . . 5
⊢ (𝑀‘(0vec‘𝑊)) = 0 | 
| 86 | 83, 85 | eqtri 2764 | . . . 4
⊢ (𝑀‘(𝑇‘(0vec‘𝑈))) = 0 | 
| 87 | 12, 8 | nvz0 30688 | . . . . . . 7
⊢ (𝑈 ∈ NrmCVec → (𝐿‘(0vec‘𝑈)) = 0) | 
| 88 | 6, 87 | ax-mp 5 | . . . . . 6
⊢ (𝐿‘(0vec‘𝑈)) = 0 | 
| 89 | 88 | oveq2i 7443 | . . . . 5
⊢ ((𝑁‘𝑇) · (𝐿‘(0vec‘𝑈))) = ((𝑁‘𝑇) · 0) | 
| 90 | 74 | recni 11276 | . . . . . 6
⊢ (𝑁‘𝑇) ∈ ℂ | 
| 91 | 90 | mul01i 11452 | . . . . 5
⊢ ((𝑁‘𝑇) · 0) = 0 | 
| 92 | 89, 91 | eqtri 2764 | . . . 4
⊢ ((𝑁‘𝑇) · (𝐿‘(0vec‘𝑈))) = 0 | 
| 93 | 79, 86, 92 | 3brtr4i 5172 | . . 3
⊢ (𝑀‘(𝑇‘(0vec‘𝑈))) ≤ ((𝑁‘𝑇) · (𝐿‘(0vec‘𝑈))) | 
| 94 | 93 | a1i 11 | . 2
⊢ (𝐴 ∈ 𝑋 → (𝑀‘(𝑇‘(0vec‘𝑈))) ≤ ((𝑁‘𝑇) · (𝐿‘(0vec‘𝑈)))) | 
| 95 | 5, 78, 94 | pm2.61ne 3026 | 1
⊢ (𝐴 ∈ 𝑋 → (𝑀‘(𝑇‘𝐴)) ≤ ((𝑁‘𝑇) · (𝐿‘𝐴))) |