Step | Hyp | Ref
| Expression |
1 | | nmopcoadj.1 |
. . . . . . 7
โข ๐ โ
BndLinOp |
2 | | adjbdlnb 31337 |
. . . . . . 7
โข (๐ โ BndLinOp โ
(adjโโ๐) โ BndLinOp) |
3 | 1, 2 | mpbi 229 |
. . . . . 6
โข
(adjโโ๐) โ BndLinOp |
4 | | bdopf 31115 |
. . . . . 6
โข
((adjโโ๐) โ BndLinOp โ
(adjโโ๐): โโถ โ) |
5 | 3, 4 | ax-mp 5 |
. . . . 5
โข
(adjโโ๐): โโถ โ |
6 | | bdopf 31115 |
. . . . . 6
โข (๐ โ BndLinOp โ ๐: โโถ
โ) |
7 | 1, 6 | ax-mp 5 |
. . . . 5
โข ๐: โโถ
โ |
8 | 5, 7 | hocofi 31019 |
. . . 4
โข
((adjโโ๐) โ ๐): โโถ โ |
9 | | nmopre 31123 |
. . . . . . 7
โข (๐ โ BndLinOp โ
(normopโ๐)
โ โ) |
10 | 1, 9 | ax-mp 5 |
. . . . . 6
โข
(normopโ๐) โ โ |
11 | 10 | resqcli 14150 |
. . . . 5
โข
((normopโ๐)โ2) โ โ |
12 | | rexr 11260 |
. . . . 5
โข
(((normopโ๐)โ2) โ โ โ
((normopโ๐)โ2) โ
โ*) |
13 | 11, 12 | ax-mp 5 |
. . . 4
โข
((normopโ๐)โ2) โ
โ* |
14 | | nmopub 31161 |
. . . 4
โข
((((adjโโ๐) โ ๐): โโถ โ โง
((normopโ๐)โ2) โ โ*) โ
((normopโ((adjโโ๐) โ ๐)) โค ((normopโ๐)โ2) โ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โ
(normโโ(((adjโโ๐) โ ๐)โ๐ฅ)) โค ((normopโ๐)โ2)))) |
15 | 8, 13, 14 | mp2an 691 |
. . 3
โข
((normopโ((adjโโ๐) โ ๐)) โค ((normopโ๐)โ2) โ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โ
(normโโ(((adjโโ๐) โ ๐)โ๐ฅ)) โค ((normopโ๐)โ2))) |
16 | 5, 7 | hocoi 31017 |
. . . . . . . 8
โข (๐ฅ โ โ โ
(((adjโโ๐) โ ๐)โ๐ฅ) = ((adjโโ๐)โ(๐โ๐ฅ))) |
17 | 16 | fveq2d 6896 |
. . . . . . 7
โข (๐ฅ โ โ โ
(normโโ(((adjโโ๐) โ ๐)โ๐ฅ)) =
(normโโ((adjโโ๐)โ(๐โ๐ฅ)))) |
18 | 17 | adantr 482 |
. . . . . 6
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ(((adjโโ๐) โ ๐)โ๐ฅ)) =
(normโโ((adjโโ๐)โ(๐โ๐ฅ)))) |
19 | 7 | ffvelcdmi 7086 |
. . . . . . . . 9
โข (๐ฅ โ โ โ (๐โ๐ฅ) โ โ) |
20 | 5 | ffvelcdmi 7086 |
. . . . . . . . 9
โข ((๐โ๐ฅ) โ โ โ
((adjโโ๐)โ(๐โ๐ฅ)) โ โ) |
21 | | normcl 30378 |
. . . . . . . . 9
โข
(((adjโโ๐)โ(๐โ๐ฅ)) โ โ โ
(normโโ((adjโโ๐)โ(๐โ๐ฅ))) โ โ) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . 8
โข (๐ฅ โ โ โ
(normโโ((adjโโ๐)โ(๐โ๐ฅ))) โ โ) |
23 | 22 | adantr 482 |
. . . . . . 7
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ((adjโโ๐)โ(๐โ๐ฅ))) โ โ) |
24 | | nmopre 31123 |
. . . . . . . . . 10
โข
((adjโโ๐) โ BndLinOp โ
(normopโ(adjโโ๐)) โ โ) |
25 | 3, 24 | ax-mp 5 |
. . . . . . . . 9
โข
(normopโ(adjโโ๐)) โ โ |
26 | | normcl 30378 |
. . . . . . . . . 10
โข ((๐โ๐ฅ) โ โ โ
(normโโ(๐โ๐ฅ)) โ โ) |
27 | 19, 26 | syl 17 |
. . . . . . . . 9
โข (๐ฅ โ โ โ
(normโโ(๐โ๐ฅ)) โ โ) |
28 | | remulcl 11195 |
. . . . . . . . 9
โข
(((normopโ(adjโโ๐)) โ โ โง
(normโโ(๐โ๐ฅ)) โ โ) โ
((normopโ(adjโโ๐)) ยท
(normโโ(๐โ๐ฅ))) โ โ) |
29 | 25, 27, 28 | sylancr 588 |
. . . . . . . 8
โข (๐ฅ โ โ โ
((normopโ(adjโโ๐)) ยท
(normโโ(๐โ๐ฅ))) โ โ) |
30 | 29 | adantr 482 |
. . . . . . 7
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normopโ(adjโโ๐)) ยท
(normโโ(๐โ๐ฅ))) โ โ) |
31 | 25, 10 | remulcli 11230 |
. . . . . . . 8
โข
((normopโ(adjโโ๐)) ยท
(normopโ๐)) โ โ |
32 | 31 | a1i 11 |
. . . . . . 7
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normopโ(adjโโ๐)) ยท (normopโ๐)) โ
โ) |
33 | 3 | nmbdoplbi 31277 |
. . . . . . . . 9
โข ((๐โ๐ฅ) โ โ โ
(normโโ((adjโโ๐)โ(๐โ๐ฅ))) โค
((normopโ(adjโโ๐)) ยท
(normโโ(๐โ๐ฅ)))) |
34 | 19, 33 | syl 17 |
. . . . . . . 8
โข (๐ฅ โ โ โ
(normโโ((adjโโ๐)โ(๐โ๐ฅ))) โค
((normopโ(adjโโ๐)) ยท
(normโโ(๐โ๐ฅ)))) |
35 | 34 | adantr 482 |
. . . . . . 7
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ((adjโโ๐)โ(๐โ๐ฅ))) โค
((normopโ(adjโโ๐)) ยท
(normโโ(๐โ๐ฅ)))) |
36 | 27 | adantr 482 |
. . . . . . . 8
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ(๐โ๐ฅ)) โ โ) |
37 | 10 | a1i 11 |
. . . . . . . 8
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normopโ๐)
โ โ) |
38 | | normcl 30378 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ
(normโโ๐ฅ) โ โ) |
39 | | remulcl 11195 |
. . . . . . . . . . 11
โข
(((normopโ๐) โ โ โง
(normโโ๐ฅ) โ โ) โ
((normopโ๐) ยท
(normโโ๐ฅ)) โ โ) |
40 | 10, 38, 39 | sylancr 588 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ
((normopโ๐) ยท
(normโโ๐ฅ)) โ โ) |
41 | 40 | adantr 482 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normopโ๐) ยท
(normโโ๐ฅ)) โ โ) |
42 | 1 | nmbdoplbi 31277 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ
(normโโ(๐โ๐ฅ)) โค ((normopโ๐) ยท
(normโโ๐ฅ))) |
43 | 42 | adantr 482 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ(๐โ๐ฅ)) โค ((normopโ๐) ยท
(normโโ๐ฅ))) |
44 | | 1re 11214 |
. . . . . . . . . . . 12
โข 1 โ
โ |
45 | | nmopge0 31164 |
. . . . . . . . . . . . . . 15
โข (๐: โโถ โ โ
0 โค (normopโ๐)) |
46 | 1, 6, 45 | mp2b 10 |
. . . . . . . . . . . . . 14
โข 0 โค
(normopโ๐) |
47 | 10, 46 | pm3.2i 472 |
. . . . . . . . . . . . 13
โข
((normopโ๐) โ โ โง 0 โค
(normopโ๐)) |
48 | | lemul2a 12069 |
. . . . . . . . . . . . 13
โข
((((normโโ๐ฅ) โ โ โง 1 โ โ โง
((normopโ๐) โ โ โง 0 โค
(normopโ๐))) โง
(normโโ๐ฅ) โค 1) โ
((normopโ๐) ยท
(normโโ๐ฅ)) โค ((normopโ๐) ยท 1)) |
49 | 47, 48 | mp3anl3 1458 |
. . . . . . . . . . . 12
โข
((((normโโ๐ฅ) โ โ โง 1 โ โ)
โง (normโโ๐ฅ) โค 1) โ
((normopโ๐) ยท
(normโโ๐ฅ)) โค ((normopโ๐) ยท 1)) |
50 | 44, 49 | mpanl2 700 |
. . . . . . . . . . 11
โข
(((normโโ๐ฅ) โ โ โง
(normโโ๐ฅ) โค 1) โ
((normopโ๐) ยท
(normโโ๐ฅ)) โค ((normopโ๐) ยท 1)) |
51 | 38, 50 | sylan 581 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normopโ๐) ยท
(normโโ๐ฅ)) โค ((normopโ๐) ยท 1)) |
52 | 10 | recni 11228 |
. . . . . . . . . . 11
โข
(normopโ๐) โ โ |
53 | 52 | mulridi 11218 |
. . . . . . . . . 10
โข
((normopโ๐) ยท 1) =
(normopโ๐) |
54 | 51, 53 | breqtrdi 5190 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normopโ๐) ยท
(normโโ๐ฅ)) โค (normopโ๐)) |
55 | 36, 41, 37, 43, 54 | letrd 11371 |
. . . . . . . 8
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ(๐โ๐ฅ)) โค (normopโ๐)) |
56 | | nmopge0 31164 |
. . . . . . . . . . 11
โข
((adjโโ๐): โโถ โ โ 0 โค
(normopโ(adjโโ๐))) |
57 | 3, 4, 56 | mp2b 10 |
. . . . . . . . . 10
โข 0 โค
(normopโ(adjโโ๐)) |
58 | 25, 57 | pm3.2i 472 |
. . . . . . . . 9
โข
((normopโ(adjโโ๐)) โ โ โง 0 โค
(normopโ(adjโโ๐))) |
59 | | lemul2a 12069 |
. . . . . . . . 9
โข
((((normโโ(๐โ๐ฅ)) โ โ โง
(normopโ๐)
โ โ โง
((normopโ(adjโโ๐)) โ โ โง 0 โค
(normopโ(adjโโ๐)))) โง
(normโโ(๐โ๐ฅ)) โค (normopโ๐)) โ
((normopโ(adjโโ๐)) ยท
(normโโ(๐โ๐ฅ))) โค
((normopโ(adjโโ๐)) ยท (normopโ๐))) |
60 | 58, 59 | mp3anl3 1458 |
. . . . . . . 8
โข
((((normโโ(๐โ๐ฅ)) โ โ โง
(normopโ๐)
โ โ) โง (normโโ(๐โ๐ฅ)) โค (normopโ๐)) โ
((normopโ(adjโโ๐)) ยท
(normโโ(๐โ๐ฅ))) โค
((normopโ(adjโโ๐)) ยท (normopโ๐))) |
61 | 36, 37, 55, 60 | syl21anc 837 |
. . . . . . 7
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normopโ(adjโโ๐)) ยท
(normโโ(๐โ๐ฅ))) โค
((normopโ(adjโโ๐)) ยท (normopโ๐))) |
62 | 23, 30, 32, 35, 61 | letrd 11371 |
. . . . . 6
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ((adjโโ๐)โ(๐โ๐ฅ))) โค
((normopโ(adjโโ๐)) ยท (normopโ๐))) |
63 | 18, 62 | eqbrtrd 5171 |
. . . . 5
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ(((adjโโ๐) โ ๐)โ๐ฅ)) โค
((normopโ(adjโโ๐)) ยท (normopโ๐))) |
64 | 1 | nmopadji 31343 |
. . . . . . 7
โข
(normopโ(adjโโ๐)) = (normopโ๐) |
65 | 64 | oveq1i 7419 |
. . . . . 6
โข
((normopโ(adjโโ๐)) ยท
(normopโ๐)) = ((normopโ๐) ยท
(normopโ๐)) |
66 | 52 | sqvali 14144 |
. . . . . 6
โข
((normopโ๐)โ2) = ((normopโ๐) ยท
(normopโ๐)) |
67 | 65, 66 | eqtr4i 2764 |
. . . . 5
โข
((normopโ(adjโโ๐)) ยท
(normopโ๐)) = ((normopโ๐)โ2) |
68 | 63, 67 | breqtrdi 5190 |
. . . 4
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ(((adjโโ๐) โ ๐)โ๐ฅ)) โค ((normopโ๐)โ2)) |
69 | 68 | ex 414 |
. . 3
โข (๐ฅ โ โ โ
((normโโ๐ฅ) โค 1 โ
(normโโ(((adjโโ๐) โ ๐)โ๐ฅ)) โค ((normopโ๐)โ2))) |
70 | 15, 69 | mprgbir 3069 |
. 2
โข
(normopโ((adjโโ๐) โ ๐)) โค ((normopโ๐)โ2) |
71 | | nmopge0 31164 |
. . . . . . . 8
โข
(((adjโโ๐) โ ๐): โโถ โ โ 0 โค
(normopโ((adjโโ๐) โ ๐))) |
72 | 8, 71 | ax-mp 5 |
. . . . . . 7
โข 0 โค
(normopโ((adjโโ๐) โ ๐)) |
73 | 3, 1 | bdopcoi 31351 |
. . . . . . . . 9
โข
((adjโโ๐) โ ๐) โ BndLinOp |
74 | | nmopre 31123 |
. . . . . . . . 9
โข
(((adjโโ๐) โ ๐) โ BndLinOp โ
(normopโ((adjโโ๐) โ ๐)) โ โ) |
75 | 73, 74 | ax-mp 5 |
. . . . . . . 8
โข
(normopโ((adjโโ๐) โ ๐)) โ โ |
76 | 75 | sqrtcli 15318 |
. . . . . . 7
โข (0 โค
(normopโ((adjโโ๐) โ ๐)) โ
(โโ(normopโ((adjโโ๐) โ ๐))) โ โ) |
77 | | rexr 11260 |
. . . . . . 7
โข
((โโ(normopโ((adjโโ๐) โ ๐))) โ โ โ
(โโ(normopโ((adjโโ๐) โ ๐))) โ โ*) |
78 | 72, 76, 77 | mp2b 10 |
. . . . . 6
โข
(โโ(normopโ((adjโโ๐) โ ๐))) โ โ* |
79 | | nmopub 31161 |
. . . . . 6
โข ((๐: โโถ โ โง
(โโ(normopโ((adjโโ๐) โ ๐))) โ โ*) โ
((normopโ๐) โค
(โโ(normopโ((adjโโ๐) โ ๐))) โ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โ
(normโโ(๐โ๐ฅ)) โค
(โโ(normopโ((adjโโ๐) โ ๐)))))) |
80 | 7, 78, 79 | mp2an 691 |
. . . . 5
โข
((normopโ๐) โค
(โโ(normopโ((adjโโ๐) โ ๐))) โ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โ
(normโโ(๐โ๐ฅ)) โค
(โโ(normopโ((adjโโ๐) โ ๐))))) |
81 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ
((adjโโ๐)โ(๐โ๐ฅ)) โ โ) |
82 | | hicl 30333 |
. . . . . . . . . . . 12
โข
((((adjโโ๐)โ(๐โ๐ฅ)) โ โ โง ๐ฅ โ โ) โ
(((adjโโ๐)โ(๐โ๐ฅ)) ยทih ๐ฅ) โ
โ) |
83 | 81, 82 | mpancom 687 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ
(((adjโโ๐)โ(๐โ๐ฅ)) ยทih ๐ฅ) โ
โ) |
84 | 83 | abscld 15383 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ
(absโ(((adjโโ๐)โ(๐โ๐ฅ)) ยทih ๐ฅ)) โ
โ) |
85 | 84 | adantr 482 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(absโ(((adjโโ๐)โ(๐โ๐ฅ)) ยทih ๐ฅ)) โ
โ) |
86 | 22, 38 | remulcld 11244 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) ยท
(normโโ๐ฅ)) โ โ) |
87 | 86 | adantr 482 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) ยท
(normโโ๐ฅ)) โ โ) |
88 | 75 | a1i 11 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normopโ((adjโโ๐) โ ๐)) โ โ) |
89 | | bcs 30434 |
. . . . . . . . . . 11
โข
((((adjโโ๐)โ(๐โ๐ฅ)) โ โ โง ๐ฅ โ โ) โ
(absโ(((adjโโ๐)โ(๐โ๐ฅ)) ยทih ๐ฅ)) โค
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) ยท
(normโโ๐ฅ))) |
90 | 81, 89 | mpancom 687 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ
(absโ(((adjโโ๐)โ(๐โ๐ฅ)) ยทih ๐ฅ)) โค
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) ยท
(normโโ๐ฅ))) |
91 | 90 | adantr 482 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(absโ(((adjโโ๐)โ(๐โ๐ฅ)) ยทih ๐ฅ)) โค
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) ยท
(normโโ๐ฅ))) |
92 | 5, 7 | hococli 31018 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ
(((adjโโ๐) โ ๐)โ๐ฅ) โ โ) |
93 | | normcl 30378 |
. . . . . . . . . . . 12
โข
((((adjโโ๐) โ ๐)โ๐ฅ) โ โ โ
(normโโ(((adjโโ๐) โ ๐)โ๐ฅ)) โ โ) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ
(normโโ(((adjโโ๐) โ ๐)โ๐ฅ)) โ โ) |
95 | 94 | adantr 482 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ(((adjโโ๐) โ ๐)โ๐ฅ)) โ โ) |
96 | 38 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ๐ฅ) โ โ) |
97 | | normge0 30379 |
. . . . . . . . . . . . . . 15
โข
(((adjโโ๐)โ(๐โ๐ฅ)) โ โ โ 0 โค
(normโโ((adjโโ๐)โ(๐โ๐ฅ)))) |
98 | 19, 20, 97 | 3syl 18 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ 0 โค
(normโโ((adjโโ๐)โ(๐โ๐ฅ)))) |
99 | 22, 98 | jca 513 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ โ
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) โ โ โง 0 โค
(normโโ((adjโโ๐)โ(๐โ๐ฅ))))) |
100 | 99 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) โ โ โง 0 โค
(normโโ((adjโโ๐)โ(๐โ๐ฅ))))) |
101 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ๐ฅ) โค 1) |
102 | | lemul2a 12069 |
. . . . . . . . . . . . 13
โข
((((normโโ๐ฅ) โ โ โง 1 โ โ โง
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) โ โ โง 0 โค
(normโโ((adjโโ๐)โ(๐โ๐ฅ))))) โง
(normโโ๐ฅ) โค 1) โ
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) ยท
(normโโ๐ฅ)) โค
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) ยท 1)) |
103 | 44, 102 | mp3anl2 1457 |
. . . . . . . . . . . 12
โข
((((normโโ๐ฅ) โ โ โง
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) โ โ โง 0 โค
(normโโ((adjโโ๐)โ(๐โ๐ฅ))))) โง
(normโโ๐ฅ) โค 1) โ
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) ยท
(normโโ๐ฅ)) โค
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) ยท 1)) |
104 | 96, 100, 101, 103 | syl21anc 837 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) ยท
(normโโ๐ฅ)) โค
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) ยท 1)) |
105 | 22 | recnd 11242 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ
(normโโ((adjโโ๐)โ(๐โ๐ฅ))) โ โ) |
106 | 105 | mulridd 11231 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ โ
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) ยท 1) =
(normโโ((adjโโ๐)โ(๐โ๐ฅ)))) |
107 | 106, 17 | eqtr4d 2776 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) ยท 1) =
(normโโ(((adjโโ๐) โ ๐)โ๐ฅ))) |
108 | 107 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) ยท 1) =
(normโโ(((adjโโ๐) โ ๐)โ๐ฅ))) |
109 | 104, 108 | breqtrd 5175 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) ยท
(normโโ๐ฅ)) โค
(normโโ(((adjโโ๐) โ ๐)โ๐ฅ))) |
110 | | remulcl 11195 |
. . . . . . . . . . . . 13
โข
(((normopโ((adjโโ๐) โ ๐)) โ โ โง
(normโโ๐ฅ) โ โ) โ
((normopโ((adjโโ๐) โ ๐)) ยท
(normโโ๐ฅ)) โ โ) |
111 | 75, 38, 110 | sylancr 588 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ
((normopโ((adjโโ๐) โ ๐)) ยท
(normโโ๐ฅ)) โ โ) |
112 | 111 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normopโ((adjโโ๐) โ ๐)) ยท
(normโโ๐ฅ)) โ โ) |
113 | 73 | nmbdoplbi 31277 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ
(normโโ(((adjโโ๐) โ ๐)โ๐ฅ)) โค
((normopโ((adjโโ๐) โ ๐)) ยท
(normโโ๐ฅ))) |
114 | 113 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ(((adjโโ๐) โ ๐)โ๐ฅ)) โค
((normopโ((adjโโ๐) โ ๐)) ยท
(normโโ๐ฅ))) |
115 | 75, 72 | pm3.2i 472 |
. . . . . . . . . . . . . . 15
โข
((normopโ((adjโโ๐) โ ๐)) โ โ โง 0 โค
(normopโ((adjโโ๐) โ ๐))) |
116 | | lemul2a 12069 |
. . . . . . . . . . . . . . 15
โข
((((normโโ๐ฅ) โ โ โง 1 โ โ โง
((normopโ((adjโโ๐) โ ๐)) โ โ โง 0 โค
(normopโ((adjโโ๐) โ ๐)))) โง
(normโโ๐ฅ) โค 1) โ
((normopโ((adjโโ๐) โ ๐)) ยท
(normโโ๐ฅ)) โค
((normopโ((adjโโ๐) โ ๐)) ยท 1)) |
117 | 115, 116 | mp3anl3 1458 |
. . . . . . . . . . . . . 14
โข
((((normโโ๐ฅ) โ โ โง 1 โ โ)
โง (normโโ๐ฅ) โค 1) โ
((normopโ((adjโโ๐) โ ๐)) ยท
(normโโ๐ฅ)) โค
((normopโ((adjโโ๐) โ ๐)) ยท 1)) |
118 | 44, 117 | mpanl2 700 |
. . . . . . . . . . . . 13
โข
(((normโโ๐ฅ) โ โ โง
(normโโ๐ฅ) โค 1) โ
((normopโ((adjโโ๐) โ ๐)) ยท
(normโโ๐ฅ)) โค
((normopโ((adjโโ๐) โ ๐)) ยท 1)) |
119 | 38, 118 | sylan 581 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normopโ((adjโโ๐) โ ๐)) ยท
(normโโ๐ฅ)) โค
((normopโ((adjโโ๐) โ ๐)) ยท 1)) |
120 | 75 | recni 11228 |
. . . . . . . . . . . . 13
โข
(normopโ((adjโโ๐) โ ๐)) โ โ |
121 | 120 | mulridi 11218 |
. . . . . . . . . . . 12
โข
((normopโ((adjโโ๐) โ ๐)) ยท 1) =
(normopโ((adjโโ๐) โ ๐)) |
122 | 119, 121 | breqtrdi 5190 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normopโ((adjโโ๐) โ ๐)) ยท
(normโโ๐ฅ)) โค
(normopโ((adjโโ๐) โ ๐))) |
123 | 95, 112, 88, 114, 122 | letrd 11371 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ(((adjโโ๐) โ ๐)โ๐ฅ)) โค
(normopโ((adjโโ๐) โ ๐))) |
124 | 87, 95, 88, 109, 123 | letrd 11371 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normโโ((adjโโ๐)โ(๐โ๐ฅ))) ยท
(normโโ๐ฅ)) โค
(normopโ((adjโโ๐) โ ๐))) |
125 | 85, 87, 88, 91, 124 | letrd 11371 |
. . . . . . . 8
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(absโ(((adjโโ๐)โ(๐โ๐ฅ)) ยทih ๐ฅ)) โค
(normopโ((adjโโ๐) โ ๐))) |
126 | | resqcl 14089 |
. . . . . . . . . . . 12
โข
((normโโ(๐โ๐ฅ)) โ โ โ
((normโโ(๐โ๐ฅ))โ2) โ โ) |
127 | | sqge0 14101 |
. . . . . . . . . . . 12
โข
((normโโ(๐โ๐ฅ)) โ โ โ 0 โค
((normโโ(๐โ๐ฅ))โ2)) |
128 | 126, 127 | absidd 15369 |
. . . . . . . . . . 11
โข
((normโโ(๐โ๐ฅ)) โ โ โ
(absโ((normโโ(๐โ๐ฅ))โ2)) =
((normโโ(๐โ๐ฅ))โ2)) |
129 | 19, 26, 128 | 3syl 18 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ
(absโ((normโโ(๐โ๐ฅ))โ2)) =
((normโโ(๐โ๐ฅ))โ2)) |
130 | | normsq 30387 |
. . . . . . . . . . . . 13
โข ((๐โ๐ฅ) โ โ โ
((normโโ(๐โ๐ฅ))โ2) = ((๐โ๐ฅ) ยทih (๐โ๐ฅ))) |
131 | 19, 130 | syl 17 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ
((normโโ(๐โ๐ฅ))โ2) = ((๐โ๐ฅ) ยทih (๐โ๐ฅ))) |
132 | | bdopadj 31335 |
. . . . . . . . . . . . . . . 16
โข
((adjโโ๐) โ BndLinOp โ
(adjโโ๐) โ dom
adjโ) |
133 | 3, 132 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข
(adjโโ๐) โ dom
adjโ |
134 | | adj2 31187 |
. . . . . . . . . . . . . . 15
โข
(((adjโโ๐) โ dom adjโ โง
(๐โ๐ฅ) โ โ โง ๐ฅ โ โ) โ
(((adjโโ๐)โ(๐โ๐ฅ)) ยทih ๐ฅ) = ((๐โ๐ฅ) ยทih
((adjโโ(adjโโ๐))โ๐ฅ))) |
135 | 133, 134 | mp3an1 1449 |
. . . . . . . . . . . . . 14
โข (((๐โ๐ฅ) โ โ โง ๐ฅ โ โ) โ
(((adjโโ๐)โ(๐โ๐ฅ)) ยทih ๐ฅ) = ((๐โ๐ฅ) ยทih
((adjโโ(adjโโ๐))โ๐ฅ))) |
136 | 19, 135 | mpancom 687 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ โ
(((adjโโ๐)โ(๐โ๐ฅ)) ยทih ๐ฅ) = ((๐โ๐ฅ) ยทih
((adjโโ(adjโโ๐))โ๐ฅ))) |
137 | | bdopadj 31335 |
. . . . . . . . . . . . . . . 16
โข (๐ โ BndLinOp โ ๐ โ dom
adjโ) |
138 | | adjadj 31189 |
. . . . . . . . . . . . . . . 16
โข (๐ โ dom
adjโ โ
(adjโโ(adjโโ๐)) = ๐) |
139 | 1, 137, 138 | mp2b 10 |
. . . . . . . . . . . . . . 15
โข
(adjโโ(adjโโ๐)) = ๐ |
140 | 139 | fveq1i 6893 |
. . . . . . . . . . . . . 14
โข
((adjโโ(adjโโ๐))โ๐ฅ) = (๐โ๐ฅ) |
141 | 140 | oveq2i 7420 |
. . . . . . . . . . . . 13
โข ((๐โ๐ฅ) ยทih
((adjโโ(adjโโ๐))โ๐ฅ)) = ((๐โ๐ฅ) ยทih (๐โ๐ฅ)) |
142 | 136, 141 | eqtr2di 2790 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ ((๐โ๐ฅ) ยทih (๐โ๐ฅ)) = (((adjโโ๐)โ(๐โ๐ฅ)) ยทih ๐ฅ)) |
143 | 131, 142 | eqtrd 2773 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ
((normโโ(๐โ๐ฅ))โ2) =
(((adjโโ๐)โ(๐โ๐ฅ)) ยทih ๐ฅ)) |
144 | 143 | fveq2d 6896 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ
(absโ((normโโ(๐โ๐ฅ))โ2)) =
(absโ(((adjโโ๐)โ(๐โ๐ฅ)) ยทih ๐ฅ))) |
145 | 129, 144 | eqtr3d 2775 |
. . . . . . . . 9
โข (๐ฅ โ โ โ
((normโโ(๐โ๐ฅ))โ2) =
(absโ(((adjโโ๐)โ(๐โ๐ฅ)) ยทih ๐ฅ))) |
146 | 145 | adantr 482 |
. . . . . . . 8
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normโโ(๐โ๐ฅ))โ2) =
(absโ(((adjโโ๐)โ(๐โ๐ฅ)) ยทih ๐ฅ))) |
147 | 75 | sqsqrti 15322 |
. . . . . . . . . 10
โข (0 โค
(normopโ((adjโโ๐) โ ๐)) โ
((โโ(normopโ((adjโโ๐) โ ๐)))โ2) =
(normopโ((adjโโ๐) โ ๐))) |
148 | 8, 71, 147 | mp2b 10 |
. . . . . . . . 9
โข
((โโ(normopโ((adjโโ๐) โ ๐)))โ2) =
(normopโ((adjโโ๐) โ ๐)) |
149 | 148 | a1i 11 |
. . . . . . . 8
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((โโ(normopโ((adjโโ๐) โ ๐)))โ2) =
(normopโ((adjโโ๐) โ ๐))) |
150 | 125, 146,
149 | 3brtr4d 5181 |
. . . . . . 7
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normโโ(๐โ๐ฅ))โ2) โค
((โโ(normopโ((adjโโ๐) โ ๐)))โ2)) |
151 | | normge0 30379 |
. . . . . . . . . 10
โข ((๐โ๐ฅ) โ โ โ 0 โค
(normโโ(๐โ๐ฅ))) |
152 | 19, 151 | syl 17 |
. . . . . . . . 9
โข (๐ฅ โ โ โ 0 โค
(normโโ(๐โ๐ฅ))) |
153 | 8, 71, 76 | mp2b 10 |
. . . . . . . . . 10
โข
(โโ(normopโ((adjโโ๐) โ ๐))) โ โ |
154 | 75 | sqrtge0i 15323 |
. . . . . . . . . . 11
โข (0 โค
(normopโ((adjโโ๐) โ ๐)) โ 0 โค
(โโ(normopโ((adjโโ๐) โ ๐)))) |
155 | 8, 71, 154 | mp2b 10 |
. . . . . . . . . 10
โข 0 โค
(โโ(normopโ((adjโโ๐) โ ๐))) |
156 | | le2sq 14099 |
. . . . . . . . . 10
โข
((((normโโ(๐โ๐ฅ)) โ โ โง 0 โค
(normโโ(๐โ๐ฅ))) โง
((โโ(normopโ((adjโโ๐) โ ๐))) โ โ โง 0 โค
(โโ(normopโ((adjโโ๐) โ ๐))))) โ
((normโโ(๐โ๐ฅ)) โค
(โโ(normopโ((adjโโ๐) โ ๐))) โ
((normโโ(๐โ๐ฅ))โ2) โค
((โโ(normopโ((adjโโ๐) โ ๐)))โ2))) |
157 | 153, 155,
156 | mpanr12 704 |
. . . . . . . . 9
โข
(((normโโ(๐โ๐ฅ)) โ โ โง 0 โค
(normโโ(๐โ๐ฅ))) โ
((normโโ(๐โ๐ฅ)) โค
(โโ(normopโ((adjโโ๐) โ ๐))) โ
((normโโ(๐โ๐ฅ))โ2) โค
((โโ(normopโ((adjโโ๐) โ ๐)))โ2))) |
158 | 27, 152, 157 | syl2anc 585 |
. . . . . . . 8
โข (๐ฅ โ โ โ
((normโโ(๐โ๐ฅ)) โค
(โโ(normopโ((adjโโ๐) โ ๐))) โ
((normโโ(๐โ๐ฅ))โ2) โค
((โโ(normopโ((adjโโ๐) โ ๐)))โ2))) |
159 | 158 | adantr 482 |
. . . . . . 7
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
((normโโ(๐โ๐ฅ)) โค
(โโ(normopโ((adjโโ๐) โ ๐))) โ
((normโโ(๐โ๐ฅ))โ2) โค
((โโ(normopโ((adjโโ๐) โ ๐)))โ2))) |
160 | 150, 159 | mpbird 257 |
. . . . . 6
โข ((๐ฅ โ โ โง
(normโโ๐ฅ) โค 1) โ
(normโโ(๐โ๐ฅ)) โค
(โโ(normopโ((adjโโ๐) โ ๐)))) |
161 | 160 | ex 414 |
. . . . 5
โข (๐ฅ โ โ โ
((normโโ๐ฅ) โค 1 โ
(normโโ(๐โ๐ฅ)) โค
(โโ(normopโ((adjโโ๐) โ ๐))))) |
162 | 80, 161 | mprgbir 3069 |
. . . 4
โข
(normopโ๐) โค
(โโ(normopโ((adjโโ๐) โ ๐))) |
163 | 10, 153 | le2sqi 14154 |
. . . . 5
โข ((0 โค
(normopโ๐)
โง 0 โค
(โโ(normopโ((adjโโ๐) โ ๐)))) โ ((normopโ๐) โค
(โโ(normopโ((adjโโ๐) โ ๐))) โ ((normopโ๐)โ2) โค
((โโ(normopโ((adjโโ๐) โ ๐)))โ2))) |
164 | 46, 155, 163 | mp2an 691 |
. . . 4
โข
((normopโ๐) โค
(โโ(normopโ((adjโโ๐) โ ๐))) โ ((normopโ๐)โ2) โค
((โโ(normopโ((adjโโ๐) โ ๐)))โ2)) |
165 | 162, 164 | mpbi 229 |
. . 3
โข
((normopโ๐)โ2) โค
((โโ(normopโ((adjโโ๐) โ ๐)))โ2) |
166 | 165, 148 | breqtri 5174 |
. 2
โข
((normopโ๐)โ2) โค
(normopโ((adjโโ๐) โ ๐)) |
167 | 75, 11 | letri3i 11330 |
. 2
โข
((normopโ((adjโโ๐) โ ๐)) = ((normopโ๐)โ2) โ
((normopโ((adjโโ๐) โ ๐)) โค ((normopโ๐)โ2) โง
((normopโ๐)โ2) โค
(normopโ((adjโโ๐) โ ๐)))) |
168 | 70, 166, 167 | mpbir2an 710 |
1
โข
(normopโ((adjโโ๐) โ ๐)) = ((normopโ๐)โ2) |