Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . . 4
โข (๐ด = 0โ โ
(๐โ๐ด) = (๐โ0โ)) |
2 | 1 | fveq2d 6850 |
. . 3
โข (๐ด = 0โ โ
(normโโ(๐โ๐ด)) = (normโโ(๐โ0โ))) |
3 | | fveq2 6846 |
. . . 4
โข (๐ด = 0โ โ
(normโโ๐ด) =
(normโโ0โ)) |
4 | 3 | oveq2d 7377 |
. . 3
โข (๐ด = 0โ โ
((normopโ๐) ยท
(normโโ๐ด)) = ((normopโ๐) ยท
(normโโ0โ))) |
5 | 2, 4 | breq12d 5122 |
. 2
โข (๐ด = 0โ โ
((normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด)) โ
(normโโ(๐โ0โ)) โค
((normopโ๐) ยท
(normโโ0โ)))) |
6 | | nmbdoplb.1 |
. . . . . . . . . . . 12
โข ๐ โ
BndLinOp |
7 | | bdopln 30852 |
. . . . . . . . . . . 12
โข (๐ โ BndLinOp โ ๐ โ LinOp) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . 11
โข ๐ โ LinOp |
9 | 8 | lnopfi 30960 |
. . . . . . . . . 10
โข ๐: โโถ
โ |
10 | 9 | ffvelcdmi 7038 |
. . . . . . . . 9
โข (๐ด โ โ โ (๐โ๐ด) โ โ) |
11 | | normcl 30116 |
. . . . . . . . 9
โข ((๐โ๐ด) โ โ โ
(normโโ(๐โ๐ด)) โ โ) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
โข (๐ด โ โ โ
(normโโ(๐โ๐ด)) โ โ) |
13 | 12 | adantr 482 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ(๐โ๐ด)) โ โ) |
14 | 13 | recnd 11191 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ(๐โ๐ด)) โ โ) |
15 | | normcl 30116 |
. . . . . . . 8
โข (๐ด โ โ โ
(normโโ๐ด) โ โ) |
16 | 15 | adantr 482 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ๐ด) โ โ) |
17 | 16 | recnd 11191 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ๐ด) โ โ) |
18 | | normne0 30121 |
. . . . . . 7
โข (๐ด โ โ โ
((normโโ๐ด) โ 0 โ ๐ด โ
0โ)) |
19 | 18 | biimpar 479 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ๐ด) โ 0) |
20 | 14, 17, 19 | divrec2d 11943 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ ((normโโ(๐โ๐ด)) / (normโโ๐ด)) = ((1 /
(normโโ๐ด)) ยท
(normโโ(๐โ๐ด)))) |
21 | 16, 19 | rereccld 11990 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (1 / (normโโ๐ด)) โ โ) |
22 | 21 | recnd 11191 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (1 / (normโโ๐ด)) โ โ) |
23 | | simpl 484 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ ๐ด โ
โ) |
24 | 8 | lnopmuli 30963 |
. . . . . . . 8
โข (((1 /
(normโโ๐ด)) โ โ โง ๐ด โ โ) โ (๐โ((1 /
(normโโ๐ด)) ยทโ ๐ด)) = ((1 /
(normโโ๐ด)) ยทโ (๐โ๐ด))) |
25 | 22, 23, 24 | syl2anc 585 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (๐โ((1 /
(normโโ๐ด)) ยทโ ๐ด)) = ((1 /
(normโโ๐ด)) ยทโ (๐โ๐ด))) |
26 | 25 | fveq2d 6850 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ(๐โ((1 /
(normโโ๐ด)) ยทโ ๐ด))) =
(normโโ((1 / (normโโ๐ด))
ยทโ (๐โ๐ด)))) |
27 | 10 | adantr 482 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (๐โ๐ด) โ
โ) |
28 | | norm-iii 30131 |
. . . . . . 7
โข (((1 /
(normโโ๐ด)) โ โ โง (๐โ๐ด) โ โ) โ
(normโโ((1 / (normโโ๐ด))
ยทโ (๐โ๐ด))) = ((absโ(1 /
(normโโ๐ด))) ยท
(normโโ(๐โ๐ด)))) |
29 | 22, 27, 28 | syl2anc 585 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ((1 /
(normโโ๐ด)) ยทโ (๐โ๐ด))) = ((absโ(1 /
(normโโ๐ด))) ยท
(normโโ(๐โ๐ด)))) |
30 | | normgt0 30118 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (๐ด โ 0โ
โ 0 < (normโโ๐ด))) |
31 | 30 | biimpa 478 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ 0 < (normโโ๐ด)) |
32 | 16, 31 | recgt0d 12097 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ 0 < (1 / (normโโ๐ด))) |
33 | | 0re 11165 |
. . . . . . . . . 10
โข 0 โ
โ |
34 | | ltle 11251 |
. . . . . . . . . 10
โข ((0
โ โ โง (1 / (normโโ๐ด)) โ โ) โ (0 < (1 /
(normโโ๐ด)) โ 0 โค (1 /
(normโโ๐ด)))) |
35 | 33, 34 | mpan 689 |
. . . . . . . . 9
โข ((1 /
(normโโ๐ด)) โ โ โ (0 < (1 /
(normโโ๐ด)) โ 0 โค (1 /
(normโโ๐ด)))) |
36 | 21, 32, 35 | sylc 65 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ 0 โค (1 / (normโโ๐ด))) |
37 | 21, 36 | absidd 15316 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (absโ(1 / (normโโ๐ด))) = (1 /
(normโโ๐ด))) |
38 | 37 | oveq1d 7376 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ ((absโ(1 / (normโโ๐ด))) ยท
(normโโ(๐โ๐ด))) = ((1 /
(normโโ๐ด)) ยท
(normโโ(๐โ๐ด)))) |
39 | 26, 29, 38 | 3eqtrrd 2778 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ ((1 / (normโโ๐ด)) ยท
(normโโ(๐โ๐ด))) = (normโโ(๐โ((1 /
(normโโ๐ด)) ยทโ ๐ด)))) |
40 | 20, 39 | eqtrd 2773 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ ((normโโ(๐โ๐ด)) / (normโโ๐ด)) =
(normโโ(๐โ((1 /
(normโโ๐ด)) ยทโ ๐ด)))) |
41 | | hvmulcl 30004 |
. . . . . 6
โข (((1 /
(normโโ๐ด)) โ โ โง ๐ด โ โ) โ ((1 /
(normโโ๐ด)) ยทโ ๐ด) โ
โ) |
42 | 22, 23, 41 | syl2anc 585 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ ((1 / (normโโ๐ด)) ยทโ ๐ด) โ
โ) |
43 | | normcl 30116 |
. . . . . . 7
โข (((1 /
(normโโ๐ด)) ยทโ ๐ด) โ โ โ
(normโโ((1 / (normโโ๐ด))
ยทโ ๐ด)) โ โ) |
44 | 42, 43 | syl 17 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ((1 /
(normโโ๐ด)) ยทโ ๐ด)) โ
โ) |
45 | | norm1 30240 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ((1 /
(normโโ๐ด)) ยทโ ๐ด)) = 1) |
46 | | eqle 11265 |
. . . . . 6
โข
(((normโโ((1 /
(normโโ๐ด)) ยทโ ๐ด)) โ โ โง
(normโโ((1 / (normโโ๐ด))
ยทโ ๐ด)) = 1) โ
(normโโ((1 / (normโโ๐ด))
ยทโ ๐ด)) โค 1) |
47 | 44, 45, 46 | syl2anc 585 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ((1 /
(normโโ๐ด)) ยทโ ๐ด)) โค 1) |
48 | | nmoplb 30898 |
. . . . . 6
โข ((๐: โโถ โ โง
((1 / (normโโ๐ด)) ยทโ ๐ด) โ โ โง
(normโโ((1 / (normโโ๐ด))
ยทโ ๐ด)) โค 1) โ
(normโโ(๐โ((1 /
(normโโ๐ด)) ยทโ ๐ด))) โค
(normopโ๐)) |
49 | 9, 48 | mp3an1 1449 |
. . . . 5
โข ((((1 /
(normโโ๐ด)) ยทโ ๐ด) โ โ โง
(normโโ((1 / (normโโ๐ด))
ยทโ ๐ด)) โค 1) โ
(normโโ(๐โ((1 /
(normโโ๐ด)) ยทโ ๐ด))) โค
(normopโ๐)) |
50 | 42, 47, 49 | syl2anc 585 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ(๐โ((1 /
(normโโ๐ด)) ยทโ ๐ด))) โค
(normopโ๐)) |
51 | 40, 50 | eqbrtrd 5131 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ ((normโโ(๐โ๐ด)) / (normโโ๐ด)) โค
(normopโ๐)) |
52 | | nmopre 30861 |
. . . . . 6
โข (๐ โ BndLinOp โ
(normopโ๐)
โ โ) |
53 | 6, 52 | ax-mp 5 |
. . . . 5
โข
(normopโ๐) โ โ |
54 | 53 | a1i 11 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normopโ๐) โ โ) |
55 | | ledivmul2 12042 |
. . . 4
โข
(((normโโ(๐โ๐ด)) โ โ โง
(normopโ๐)
โ โ โง ((normโโ๐ด) โ โ โง 0 <
(normโโ๐ด))) โ
(((normโโ(๐โ๐ด)) / (normโโ๐ด)) โค
(normopโ๐)
โ (normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด)))) |
56 | 13, 54, 16, 31, 55 | syl112anc 1375 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (((normโโ(๐โ๐ด)) / (normโโ๐ด)) โค
(normopโ๐)
โ (normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด)))) |
57 | 51, 56 | mpbid 231 |
. 2
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด))) |
58 | | 0le0 12262 |
. . . 4
โข 0 โค
0 |
59 | 8 | lnop0i 30961 |
. . . . . 6
โข (๐โ0โ) =
0โ |
60 | 59 | fveq2i 6849 |
. . . . 5
โข
(normโโ(๐โ0โ)) =
(normโโ0โ) |
61 | | norm0 30119 |
. . . . 5
โข
(normโโ0โ) =
0 |
62 | 60, 61 | eqtri 2761 |
. . . 4
โข
(normโโ(๐โ0โ)) =
0 |
63 | 61 | oveq2i 7372 |
. . . . 5
โข
((normopโ๐) ยท
(normโโ0โ)) =
((normopโ๐) ยท 0) |
64 | 53 | recni 11177 |
. . . . . 6
โข
(normopโ๐) โ โ |
65 | 64 | mul01i 11353 |
. . . . 5
โข
((normopโ๐) ยท 0) = 0 |
66 | 63, 65 | eqtri 2761 |
. . . 4
โข
((normopโ๐) ยท
(normโโ0โ)) = 0 |
67 | 58, 62, 66 | 3brtr4i 5139 |
. . 3
โข
(normโโ(๐โ0โ)) โค
((normopโ๐) ยท
(normโโ0โ)) |
68 | 67 | a1i 11 |
. 2
โข (๐ด โ โ โ
(normโโ(๐โ0โ)) โค
((normopโ๐) ยท
(normโโ0โ))) |
69 | 5, 57, 68 | pm2.61ne 3027 |
1
โข (๐ด โ โ โ
(normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด))) |