Step | Hyp | Ref
| Expression |
1 | | normcl 30116 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ
(normโโ๐ฅ) โ โ) |
2 | 1 | recnd 11191 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ โ
(normโโ๐ฅ) โ โ) |
3 | 2 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ
(normโโ๐ฅ) โ โ) |
4 | | norm-i 30120 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โ โ
((normโโ๐ฅ) = 0 โ ๐ฅ = 0โ)) |
5 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = 0โ โ
(๐โ๐ฅ) = (๐โ0โ)) |
6 | | nmlnop0.1 |
. . . . . . . . . . . . . . . . 17
โข ๐ โ LinOp |
7 | 6 | lnop0i 30961 |
. . . . . . . . . . . . . . . 16
โข (๐โ0โ) =
0โ |
8 | 5, 7 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = 0โ โ
(๐โ๐ฅ) = 0โ) |
9 | 4, 8 | syl6bi 253 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ
((normโโ๐ฅ) = 0 โ (๐โ๐ฅ) = 0โ)) |
10 | 9 | necon3d 2961 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ โ ((๐โ๐ฅ) โ 0โ โ
(normโโ๐ฅ) โ 0)) |
11 | 10 | imp 408 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ
(normโโ๐ฅ) โ 0) |
12 | 3, 11 | recne0d 11933 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ (1 /
(normโโ๐ฅ)) โ 0) |
13 | | simpr 486 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ (๐โ๐ฅ) โ 0โ) |
14 | 3, 11 | reccld 11932 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ (1 /
(normโโ๐ฅ)) โ โ) |
15 | 6 | lnopfi 30960 |
. . . . . . . . . . . . . . . 16
โข ๐: โโถ
โ |
16 | 15 | ffvelcdmi 7038 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โ โ (๐โ๐ฅ) โ โ) |
17 | 16 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ (๐โ๐ฅ) โ โ) |
18 | | hvmul0or 30016 |
. . . . . . . . . . . . . 14
โข (((1 /
(normโโ๐ฅ)) โ โ โง (๐โ๐ฅ) โ โ) โ (((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ)) = 0โ โ ((1 /
(normโโ๐ฅ)) = 0 โจ (๐โ๐ฅ) = 0โ))) |
19 | 14, 17, 18 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ (((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ)) = 0โ โ ((1 /
(normโโ๐ฅ)) = 0 โจ (๐โ๐ฅ) = 0โ))) |
20 | 19 | necon3abid 2977 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ (((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ)) โ 0โ โ ยฌ ((1
/ (normโโ๐ฅ)) = 0 โจ (๐โ๐ฅ) = 0โ))) |
21 | | neanior 3034 |
. . . . . . . . . . . 12
โข (((1 /
(normโโ๐ฅ)) โ 0 โง (๐โ๐ฅ) โ 0โ) โ ยฌ ((1
/ (normโโ๐ฅ)) = 0 โจ (๐โ๐ฅ) = 0โ)) |
22 | 20, 21 | bitr4di 289 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ (((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ)) โ 0โ โ ((1 /
(normโโ๐ฅ)) โ 0 โง (๐โ๐ฅ) โ
0โ))) |
23 | 12, 13, 22 | mpbir2and 712 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ ((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ)) โ
0โ) |
24 | | hvmulcl 30004 |
. . . . . . . . . . . 12
โข (((1 /
(normโโ๐ฅ)) โ โ โง (๐โ๐ฅ) โ โ) โ ((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ)) โ โ) |
25 | 14, 17, 24 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ ((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ)) โ โ) |
26 | | normgt0 30118 |
. . . . . . . . . . 11
โข (((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ)) โ โ โ (((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ)) โ 0โ โ 0 <
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ (((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ)) โ 0โ โ 0 <
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))))) |
28 | 23, 27 | mpbid 231 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ 0 <
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ)))) |
29 | 28 | ex 414 |
. . . . . . . 8
โข (๐ฅ โ โ โ ((๐โ๐ฅ) โ 0โ โ 0 <
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))))) |
30 | 29 | adantl 483 |
. . . . . . 7
โข
(((normopโ๐) = 0 โง ๐ฅ โ โ) โ ((๐โ๐ฅ) โ 0โ โ 0 <
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))))) |
31 | | nmopsetretHIL 30855 |
. . . . . . . . . . . . . 14
โข (๐: โโถ โ โ
{๐ฆ โฃ โ๐ง โ โ
((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง)))} โ โ) |
32 | 15, 31 | ax-mp 5 |
. . . . . . . . . . . . 13
โข {๐ฆ โฃ โ๐ง โ โ
((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง)))} โ โ |
33 | | ressxr 11207 |
. . . . . . . . . . . . 13
โข โ
โ โ* |
34 | 32, 33 | sstri 3957 |
. . . . . . . . . . . 12
โข {๐ฆ โฃ โ๐ง โ โ
((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง)))} โ
โ* |
35 | | simpl 484 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ ๐ฅ โ
โ) |
36 | | hvmulcl 30004 |
. . . . . . . . . . . . . . 15
โข (((1 /
(normโโ๐ฅ)) โ โ โง ๐ฅ โ โ) โ ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ) โ
โ) |
37 | 14, 35, 36 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ) โ
โ) |
38 | 8 | necon3i 2973 |
. . . . . . . . . . . . . . . . 17
โข ((๐โ๐ฅ) โ 0โ โ ๐ฅ โ
0โ) |
39 | | norm1 30240 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฅ โ โ โง ๐ฅ โ 0โ)
โ (normโโ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ)) = 1) |
40 | 38, 39 | sylan2 594 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ
(normโโ((1 / (normโโ๐ฅ))
ยทโ ๐ฅ)) = 1) |
41 | | 1re 11163 |
. . . . . . . . . . . . . . . 16
โข 1 โ
โ |
42 | 40, 41 | eqeltrdi 2842 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ
(normโโ((1 / (normโโ๐ฅ))
ยทโ ๐ฅ)) โ โ) |
43 | | eqle 11265 |
. . . . . . . . . . . . . . 15
โข
(((normโโ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ)) โ โ โง
(normโโ((1 / (normโโ๐ฅ))
ยทโ ๐ฅ)) = 1) โ
(normโโ((1 / (normโโ๐ฅ))
ยทโ ๐ฅ)) โค 1) |
44 | 42, 40, 43 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ
(normโโ((1 / (normโโ๐ฅ))
ยทโ ๐ฅ)) โค 1) |
45 | 6 | lnopmuli 30963 |
. . . . . . . . . . . . . . . . 17
โข (((1 /
(normโโ๐ฅ)) โ โ โง ๐ฅ โ โ) โ (๐โ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ)) = ((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ))) |
46 | 14, 35, 45 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ (๐โ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ)) = ((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ))) |
47 | 46 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ ((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ)) = (๐โ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ))) |
48 | 47 | fveq2d 6850 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) = (normโโ(๐โ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ)))) |
49 | | fveq2 6846 |
. . . . . . . . . . . . . . . . 17
โข (๐ง = ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ) โ
(normโโ๐ง) = (normโโ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ))) |
50 | 49 | breq1d 5119 |
. . . . . . . . . . . . . . . 16
โข (๐ง = ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ) โ
((normโโ๐ง) โค 1 โ
(normโโ((1 / (normโโ๐ฅ))
ยทโ ๐ฅ)) โค 1)) |
51 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . 18
โข (๐ง = ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ) โ (๐โ๐ง) = (๐โ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ))) |
52 | 51 | fveq2d 6850 |
. . . . . . . . . . . . . . . . 17
โข (๐ง = ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ) โ
(normโโ(๐โ๐ง)) = (normโโ(๐โ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ)))) |
53 | 52 | eqeq2d 2744 |
. . . . . . . . . . . . . . . 16
โข (๐ง = ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ) โ
((normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) = (normโโ(๐โ๐ง)) โ (normโโ((1
/ (normโโ๐ฅ)) ยทโ (๐โ๐ฅ))) = (normโโ(๐โ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ))))) |
54 | 50, 53 | anbi12d 632 |
. . . . . . . . . . . . . . 15
โข (๐ง = ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ) โ
(((normโโ๐ง) โค 1 โง
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) = (normโโ(๐โ๐ง))) โ
((normโโ((1 / (normโโ๐ฅ))
ยทโ ๐ฅ)) โค 1 โง
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) = (normโโ(๐โ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ)))))) |
55 | 54 | rspcev 3583 |
. . . . . . . . . . . . . 14
โข ((((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ) โ โ โง
((normโโ((1 / (normโโ๐ฅ))
ยทโ ๐ฅ)) โค 1 โง
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) = (normโโ(๐โ((1 /
(normโโ๐ฅ)) ยทโ ๐ฅ))))) โ โ๐ง โ โ
((normโโ๐ง) โค 1 โง
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) = (normโโ(๐โ๐ง)))) |
56 | 37, 44, 48, 55 | syl12anc 836 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ
โ๐ง โ โ
((normโโ๐ง) โค 1 โง
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) = (normโโ(๐โ๐ง)))) |
57 | | fvex 6859 |
. . . . . . . . . . . . . 14
โข
(normโโ((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ))) โ V |
58 | | eqeq1 2737 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ =
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) โ (๐ฆ = (normโโ(๐โ๐ง)) โ (normโโ((1
/ (normโโ๐ฅ)) ยทโ (๐โ๐ฅ))) = (normโโ(๐โ๐ง)))) |
59 | 58 | anbi2d 630 |
. . . . . . . . . . . . . . 15
โข (๐ฆ =
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) โ
(((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง))) โ
((normโโ๐ง) โค 1 โง
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) = (normโโ(๐โ๐ง))))) |
60 | 59 | rexbidv 3172 |
. . . . . . . . . . . . . 14
โข (๐ฆ =
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) โ (โ๐ง โ โ
((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง))) โ โ๐ง โ โ
((normโโ๐ง) โค 1 โง
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) = (normโโ(๐โ๐ง))))) |
61 | 57, 60 | elab 3634 |
. . . . . . . . . . . . 13
โข
((normโโ((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ))) โ {๐ฆ โฃ โ๐ง โ โ
((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง)))} โ โ๐ง โ โ
((normโโ๐ง) โค 1 โง
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) = (normโโ(๐โ๐ง)))) |
62 | 56, 61 | sylibr 233 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) โ {๐ฆ โฃ โ๐ง โ โ
((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง)))}) |
63 | | supxrub 13252 |
. . . . . . . . . . . 12
โข (({๐ฆ โฃ โ๐ง โ โ
((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง)))} โ โ* โง
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) โ {๐ฆ โฃ โ๐ง โ โ
((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง)))}) โ
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) โค sup({๐ฆ โฃ โ๐ง โ โ
((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง)))}, โ*, <
)) |
64 | 34, 62, 63 | sylancr 588 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) โค sup({๐ฆ โฃ โ๐ง โ โ
((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง)))}, โ*, <
)) |
65 | 64 | adantll 713 |
. . . . . . . . . 10
โข
((((normopโ๐) = 0 โง ๐ฅ โ โ) โง (๐โ๐ฅ) โ 0โ) โ
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) โค sup({๐ฆ โฃ โ๐ง โ โ
((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง)))}, โ*, <
)) |
66 | | nmopval 30847 |
. . . . . . . . . . . . . 14
โข (๐: โโถ โ โ
(normopโ๐)
= sup({๐ฆ โฃ
โ๐ง โ โ
((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง)))}, โ*, <
)) |
67 | 15, 66 | ax-mp 5 |
. . . . . . . . . . . . 13
โข
(normopโ๐) = sup({๐ฆ โฃ โ๐ง โ โ
((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง)))}, โ*, <
) |
68 | 67 | eqeq1i 2738 |
. . . . . . . . . . . 12
โข
((normopโ๐) = 0 โ sup({๐ฆ โฃ โ๐ง โ โ
((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง)))}, โ*, < ) =
0) |
69 | 68 | biimpi 215 |
. . . . . . . . . . 11
โข
((normopโ๐) = 0 โ sup({๐ฆ โฃ โ๐ง โ โ
((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง)))}, โ*, < ) =
0) |
70 | 69 | ad2antrr 725 |
. . . . . . . . . 10
โข
((((normopโ๐) = 0 โง ๐ฅ โ โ) โง (๐โ๐ฅ) โ 0โ) โ
sup({๐ฆ โฃ โ๐ง โ โ
((normโโ๐ง) โค 1 โง ๐ฆ = (normโโ(๐โ๐ง)))}, โ*, < ) =
0) |
71 | 65, 70 | breqtrd 5135 |
. . . . . . . . 9
โข
((((normopโ๐) = 0 โง ๐ฅ โ โ) โง (๐โ๐ฅ) โ 0โ) โ
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) โค 0) |
72 | | normcl 30116 |
. . . . . . . . . . . 12
โข (((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ)) โ โ โ
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) โ โ) |
73 | 25, 72 | syl 17 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) โ โ) |
74 | | 0re 11165 |
. . . . . . . . . . 11
โข 0 โ
โ |
75 | | lenlt 11241 |
. . . . . . . . . . 11
โข
(((normโโ((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ))) โ โ โง 0 โ โ)
โ ((normโโ((1 /
(normโโ๐ฅ)) ยทโ (๐โ๐ฅ))) โค 0 โ ยฌ 0 <
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))))) |
76 | 73, 74, 75 | sylancl 587 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง (๐โ๐ฅ) โ 0โ) โ
((normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) โค 0 โ ยฌ 0 <
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))))) |
77 | 76 | adantll 713 |
. . . . . . . . 9
โข
((((normopโ๐) = 0 โง ๐ฅ โ โ) โง (๐โ๐ฅ) โ 0โ) โ
((normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))) โค 0 โ ยฌ 0 <
(normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))))) |
78 | 71, 77 | mpbid 231 |
. . . . . . . 8
โข
((((normopโ๐) = 0 โง ๐ฅ โ โ) โง (๐โ๐ฅ) โ 0โ) โ ยฌ 0
< (normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ)))) |
79 | 78 | ex 414 |
. . . . . . 7
โข
(((normopโ๐) = 0 โง ๐ฅ โ โ) โ ((๐โ๐ฅ) โ 0โ โ ยฌ 0
< (normโโ((1 / (normโโ๐ฅ))
ยทโ (๐โ๐ฅ))))) |
80 | 30, 79 | pm2.65d 195 |
. . . . . 6
โข
(((normopโ๐) = 0 โง ๐ฅ โ โ) โ ยฌ (๐โ๐ฅ) โ 0โ) |
81 | | nne 2944 |
. . . . . 6
โข (ยฌ
(๐โ๐ฅ) โ 0โ โ (๐โ๐ฅ) = 0โ) |
82 | 80, 81 | sylib 217 |
. . . . 5
โข
(((normopโ๐) = 0 โง ๐ฅ โ โ) โ (๐โ๐ฅ) = 0โ) |
83 | | ho0val 30741 |
. . . . . 6
โข (๐ฅ โ โ โ (
0hop โ๐ฅ) =
0โ) |
84 | 83 | adantl 483 |
. . . . 5
โข
(((normopโ๐) = 0 โง ๐ฅ โ โ) โ ( 0hop
โ๐ฅ) =
0โ) |
85 | 82, 84 | eqtr4d 2776 |
. . . 4
โข
(((normopโ๐) = 0 โง ๐ฅ โ โ) โ (๐โ๐ฅ) = ( 0hop โ๐ฅ)) |
86 | 85 | ralrimiva 3140 |
. . 3
โข
((normopโ๐) = 0 โ โ๐ฅ โ โ (๐โ๐ฅ) = ( 0hop โ๐ฅ)) |
87 | | ffn 6672 |
. . . . 5
โข (๐: โโถ โ โ
๐ Fn
โ) |
88 | 15, 87 | ax-mp 5 |
. . . 4
โข ๐ Fn โ |
89 | | ho0f 30742 |
. . . . 5
โข
0hop : โโถ โ |
90 | | ffn 6672 |
. . . . 5
โข (
0hop : โโถ โ โ 0hop Fn
โ) |
91 | 89, 90 | ax-mp 5 |
. . . 4
โข
0hop Fn โ |
92 | | eqfnfv 6986 |
. . . 4
โข ((๐ Fn โ โง
0hop Fn โ) โ (๐ = 0hop โ โ๐ฅ โ โ (๐โ๐ฅ) = ( 0hop โ๐ฅ))) |
93 | 88, 91, 92 | mp2an 691 |
. . 3
โข (๐ = 0hop โ
โ๐ฅ โ โ
(๐โ๐ฅ) = ( 0hop โ๐ฅ)) |
94 | 86, 93 | sylibr 233 |
. 2
โข
((normopโ๐) = 0 โ ๐ = 0hop ) |
95 | | fveq2 6846 |
. . 3
โข (๐ = 0hop โ
(normopโ๐)
= (normopโ 0hop )) |
96 | | nmop0 30977 |
. . 3
โข
(normopโ 0hop ) = 0 |
97 | 95, 96 | eqtrdi 2789 |
. 2
โข (๐ = 0hop โ
(normopโ๐)
= 0) |
98 | 94, 97 | impbii 208 |
1
โข
((normopโ๐) = 0 โ ๐ = 0hop ) |