Step | Hyp | Ref
| Expression |
1 | | breq1 5109 |
. 2
โข
((normโโ(๐นโ๐ด)) = 0 โ
((normโโ(๐นโ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด)) โ 0 โค
((normopโ๐) ยท
(normโโ๐ด)))) |
2 | | cnlnadjlem.1 |
. . . . . . . . . 10
โข ๐ โ LinOp |
3 | | cnlnadjlem.2 |
. . . . . . . . . 10
โข ๐ โ ContOp |
4 | | cnlnadjlem.3 |
. . . . . . . . . 10
โข ๐บ = (๐ โ โ โฆ ((๐โ๐) ยทih ๐ฆ)) |
5 | | cnlnadjlem.4 |
. . . . . . . . . 10
โข ๐ต = (โฉ๐ค โ โ โ๐ฃ โ โ ((๐โ๐ฃ) ยทih ๐ฆ) = (๐ฃ ยทih ๐ค)) |
6 | | cnlnadjlem.5 |
. . . . . . . . . 10
โข ๐น = (๐ฆ โ โ โฆ ๐ต) |
7 | 2, 3, 4, 5, 6 | cnlnadjlem4 31054 |
. . . . . . . . 9
โข (๐ด โ โ โ (๐นโ๐ด) โ โ) |
8 | 2 | lnopfi 30953 |
. . . . . . . . . 10
โข ๐: โโถ
โ |
9 | 8 | ffvelcdmi 7035 |
. . . . . . . . 9
โข ((๐นโ๐ด) โ โ โ (๐โ(๐นโ๐ด)) โ โ) |
10 | 7, 9 | syl 17 |
. . . . . . . 8
โข (๐ด โ โ โ (๐โ(๐นโ๐ด)) โ โ) |
11 | | hicl 30064 |
. . . . . . . 8
โข (((๐โ(๐นโ๐ด)) โ โ โง ๐ด โ โ) โ ((๐โ(๐นโ๐ด)) ยทih ๐ด) โ
โ) |
12 | 10, 11 | mpancom 687 |
. . . . . . 7
โข (๐ด โ โ โ ((๐โ(๐นโ๐ด)) ยทih ๐ด) โ
โ) |
13 | 12 | abscld 15327 |
. . . . . 6
โข (๐ด โ โ โ
(absโ((๐โ(๐นโ๐ด)) ยทih ๐ด)) โ
โ) |
14 | | normcl 30109 |
. . . . . . . 8
โข ((๐โ(๐นโ๐ด)) โ โ โ
(normโโ(๐โ(๐นโ๐ด))) โ โ) |
15 | 10, 14 | syl 17 |
. . . . . . 7
โข (๐ด โ โ โ
(normโโ(๐โ(๐นโ๐ด))) โ โ) |
16 | | normcl 30109 |
. . . . . . 7
โข (๐ด โ โ โ
(normโโ๐ด) โ โ) |
17 | 15, 16 | remulcld 11190 |
. . . . . 6
โข (๐ด โ โ โ
((normโโ(๐โ(๐นโ๐ด))) ยท
(normโโ๐ด)) โ โ) |
18 | 2, 3 | nmcopexi 31011 |
. . . . . . . 8
โข
(normopโ๐) โ โ |
19 | | normcl 30109 |
. . . . . . . . 9
โข ((๐นโ๐ด) โ โ โ
(normโโ(๐นโ๐ด)) โ โ) |
20 | 7, 19 | syl 17 |
. . . . . . . 8
โข (๐ด โ โ โ
(normโโ(๐นโ๐ด)) โ โ) |
21 | | remulcl 11141 |
. . . . . . . 8
โข
(((normopโ๐) โ โ โง
(normโโ(๐นโ๐ด)) โ โ) โ
((normopโ๐) ยท
(normโโ(๐นโ๐ด))) โ โ) |
22 | 18, 20, 21 | sylancr 588 |
. . . . . . 7
โข (๐ด โ โ โ
((normopโ๐) ยท
(normโโ(๐นโ๐ด))) โ โ) |
23 | 22, 16 | remulcld 11190 |
. . . . . 6
โข (๐ด โ โ โ
(((normopโ๐) ยท
(normโโ(๐นโ๐ด))) ยท
(normโโ๐ด)) โ โ) |
24 | | bcs 30165 |
. . . . . . 7
โข (((๐โ(๐นโ๐ด)) โ โ โง ๐ด โ โ) โ (absโ((๐โ(๐นโ๐ด)) ยทih ๐ด)) โค
((normโโ(๐โ(๐นโ๐ด))) ยท
(normโโ๐ด))) |
25 | 10, 24 | mpancom 687 |
. . . . . 6
โข (๐ด โ โ โ
(absโ((๐โ(๐นโ๐ด)) ยทih ๐ด)) โค
((normโโ(๐โ(๐นโ๐ด))) ยท
(normโโ๐ด))) |
26 | | normge0 30110 |
. . . . . . 7
โข (๐ด โ โ โ 0 โค
(normโโ๐ด)) |
27 | 2, 3 | nmcoplbi 31012 |
. . . . . . . 8
โข ((๐นโ๐ด) โ โ โ
(normโโ(๐โ(๐นโ๐ด))) โค ((normopโ๐) ยท
(normโโ(๐นโ๐ด)))) |
28 | 7, 27 | syl 17 |
. . . . . . 7
โข (๐ด โ โ โ
(normโโ(๐โ(๐นโ๐ด))) โค ((normopโ๐) ยท
(normโโ(๐นโ๐ด)))) |
29 | 15, 22, 16, 26, 28 | lemul1ad 12099 |
. . . . . 6
โข (๐ด โ โ โ
((normโโ(๐โ(๐นโ๐ด))) ยท
(normโโ๐ด)) โค (((normopโ๐) ยท
(normโโ(๐นโ๐ด))) ยท
(normโโ๐ด))) |
30 | 13, 17, 23, 25, 29 | letrd 11317 |
. . . . 5
โข (๐ด โ โ โ
(absโ((๐โ(๐นโ๐ด)) ยทih ๐ด)) โค
(((normopโ๐) ยท
(normโโ(๐นโ๐ด))) ยท
(normโโ๐ด))) |
31 | 2, 3, 4, 5, 6 | cnlnadjlem5 31055 |
. . . . . . . 8
โข ((๐ด โ โ โง (๐นโ๐ด) โ โ) โ ((๐โ(๐นโ๐ด)) ยทih ๐ด) = ((๐นโ๐ด) ยทih (๐นโ๐ด))) |
32 | 7, 31 | mpdan 686 |
. . . . . . 7
โข (๐ด โ โ โ ((๐โ(๐นโ๐ด)) ยทih ๐ด) = ((๐นโ๐ด) ยทih (๐นโ๐ด))) |
33 | 32 | fveq2d 6847 |
. . . . . 6
โข (๐ด โ โ โ
(absโ((๐โ(๐นโ๐ด)) ยทih ๐ด)) = (absโ((๐นโ๐ด) ยทih (๐นโ๐ด)))) |
34 | | hiidrcl 30079 |
. . . . . . . 8
โข ((๐นโ๐ด) โ โ โ ((๐นโ๐ด) ยทih (๐นโ๐ด)) โ โ) |
35 | 7, 34 | syl 17 |
. . . . . . 7
โข (๐ด โ โ โ ((๐นโ๐ด) ยทih (๐นโ๐ด)) โ โ) |
36 | | hiidge0 30082 |
. . . . . . . 8
โข ((๐นโ๐ด) โ โ โ 0 โค ((๐นโ๐ด) ยทih (๐นโ๐ด))) |
37 | 7, 36 | syl 17 |
. . . . . . 7
โข (๐ด โ โ โ 0 โค
((๐นโ๐ด) ยทih (๐นโ๐ด))) |
38 | 35, 37 | absidd 15313 |
. . . . . 6
โข (๐ด โ โ โ
(absโ((๐นโ๐ด)
ยทih (๐นโ๐ด))) = ((๐นโ๐ด) ยทih (๐นโ๐ด))) |
39 | | normsq 30118 |
. . . . . . . 8
โข ((๐นโ๐ด) โ โ โ
((normโโ(๐นโ๐ด))โ2) = ((๐นโ๐ด) ยทih (๐นโ๐ด))) |
40 | 7, 39 | syl 17 |
. . . . . . 7
โข (๐ด โ โ โ
((normโโ(๐นโ๐ด))โ2) = ((๐นโ๐ด) ยทih (๐นโ๐ด))) |
41 | 20 | recnd 11188 |
. . . . . . . 8
โข (๐ด โ โ โ
(normโโ(๐นโ๐ด)) โ โ) |
42 | 41 | sqvald 14054 |
. . . . . . 7
โข (๐ด โ โ โ
((normโโ(๐นโ๐ด))โ2) =
((normโโ(๐นโ๐ด)) ยท
(normโโ(๐นโ๐ด)))) |
43 | 40, 42 | eqtr3d 2775 |
. . . . . 6
โข (๐ด โ โ โ ((๐นโ๐ด) ยทih (๐นโ๐ด)) = ((normโโ(๐นโ๐ด)) ยท
(normโโ(๐นโ๐ด)))) |
44 | 33, 38, 43 | 3eqtrd 2777 |
. . . . 5
โข (๐ด โ โ โ
(absโ((๐โ(๐นโ๐ด)) ยทih ๐ด)) =
((normโโ(๐นโ๐ด)) ยท
(normโโ(๐นโ๐ด)))) |
45 | 16 | recnd 11188 |
. . . . . 6
โข (๐ด โ โ โ
(normโโ๐ด) โ โ) |
46 | 18 | recni 11174 |
. . . . . . 7
โข
(normopโ๐) โ โ |
47 | | mul32 11326 |
. . . . . . 7
โข
(((normopโ๐) โ โ โง
(normโโ(๐นโ๐ด)) โ โ โง
(normโโ๐ด) โ โ) โ
(((normopโ๐) ยท
(normโโ(๐นโ๐ด))) ยท
(normโโ๐ด)) = (((normopโ๐) ยท
(normโโ๐ด)) ยท
(normโโ(๐นโ๐ด)))) |
48 | 46, 47 | mp3an1 1449 |
. . . . . 6
โข
(((normโโ(๐นโ๐ด)) โ โ โง
(normโโ๐ด) โ โ) โ
(((normopโ๐) ยท
(normโโ(๐นโ๐ด))) ยท
(normโโ๐ด)) = (((normopโ๐) ยท
(normโโ๐ด)) ยท
(normโโ(๐นโ๐ด)))) |
49 | 41, 45, 48 | syl2anc 585 |
. . . . 5
โข (๐ด โ โ โ
(((normopโ๐) ยท
(normโโ(๐นโ๐ด))) ยท
(normโโ๐ด)) = (((normopโ๐) ยท
(normโโ๐ด)) ยท
(normโโ(๐นโ๐ด)))) |
50 | 30, 44, 49 | 3brtr3d 5137 |
. . . 4
โข (๐ด โ โ โ
((normโโ(๐นโ๐ด)) ยท
(normโโ(๐นโ๐ด))) โค (((normopโ๐) ยท
(normโโ๐ด)) ยท
(normโโ(๐นโ๐ด)))) |
51 | 50 | adantr 482 |
. . 3
โข ((๐ด โ โ โง
(normโโ(๐นโ๐ด)) โ 0) โ
((normโโ(๐นโ๐ด)) ยท
(normโโ(๐นโ๐ด))) โค (((normopโ๐) ยท
(normโโ๐ด)) ยท
(normโโ(๐นโ๐ด)))) |
52 | 20 | adantr 482 |
. . . 4
โข ((๐ด โ โ โง
(normโโ(๐นโ๐ด)) โ 0) โ
(normโโ(๐นโ๐ด)) โ โ) |
53 | | remulcl 11141 |
. . . . . 6
โข
(((normopโ๐) โ โ โง
(normโโ๐ด) โ โ) โ
((normopโ๐) ยท
(normโโ๐ด)) โ โ) |
54 | 18, 16, 53 | sylancr 588 |
. . . . 5
โข (๐ด โ โ โ
((normopโ๐) ยท
(normโโ๐ด)) โ โ) |
55 | 54 | adantr 482 |
. . . 4
โข ((๐ด โ โ โง
(normโโ(๐นโ๐ด)) โ 0) โ
((normopโ๐) ยท
(normโโ๐ด)) โ โ) |
56 | | normge0 30110 |
. . . . . . 7
โข ((๐นโ๐ด) โ โ โ 0 โค
(normโโ(๐นโ๐ด))) |
57 | | 0re 11162 |
. . . . . . . 8
โข 0 โ
โ |
58 | | leltne 11249 |
. . . . . . . 8
โข ((0
โ โ โง (normโโ(๐นโ๐ด)) โ โ โง 0 โค
(normโโ(๐นโ๐ด))) โ (0 <
(normโโ(๐นโ๐ด)) โ
(normโโ(๐นโ๐ด)) โ 0)) |
59 | 57, 58 | mp3an1 1449 |
. . . . . . 7
โข
(((normโโ(๐นโ๐ด)) โ โ โง 0 โค
(normโโ(๐นโ๐ด))) โ (0 <
(normโโ(๐นโ๐ด)) โ
(normโโ(๐นโ๐ด)) โ 0)) |
60 | 19, 56, 59 | syl2anc 585 |
. . . . . 6
โข ((๐นโ๐ด) โ โ โ (0 <
(normโโ(๐นโ๐ด)) โ
(normโโ(๐นโ๐ด)) โ 0)) |
61 | 60 | biimpar 479 |
. . . . 5
โข (((๐นโ๐ด) โ โ โง
(normโโ(๐นโ๐ด)) โ 0) โ 0 <
(normโโ(๐นโ๐ด))) |
62 | 7, 61 | sylan 581 |
. . . 4
โข ((๐ด โ โ โง
(normโโ(๐นโ๐ด)) โ 0) โ 0 <
(normโโ(๐นโ๐ด))) |
63 | | lemul1 12012 |
. . . 4
โข
(((normโโ(๐นโ๐ด)) โ โ โง
((normopโ๐) ยท
(normโโ๐ด)) โ โ โง
((normโโ(๐นโ๐ด)) โ โ โง 0 <
(normโโ(๐นโ๐ด)))) โ
((normโโ(๐นโ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด)) โ
((normโโ(๐นโ๐ด)) ยท
(normโโ(๐นโ๐ด))) โค (((normopโ๐) ยท
(normโโ๐ด)) ยท
(normโโ(๐นโ๐ด))))) |
64 | 52, 55, 52, 62, 63 | syl112anc 1375 |
. . 3
โข ((๐ด โ โ โง
(normโโ(๐นโ๐ด)) โ 0) โ
((normโโ(๐นโ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด)) โ
((normโโ(๐นโ๐ด)) ยท
(normโโ(๐นโ๐ด))) โค (((normopโ๐) ยท
(normโโ๐ด)) ยท
(normโโ(๐นโ๐ด))))) |
65 | 51, 64 | mpbird 257 |
. 2
โข ((๐ด โ โ โง
(normโโ(๐นโ๐ด)) โ 0) โ
(normโโ(๐นโ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด))) |
66 | | nmopge0 30895 |
. . . . 5
โข (๐: โโถ โ โ
0 โค (normopโ๐)) |
67 | 8, 66 | ax-mp 5 |
. . . 4
โข 0 โค
(normopโ๐) |
68 | | mulge0 11678 |
. . . 4
โข
((((normopโ๐) โ โ โง 0 โค
(normopโ๐)) โง
((normโโ๐ด) โ โ โง 0 โค
(normโโ๐ด))) โ 0 โค
((normopโ๐) ยท
(normโโ๐ด))) |
69 | 18, 67, 68 | mpanl12 701 |
. . 3
โข
(((normโโ๐ด) โ โ โง 0 โค
(normโโ๐ด)) โ 0 โค
((normopโ๐) ยท
(normโโ๐ด))) |
70 | 16, 26, 69 | syl2anc 585 |
. 2
โข (๐ด โ โ โ 0 โค
((normopโ๐) ยท
(normโโ๐ด))) |
71 | 1, 65, 70 | pm2.61ne 3027 |
1
โข (๐ด โ โ โ
(normโโ(๐นโ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด))) |