Step |
Hyp |
Ref |
Expression |
1 |
|
nmcopex.1 |
โข ๐ โ LinOp |
2 |
|
nmcopex.2 |
โข ๐ โ ContOp |
3 |
|
0le0 |
โข 0 โค 0 |
4 |
3
|
a1i |
โข ( ๐ด = 0โ โ 0 โค 0 ) |
5 |
|
fveq2 |
โข ( ๐ด = 0โ โ ( ๐ โ ๐ด ) = ( ๐ โ 0โ ) ) |
6 |
1
|
lnop0i |
โข ( ๐ โ 0โ ) = 0โ |
7 |
5 6
|
eqtrdi |
โข ( ๐ด = 0โ โ ( ๐ โ ๐ด ) = 0โ ) |
8 |
7
|
fveq2d |
โข ( ๐ด = 0โ โ ( normโ โ ( ๐ โ ๐ด ) ) = ( normโ โ 0โ ) ) |
9 |
|
norm0 |
โข ( normโ โ 0โ ) = 0 |
10 |
8 9
|
eqtrdi |
โข ( ๐ด = 0โ โ ( normโ โ ( ๐ โ ๐ด ) ) = 0 ) |
11 |
|
fveq2 |
โข ( ๐ด = 0โ โ ( normโ โ ๐ด ) = ( normโ โ 0โ ) ) |
12 |
11 9
|
eqtrdi |
โข ( ๐ด = 0โ โ ( normโ โ ๐ด ) = 0 ) |
13 |
12
|
oveq2d |
โข ( ๐ด = 0โ โ ( ( normop โ ๐ ) ยท ( normโ โ ๐ด ) ) = ( ( normop โ ๐ ) ยท 0 ) ) |
14 |
1 2
|
nmcopexi |
โข ( normop โ ๐ ) โ โ |
15 |
14
|
recni |
โข ( normop โ ๐ ) โ โ |
16 |
15
|
mul01i |
โข ( ( normop โ ๐ ) ยท 0 ) = 0 |
17 |
13 16
|
eqtrdi |
โข ( ๐ด = 0โ โ ( ( normop โ ๐ ) ยท ( normโ โ ๐ด ) ) = 0 ) |
18 |
4 10 17
|
3brtr4d |
โข ( ๐ด = 0โ โ ( normโ โ ( ๐ โ ๐ด ) ) โค ( ( normop โ ๐ ) ยท ( normโ โ ๐ด ) ) ) |
19 |
18
|
adantl |
โข ( ( ๐ด โ โ โง ๐ด = 0โ ) โ ( normโ โ ( ๐ โ ๐ด ) ) โค ( ( normop โ ๐ ) ยท ( normโ โ ๐ด ) ) ) |
20 |
|
normcl |
โข ( ๐ด โ โ โ ( normโ โ ๐ด ) โ โ ) |
21 |
20
|
adantr |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( normโ โ ๐ด ) โ โ ) |
22 |
|
normne0 |
โข ( ๐ด โ โ โ ( ( normโ โ ๐ด ) โ 0 โ ๐ด โ 0โ ) ) |
23 |
22
|
biimpar |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( normโ โ ๐ด ) โ 0 ) |
24 |
21 23
|
rereccld |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( 1 / ( normโ โ ๐ด ) ) โ โ ) |
25 |
|
normgt0 |
โข ( ๐ด โ โ โ ( ๐ด โ 0โ โ 0 < ( normโ โ ๐ด ) ) ) |
26 |
25
|
biimpa |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ 0 < ( normโ โ ๐ด ) ) |
27 |
21 26
|
recgt0d |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ 0 < ( 1 / ( normโ โ ๐ด ) ) ) |
28 |
|
0re |
โข 0 โ โ |
29 |
|
ltle |
โข ( ( 0 โ โ โง ( 1 / ( normโ โ ๐ด ) ) โ โ ) โ ( 0 < ( 1 / ( normโ โ ๐ด ) ) โ 0 โค ( 1 / ( normโ โ ๐ด ) ) ) ) |
30 |
28 29
|
mpan |
โข ( ( 1 / ( normโ โ ๐ด ) ) โ โ โ ( 0 < ( 1 / ( normโ โ ๐ด ) ) โ 0 โค ( 1 / ( normโ โ ๐ด ) ) ) ) |
31 |
24 27 30
|
sylc |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ 0 โค ( 1 / ( normโ โ ๐ด ) ) ) |
32 |
24 31
|
absidd |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( abs โ ( 1 / ( normโ โ ๐ด ) ) ) = ( 1 / ( normโ โ ๐ด ) ) ) |
33 |
32
|
oveq1d |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( ( abs โ ( 1 / ( normโ โ ๐ด ) ) ) ยท ( normโ โ ( ๐ โ ๐ด ) ) ) = ( ( 1 / ( normโ โ ๐ด ) ) ยท ( normโ โ ( ๐ โ ๐ด ) ) ) ) |
34 |
24
|
recnd |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( 1 / ( normโ โ ๐ด ) ) โ โ ) |
35 |
|
simpl |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ๐ด โ โ ) |
36 |
1
|
lnopmuli |
โข ( ( ( 1 / ( normโ โ ๐ด ) ) โ โ โง ๐ด โ โ ) โ ( ๐ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) = ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ( ๐ โ ๐ด ) ) ) |
37 |
34 35 36
|
syl2anc |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( ๐ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) = ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ( ๐ โ ๐ด ) ) ) |
38 |
37
|
fveq2d |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( normโ โ ( ๐ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) ) = ( normโ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ( ๐ โ ๐ด ) ) ) ) |
39 |
1
|
lnopfi |
โข ๐ : โ โถ โ |
40 |
39
|
ffvelcdmi |
โข ( ๐ด โ โ โ ( ๐ โ ๐ด ) โ โ ) |
41 |
40
|
adantr |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( ๐ โ ๐ด ) โ โ ) |
42 |
|
norm-iii |
โข ( ( ( 1 / ( normโ โ ๐ด ) ) โ โ โง ( ๐ โ ๐ด ) โ โ ) โ ( normโ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ( ๐ โ ๐ด ) ) ) = ( ( abs โ ( 1 / ( normโ โ ๐ด ) ) ) ยท ( normโ โ ( ๐ โ ๐ด ) ) ) ) |
43 |
34 41 42
|
syl2anc |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( normโ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ( ๐ โ ๐ด ) ) ) = ( ( abs โ ( 1 / ( normโ โ ๐ด ) ) ) ยท ( normโ โ ( ๐ โ ๐ด ) ) ) ) |
44 |
38 43
|
eqtrd |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( normโ โ ( ๐ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) ) = ( ( abs โ ( 1 / ( normโ โ ๐ด ) ) ) ยท ( normโ โ ( ๐ โ ๐ด ) ) ) ) |
45 |
|
normcl |
โข ( ( ๐ โ ๐ด ) โ โ โ ( normโ โ ( ๐ โ ๐ด ) ) โ โ ) |
46 |
40 45
|
syl |
โข ( ๐ด โ โ โ ( normโ โ ( ๐ โ ๐ด ) ) โ โ ) |
47 |
46
|
adantr |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( normโ โ ( ๐ โ ๐ด ) ) โ โ ) |
48 |
47
|
recnd |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( normโ โ ( ๐ โ ๐ด ) ) โ โ ) |
49 |
21
|
recnd |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( normโ โ ๐ด ) โ โ ) |
50 |
48 49 23
|
divrec2d |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( ( normโ โ ( ๐ โ ๐ด ) ) / ( normโ โ ๐ด ) ) = ( ( 1 / ( normโ โ ๐ด ) ) ยท ( normโ โ ( ๐ โ ๐ด ) ) ) ) |
51 |
33 44 50
|
3eqtr4rd |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( ( normโ โ ( ๐ โ ๐ด ) ) / ( normโ โ ๐ด ) ) = ( normโ โ ( ๐ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) ) ) |
52 |
|
hvmulcl |
โข ( ( ( 1 / ( normโ โ ๐ด ) ) โ โ โง ๐ด โ โ ) โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) โ โ ) |
53 |
34 35 52
|
syl2anc |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) โ โ ) |
54 |
|
normcl |
โข ( ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) โ โ โ ( normโ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) โ โ ) |
55 |
53 54
|
syl |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( normโ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) โ โ ) |
56 |
|
norm1 |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( normโ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) = 1 ) |
57 |
|
eqle |
โข ( ( ( normโ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) โ โ โง ( normโ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) = 1 ) โ ( normโ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) โค 1 ) |
58 |
55 56 57
|
syl2anc |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( normโ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) โค 1 ) |
59 |
|
nmoplb |
โข ( ( ๐ : โ โถ โ โง ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) โ โ โง ( normโ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) โค 1 ) โ ( normโ โ ( ๐ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) ) โค ( normop โ ๐ ) ) |
60 |
39 59
|
mp3an1 |
โข ( ( ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) โ โ โง ( normโ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) โค 1 ) โ ( normโ โ ( ๐ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) ) โค ( normop โ ๐ ) ) |
61 |
53 58 60
|
syl2anc |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( normโ โ ( ๐ โ ( ( 1 / ( normโ โ ๐ด ) ) ยทโ ๐ด ) ) ) โค ( normop โ ๐ ) ) |
62 |
51 61
|
eqbrtrd |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( ( normโ โ ( ๐ โ ๐ด ) ) / ( normโ โ ๐ด ) ) โค ( normop โ ๐ ) ) |
63 |
14
|
a1i |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( normop โ ๐ ) โ โ ) |
64 |
|
ledivmul2 |
โข ( ( ( normโ โ ( ๐ โ ๐ด ) ) โ โ โง ( normop โ ๐ ) โ โ โง ( ( normโ โ ๐ด ) โ โ โง 0 < ( normโ โ ๐ด ) ) ) โ ( ( ( normโ โ ( ๐ โ ๐ด ) ) / ( normโ โ ๐ด ) ) โค ( normop โ ๐ ) โ ( normโ โ ( ๐ โ ๐ด ) ) โค ( ( normop โ ๐ ) ยท ( normโ โ ๐ด ) ) ) ) |
65 |
47 63 21 26 64
|
syl112anc |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( ( ( normโ โ ( ๐ โ ๐ด ) ) / ( normโ โ ๐ด ) ) โค ( normop โ ๐ ) โ ( normโ โ ( ๐ โ ๐ด ) ) โค ( ( normop โ ๐ ) ยท ( normโ โ ๐ด ) ) ) ) |
66 |
62 65
|
mpbid |
โข ( ( ๐ด โ โ โง ๐ด โ 0โ ) โ ( normโ โ ( ๐ โ ๐ด ) ) โค ( ( normop โ ๐ ) ยท ( normโ โ ๐ด ) ) ) |
67 |
19 66
|
pm2.61dane |
โข ( ๐ด โ โ โ ( normโ โ ( ๐ โ ๐ด ) ) โค ( ( normop โ ๐ ) ยท ( normโ โ ๐ด ) ) ) |