Step | Hyp | Ref
| Expression |
1 | | nmcopex.2 |
. . . 4
โข ๐ โ ContOp |
2 | | ax-hv0cl 30760 |
. . . 4
โข
0โ โ โ |
3 | | 1rp 12981 |
. . . 4
โข 1 โ
โ+ |
4 | | cnopc 31670 |
. . . 4
โข ((๐ โ ContOp โง
0โ โ โ โง 1 โ โ+) โ
โ๐ฆ โ
โ+ โ๐ง โ โ
((normโโ(๐ง โโ
0โ)) < ๐ฆ โ
(normโโ((๐โ๐ง) โโ (๐โ0โ)))
< 1)) |
5 | 1, 2, 3, 4 | mp3an 1457 |
. . 3
โข
โ๐ฆ โ
โ+ โ๐ง โ โ
((normโโ(๐ง โโ
0โ)) < ๐ฆ โ
(normโโ((๐โ๐ง) โโ (๐โ0โ)))
< 1) |
6 | | hvsub0 30833 |
. . . . . . . 8
โข (๐ง โ โ โ (๐ง โโ
0โ) = ๐ง) |
7 | 6 | fveq2d 6888 |
. . . . . . 7
โข (๐ง โ โ โ
(normโโ(๐ง โโ
0โ)) = (normโโ๐ง)) |
8 | 7 | breq1d 5151 |
. . . . . 6
โข (๐ง โ โ โ
((normโโ(๐ง โโ
0โ)) < ๐ฆ โ (normโโ๐ง) < ๐ฆ)) |
9 | | nmcopex.1 |
. . . . . . . . . . 11
โข ๐ โ LinOp |
10 | 9 | lnop0i 31727 |
. . . . . . . . . 10
โข (๐โ0โ) =
0โ |
11 | 10 | oveq2i 7415 |
. . . . . . . . 9
โข ((๐โ๐ง) โโ (๐โ0โ)) =
((๐โ๐ง) โโ
0โ) |
12 | 9 | lnopfi 31726 |
. . . . . . . . . . 11
โข ๐: โโถ
โ |
13 | 12 | ffvelcdmi 7078 |
. . . . . . . . . 10
โข (๐ง โ โ โ (๐โ๐ง) โ โ) |
14 | | hvsub0 30833 |
. . . . . . . . . 10
โข ((๐โ๐ง) โ โ โ ((๐โ๐ง) โโ
0โ) = (๐โ๐ง)) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
โข (๐ง โ โ โ ((๐โ๐ง) โโ
0โ) = (๐โ๐ง)) |
16 | 11, 15 | eqtrid 2778 |
. . . . . . . 8
โข (๐ง โ โ โ ((๐โ๐ง) โโ (๐โ0โ)) =
(๐โ๐ง)) |
17 | 16 | fveq2d 6888 |
. . . . . . 7
โข (๐ง โ โ โ
(normโโ((๐โ๐ง) โโ (๐โ0โ))) =
(normโโ(๐โ๐ง))) |
18 | 17 | breq1d 5151 |
. . . . . 6
โข (๐ง โ โ โ
((normโโ((๐โ๐ง) โโ (๐โ0โ)))
< 1 โ (normโโ(๐โ๐ง)) < 1)) |
19 | 8, 18 | imbi12d 344 |
. . . . 5
โข (๐ง โ โ โ
(((normโโ(๐ง โโ
0โ)) < ๐ฆ โ
(normโโ((๐โ๐ง) โโ (๐โ0โ)))
< 1) โ ((normโโ๐ง) < ๐ฆ โ (normโโ(๐โ๐ง)) < 1))) |
20 | 19 | ralbiia 3085 |
. . . 4
โข
(โ๐ง โ
โ ((normโโ(๐ง โโ
0โ)) < ๐ฆ โ
(normโโ((๐โ๐ง) โโ (๐โ0โ)))
< 1) โ โ๐ง
โ โ ((normโโ๐ง) < ๐ฆ โ (normโโ(๐โ๐ง)) < 1)) |
21 | 20 | rexbii 3088 |
. . 3
โข
(โ๐ฆ โ
โ+ โ๐ง โ โ
((normโโ(๐ง โโ
0โ)) < ๐ฆ โ
(normโโ((๐โ๐ง) โโ (๐โ0โ)))
< 1) โ โ๐ฆ
โ โ+ โ๐ง โ โ
((normโโ๐ง) < ๐ฆ โ (normโโ(๐โ๐ง)) < 1)) |
22 | 5, 21 | mpbi 229 |
. 2
โข
โ๐ฆ โ
โ+ โ๐ง โ โ
((normโโ๐ง) < ๐ฆ โ (normโโ(๐โ๐ง)) < 1) |
23 | | nmopval 31613 |
. . 3
โข (๐: โโถ โ โ
(normopโ๐)
= sup({๐ โฃ
โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (normโโ(๐โ๐ฅ)))}, โ*, <
)) |
24 | 12, 23 | ax-mp 5 |
. 2
โข
(normopโ๐) = sup({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (normโโ(๐โ๐ฅ)))}, โ*, <
) |
25 | 12 | ffvelcdmi 7078 |
. . 3
โข (๐ฅ โ โ โ (๐โ๐ฅ) โ โ) |
26 | | normcl 30882 |
. . 3
โข ((๐โ๐ฅ) โ โ โ
(normโโ(๐โ๐ฅ)) โ โ) |
27 | 25, 26 | syl 17 |
. 2
โข (๐ฅ โ โ โ
(normโโ(๐โ๐ฅ)) โ โ) |
28 | 10 | fveq2i 6887 |
. . 3
โข
(normโโ(๐โ0โ)) =
(normโโ0โ) |
29 | | norm0 30885 |
. . 3
โข
(normโโ0โ) =
0 |
30 | 28, 29 | eqtri 2754 |
. 2
โข
(normโโ(๐โ0โ)) =
0 |
31 | | rpcn 12987 |
. . . . 5
โข ((๐ฆ / 2) โ โ+
โ (๐ฆ / 2) โ
โ) |
32 | 9 | lnopmuli 31729 |
. . . . 5
โข (((๐ฆ / 2) โ โ โง ๐ฅ โ โ) โ (๐โ((๐ฆ / 2) ยทโ
๐ฅ)) = ((๐ฆ / 2) ยทโ
(๐โ๐ฅ))) |
33 | 31, 32 | sylan 579 |
. . . 4
โข (((๐ฆ / 2) โ โ+
โง ๐ฅ โ โ)
โ (๐โ((๐ฆ / 2)
ยทโ ๐ฅ)) = ((๐ฆ / 2) ยทโ
(๐โ๐ฅ))) |
34 | 33 | fveq2d 6888 |
. . 3
โข (((๐ฆ / 2) โ โ+
โง ๐ฅ โ โ)
โ (normโโ(๐โ((๐ฆ / 2) ยทโ
๐ฅ))) =
(normโโ((๐ฆ / 2) ยทโ
(๐โ๐ฅ)))) |
35 | | norm-iii 30897 |
. . . 4
โข (((๐ฆ / 2) โ โ โง
(๐โ๐ฅ) โ โ) โ
(normโโ((๐ฆ / 2) ยทโ
(๐โ๐ฅ))) = ((absโ(๐ฆ / 2)) ยท
(normโโ(๐โ๐ฅ)))) |
36 | 31, 25, 35 | syl2an 595 |
. . 3
โข (((๐ฆ / 2) โ โ+
โง ๐ฅ โ โ)
โ (normโโ((๐ฆ / 2) ยทโ
(๐โ๐ฅ))) = ((absโ(๐ฆ / 2)) ยท
(normโโ(๐โ๐ฅ)))) |
37 | | rpre 12985 |
. . . . . 6
โข ((๐ฆ / 2) โ โ+
โ (๐ฆ / 2) โ
โ) |
38 | | rpge0 12990 |
. . . . . 6
โข ((๐ฆ / 2) โ โ+
โ 0 โค (๐ฆ /
2)) |
39 | 37, 38 | absidd 15372 |
. . . . 5
โข ((๐ฆ / 2) โ โ+
โ (absโ(๐ฆ / 2))
= (๐ฆ / 2)) |
40 | 39 | adantr 480 |
. . . 4
โข (((๐ฆ / 2) โ โ+
โง ๐ฅ โ โ)
โ (absโ(๐ฆ / 2))
= (๐ฆ / 2)) |
41 | 40 | oveq1d 7419 |
. . 3
โข (((๐ฆ / 2) โ โ+
โง ๐ฅ โ โ)
โ ((absโ(๐ฆ / 2))
ยท (normโโ(๐โ๐ฅ))) = ((๐ฆ / 2) ยท
(normโโ(๐โ๐ฅ)))) |
42 | 34, 36, 41 | 3eqtrrd 2771 |
. 2
โข (((๐ฆ / 2) โ โ+
โง ๐ฅ โ โ)
โ ((๐ฆ / 2) ยท
(normโโ(๐โ๐ฅ))) = (normโโ(๐โ((๐ฆ / 2) ยทโ
๐ฅ)))) |
43 | 22, 24, 27, 30, 42 | nmcexi 31783 |
1
โข
(normopโ๐) โ โ |