Step | Hyp | Ref
| Expression |
1 | | nrgring 22467 |
. . . 4
NrmRing |
2 | | nrginvrcn.u |
. . . . 5
Unit |
3 | | eqid 2622 |
. . . . 5
mulGrp
↾s mulGrp ↾s |
4 | 2, 3 | unitgrp 18667 |
. . . 4
mulGrp
↾s |
5 | 2, 3 | unitgrpbas 18666 |
. . . . 5
mulGrp ↾s |
6 | | nrginvrcn.i |
. . . . . 6
|
7 | 2, 3, 6 | invrfval 18673 |
. . . . 5
mulGrp ↾s |
8 | 5, 7 | grpinvf 17466 |
. . . 4
mulGrp ↾s |
9 | 1, 4, 8 | 3syl 18 |
. . 3
NrmRing |
10 | | 1rp 11836 |
. . . . . . . 8
|
11 | 10 | ne0ii 3923 |
. . . . . . 7
|
12 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . 14
NrmRing
|
13 | | nrginvrcn.x |
. . . . . . . . . . . . . . . 16
|
14 | 13, 2 | unitss 18660 |
. . . . . . . . . . . . . . 15
|
15 | | simplrl 800 |
. . . . . . . . . . . . . . 15
NrmRing
|
16 | 14, 15 | sseldi 3601 |
. . . . . . . . . . . . . 14
NrmRing
|
17 | | simpr 477 |
. . . . . . . . . . . . . . 15
NrmRing
|
18 | 14, 17 | sseldi 3601 |
. . . . . . . . . . . . . 14
NrmRing
|
19 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
20 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
21 | 13, 19, 20 | ring1eq0 18590 |
. . . . . . . . . . . . . 14
|
22 | 12, 16, 18, 21 | syl3anc 1326 |
. . . . . . . . . . . . 13
NrmRing
|
23 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
24 | | nrgngp 22466 |
. . . . . . . . . . . . . . . . . . 19
NrmRing NrmGrp |
25 | | ngpms 22404 |
. . . . . . . . . . . . . . . . . . 19
NrmGrp |
26 | | msxms 22259 |
. . . . . . . . . . . . . . . . . . 19
|
27 | 24, 25, 26 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
NrmRing |
28 | 27 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
NrmRing
|
29 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
NrmRing
|
30 | 29 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . 18
NrmRing
|
31 | 14, 30 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
NrmRing
|
32 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
33 | 13, 32 | xmseq0 22269 |
. . . . . . . . . . . . . . . . 17
|
34 | 28, 31, 31, 33 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
NrmRing
|
35 | 23, 34 | mpbiri 248 |
. . . . . . . . . . . . . . 15
NrmRing
|
36 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
NrmRing
|
37 | 36 | rpgt0d 11875 |
. . . . . . . . . . . . . . 15
NrmRing
|
38 | 35, 37 | eqbrtrd 4675 |
. . . . . . . . . . . . . 14
NrmRing
|
39 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
40 | 39 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
41 | 40 | breq1d 4663 |
. . . . . . . . . . . . . 14
|
42 | 38, 41 | syl5ibrcom 237 |
. . . . . . . . . . . . 13
NrmRing
|
43 | 22, 42 | syld 47 |
. . . . . . . . . . . 12
NrmRing
|
44 | 43 | imp 445 |
. . . . . . . . . . 11
NrmRing
|
45 | 44 | an32s 846 |
. . . . . . . . . 10
NrmRing
|
46 | 45 | a1d 25 |
. . . . . . . . 9
NrmRing
|
47 | 46 | ralrimiva 2966 |
. . . . . . . 8
NrmRing
|
48 | 47 | ralrimivw 2967 |
. . . . . . 7
NrmRing
|
49 | | r19.2z 4060 |
. . . . . . 7
|
50 | 11, 48, 49 | sylancr 695 |
. . . . . 6
NrmRing
|
51 | | eqid 2622 |
. . . . . . 7
|
52 | | simpll 790 |
. . . . . . 7
NrmRing
NrmRing |
53 | 1 | ad2antrr 762 |
. . . . . . . 8
NrmRing
|
54 | | simpr 477 |
. . . . . . . 8
NrmRing
|
55 | 19, 20 | isnzr 19259 |
. . . . . . . 8
NzRing |
56 | 53, 54, 55 | sylanbrc 698 |
. . . . . . 7
NrmRing
NzRing |
57 | | simplrl 800 |
. . . . . . 7
NrmRing
|
58 | | simplrr 801 |
. . . . . . 7
NrmRing
|
59 | | eqid 2622 |
. . . . . . 7
|
60 | 13, 2, 6, 51, 32, 52, 56, 57, 58, 59 | nrginvrcnlem 22495 |
. . . . . 6
NrmRing
|
61 | 50, 60 | pm2.61dane 2881 |
. . . . 5
NrmRing
|
62 | 15, 17 | ovresd 6801 |
. . . . . . . . 9
NrmRing
|
63 | 62 | breq1d 4663 |
. . . . . . . 8
NrmRing
|
64 | | simpl 473 |
. . . . . . . . . . . 12
|
65 | | ffvelrn 6357 |
. . . . . . . . . . . 12
|
66 | 9, 64, 65 | syl2an 494 |
. . . . . . . . . . 11
NrmRing
|
67 | 66 | adantr 481 |
. . . . . . . . . 10
NrmRing
|
68 | 67, 30 | ovresd 6801 |
. . . . . . . . 9
NrmRing
|
69 | 68 | breq1d 4663 |
. . . . . . . 8
NrmRing
|
70 | 63, 69 | imbi12d 334 |
. . . . . . 7
NrmRing
|
71 | 70 | ralbidva 2985 |
. . . . . 6
NrmRing
|
72 | 71 | rexbidv 3052 |
. . . . 5
NrmRing
|
73 | 61, 72 | mpbird 247 |
. . . 4
NrmRing
|
74 | 73 | ralrimivva 2971 |
. . 3
NrmRing
|
75 | | xpss12 5225 |
. . . . . . 7
|
76 | 14, 14, 75 | mp2an 708 |
. . . . . 6
|
77 | | resabs1 5427 |
. . . . . 6
|
78 | 76, 77 | ax-mp 5 |
. . . . 5
|
79 | | eqid 2622 |
. . . . . . . 8
|
80 | 13, 79 | xmsxmet 22261 |
. . . . . . 7
|
81 | 24, 25, 26, 80 | 4syl 19 |
. . . . . 6
NrmRing |
82 | | xmetres2 22166 |
. . . . . 6
|
83 | 81, 14, 82 | sylancl 694 |
. . . . 5
NrmRing |
84 | 78, 83 | syl5eqelr 2706 |
. . . 4
NrmRing |
85 | | eqid 2622 |
. . . . 5
|
86 | 85, 85 | metcn 22348 |
. . . 4
|
87 | 84, 84, 86 | syl2anc 693 |
. . 3
NrmRing
|
88 | 9, 74, 87 | mpbir2and 957 |
. 2
NrmRing
|
89 | | nrginvrcn.j |
. . . . . . 7
|
90 | 89, 13, 79 | mstopn 22257 |
. . . . . 6
|
91 | 24, 25, 90 | 3syl 18 |
. . . . 5
NrmRing |
92 | 91 | oveq1d 6665 |
. . . 4
NrmRing ↾t ↾t |
93 | 78 | eqcomi 2631 |
. . . . . 6
|
94 | | eqid 2622 |
. . . . . 6
|
95 | 93, 94, 85 | metrest 22329 |
. . . . 5
↾t |
96 | 81, 14, 95 | sylancl 694 |
. . . 4
NrmRing ↾t |
97 | 92, 96 | eqtrd 2656 |
. . 3
NrmRing ↾t |
98 | 97, 97 | oveq12d 6668 |
. 2
NrmRing ↾t ↾t
|
99 | 88, 98 | eleqtrrd 2704 |
1
NrmRing
↾t ↾t |