Step | Hyp | Ref
| Expression |
1 | | 2fveq3 6848 |
. . 3
β’ (π΄ = 0β β
(normfnβ(braβπ΄)) =
(normfnβ(braβ0β))) |
2 | | fveq2 6843 |
. . 3
β’ (π΄ = 0β β
(normββπ΄) =
(normββ0β)) |
3 | 1, 2 | eqeq12d 2749 |
. 2
β’ (π΄ = 0β β
((normfnβ(braβπ΄)) = (normββπ΄) β
(normfnβ(braβ0β)) =
(normββ0β))) |
4 | | brafn 30931 |
. . . . 5
β’ (π΄ β β β
(braβπ΄):
ββΆβ) |
5 | | nmfnval 30860 |
. . . . 5
β’
((braβπ΄):
ββΆβ β (normfnβ(braβπ΄)) = sup({π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))}, β*, <
)) |
6 | 4, 5 | syl 17 |
. . . 4
β’ (π΄ β β β
(normfnβ(braβπ΄)) = sup({π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))}, β*, <
)) |
7 | 6 | adantr 482 |
. . 3
β’ ((π΄ β β β§ π΄ β 0β)
β (normfnβ(braβπ΄)) = sup({π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))}, β*, <
)) |
8 | | nmfnsetre 30861 |
. . . . . . . 8
β’
((braβπ΄):
ββΆβ β {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))} β β) |
9 | 4, 8 | syl 17 |
. . . . . . 7
β’ (π΄ β β β {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))} β β) |
10 | | ressxr 11204 |
. . . . . . 7
β’ β
β β* |
11 | 9, 10 | sstrdi 3957 |
. . . . . 6
β’ (π΄ β β β {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))} β
β*) |
12 | | normcl 30109 |
. . . . . . 7
β’ (π΄ β β β
(normββπ΄) β β) |
13 | 12 | rexrd 11210 |
. . . . . 6
β’ (π΄ β β β
(normββπ΄) β
β*) |
14 | 11, 13 | jca 513 |
. . . . 5
β’ (π΄ β β β ({π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))} β β* β§
(normββπ΄) β
β*)) |
15 | 14 | adantr 482 |
. . . 4
β’ ((π΄ β β β§ π΄ β 0β)
β ({π₯ β£
βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))} β β* β§
(normββπ΄) β
β*)) |
16 | | vex 3448 |
. . . . . . . 8
β’ π§ β V |
17 | | eqeq1 2737 |
. . . . . . . . . 10
β’ (π₯ = π§ β (π₯ = (absβ((braβπ΄)βπ¦)) β π§ = (absβ((braβπ΄)βπ¦)))) |
18 | 17 | anbi2d 630 |
. . . . . . . . 9
β’ (π₯ = π§ β
(((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦))) β
((normββπ¦) β€ 1 β§ π§ = (absβ((braβπ΄)βπ¦))))) |
19 | 18 | rexbidv 3172 |
. . . . . . . 8
β’ (π₯ = π§ β (βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦))) β βπ¦ β β
((normββπ¦) β€ 1 β§ π§ = (absβ((braβπ΄)βπ¦))))) |
20 | 16, 19 | elab 3631 |
. . . . . . 7
β’ (π§ β {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))} β βπ¦ β β
((normββπ¦) β€ 1 β§ π§ = (absβ((braβπ΄)βπ¦)))) |
21 | | id 22 |
. . . . . . . . . . . . 13
β’ (π§ = (absβ((braβπ΄)βπ¦)) β π§ = (absβ((braβπ΄)βπ¦))) |
22 | | braval 30928 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ π¦ β β) β
((braβπ΄)βπ¦) = (π¦ Β·ih π΄)) |
23 | 22 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ π¦ β β) β
(absβ((braβπ΄)βπ¦)) = (absβ(π¦ Β·ih π΄))) |
24 | 23 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§ π¦ β β) β§
(normββπ¦) β€ 1) β (absβ((braβπ΄)βπ¦)) = (absβ(π¦ Β·ih π΄))) |
25 | 21, 24 | sylan9eqr 2795 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§ π¦ β β) β§
(normββπ¦) β€ 1) β§ π§ = (absβ((braβπ΄)βπ¦))) β π§ = (absβ(π¦ Β·ih π΄))) |
26 | | bcs2 30166 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β β β§ π΄ β β β§
(normββπ¦) β€ 1) β (absβ(π¦
Β·ih π΄)) β€ (normββπ΄)) |
27 | 26 | 3expa 1119 |
. . . . . . . . . . . . . 14
β’ (((π¦ β β β§ π΄ β β) β§
(normββπ¦) β€ 1) β (absβ(π¦
Β·ih π΄)) β€ (normββπ΄)) |
28 | 27 | ancom1s 652 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§ π¦ β β) β§
(normββπ¦) β€ 1) β (absβ(π¦
Β·ih π΄)) β€ (normββπ΄)) |
29 | 28 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§ π¦ β β) β§
(normββπ¦) β€ 1) β§ π§ = (absβ((braβπ΄)βπ¦))) β (absβ(π¦ Β·ih π΄)) β€
(normββπ΄)) |
30 | 25, 29 | eqbrtrd 5128 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§ π¦ β β) β§
(normββπ¦) β€ 1) β§ π§ = (absβ((braβπ΄)βπ¦))) β π§ β€ (normββπ΄)) |
31 | 30 | exp41 436 |
. . . . . . . . . 10
β’ (π΄ β β β (π¦ β β β
((normββπ¦) β€ 1 β (π§ = (absβ((braβπ΄)βπ¦)) β π§ β€ (normββπ΄))))) |
32 | 31 | imp4a 424 |
. . . . . . . . 9
β’ (π΄ β β β (π¦ β β β
(((normββπ¦) β€ 1 β§ π§ = (absβ((braβπ΄)βπ¦))) β π§ β€ (normββπ΄)))) |
33 | 32 | rexlimdv 3147 |
. . . . . . . 8
β’ (π΄ β β β
(βπ¦ β β
((normββπ¦) β€ 1 β§ π§ = (absβ((braβπ΄)βπ¦))) β π§ β€ (normββπ΄))) |
34 | 33 | imp 408 |
. . . . . . 7
β’ ((π΄ β β β§
βπ¦ β β
((normββπ¦) β€ 1 β§ π§ = (absβ((braβπ΄)βπ¦)))) β π§ β€ (normββπ΄)) |
35 | 20, 34 | sylan2b 595 |
. . . . . 6
β’ ((π΄ β β β§ π§ β {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))}) β π§ β€ (normββπ΄)) |
36 | 35 | ralrimiva 3140 |
. . . . 5
β’ (π΄ β β β
βπ§ β {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))}π§ β€ (normββπ΄)) |
37 | 36 | adantr 482 |
. . . 4
β’ ((π΄ β β β§ π΄ β 0β)
β βπ§ β
{π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))}π§ β€ (normββπ΄)) |
38 | 12 | recnd 11188 |
. . . . . . . . . 10
β’ (π΄ β β β
(normββπ΄) β β) |
39 | 38 | adantr 482 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΄ β 0β)
β (normββπ΄) β β) |
40 | | normne0 30114 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β
((normββπ΄) β 0 β π΄ β
0β)) |
41 | 40 | biimpar 479 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΄ β 0β)
β (normββπ΄) β 0) |
42 | 39, 41 | reccld 11929 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π΄ β 0β)
β (1 / (normββπ΄)) β β) |
43 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π΄ β 0β)
β π΄ β
β) |
44 | | hvmulcl 29997 |
. . . . . . . . . . . 12
β’ (((1 /
(normββπ΄)) β β β§ π΄ β β) β ((1 /
(normββπ΄)) Β·β π΄) β
β) |
45 | 42, 43, 44 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΄ β 0β)
β ((1 / (normββπ΄)) Β·β π΄) β
β) |
46 | | norm1 30233 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π΄ β 0β)
β (normββ((1 /
(normββπ΄)) Β·β π΄)) = 1) |
47 | | 1le1 11788 |
. . . . . . . . . . . 12
β’ 1 β€
1 |
48 | 46, 47 | eqbrtrdi 5145 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΄ β 0β)
β (normββ((1 /
(normββπ΄)) Β·β π΄)) β€ 1) |
49 | | ax-his3 30068 |
. . . . . . . . . . . . 13
β’ (((1 /
(normββπ΄)) β β β§ π΄ β β β§ π΄ β β) β (((1 /
(normββπ΄)) Β·β π΄)
Β·ih π΄) = ((1 /
(normββπ΄)) Β· (π΄ Β·ih π΄))) |
50 | 42, 43, 43, 49 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π΄ β 0β)
β (((1 / (normββπ΄)) Β·β π΄)
Β·ih π΄) = ((1 /
(normββπ΄)) Β· (π΄ Β·ih π΄))) |
51 | 12 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§ π΄ β 0β)
β (normββπ΄) β β) |
52 | 51, 41 | rereccld 11987 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ π΄ β 0β)
β (1 / (normββπ΄)) β β) |
53 | | hiidrcl 30079 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β (π΄
Β·ih π΄) β β) |
54 | 53 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ π΄ β 0β)
β (π΄
Β·ih π΄) β β) |
55 | 52, 54 | remulcld 11190 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ π΄ β 0β)
β ((1 / (normββπ΄)) Β· (π΄ Β·ih π΄)) β
β) |
56 | 50, 55 | eqeltrd 2834 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΄ β 0β)
β (((1 / (normββπ΄)) Β·β π΄)
Β·ih π΄) β β) |
57 | | normgt0 30111 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β β β (π΄ β 0β
β 0 < (normββπ΄))) |
58 | 57 | biimpa 478 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β β§ π΄ β 0β)
β 0 < (normββπ΄)) |
59 | 51, 58 | recgt0d 12094 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§ π΄ β 0β)
β 0 < (1 / (normββπ΄))) |
60 | | 0re 11162 |
. . . . . . . . . . . . . . . . 17
β’ 0 β
β |
61 | | ltle 11248 |
. . . . . . . . . . . . . . . . 17
β’ ((0
β β β§ (1 / (normββπ΄)) β β) β (0 < (1 /
(normββπ΄)) β 0 β€ (1 /
(normββπ΄)))) |
62 | 60, 61 | mpan 689 |
. . . . . . . . . . . . . . . 16
β’ ((1 /
(normββπ΄)) β β β (0 < (1 /
(normββπ΄)) β 0 β€ (1 /
(normββπ΄)))) |
63 | 52, 59, 62 | sylc 65 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ π΄ β 0β)
β 0 β€ (1 / (normββπ΄))) |
64 | | hiidge0 30082 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β 0 β€
(π΄
Β·ih π΄)) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ π΄ β 0β)
β 0 β€ (π΄
Β·ih π΄)) |
66 | 52, 54, 63, 65 | mulge0d 11737 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ π΄ β 0β)
β 0 β€ ((1 / (normββπ΄)) Β· (π΄ Β·ih π΄))) |
67 | 66, 50 | breqtrrd 5134 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΄ β 0β)
β 0 β€ (((1 / (normββπ΄)) Β·β π΄)
Β·ih π΄)) |
68 | 56, 67 | absidd 15313 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π΄ β 0β)
β (absβ(((1 / (normββπ΄)) Β·β π΄)
Β·ih π΄)) = (((1 /
(normββπ΄)) Β·β π΄)
Β·ih π΄)) |
69 | 39, 41 | recid2d 11932 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ π΄ β 0β)
β ((1 / (normββπ΄)) Β·
(normββπ΄)) = 1) |
70 | 69 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΄ β 0β)
β ((normββπ΄) Β· ((1 /
(normββπ΄)) Β·
(normββπ΄))) = ((normββπ΄) Β· 1)) |
71 | 39, 42, 39 | mul12d 11369 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ π΄ β 0β)
β ((normββπ΄) Β· ((1 /
(normββπ΄)) Β·
(normββπ΄))) = ((1 /
(normββπ΄)) Β·
((normββπ΄) Β·
(normββπ΄)))) |
72 | 38 | sqvald 14054 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β β
((normββπ΄)β2) =
((normββπ΄) Β·
(normββπ΄))) |
73 | | normsq 30118 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β β
((normββπ΄)β2) = (π΄ Β·ih π΄)) |
74 | 72, 73 | eqtr3d 2775 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β
((normββπ΄) Β·
(normββπ΄)) = (π΄ Β·ih π΄)) |
75 | 74 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ π΄ β 0β)
β ((normββπ΄) Β·
(normββπ΄)) = (π΄ Β·ih π΄)) |
76 | 75 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ π΄ β 0β)
β ((1 / (normββπ΄)) Β·
((normββπ΄) Β·
(normββπ΄))) = ((1 /
(normββπ΄)) Β· (π΄ Β·ih π΄))) |
77 | 71, 76 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΄ β 0β)
β ((normββπ΄) Β· ((1 /
(normββπ΄)) Β·
(normββπ΄))) = ((1 /
(normββπ΄)) Β· (π΄ Β·ih π΄))) |
78 | 38 | mulid1d 11177 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β
((normββπ΄) Β· 1) =
(normββπ΄)) |
79 | 78 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΄ β 0β)
β ((normββπ΄) Β· 1) =
(normββπ΄)) |
80 | 70, 77, 79 | 3eqtr3rd 2782 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π΄ β 0β)
β (normββπ΄) = ((1 /
(normββπ΄)) Β· (π΄ Β·ih π΄))) |
81 | 50, 68, 80 | 3eqtr4rd 2784 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΄ β 0β)
β (normββπ΄) = (absβ(((1 /
(normββπ΄)) Β·β π΄)
Β·ih π΄))) |
82 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π¦ = ((1 /
(normββπ΄)) Β·β π΄) β
(normββπ¦) = (normββ((1 /
(normββπ΄)) Β·β π΄))) |
83 | 82 | breq1d 5116 |
. . . . . . . . . . . . 13
β’ (π¦ = ((1 /
(normββπ΄)) Β·β π΄) β
((normββπ¦) β€ 1 β
(normββ((1 / (normββπ΄))
Β·β π΄)) β€ 1)) |
84 | | fvoveq1 7381 |
. . . . . . . . . . . . . 14
β’ (π¦ = ((1 /
(normββπ΄)) Β·β π΄) β (absβ(π¦
Β·ih π΄)) = (absβ(((1 /
(normββπ΄)) Β·β π΄)
Β·ih π΄))) |
85 | 84 | eqeq2d 2744 |
. . . . . . . . . . . . 13
β’ (π¦ = ((1 /
(normββπ΄)) Β·β π΄) β
((normββπ΄) = (absβ(π¦ Β·ih π΄)) β
(normββπ΄) = (absβ(((1 /
(normββπ΄)) Β·β π΄)
Β·ih π΄)))) |
86 | 83, 85 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π¦ = ((1 /
(normββπ΄)) Β·β π΄) β
(((normββπ¦) β€ 1 β§
(normββπ΄) = (absβ(π¦ Β·ih π΄))) β
((normββ((1 / (normββπ΄))
Β·β π΄)) β€ 1 β§
(normββπ΄) = (absβ(((1 /
(normββπ΄)) Β·β π΄)
Β·ih π΄))))) |
87 | 86 | rspcev 3580 |
. . . . . . . . . . 11
β’ ((((1 /
(normββπ΄)) Β·β π΄) β β β§
((normββ((1 / (normββπ΄))
Β·β π΄)) β€ 1 β§
(normββπ΄) = (absβ(((1 /
(normββπ΄)) Β·β π΄)
Β·ih π΄)))) β βπ¦ β β
((normββπ¦) β€ 1 β§
(normββπ΄) = (absβ(π¦ Β·ih π΄)))) |
88 | 45, 48, 81, 87 | syl12anc 836 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΄ β 0β)
β βπ¦ β
β ((normββπ¦) β€ 1 β§
(normββπ΄) = (absβ(π¦ Β·ih π΄)))) |
89 | 23 | eqeq2d 2744 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π¦ β β) β
((normββπ΄) = (absβ((braβπ΄)βπ¦)) β
(normββπ΄) = (absβ(π¦ Β·ih π΄)))) |
90 | 89 | anbi2d 630 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π¦ β β) β
(((normββπ¦) β€ 1 β§
(normββπ΄) = (absβ((braβπ΄)βπ¦))) β
((normββπ¦) β€ 1 β§
(normββπ΄) = (absβ(π¦ Β·ih π΄))))) |
91 | 90 | rexbidva 3170 |
. . . . . . . . . . 11
β’ (π΄ β β β
(βπ¦ β β
((normββπ¦) β€ 1 β§
(normββπ΄) = (absβ((braβπ΄)βπ¦))) β βπ¦ β β
((normββπ¦) β€ 1 β§
(normββπ΄) = (absβ(π¦ Β·ih π΄))))) |
92 | 91 | adantr 482 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΄ β 0β)
β (βπ¦ β
β ((normββπ¦) β€ 1 β§
(normββπ΄) = (absβ((braβπ΄)βπ¦))) β βπ¦ β β
((normββπ¦) β€ 1 β§
(normββπ΄) = (absβ(π¦ Β·ih π΄))))) |
93 | 88, 92 | mpbird 257 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΄ β 0β)
β βπ¦ β
β ((normββπ¦) β€ 1 β§
(normββπ΄) = (absβ((braβπ΄)βπ¦)))) |
94 | | eqeq1 2737 |
. . . . . . . . . . 11
β’ (π₯ =
(normββπ΄) β (π₯ = (absβ((braβπ΄)βπ¦)) β
(normββπ΄) = (absβ((braβπ΄)βπ¦)))) |
95 | 94 | anbi2d 630 |
. . . . . . . . . 10
β’ (π₯ =
(normββπ΄) β
(((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦))) β
((normββπ¦) β€ 1 β§
(normββπ΄) = (absβ((braβπ΄)βπ¦))))) |
96 | 95 | rexbidv 3172 |
. . . . . . . . 9
β’ (π₯ =
(normββπ΄) β (βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦))) β βπ¦ β β
((normββπ¦) β€ 1 β§
(normββπ΄) = (absβ((braβπ΄)βπ¦))))) |
97 | 39, 93, 96 | elabd 3634 |
. . . . . . . 8
β’ ((π΄ β β β§ π΄ β 0β)
β (normββπ΄) β {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))}) |
98 | | breq2 5110 |
. . . . . . . . 9
β’ (π€ =
(normββπ΄) β (π§ < π€ β π§ < (normββπ΄))) |
99 | 98 | rspcev 3580 |
. . . . . . . 8
β’
(((normββπ΄) β {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))} β§ π§ < (normββπ΄)) β βπ€ β {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))}π§ < π€) |
100 | 97, 99 | sylan 581 |
. . . . . . 7
β’ (((π΄ β β β§ π΄ β 0β)
β§ π§ <
(normββπ΄)) β βπ€ β {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))}π§ < π€) |
101 | 100 | adantlr 714 |
. . . . . 6
β’ ((((π΄ β β β§ π΄ β 0β)
β§ π§ β β)
β§ π§ <
(normββπ΄)) β βπ€ β {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))}π§ < π€) |
102 | 101 | ex 414 |
. . . . 5
β’ (((π΄ β β β§ π΄ β 0β)
β§ π§ β β)
β (π§ <
(normββπ΄) β βπ€ β {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))}π§ < π€)) |
103 | 102 | ralrimiva 3140 |
. . . 4
β’ ((π΄ β β β§ π΄ β 0β)
β βπ§ β
β (π§ <
(normββπ΄) β βπ€ β {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))}π§ < π€)) |
104 | | supxr2 13239 |
. . . 4
β’ ((({π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))} β β* β§
(normββπ΄) β β*) β§
(βπ§ β {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))}π§ β€ (normββπ΄) β§ βπ§ β β (π§ <
(normββπ΄) β βπ€ β {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))}π§ < π€))) β sup({π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))}, β*, < ) =
(normββπ΄)) |
105 | 15, 37, 103, 104 | syl12anc 836 |
. . 3
β’ ((π΄ β β β§ π΄ β 0β)
β sup({π₯ β£
βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ((braβπ΄)βπ¦)))}, β*, < ) =
(normββπ΄)) |
106 | 7, 105 | eqtrd 2773 |
. 2
β’ ((π΄ β β β§ π΄ β 0β)
β (normfnβ(braβπ΄)) = (normββπ΄)) |
107 | | nmfn0 30971 |
. . . 4
β’
(normfnβ( β Γ {0})) = 0 |
108 | | bra0 30934 |
. . . . 5
β’
(braβ0β) = ( β Γ
{0}) |
109 | 108 | fveq2i 6846 |
. . . 4
β’
(normfnβ(braβ0β)) =
(normfnβ( β Γ {0})) |
110 | | norm0 30112 |
. . . 4
β’
(normββ0β) =
0 |
111 | 107, 109,
110 | 3eqtr4i 2771 |
. . 3
β’
(normfnβ(braβ0β)) =
(normββ0β) |
112 | 111 | a1i 11 |
. 2
β’ (π΄ β β β
(normfnβ(braβ0β)) =
(normββ0β)) |
113 | 3, 106, 112 | pm2.61ne 3027 |
1
β’ (π΄ β β β
(normfnβ(braβπ΄)) = (normββπ΄)) |