Step | Hyp | Ref
| Expression |
1 | | nmophm.1 |
. . . . . . . . . . 11
โข ๐ โ
BndLinOp |
2 | | bdopf 30853 |
. . . . . . . . . . 11
โข (๐ โ BndLinOp โ ๐: โโถ
โ) |
3 | 1, 2 | ax-mp 5 |
. . . . . . . . . 10
โข ๐: โโถ
โ |
4 | | homval 30732 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐ฅ โ โ) โ
((๐ด
ยทop ๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
5 | 3, 4 | mp3an2 1450 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ฅ โ โ) โ ((๐ด ยทop
๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
6 | 5 | fveq2d 6850 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ฅ โ โ) โ
(normโโ((๐ด ยทop ๐)โ๐ฅ)) = (normโโ(๐ด
ยทโ (๐โ๐ฅ)))) |
7 | 3 | ffvelcdmi 7038 |
. . . . . . . . 9
โข (๐ฅ โ โ โ (๐โ๐ฅ) โ โ) |
8 | | norm-iii 30131 |
. . . . . . . . 9
โข ((๐ด โ โ โง (๐โ๐ฅ) โ โ) โ
(normโโ(๐ด ยทโ (๐โ๐ฅ))) = ((absโ๐ด) ยท
(normโโ(๐โ๐ฅ)))) |
9 | 7, 8 | sylan2 594 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ฅ โ โ) โ
(normโโ(๐ด ยทโ (๐โ๐ฅ))) = ((absโ๐ด) ยท
(normโโ(๐โ๐ฅ)))) |
10 | 6, 9 | eqtrd 2773 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ฅ โ โ) โ
(normโโ((๐ด ยทop ๐)โ๐ฅ)) = ((absโ๐ด) ยท
(normโโ(๐โ๐ฅ)))) |
11 | 10 | adantr 482 |
. . . . . 6
โข (((๐ด โ โ โง ๐ฅ โ โ) โง
(normโโ๐ฅ) โค 1) โ
(normโโ((๐ด ยทop ๐)โ๐ฅ)) = ((absโ๐ด) ยท
(normโโ(๐โ๐ฅ)))) |
12 | | normcl 30116 |
. . . . . . . . 9
โข ((๐โ๐ฅ) โ โ โ
(normโโ(๐โ๐ฅ)) โ โ) |
13 | 7, 12 | syl 17 |
. . . . . . . 8
โข (๐ฅ โ โ โ
(normโโ(๐โ๐ฅ)) โ โ) |
14 | 13 | ad2antlr 726 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ฅ โ โ) โง
(normโโ๐ฅ) โค 1) โ
(normโโ(๐โ๐ฅ)) โ โ) |
15 | | abscl 15172 |
. . . . . . . . 9
โข (๐ด โ โ โ
(absโ๐ด) โ
โ) |
16 | | absge0 15181 |
. . . . . . . . 9
โข (๐ด โ โ โ 0 โค
(absโ๐ด)) |
17 | 15, 16 | jca 513 |
. . . . . . . 8
โข (๐ด โ โ โ
((absโ๐ด) โ
โ โง 0 โค (absโ๐ด))) |
18 | 17 | ad2antrr 725 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ฅ โ โ) โง
(normโโ๐ฅ) โค 1) โ ((absโ๐ด) โ โ โง 0 โค
(absโ๐ด))) |
19 | | nmoplb 30898 |
. . . . . . . . 9
โข ((๐: โโถ โ โง
๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ(๐โ๐ฅ)) โค (normopโ๐)) |
20 | 3, 19 | mp3an1 1449 |
. . . . . . . 8
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ(๐โ๐ฅ)) โค (normopโ๐)) |
21 | 20 | adantll 713 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ฅ โ โ) โง
(normโโ๐ฅ) โค 1) โ
(normโโ(๐โ๐ฅ)) โค (normopโ๐)) |
22 | | nmopre 30861 |
. . . . . . . . 9
โข (๐ โ BndLinOp โ
(normopโ๐)
โ โ) |
23 | 1, 22 | ax-mp 5 |
. . . . . . . 8
โข
(normopโ๐) โ โ |
24 | | lemul2a 12018 |
. . . . . . . 8
โข
((((normโโ(๐โ๐ฅ)) โ โ โง
(normopโ๐)
โ โ โง ((absโ๐ด) โ โ โง 0 โค
(absโ๐ด))) โง
(normโโ(๐โ๐ฅ)) โค (normopโ๐)) โ ((absโ๐ด) ยท
(normโโ(๐โ๐ฅ))) โค ((absโ๐ด) ยท (normopโ๐))) |
25 | 23, 24 | mp3anl2 1457 |
. . . . . . 7
โข
((((normโโ(๐โ๐ฅ)) โ โ โง ((absโ๐ด) โ โ โง 0 โค
(absโ๐ด))) โง
(normโโ(๐โ๐ฅ)) โค (normopโ๐)) โ ((absโ๐ด) ยท
(normโโ(๐โ๐ฅ))) โค ((absโ๐ด) ยท (normopโ๐))) |
26 | 14, 18, 21, 25 | syl21anc 837 |
. . . . . 6
โข (((๐ด โ โ โง ๐ฅ โ โ) โง
(normโโ๐ฅ) โค 1) โ ((absโ๐ด) ยท
(normโโ(๐โ๐ฅ))) โค ((absโ๐ด) ยท (normopโ๐))) |
27 | 11, 26 | eqbrtrd 5131 |
. . . . 5
โข (((๐ด โ โ โง ๐ฅ โ โ) โง
(normโโ๐ฅ) โค 1) โ
(normโโ((๐ด ยทop ๐)โ๐ฅ)) โค ((absโ๐ด) ยท (normopโ๐))) |
28 | 27 | ex 414 |
. . . 4
โข ((๐ด โ โ โง ๐ฅ โ โ) โ
((normโโ๐ฅ) โค 1 โ
(normโโ((๐ด ยทop ๐)โ๐ฅ)) โค ((absโ๐ด) ยท (normopโ๐)))) |
29 | 28 | ralrimiva 3140 |
. . 3
โข (๐ด โ โ โ
โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โ
(normโโ((๐ด ยทop ๐)โ๐ฅ)) โค ((absโ๐ด) ยท (normopโ๐)))) |
30 | | homulcl 30750 |
. . . . 5
โข ((๐ด โ โ โง ๐: โโถ โ)
โ (๐ด
ยทop ๐): โโถ โ) |
31 | 3, 30 | mpan2 690 |
. . . 4
โข (๐ด โ โ โ (๐ด ยทop
๐): โโถ
โ) |
32 | | remulcl 11144 |
. . . . . 6
โข
(((absโ๐ด)
โ โ โง (normopโ๐) โ โ) โ ((absโ๐ด) ยท
(normopโ๐)) โ โ) |
33 | 15, 23, 32 | sylancl 587 |
. . . . 5
โข (๐ด โ โ โ
((absโ๐ด) ยท
(normopโ๐)) โ โ) |
34 | 33 | rexrd 11213 |
. . . 4
โข (๐ด โ โ โ
((absโ๐ด) ยท
(normopโ๐)) โ
โ*) |
35 | | nmopub 30899 |
. . . 4
โข (((๐ด ยทop
๐): โโถ โ
โง ((absโ๐ด)
ยท (normopโ๐)) โ โ*) โ
((normopโ(๐ด ยทop ๐)) โค ((absโ๐ด) ยท
(normopโ๐)) โ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โ
(normโโ((๐ด ยทop ๐)โ๐ฅ)) โค ((absโ๐ด) ยท (normopโ๐))))) |
36 | 31, 34, 35 | syl2anc 585 |
. . 3
โข (๐ด โ โ โ
((normopโ(๐ด ยทop ๐)) โค ((absโ๐ด) ยท
(normopโ๐)) โ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โ
(normโโ((๐ด ยทop ๐)โ๐ฅ)) โค ((absโ๐ด) ยท (normopโ๐))))) |
37 | 29, 36 | mpbird 257 |
. 2
โข (๐ด โ โ โ
(normopโ(๐ด
ยทop ๐)) โค ((absโ๐ด) ยท (normopโ๐))) |
38 | | fveq2 6846 |
. . . . . . . 8
โข (๐ด = 0 โ (absโ๐ด) =
(absโ0)) |
39 | | abs0 15179 |
. . . . . . . 8
โข
(absโ0) = 0 |
40 | 38, 39 | eqtrdi 2789 |
. . . . . . 7
โข (๐ด = 0 โ (absโ๐ด) = 0) |
41 | 40 | oveq1d 7376 |
. . . . . 6
โข (๐ด = 0 โ ((absโ๐ด) ยท
(normopโ๐)) = (0 ยท
(normopโ๐))) |
42 | 23 | recni 11177 |
. . . . . . 7
โข
(normopโ๐) โ โ |
43 | 42 | mul02i 11352 |
. . . . . 6
โข (0
ยท (normopโ๐)) = 0 |
44 | 41, 43 | eqtrdi 2789 |
. . . . 5
โข (๐ด = 0 โ ((absโ๐ด) ยท
(normopโ๐)) = 0) |
45 | 44 | adantl 483 |
. . . 4
โข ((๐ด โ โ โง ๐ด = 0) โ ((absโ๐ด) ยท
(normopโ๐)) = 0) |
46 | | nmopge0 30902 |
. . . . . 6
โข ((๐ด ยทop
๐): โโถ โ
โ 0 โค (normopโ(๐ด ยทop ๐))) |
47 | 31, 46 | syl 17 |
. . . . 5
โข (๐ด โ โ โ 0 โค
(normopโ(๐ด
ยทop ๐))) |
48 | 47 | adantr 482 |
. . . 4
โข ((๐ด โ โ โง ๐ด = 0) โ 0 โค
(normopโ(๐ด
ยทop ๐))) |
49 | 45, 48 | eqbrtrd 5131 |
. . 3
โข ((๐ด โ โ โง ๐ด = 0) โ ((absโ๐ด) ยท
(normopโ๐)) โค (normopโ(๐ด ยทop
๐))) |
50 | | nmoplb 30898 |
. . . . . . . . . . . 12
โข (((๐ด ยทop
๐): โโถ โ
โง ๐ฅ โ โ
โง (normโโ๐ฅ) โค 1) โ
(normโโ((๐ด ยทop ๐)โ๐ฅ)) โค (normopโ(๐ด ยทop
๐))) |
51 | 31, 50 | syl3an1 1164 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ((๐ด ยทop ๐)โ๐ฅ)) โค (normopโ(๐ด ยทop
๐))) |
52 | 51 | 3expa 1119 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ฅ โ โ) โง
(normโโ๐ฅ) โค 1) โ
(normโโ((๐ด ยทop ๐)โ๐ฅ)) โค (normopโ(๐ด ยทop
๐))) |
53 | 11, 52 | eqbrtrrd 5133 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ฅ โ โ) โง
(normโโ๐ฅ) โค 1) โ ((absโ๐ด) ยท
(normโโ(๐โ๐ฅ))) โค (normopโ(๐ด ยทop
๐))) |
54 | 53 | adantllr 718 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ฅ โ โ) โง
(normโโ๐ฅ) โค 1) โ ((absโ๐ด) ยท
(normโโ(๐โ๐ฅ))) โค (normopโ(๐ด ยทop
๐))) |
55 | 13 | adantl 483 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ฅ โ โ) โ
(normโโ(๐โ๐ฅ)) โ โ) |
56 | | nmopxr 30857 |
. . . . . . . . . . . . 13
โข ((๐ด ยทop
๐): โโถ โ
โ (normopโ(๐ด ยทop ๐)) โ
โ*) |
57 | 31, 56 | syl 17 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ
(normopโ(๐ด
ยทop ๐)) โ
โ*) |
58 | | nmopgtmnf 30859 |
. . . . . . . . . . . . 13
โข ((๐ด ยทop
๐): โโถ โ
โ -โ < (normopโ(๐ด ยทop ๐))) |
59 | 31, 58 | syl 17 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ -โ
< (normopโ(๐ด ยทop ๐))) |
60 | | xrre 13097 |
. . . . . . . . . . . 12
โข
((((normopโ(๐ด ยทop ๐)) โ โ*
โง ((absโ๐ด)
ยท (normopโ๐)) โ โ) โง (-โ <
(normopโ(๐ด
ยทop ๐)) โง (normopโ(๐ด ยทop
๐)) โค ((absโ๐ด) ยท
(normopโ๐)))) โ (normopโ(๐ด ยทop
๐)) โ
โ) |
61 | 57, 33, 59, 37, 60 | syl22anc 838 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(normopโ(๐ด
ยทop ๐)) โ โ) |
62 | 61 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ฅ โ โ) โ
(normopโ(๐ด
ยทop ๐)) โ โ) |
63 | 15 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ฅ โ โ) โ
(absโ๐ด) โ
โ) |
64 | | absgt0 15218 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ (๐ด โ 0 โ 0 <
(absโ๐ด))) |
65 | 64 | biimpa 478 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด โ 0) โ 0 <
(absโ๐ด)) |
66 | 65 | adantr 482 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ฅ โ โ) โ 0 <
(absโ๐ด)) |
67 | | lemuldiv2 12044 |
. . . . . . . . . 10
โข
(((normโโ(๐โ๐ฅ)) โ โ โง
(normopโ(๐ด
ยทop ๐)) โ โ โง ((absโ๐ด) โ โ โง 0 <
(absโ๐ด))) โ
(((absโ๐ด) ยท
(normโโ(๐โ๐ฅ))) โค (normopโ(๐ด ยทop
๐)) โ
(normโโ(๐โ๐ฅ)) โค ((normopโ(๐ด ยทop
๐)) / (absโ๐ด)))) |
68 | 55, 62, 63, 66, 67 | syl112anc 1375 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ฅ โ โ) โ
(((absโ๐ด) ยท
(normโโ(๐โ๐ฅ))) โค (normopโ(๐ด ยทop
๐)) โ
(normโโ(๐โ๐ฅ)) โค ((normopโ(๐ด ยทop
๐)) / (absโ๐ด)))) |
69 | 68 | adantr 482 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ฅ โ โ) โง
(normโโ๐ฅ) โค 1) โ (((absโ๐ด) ยท
(normโโ(๐โ๐ฅ))) โค (normopโ(๐ด ยทop
๐)) โ
(normโโ(๐โ๐ฅ)) โค ((normopโ(๐ด ยทop
๐)) / (absโ๐ด)))) |
70 | 54, 69 | mpbid 231 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ฅ โ โ) โง
(normโโ๐ฅ) โค 1) โ
(normโโ(๐โ๐ฅ)) โค ((normopโ(๐ด ยทop
๐)) / (absโ๐ด))) |
71 | 70 | ex 414 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ฅ โ โ) โ
((normโโ๐ฅ) โค 1 โ
(normโโ(๐โ๐ฅ)) โค ((normopโ(๐ด ยทop
๐)) / (absโ๐ด)))) |
72 | 71 | ralrimiva 3140 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0) โ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โ
(normโโ(๐โ๐ฅ)) โค ((normopโ(๐ด ยทop
๐)) / (absโ๐ด)))) |
73 | 61 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0) โ
(normopโ(๐ด
ยทop ๐)) โ โ) |
74 | 15 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0) โ (absโ๐ด) โ
โ) |
75 | | abs00 15183 |
. . . . . . . . . 10
โข (๐ด โ โ โ
((absโ๐ด) = 0 โ
๐ด = 0)) |
76 | 75 | necon3bid 2985 |
. . . . . . . . 9
โข (๐ด โ โ โ
((absโ๐ด) โ 0
โ ๐ด โ
0)) |
77 | 76 | biimpar 479 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0) โ (absโ๐ด) โ 0) |
78 | 73, 74, 77 | redivcld 11991 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0) โ
((normopโ(๐ด ยทop ๐)) / (absโ๐ด)) โ
โ) |
79 | 78 | rexrd 11213 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0) โ
((normopโ(๐ด ยทop ๐)) / (absโ๐ด)) โ
โ*) |
80 | | nmopub 30899 |
. . . . . 6
โข ((๐: โโถ โ โง
((normopโ(๐ด ยทop ๐)) / (absโ๐ด)) โ โ*)
โ ((normopโ๐) โค ((normopโ(๐ด ยทop
๐)) / (absโ๐ด)) โ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โ
(normโโ(๐โ๐ฅ)) โค ((normopโ(๐ด ยทop
๐)) / (absโ๐ด))))) |
81 | 3, 79, 80 | sylancr 588 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0) โ
((normopโ๐) โค ((normopโ(๐ด ยทop
๐)) / (absโ๐ด)) โ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โ
(normโโ(๐โ๐ฅ)) โค ((normopโ(๐ด ยทop
๐)) / (absโ๐ด))))) |
82 | 72, 81 | mpbird 257 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0) โ
(normopโ๐)
โค ((normopโ(๐ด ยทop ๐)) / (absโ๐ด))) |
83 | 23 | a1i 11 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0) โ
(normopโ๐)
โ โ) |
84 | | lemuldiv2 12044 |
. . . . 5
โข
(((normopโ๐) โ โ โง
(normopโ(๐ด
ยทop ๐)) โ โ โง ((absโ๐ด) โ โ โง 0 <
(absโ๐ด))) โ
(((absโ๐ด) ยท
(normopโ๐)) โค (normopโ(๐ด ยทop
๐)) โ
(normopโ๐)
โค ((normopโ(๐ด ยทop ๐)) / (absโ๐ด)))) |
85 | 83, 73, 74, 65, 84 | syl112anc 1375 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0) โ
(((absโ๐ด) ยท
(normopโ๐)) โค (normopโ(๐ด ยทop
๐)) โ
(normopโ๐)
โค ((normopโ(๐ด ยทop ๐)) / (absโ๐ด)))) |
86 | 82, 85 | mpbird 257 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 0) โ
((absโ๐ด) ยท
(normopโ๐)) โค (normopโ(๐ด ยทop
๐))) |
87 | 49, 86 | pm2.61dane 3029 |
. 2
โข (๐ด โ โ โ
((absโ๐ด) ยท
(normopโ๐)) โค (normopโ(๐ด ยทop
๐))) |
88 | 61, 33 | letri3d 11305 |
. 2
โข (๐ด โ โ โ
((normopโ(๐ด ยทop ๐)) = ((absโ๐ด) ยท
(normopโ๐)) โ ((normopโ(๐ด ยทop
๐)) โค ((absโ๐ด) ยท
(normopโ๐)) โง ((absโ๐ด) ยท (normopโ๐)) โค
(normopโ(๐ด
ยทop ๐))))) |
89 | 37, 87, 88 | mpbir2and 712 |
1
โข (๐ด โ โ โ
(normopโ(๐ด
ยทop ๐)) = ((absโ๐ด) ยท (normopโ๐))) |