Step |
Hyp |
Ref |
Expression |
1 |
|
nmlnoubi.1 |
⊢ 𝑋 = ( BaseSet ‘ 𝑈 ) |
2 |
|
nmlnoubi.z |
⊢ 𝑍 = ( 0vec ‘ 𝑈 ) |
3 |
|
nmlnoubi.k |
⊢ 𝐾 = ( normCV ‘ 𝑈 ) |
4 |
|
nmlnoubi.m |
⊢ 𝑀 = ( normCV ‘ 𝑊 ) |
5 |
|
nmlnoubi.3 |
⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 ) |
6 |
|
nmlnoubi.7 |
⊢ 𝐿 = ( 𝑈 LnOp 𝑊 ) |
7 |
|
nmlnoubi.u |
⊢ 𝑈 ∈ NrmCVec |
8 |
|
nmlnoubi.w |
⊢ 𝑊 ∈ NrmCVec |
9 |
|
2fveq3 |
⊢ ( 𝑥 = 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) ) |
10 |
|
fveq2 |
⊢ ( 𝑥 = 𝑍 → ( 𝐾 ‘ 𝑥 ) = ( 𝐾 ‘ 𝑍 ) ) |
11 |
10
|
oveq2d |
⊢ ( 𝑥 = 𝑍 → ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) = ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) ) |
12 |
9 11
|
breq12d |
⊢ ( 𝑥 = 𝑍 → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ↔ ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) ) ) |
13 |
|
id |
⊢ ( ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) → ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) |
14 |
13
|
imp |
⊢ ( ( ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ∧ 𝑥 ≠ 𝑍 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) |
15 |
14
|
adantll |
⊢ ( ( ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) ∧ ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ≠ 𝑍 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) |
16 |
|
0le0 |
⊢ 0 ≤ 0 |
17 |
|
eqid |
⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 ) |
18 |
|
eqid |
⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 ) |
19 |
1 17 2 18 6
|
lno0 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ‘ 𝑍 ) = ( 0vec ‘ 𝑊 ) ) |
20 |
7 8 19
|
mp3an12 |
⊢ ( 𝑇 ∈ 𝐿 → ( 𝑇 ‘ 𝑍 ) = ( 0vec ‘ 𝑊 ) ) |
21 |
20
|
fveq2d |
⊢ ( 𝑇 ∈ 𝐿 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) = ( 𝑀 ‘ ( 0vec ‘ 𝑊 ) ) ) |
22 |
18 4
|
nvz0 |
⊢ ( 𝑊 ∈ NrmCVec → ( 𝑀 ‘ ( 0vec ‘ 𝑊 ) ) = 0 ) |
23 |
8 22
|
ax-mp |
⊢ ( 𝑀 ‘ ( 0vec ‘ 𝑊 ) ) = 0 |
24 |
21 23
|
eqtrdi |
⊢ ( 𝑇 ∈ 𝐿 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) = 0 ) |
25 |
24
|
adantr |
⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) = 0 ) |
26 |
2 3
|
nvz0 |
⊢ ( 𝑈 ∈ NrmCVec → ( 𝐾 ‘ 𝑍 ) = 0 ) |
27 |
7 26
|
ax-mp |
⊢ ( 𝐾 ‘ 𝑍 ) = 0 |
28 |
27
|
oveq2i |
⊢ ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) = ( 𝐴 · 0 ) |
29 |
|
recn |
⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ ) |
30 |
29
|
mul01d |
⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) = 0 ) |
31 |
28 30
|
syl5eq |
⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) = 0 ) |
32 |
31
|
ad2antrl |
⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) = 0 ) |
33 |
25 32
|
breq12d |
⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) ↔ 0 ≤ 0 ) ) |
34 |
16 33
|
mpbiri |
⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) ) |
35 |
34
|
adantr |
⊢ ( ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) ∧ ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) ) |
36 |
12 15 35
|
pm2.61ne |
⊢ ( ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) ∧ ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) |
37 |
36
|
ex |
⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) |
38 |
37
|
ralimdv |
⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) |
39 |
38
|
3impia |
⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) |
40 |
1 17 6
|
lnof |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ) |
41 |
7 8 40
|
mp3an12 |
⊢ ( 𝑇 ∈ 𝐿 → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ) |
42 |
1 17 3 4 5 7 8
|
nmoub2i |
⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 ) |
43 |
41 42
|
syl3an1 |
⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 ) |
44 |
39 43
|
syld3an3 |
⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 ) |