Step |
Hyp |
Ref |
Expression |
1 |
|
nmopcoadj.1 |
โข ๐ โ BndLinOp |
2 |
|
adjbdlnb |
โข ( ๐ โ BndLinOp โ ( adjโ โ ๐ ) โ BndLinOp ) |
3 |
1 2
|
mpbi |
โข ( adjโ โ ๐ ) โ BndLinOp |
4 |
|
bdopf |
โข ( ( adjโ โ ๐ ) โ BndLinOp โ ( adjโ โ ๐ ) : โ โถ โ ) |
5 |
3 4
|
ax-mp |
โข ( adjโ โ ๐ ) : โ โถ โ |
6 |
|
bdopf |
โข ( ๐ โ BndLinOp โ ๐ : โ โถ โ ) |
7 |
1 6
|
ax-mp |
โข ๐ : โ โถ โ |
8 |
5 7
|
hocofi |
โข ( ( adjโ โ ๐ ) โ ๐ ) : โ โถ โ |
9 |
|
nmopre |
โข ( ๐ โ BndLinOp โ ( normop โ ๐ ) โ โ ) |
10 |
1 9
|
ax-mp |
โข ( normop โ ๐ ) โ โ |
11 |
10
|
resqcli |
โข ( ( normop โ ๐ ) โ 2 ) โ โ |
12 |
|
rexr |
โข ( ( ( normop โ ๐ ) โ 2 ) โ โ โ ( ( normop โ ๐ ) โ 2 ) โ โ* ) |
13 |
11 12
|
ax-mp |
โข ( ( normop โ ๐ ) โ 2 ) โ โ* |
14 |
|
nmopub |
โข ( ( ( ( adjโ โ ๐ ) โ ๐ ) : โ โถ โ โง ( ( normop โ ๐ ) โ 2 ) โ โ* ) โ ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) โค ( ( normop โ ๐ ) โ 2 ) โ โ ๐ฅ โ โ ( ( normโ โ ๐ฅ ) โค 1 โ ( normโ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) ) โค ( ( normop โ ๐ ) โ 2 ) ) ) ) |
15 |
8 13 14
|
mp2an |
โข ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) โค ( ( normop โ ๐ ) โ 2 ) โ โ ๐ฅ โ โ ( ( normโ โ ๐ฅ ) โค 1 โ ( normโ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) ) โค ( ( normop โ ๐ ) โ 2 ) ) ) |
16 |
5 7
|
hocoi |
โข ( ๐ฅ โ โ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) = ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) |
17 |
16
|
fveq2d |
โข ( ๐ฅ โ โ โ ( normโ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) ) = ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ) |
18 |
17
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normโ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) ) = ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ) |
19 |
7
|
ffvelrni |
โข ( ๐ฅ โ โ โ ( ๐ โ ๐ฅ ) โ โ ) |
20 |
5
|
ffvelrni |
โข ( ( ๐ โ ๐ฅ ) โ โ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) โ โ ) |
21 |
|
normcl |
โข ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) โ โ โ ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) โ โ ) |
22 |
19 20 21
|
3syl |
โข ( ๐ฅ โ โ โ ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) โ โ ) |
23 |
22
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) โ โ ) |
24 |
|
nmopre |
โข ( ( adjโ โ ๐ ) โ BndLinOp โ ( normop โ ( adjโ โ ๐ ) ) โ โ ) |
25 |
3 24
|
ax-mp |
โข ( normop โ ( adjโ โ ๐ ) ) โ โ |
26 |
|
normcl |
โข ( ( ๐ โ ๐ฅ ) โ โ โ ( normโ โ ( ๐ โ ๐ฅ ) ) โ โ ) |
27 |
19 26
|
syl |
โข ( ๐ฅ โ โ โ ( normโ โ ( ๐ โ ๐ฅ ) ) โ โ ) |
28 |
|
remulcl |
โข ( ( ( normop โ ( adjโ โ ๐ ) ) โ โ โง ( normโ โ ( ๐ โ ๐ฅ ) ) โ โ ) โ ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normโ โ ( ๐ โ ๐ฅ ) ) ) โ โ ) |
29 |
25 27 28
|
sylancr |
โข ( ๐ฅ โ โ โ ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normโ โ ( ๐ โ ๐ฅ ) ) ) โ โ ) |
30 |
29
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normโ โ ( ๐ โ ๐ฅ ) ) ) โ โ ) |
31 |
25 10
|
remulcli |
โข ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normop โ ๐ ) ) โ โ |
32 |
31
|
a1i |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normop โ ๐ ) ) โ โ ) |
33 |
3
|
nmbdoplbi |
โข ( ( ๐ โ ๐ฅ ) โ โ โ ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) โค ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normโ โ ( ๐ โ ๐ฅ ) ) ) ) |
34 |
19 33
|
syl |
โข ( ๐ฅ โ โ โ ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) โค ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normโ โ ( ๐ โ ๐ฅ ) ) ) ) |
35 |
34
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) โค ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normโ โ ( ๐ โ ๐ฅ ) ) ) ) |
36 |
27
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normโ โ ( ๐ โ ๐ฅ ) ) โ โ ) |
37 |
10
|
a1i |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normop โ ๐ ) โ โ ) |
38 |
|
normcl |
โข ( ๐ฅ โ โ โ ( normโ โ ๐ฅ ) โ โ ) |
39 |
|
remulcl |
โข ( ( ( normop โ ๐ ) โ โ โง ( normโ โ ๐ฅ ) โ โ ) โ ( ( normop โ ๐ ) ยท ( normโ โ ๐ฅ ) ) โ โ ) |
40 |
10 38 39
|
sylancr |
โข ( ๐ฅ โ โ โ ( ( normop โ ๐ ) ยท ( normโ โ ๐ฅ ) ) โ โ ) |
41 |
40
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normop โ ๐ ) ยท ( normโ โ ๐ฅ ) ) โ โ ) |
42 |
1
|
nmbdoplbi |
โข ( ๐ฅ โ โ โ ( normโ โ ( ๐ โ ๐ฅ ) ) โค ( ( normop โ ๐ ) ยท ( normโ โ ๐ฅ ) ) ) |
43 |
42
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normโ โ ( ๐ โ ๐ฅ ) ) โค ( ( normop โ ๐ ) ยท ( normโ โ ๐ฅ ) ) ) |
44 |
|
1re |
โข 1 โ โ |
45 |
|
nmopge0 |
โข ( ๐ : โ โถ โ โ 0 โค ( normop โ ๐ ) ) |
46 |
1 6 45
|
mp2b |
โข 0 โค ( normop โ ๐ ) |
47 |
10 46
|
pm3.2i |
โข ( ( normop โ ๐ ) โ โ โง 0 โค ( normop โ ๐ ) ) |
48 |
|
lemul2a |
โข ( ( ( ( normโ โ ๐ฅ ) โ โ โง 1 โ โ โง ( ( normop โ ๐ ) โ โ โง 0 โค ( normop โ ๐ ) ) ) โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normop โ ๐ ) ยท ( normโ โ ๐ฅ ) ) โค ( ( normop โ ๐ ) ยท 1 ) ) |
49 |
47 48
|
mp3anl3 |
โข ( ( ( ( normโ โ ๐ฅ ) โ โ โง 1 โ โ ) โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normop โ ๐ ) ยท ( normโ โ ๐ฅ ) ) โค ( ( normop โ ๐ ) ยท 1 ) ) |
50 |
44 49
|
mpanl2 |
โข ( ( ( normโ โ ๐ฅ ) โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normop โ ๐ ) ยท ( normโ โ ๐ฅ ) ) โค ( ( normop โ ๐ ) ยท 1 ) ) |
51 |
38 50
|
sylan |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normop โ ๐ ) ยท ( normโ โ ๐ฅ ) ) โค ( ( normop โ ๐ ) ยท 1 ) ) |
52 |
10
|
recni |
โข ( normop โ ๐ ) โ โ |
53 |
52
|
mulid1i |
โข ( ( normop โ ๐ ) ยท 1 ) = ( normop โ ๐ ) |
54 |
51 53
|
breqtrdi |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normop โ ๐ ) ยท ( normโ โ ๐ฅ ) ) โค ( normop โ ๐ ) ) |
55 |
36 41 37 43 54
|
letrd |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normโ โ ( ๐ โ ๐ฅ ) ) โค ( normop โ ๐ ) ) |
56 |
|
nmopge0 |
โข ( ( adjโ โ ๐ ) : โ โถ โ โ 0 โค ( normop โ ( adjโ โ ๐ ) ) ) |
57 |
3 4 56
|
mp2b |
โข 0 โค ( normop โ ( adjโ โ ๐ ) ) |
58 |
25 57
|
pm3.2i |
โข ( ( normop โ ( adjโ โ ๐ ) ) โ โ โง 0 โค ( normop โ ( adjโ โ ๐ ) ) ) |
59 |
|
lemul2a |
โข ( ( ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ โ โง ( normop โ ๐ ) โ โ โง ( ( normop โ ( adjโ โ ๐ ) ) โ โ โง 0 โค ( normop โ ( adjโ โ ๐ ) ) ) ) โง ( normโ โ ( ๐ โ ๐ฅ ) ) โค ( normop โ ๐ ) ) โ ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normโ โ ( ๐ โ ๐ฅ ) ) ) โค ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normop โ ๐ ) ) ) |
60 |
58 59
|
mp3anl3 |
โข ( ( ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ โ โง ( normop โ ๐ ) โ โ ) โง ( normโ โ ( ๐ โ ๐ฅ ) ) โค ( normop โ ๐ ) ) โ ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normโ โ ( ๐ โ ๐ฅ ) ) ) โค ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normop โ ๐ ) ) ) |
61 |
36 37 55 60
|
syl21anc |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normโ โ ( ๐ โ ๐ฅ ) ) ) โค ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normop โ ๐ ) ) ) |
62 |
23 30 32 35 61
|
letrd |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) โค ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normop โ ๐ ) ) ) |
63 |
18 62
|
eqbrtrd |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normโ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) ) โค ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normop โ ๐ ) ) ) |
64 |
1
|
nmopadji |
โข ( normop โ ( adjโ โ ๐ ) ) = ( normop โ ๐ ) |
65 |
64
|
oveq1i |
โข ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normop โ ๐ ) ) = ( ( normop โ ๐ ) ยท ( normop โ ๐ ) ) |
66 |
52
|
sqvali |
โข ( ( normop โ ๐ ) โ 2 ) = ( ( normop โ ๐ ) ยท ( normop โ ๐ ) ) |
67 |
65 66
|
eqtr4i |
โข ( ( normop โ ( adjโ โ ๐ ) ) ยท ( normop โ ๐ ) ) = ( ( normop โ ๐ ) โ 2 ) |
68 |
63 67
|
breqtrdi |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normโ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) ) โค ( ( normop โ ๐ ) โ 2 ) ) |
69 |
68
|
ex |
โข ( ๐ฅ โ โ โ ( ( normโ โ ๐ฅ ) โค 1 โ ( normโ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) ) โค ( ( normop โ ๐ ) โ 2 ) ) ) |
70 |
15 69
|
mprgbir |
โข ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) โค ( ( normop โ ๐ ) โ 2 ) |
71 |
|
nmopge0 |
โข ( ( ( adjโ โ ๐ ) โ ๐ ) : โ โถ โ โ 0 โค ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) |
72 |
8 71
|
ax-mp |
โข 0 โค ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) |
73 |
3 1
|
bdopcoi |
โข ( ( adjโ โ ๐ ) โ ๐ ) โ BndLinOp |
74 |
|
nmopre |
โข ( ( ( adjโ โ ๐ ) โ ๐ ) โ BndLinOp โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) โ โ ) |
75 |
73 74
|
ax-mp |
โข ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) โ โ |
76 |
75
|
sqrtcli |
โข ( 0 โค ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) โ ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ โ ) |
77 |
|
rexr |
โข ( ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ โ โ ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ โ* ) |
78 |
72 76 77
|
mp2b |
โข ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ โ* |
79 |
|
nmopub |
โข ( ( ๐ : โ โถ โ โง ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ โ* ) โ ( ( normop โ ๐ ) โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ โ ๐ฅ โ โ ( ( normโ โ ๐ฅ ) โค 1 โ ( normโ โ ( ๐ โ ๐ฅ ) ) โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) ) ) ) |
80 |
7 78 79
|
mp2an |
โข ( ( normop โ ๐ ) โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ โ ๐ฅ โ โ ( ( normโ โ ๐ฅ ) โค 1 โ ( normโ โ ( ๐ โ ๐ฅ ) ) โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) ) ) |
81 |
19 20
|
syl |
โข ( ๐ฅ โ โ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) โ โ ) |
82 |
|
hicl |
โข ( ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) โ โ โง ๐ฅ โ โ ) โ ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ยทih ๐ฅ ) โ โ ) |
83 |
81 82
|
mpancom |
โข ( ๐ฅ โ โ โ ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ยทih ๐ฅ ) โ โ ) |
84 |
83
|
abscld |
โข ( ๐ฅ โ โ โ ( abs โ ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ยทih ๐ฅ ) ) โ โ ) |
85 |
84
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( abs โ ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ยทih ๐ฅ ) ) โ โ ) |
86 |
22 38
|
remulcld |
โข ( ๐ฅ โ โ โ ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ยท ( normโ โ ๐ฅ ) ) โ โ ) |
87 |
86
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ยท ( normโ โ ๐ฅ ) ) โ โ ) |
88 |
75
|
a1i |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) โ โ ) |
89 |
|
bcs |
โข ( ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) โ โ โง ๐ฅ โ โ ) โ ( abs โ ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ยทih ๐ฅ ) ) โค ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ยท ( normโ โ ๐ฅ ) ) ) |
90 |
81 89
|
mpancom |
โข ( ๐ฅ โ โ โ ( abs โ ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ยทih ๐ฅ ) ) โค ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ยท ( normโ โ ๐ฅ ) ) ) |
91 |
90
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( abs โ ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ยทih ๐ฅ ) ) โค ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ยท ( normโ โ ๐ฅ ) ) ) |
92 |
5 7
|
hococli |
โข ( ๐ฅ โ โ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) โ โ ) |
93 |
|
normcl |
โข ( ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) โ โ โ ( normโ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) ) โ โ ) |
94 |
92 93
|
syl |
โข ( ๐ฅ โ โ โ ( normโ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) ) โ โ ) |
95 |
94
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normโ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) ) โ โ ) |
96 |
38
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normโ โ ๐ฅ ) โ โ ) |
97 |
|
normge0 |
โข ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) โ โ โ 0 โค ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ) |
98 |
19 20 97
|
3syl |
โข ( ๐ฅ โ โ โ 0 โค ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ) |
99 |
22 98
|
jca |
โข ( ๐ฅ โ โ โ ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) โ โ โง 0 โค ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ) ) |
100 |
99
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) โ โ โง 0 โค ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ) ) |
101 |
|
simpr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normโ โ ๐ฅ ) โค 1 ) |
102 |
|
lemul2a |
โข ( ( ( ( normโ โ ๐ฅ ) โ โ โง 1 โ โ โง ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) โ โ โง 0 โค ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ) ) โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ยท ( normโ โ ๐ฅ ) ) โค ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ยท 1 ) ) |
103 |
44 102
|
mp3anl2 |
โข ( ( ( ( normโ โ ๐ฅ ) โ โ โง ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) โ โ โง 0 โค ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ) ) โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ยท ( normโ โ ๐ฅ ) ) โค ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ยท 1 ) ) |
104 |
96 100 101 103
|
syl21anc |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ยท ( normโ โ ๐ฅ ) ) โค ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ยท 1 ) ) |
105 |
22
|
recnd |
โข ( ๐ฅ โ โ โ ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) โ โ ) |
106 |
105
|
mulid1d |
โข ( ๐ฅ โ โ โ ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ยท 1 ) = ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ) |
107 |
106 17
|
eqtr4d |
โข ( ๐ฅ โ โ โ ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ยท 1 ) = ( normโ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) ) ) |
108 |
107
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ยท 1 ) = ( normโ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) ) ) |
109 |
104 108
|
breqtrd |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ยท ( normโ โ ๐ฅ ) ) โค ( normโ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) ) ) |
110 |
|
remulcl |
โข ( ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) โ โ โง ( normโ โ ๐ฅ ) โ โ ) โ ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ยท ( normโ โ ๐ฅ ) ) โ โ ) |
111 |
75 38 110
|
sylancr |
โข ( ๐ฅ โ โ โ ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ยท ( normโ โ ๐ฅ ) ) โ โ ) |
112 |
111
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ยท ( normโ โ ๐ฅ ) ) โ โ ) |
113 |
73
|
nmbdoplbi |
โข ( ๐ฅ โ โ โ ( normโ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) ) โค ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ยท ( normโ โ ๐ฅ ) ) ) |
114 |
113
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normโ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) ) โค ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ยท ( normโ โ ๐ฅ ) ) ) |
115 |
75 72
|
pm3.2i |
โข ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) โ โ โง 0 โค ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) |
116 |
|
lemul2a |
โข ( ( ( ( normโ โ ๐ฅ ) โ โ โง 1 โ โ โง ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) โ โ โง 0 โค ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) ) โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ยท ( normโ โ ๐ฅ ) ) โค ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ยท 1 ) ) |
117 |
115 116
|
mp3anl3 |
โข ( ( ( ( normโ โ ๐ฅ ) โ โ โง 1 โ โ ) โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ยท ( normโ โ ๐ฅ ) ) โค ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ยท 1 ) ) |
118 |
44 117
|
mpanl2 |
โข ( ( ( normโ โ ๐ฅ ) โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ยท ( normโ โ ๐ฅ ) ) โค ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ยท 1 ) ) |
119 |
38 118
|
sylan |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ยท ( normโ โ ๐ฅ ) ) โค ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ยท 1 ) ) |
120 |
75
|
recni |
โข ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) โ โ |
121 |
120
|
mulid1i |
โข ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ยท 1 ) = ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) |
122 |
119 121
|
breqtrdi |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ยท ( normโ โ ๐ฅ ) ) โค ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) |
123 |
95 112 88 114 122
|
letrd |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normโ โ ( ( ( adjโ โ ๐ ) โ ๐ ) โ ๐ฅ ) ) โค ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) |
124 |
87 95 88 109 123
|
letrd |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normโ โ ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ) ยท ( normโ โ ๐ฅ ) ) โค ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) |
125 |
85 87 88 91 124
|
letrd |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( abs โ ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ยทih ๐ฅ ) ) โค ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) |
126 |
|
resqcl |
โข ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ โ โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) โ โ ) |
127 |
|
sqge0 |
โข ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ โ โ 0 โค ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) ) |
128 |
126 127
|
absidd |
โข ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ โ โ ( abs โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) ) = ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) ) |
129 |
19 26 128
|
3syl |
โข ( ๐ฅ โ โ โ ( abs โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) ) = ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) ) |
130 |
|
normsq |
โข ( ( ๐ โ ๐ฅ ) โ โ โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) = ( ( ๐ โ ๐ฅ ) ยทih ( ๐ โ ๐ฅ ) ) ) |
131 |
19 130
|
syl |
โข ( ๐ฅ โ โ โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) = ( ( ๐ โ ๐ฅ ) ยทih ( ๐ โ ๐ฅ ) ) ) |
132 |
|
bdopadj |
โข ( ( adjโ โ ๐ ) โ BndLinOp โ ( adjโ โ ๐ ) โ dom adjโ ) |
133 |
3 132
|
ax-mp |
โข ( adjโ โ ๐ ) โ dom adjโ |
134 |
|
adj2 |
โข ( ( ( adjโ โ ๐ ) โ dom adjโ โง ( ๐ โ ๐ฅ ) โ โ โง ๐ฅ โ โ ) โ ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ยทih ๐ฅ ) = ( ( ๐ โ ๐ฅ ) ยทih ( ( adjโ โ ( adjโ โ ๐ ) ) โ ๐ฅ ) ) ) |
135 |
133 134
|
mp3an1 |
โข ( ( ( ๐ โ ๐ฅ ) โ โ โง ๐ฅ โ โ ) โ ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ยทih ๐ฅ ) = ( ( ๐ โ ๐ฅ ) ยทih ( ( adjโ โ ( adjโ โ ๐ ) ) โ ๐ฅ ) ) ) |
136 |
19 135
|
mpancom |
โข ( ๐ฅ โ โ โ ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ยทih ๐ฅ ) = ( ( ๐ โ ๐ฅ ) ยทih ( ( adjโ โ ( adjโ โ ๐ ) ) โ ๐ฅ ) ) ) |
137 |
|
bdopadj |
โข ( ๐ โ BndLinOp โ ๐ โ dom adjโ ) |
138 |
|
adjadj |
โข ( ๐ โ dom adjโ โ ( adjโ โ ( adjโ โ ๐ ) ) = ๐ ) |
139 |
1 137 138
|
mp2b |
โข ( adjโ โ ( adjโ โ ๐ ) ) = ๐ |
140 |
139
|
fveq1i |
โข ( ( adjโ โ ( adjโ โ ๐ ) ) โ ๐ฅ ) = ( ๐ โ ๐ฅ ) |
141 |
140
|
oveq2i |
โข ( ( ๐ โ ๐ฅ ) ยทih ( ( adjโ โ ( adjโ โ ๐ ) ) โ ๐ฅ ) ) = ( ( ๐ โ ๐ฅ ) ยทih ( ๐ โ ๐ฅ ) ) |
142 |
136 141
|
eqtr2di |
โข ( ๐ฅ โ โ โ ( ( ๐ โ ๐ฅ ) ยทih ( ๐ โ ๐ฅ ) ) = ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ยทih ๐ฅ ) ) |
143 |
131 142
|
eqtrd |
โข ( ๐ฅ โ โ โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) = ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ยทih ๐ฅ ) ) |
144 |
143
|
fveq2d |
โข ( ๐ฅ โ โ โ ( abs โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) ) = ( abs โ ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ยทih ๐ฅ ) ) ) |
145 |
129 144
|
eqtr3d |
โข ( ๐ฅ โ โ โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) = ( abs โ ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ยทih ๐ฅ ) ) ) |
146 |
145
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) = ( abs โ ( ( ( adjโ โ ๐ ) โ ( ๐ โ ๐ฅ ) ) ยทih ๐ฅ ) ) ) |
147 |
75
|
sqsqrti |
โข ( 0 โค ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) โ ( ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ 2 ) = ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) |
148 |
8 71 147
|
mp2b |
โข ( ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ 2 ) = ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) |
149 |
148
|
a1i |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ 2 ) = ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) |
150 |
125 146 149
|
3brtr4d |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) โค ( ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ 2 ) ) |
151 |
|
normge0 |
โข ( ( ๐ โ ๐ฅ ) โ โ โ 0 โค ( normโ โ ( ๐ โ ๐ฅ ) ) ) |
152 |
19 151
|
syl |
โข ( ๐ฅ โ โ โ 0 โค ( normโ โ ( ๐ โ ๐ฅ ) ) ) |
153 |
8 71 76
|
mp2b |
โข ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ โ |
154 |
75
|
sqrtge0i |
โข ( 0 โค ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) โ 0 โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) ) |
155 |
8 71 154
|
mp2b |
โข 0 โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) |
156 |
|
le2sq |
โข ( ( ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ โ โง 0 โค ( normโ โ ( ๐ โ ๐ฅ ) ) ) โง ( ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ โ โง 0 โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) ) ) โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) โค ( ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ 2 ) ) ) |
157 |
153 155 156
|
mpanr12 |
โข ( ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ โ โง 0 โค ( normโ โ ( ๐ โ ๐ฅ ) ) ) โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) โค ( ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ 2 ) ) ) |
158 |
27 152 157
|
syl2anc |
โข ( ๐ฅ โ โ โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) โค ( ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ 2 ) ) ) |
159 |
158
|
adantr |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ ( ( normโ โ ( ๐ โ ๐ฅ ) ) โ 2 ) โค ( ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ 2 ) ) ) |
160 |
150 159
|
mpbird |
โข ( ( ๐ฅ โ โ โง ( normโ โ ๐ฅ ) โค 1 ) โ ( normโ โ ( ๐ โ ๐ฅ ) ) โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) ) |
161 |
160
|
ex |
โข ( ๐ฅ โ โ โ ( ( normโ โ ๐ฅ ) โค 1 โ ( normโ โ ( ๐ โ ๐ฅ ) ) โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) ) ) |
162 |
80 161
|
mprgbir |
โข ( normop โ ๐ ) โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) |
163 |
10 153
|
le2sqi |
โข ( ( 0 โค ( normop โ ๐ ) โง 0 โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) ) โ ( ( normop โ ๐ ) โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ ( ( normop โ ๐ ) โ 2 ) โค ( ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ 2 ) ) ) |
164 |
46 155 163
|
mp2an |
โข ( ( normop โ ๐ ) โค ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ ( ( normop โ ๐ ) โ 2 ) โค ( ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ 2 ) ) |
165 |
162 164
|
mpbi |
โข ( ( normop โ ๐ ) โ 2 ) โค ( ( โ โ ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) โ 2 ) |
166 |
165 148
|
breqtri |
โข ( ( normop โ ๐ ) โ 2 ) โค ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) |
167 |
75 11
|
letri3i |
โข ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) = ( ( normop โ ๐ ) โ 2 ) โ ( ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) โค ( ( normop โ ๐ ) โ 2 ) โง ( ( normop โ ๐ ) โ 2 ) โค ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) ) ) |
168 |
70 166 167
|
mpbir2an |
โข ( normop โ ( ( adjโ โ ๐ ) โ ๐ ) ) = ( ( normop โ ๐ ) โ 2 ) |