Step | Hyp | Ref
| Expression |
1 | | isofld 29802 |
. . . 4
oField Field oRing |
2 | 1 | simprbi 480 |
. . 3
oField oRing |
3 | | orngogrp 29801 |
. . 3
oRing oGrp |
4 | | isarchiofld.b |
. . . 4
|
5 | | eqid 2622 |
. . . 4
|
6 | | isarchiofld.l |
. . . 4
|
7 | | eqid 2622 |
. . . 4
.g .g |
8 | 4, 5, 6, 7 | isarchi3 29741 |
. . 3
oGrp Archi
.g |
9 | 2, 3, 8 | 3syl 18 |
. 2
oField Archi
.g |
10 | | orngring 29800 |
. . . . . . 7
oRing |
11 | | eqid 2622 |
. . . . . . . 8
|
12 | 4, 11 | ringidcl 18568 |
. . . . . . 7
|
13 | 2, 10, 12 | 3syl 18 |
. . . . . 6
oField |
14 | | breq2 4657 |
. . . . . . . . 9
|
15 | | oveq2 6658 |
. . . . . . . . . . 11
.g .g |
16 | 15 | breq2d 4665 |
. . . . . . . . . 10
.g .g |
17 | 16 | rexbidv 3052 |
. . . . . . . . 9
.g
.g |
18 | 14, 17 | imbi12d 334 |
. . . . . . . 8
.g
.g |
19 | 18 | ralbidv 2986 |
. . . . . . 7
.g
.g |
20 | 19 | rspcv 3305 |
. . . . . 6
.g
.g |
21 | 13, 20 | syl 17 |
. . . . 5
oField
.g
.g |
22 | 5, 11, 6 | ofldlt1 29813 |
. . . . . . 7
oField |
23 | | pm5.5 351 |
. . . . . . 7
.g
.g |
24 | 22, 23 | syl 17 |
. . . . . 6
oField
.g
.g |
25 | 24 | ralbidv 2986 |
. . . . 5
oField
.g
.g |
26 | 21, 25 | sylibd 229 |
. . . 4
oField
.g
.g |
27 | 2, 10 | syl 17 |
. . . . . . . 8
oField |
28 | | nnz 11399 |
. . . . . . . 8
|
29 | | isarchiofld.h |
. . . . . . . . 9
RHom |
30 | 29, 7, 11 | zrhmulg 19858 |
. . . . . . . 8
.g |
31 | 27, 28, 30 | syl2an 494 |
. . . . . . 7
oField
.g |
32 | 31 | breq2d 4665 |
. . . . . 6
oField
.g |
33 | 32 | rexbidva 3049 |
. . . . 5
oField .g |
34 | 33 | ralbidv 2986 |
. . . 4
oField
.g |
35 | 26, 34 | sylibrd 249 |
. . 3
oField
.g
|
36 | | nfv 1843 |
. . . . . . . 8
oField |
37 | | nfra1 2941 |
. . . . . . . 8
|
38 | 36, 37 | nfan 1828 |
. . . . . . 7
oField
|
39 | | nfv 1843 |
. . . . . . 7
|
40 | 38, 39 | nfan 1828 |
. . . . . 6
oField
|
41 | 27 | ad3antrrr 766 |
. . . . . . . . . . 11
oField
|
42 | | simplrr 801 |
. . . . . . . . . . 11
oField
|
43 | | simplrl 800 |
. . . . . . . . . . . 12
oField
|
44 | | simpr 477 |
. . . . . . . . . . . . . 14
oField
|
45 | | simplll 798 |
. . . . . . . . . . . . . . 15
oField
oField |
46 | | ringgrp 18552 |
. . . . . . . . . . . . . . . 16
|
47 | 4, 5 | grpidcl 17450 |
. . . . . . . . . . . . . . . 16
|
48 | 41, 46, 47 | 3syl 18 |
. . . . . . . . . . . . . . 15
oField
|
49 | 6 | pltne 16962 |
. . . . . . . . . . . . . . 15
oField
|
50 | 45, 48, 43, 49 | syl3anc 1326 |
. . . . . . . . . . . . . 14
oField
|
51 | 44, 50 | mpd 15 |
. . . . . . . . . . . . 13
oField
|
52 | 51 | necomd 2849 |
. . . . . . . . . . . 12
oField
|
53 | 1 | simplbi 476 |
. . . . . . . . . . . . . 14
oField Field |
54 | | isfld 18756 |
. . . . . . . . . . . . . . 15
Field
|
55 | 54 | simplbi 476 |
. . . . . . . . . . . . . 14
Field |
56 | 53, 55 | syl 17 |
. . . . . . . . . . . . 13
oField |
57 | | eqid 2622 |
. . . . . . . . . . . . . 14
Unit Unit |
58 | 4, 57, 5 | drngunit 18752 |
. . . . . . . . . . . . 13
Unit |
59 | 45, 56, 58 | 3syl 18 |
. . . . . . . . . . . 12
oField
Unit
|
60 | 43, 52, 59 | mpbir2and 957 |
. . . . . . . . . . 11
oField
Unit |
61 | | eqid 2622 |
. . . . . . . . . . . 12
/r /r |
62 | 4, 57, 61 | dvrcl 18686 |
. . . . . . . . . . 11
Unit
/r |
63 | 41, 42, 60, 62 | syl3anc 1326 |
. . . . . . . . . 10
oField
/r |
64 | | simpr 477 |
. . . . . . . . . . . 12
oField
|
65 | | breq1 4656 |
. . . . . . . . . . . . . 14
|
66 | 65 | rexbidv 3052 |
. . . . . . . . . . . . 13
|
67 | 66 | cbvralv 3171 |
. . . . . . . . . . . 12
|
68 | 64, 67 | sylib 208 |
. . . . . . . . . . 11
oField
|
69 | 68 | ad2antrr 762 |
. . . . . . . . . 10
oField
|
70 | | breq1 4656 |
. . . . . . . . . . . 12
/r /r |
71 | 70 | rexbidv 3052 |
. . . . . . . . . . 11
/r /r
|
72 | 71 | rspcv 3305 |
. . . . . . . . . 10
/r /r |
73 | 63, 69, 72 | sylc 65 |
. . . . . . . . 9
oField
/r |
74 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
75 | | simp-4l 806 |
. . . . . . . . . . . . . . 15
oField /r
oField |
76 | 75, 2 | syl 17 |
. . . . . . . . . . . . . 14
oField /r
oRing |
77 | 75, 27 | syl 17 |
. . . . . . . . . . . . . . 15
oField /r
|
78 | | simp-4r 807 |
. . . . . . . . . . . . . . . 16
oField /r
|
79 | 78 | simprd 479 |
. . . . . . . . . . . . . . 15
oField /r
|
80 | 78 | simpld 475 |
. . . . . . . . . . . . . . . 16
oField /r
|
81 | | simpllr 799 |
. . . . . . . . . . . . . . . . . 18
oField /r
|
82 | 77, 46, 47 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
oField /r
|
83 | 75, 82, 80, 49 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
oField /r
|
84 | 81, 83 | mpd 15 |
. . . . . . . . . . . . . . . . 17
oField /r
|
85 | 84 | necomd 2849 |
. . . . . . . . . . . . . . . 16
oField /r
|
86 | 75, 56, 58 | 3syl 18 |
. . . . . . . . . . . . . . . 16
oField /r
Unit
|
87 | 80, 85, 86 | mpbir2and 957 |
. . . . . . . . . . . . . . 15
oField /r
Unit |
88 | 77, 79, 87, 62 | syl3anc 1326 |
. . . . . . . . . . . . . 14
oField /r
/r |
89 | | simplr 792 |
. . . . . . . . . . . . . . . 16
oField /r
|
90 | 75, 89, 31 | syl2anc 693 |
. . . . . . . . . . . . . . 15
oField /r
.g |
91 | 77, 46 | syl 17 |
. . . . . . . . . . . . . . . 16
oField /r
|
92 | 89, 28 | syl 17 |
. . . . . . . . . . . . . . . 16
oField /r
|
93 | 77, 12 | syl 17 |
. . . . . . . . . . . . . . . 16
oField /r
|
94 | 4, 7 | mulgcl 17559 |
. . . . . . . . . . . . . . . 16
.g |
95 | 91, 92, 93, 94 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
oField /r
.g |
96 | 90, 95 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
oField /r
|
97 | 75, 56 | syl 17 |
. . . . . . . . . . . . . 14
oField /r
|
98 | | simpr 477 |
. . . . . . . . . . . . . 14
oField /r
/r |
99 | 4, 74, 5, 76, 88, 96, 80, 6, 97, 98, 81 | orngrmullt 29808 |
. . . . . . . . . . . . 13
oField /r
/r |
100 | 4, 57, 61, 74 | dvrcan1 18691 |
. . . . . . . . . . . . . 14
Unit
/r |
101 | 77, 79, 87, 100 | syl3anc 1326 |
. . . . . . . . . . . . 13
oField /r
/r |
102 | 90 | oveq1d 6665 |
. . . . . . . . . . . . . 14
oField /r
.g |
103 | 4, 7, 74 | mulgass2 18601 |
. . . . . . . . . . . . . . 15
.g .g |
104 | 77, 92, 93, 80, 103 | syl13anc 1328 |
. . . . . . . . . . . . . 14
oField /r
.g .g |
105 | 4, 74, 11 | ringlidm 18571 |
. . . . . . . . . . . . . . . 16
|
106 | 77, 80, 105 | syl2anc 693 |
. . . . . . . . . . . . . . 15
oField /r
|
107 | 106 | oveq2d 6666 |
. . . . . . . . . . . . . 14
oField /r
.g .g |
108 | 102, 104,
107 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
oField /r
.g |
109 | 99, 101, 108 | 3brtr3d 4684 |
. . . . . . . . . . . 12
oField /r
.g |
110 | 109 | ex 450 |
. . . . . . . . . . 11
oField
/r
.g |
111 | 110 | reximdva 3017 |
. . . . . . . . . 10
oField
/r
.g |
112 | 111 | adantllr 755 |
. . . . . . . . 9
oField
/r
.g |
113 | 73, 112 | mpd 15 |
. . . . . . . 8
oField
.g |
114 | 113 | ex 450 |
. . . . . . 7
oField
.g |
115 | 114 | expr 643 |
. . . . . 6
oField
.g |
116 | 40, 115 | ralrimi 2957 |
. . . . 5
oField
.g |
117 | 116 | ralrimiva 2966 |
. . . 4
oField
.g |
118 | 117 | ex 450 |
. . 3
oField
.g |
119 | 35, 118 | impbid 202 |
. 2
oField
.g
|
120 | 9, 119 | bitrd 268 |
1
oField Archi
|