Step | Hyp | Ref
| Expression |
1 | | neeq1 3005 |
. . 3
โข (๐ฅ = ๐ง โ (๐ฅ โ 0โ โ ๐ง โ
0โ)) |
2 | 1 | cbvrexvw 3225 |
. 2
โข
(โ๐ฅ โ
๐ป ๐ฅ โ 0โ โ
โ๐ง โ ๐ป ๐ง โ 0โ) |
3 | | norm1ex.1 |
. . . . . . . . . . 11
โข ๐ป โ
Sโ |
4 | 3 | sheli 29955 |
. . . . . . . . . 10
โข (๐ง โ ๐ป โ ๐ง โ โ) |
5 | | normcl 29866 |
. . . . . . . . . 10
โข (๐ง โ โ โ
(normโโ๐ง) โ โ) |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
โข (๐ง โ ๐ป โ (normโโ๐ง) โ
โ) |
7 | 6 | adantr 482 |
. . . . . . . 8
โข ((๐ง โ ๐ป โง ๐ง โ 0โ) โ
(normโโ๐ง) โ โ) |
8 | | normne0 29871 |
. . . . . . . . . 10
โข (๐ง โ โ โ
((normโโ๐ง) โ 0 โ ๐ง โ 0โ)) |
9 | 4, 8 | syl 17 |
. . . . . . . . 9
โข (๐ง โ ๐ป โ
((normโโ๐ง) โ 0 โ ๐ง โ 0โ)) |
10 | 9 | biimpar 479 |
. . . . . . . 8
โข ((๐ง โ ๐ป โง ๐ง โ 0โ) โ
(normโโ๐ง) โ 0) |
11 | 7, 10 | rereccld 11916 |
. . . . . . 7
โข ((๐ง โ ๐ป โง ๐ง โ 0โ) โ (1 /
(normโโ๐ง)) โ โ) |
12 | 11 | recnd 11117 |
. . . . . 6
โข ((๐ง โ ๐ป โง ๐ง โ 0โ) โ (1 /
(normโโ๐ง)) โ โ) |
13 | | simpl 484 |
. . . . . 6
โข ((๐ง โ ๐ป โง ๐ง โ 0โ) โ ๐ง โ ๐ป) |
14 | | shmulcl 29959 |
. . . . . . 7
โข ((๐ป โ
Sโ โง (1 /
(normโโ๐ง)) โ โ โง ๐ง โ ๐ป) โ ((1 /
(normโโ๐ง)) ยทโ ๐ง) โ ๐ป) |
15 | 3, 14 | mp3an1 1449 |
. . . . . 6
โข (((1 /
(normโโ๐ง)) โ โ โง ๐ง โ ๐ป) โ ((1 /
(normโโ๐ง)) ยทโ ๐ง) โ ๐ป) |
16 | 12, 13, 15 | syl2anc 585 |
. . . . 5
โข ((๐ง โ ๐ป โง ๐ง โ 0โ) โ ((1 /
(normโโ๐ง)) ยทโ ๐ง) โ ๐ป) |
17 | | norm1 29990 |
. . . . . 6
โข ((๐ง โ โ โง ๐ง โ 0โ)
โ (normโโ((1 /
(normโโ๐ง)) ยทโ ๐ง)) = 1) |
18 | 4, 17 | sylan 581 |
. . . . 5
โข ((๐ง โ ๐ป โง ๐ง โ 0โ) โ
(normโโ((1 / (normโโ๐ง))
ยทโ ๐ง)) = 1) |
19 | | fveqeq2 6847 |
. . . . . 6
โข (๐ฆ = ((1 /
(normโโ๐ง)) ยทโ ๐ง) โ
((normโโ๐ฆ) = 1 โ
(normโโ((1 / (normโโ๐ง))
ยทโ ๐ง)) = 1)) |
20 | 19 | rspcev 3580 |
. . . . 5
โข ((((1 /
(normโโ๐ง)) ยทโ ๐ง) โ ๐ป โง (normโโ((1 /
(normโโ๐ง)) ยทโ ๐ง)) = 1) โ โ๐ฆ โ ๐ป (normโโ๐ฆ) = 1) |
21 | 16, 18, 20 | syl2anc 585 |
. . . 4
โข ((๐ง โ ๐ป โง ๐ง โ 0โ) โ
โ๐ฆ โ ๐ป
(normโโ๐ฆ) = 1) |
22 | 21 | rexlimiva 3143 |
. . 3
โข
(โ๐ง โ
๐ป ๐ง โ 0โ โ
โ๐ฆ โ ๐ป
(normโโ๐ฆ) = 1) |
23 | | ax-1ne0 11054 |
. . . . . . . 8
โข 1 โ
0 |
24 | 23 | neii 2944 |
. . . . . . 7
โข ยฌ 1
= 0 |
25 | | eqeq1 2742 |
. . . . . . 7
โข
((normโโ๐ฆ) = 1 โ
((normโโ๐ฆ) = 0 โ 1 = 0)) |
26 | 24, 25 | mtbiri 327 |
. . . . . 6
โข
((normโโ๐ฆ) = 1 โ ยฌ
(normโโ๐ฆ) = 0) |
27 | 3 | sheli 29955 |
. . . . . . . 8
โข (๐ฆ โ ๐ป โ ๐ฆ โ โ) |
28 | | norm-i 29870 |
. . . . . . . 8
โข (๐ฆ โ โ โ
((normโโ๐ฆ) = 0 โ ๐ฆ = 0โ)) |
29 | 27, 28 | syl 17 |
. . . . . . 7
โข (๐ฆ โ ๐ป โ
((normโโ๐ฆ) = 0 โ ๐ฆ = 0โ)) |
30 | 29 | necon3bbid 2980 |
. . . . . 6
โข (๐ฆ โ ๐ป โ (ยฌ
(normโโ๐ฆ) = 0 โ ๐ฆ โ 0โ)) |
31 | 26, 30 | syl5ib 244 |
. . . . 5
โข (๐ฆ โ ๐ป โ
((normโโ๐ฆ) = 1 โ ๐ฆ โ 0โ)) |
32 | 31 | reximia 3083 |
. . . 4
โข
(โ๐ฆ โ
๐ป
(normโโ๐ฆ) = 1 โ โ๐ฆ โ ๐ป ๐ฆ โ 0โ) |
33 | | neeq1 3005 |
. . . . 5
โข (๐ฆ = ๐ง โ (๐ฆ โ 0โ โ ๐ง โ
0โ)) |
34 | 33 | cbvrexvw 3225 |
. . . 4
โข
(โ๐ฆ โ
๐ป ๐ฆ โ 0โ โ
โ๐ง โ ๐ป ๐ง โ 0โ) |
35 | 32, 34 | sylib 217 |
. . 3
โข
(โ๐ฆ โ
๐ป
(normโโ๐ฆ) = 1 โ โ๐ง โ ๐ป ๐ง โ 0โ) |
36 | 22, 35 | impbii 208 |
. 2
โข
(โ๐ง โ
๐ป ๐ง โ 0โ โ
โ๐ฆ โ ๐ป
(normโโ๐ฆ) = 1) |
37 | 2, 36 | bitri 275 |
1
โข
(โ๐ฅ โ
๐ป ๐ฅ โ 0โ โ
โ๐ฆ โ ๐ป
(normโโ๐ฆ) = 1) |