Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. 2
oRing
↾s ↾s |
2 | | ringgrp 18552 |
. . . 4
↾s
↾s |
3 | 2 | adantl 482 |
. . 3
oRing
↾s ↾s |
4 | | orngogrp 29801 |
. . . . 5
oRing oGrp |
5 | | isogrp 29702 |
. . . . . 6
oGrp oMnd |
6 | 5 | simprbi 480 |
. . . . 5
oGrp oMnd |
7 | 4, 6 | syl 17 |
. . . 4
oRing oMnd |
8 | | ringmnd 18556 |
. . . 4
↾s
↾s |
9 | | submomnd 29710 |
. . . 4
oMnd ↾s ↾s oMnd |
10 | 7, 8, 9 | syl2an 494 |
. . 3
oRing
↾s ↾s oMnd |
11 | | isogrp 29702 |
. . 3
↾s oGrp
↾s
↾s oMnd |
12 | 3, 10, 11 | sylanbrc 698 |
. 2
oRing
↾s ↾s oGrp |
13 | | simp-4l 806 |
. . . . . . 7
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
oRing |
14 | | reldmress 15926 |
. . . . . . . . . . . . . . 15
↾s |
15 | 14 | ovprc2 6685 |
. . . . . . . . . . . . . 14
↾s |
16 | 15 | fveq2d 6195 |
. . . . . . . . . . . . 13
↾s |
17 | 16 | adantl 482 |
. . . . . . . . . . . 12
oRing ↾s ↾s |
18 | | base0 15912 |
. . . . . . . . . . . 12
|
19 | 17, 18 | syl6eqr 2674 |
. . . . . . . . . . 11
oRing ↾s ↾s |
20 | | eqid 2622 |
. . . . . . . . . . . . . . 15
↾s ↾s |
21 | | eqid 2622 |
. . . . . . . . . . . . . . 15
↾s ↾s |
22 | 20, 21 | ringidcl 18568 |
. . . . . . . . . . . . . 14
↾s ↾s ↾s |
23 | | ne0i 3921 |
. . . . . . . . . . . . . 14
↾s ↾s ↾s |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . 13
↾s ↾s |
25 | 24 | ad2antlr 763 |
. . . . . . . . . . . 12
oRing ↾s ↾s |
26 | 25 | neneqd 2799 |
. . . . . . . . . . 11
oRing ↾s ↾s |
27 | 19, 26 | condan 835 |
. . . . . . . . . 10
oRing
↾s |
28 | | eqid 2622 |
. . . . . . . . . . . 12
↾s ↾s |
29 | | eqid 2622 |
. . . . . . . . . . . 12
|
30 | 28, 29 | ressbas 15930 |
. . . . . . . . . . 11
↾s |
31 | | inss2 3834 |
. . . . . . . . . . 11
|
32 | 30, 31 | syl6eqssr 3656 |
. . . . . . . . . 10
↾s
|
33 | 27, 32 | syl 17 |
. . . . . . . . 9
oRing
↾s ↾s |
34 | 33 | ad3antrrr 766 |
. . . . . . . 8
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
↾s |
35 | | simpllr 799 |
. . . . . . . 8
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
↾s |
36 | 34, 35 | sseldd 3604 |
. . . . . . 7
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
|
37 | | simprl 794 |
. . . . . . . 8
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
↾s ↾s |
38 | | orngring 29800 |
. . . . . . . . . . . . . . . 16
oRing |
39 | | ringgrp 18552 |
. . . . . . . . . . . . . . . 16
|
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . 15
oRing |
41 | 40 | adantr 481 |
. . . . . . . . . . . . . 14
oRing
↾s |
42 | 29 | ressinbas 15936 |
. . . . . . . . . . . . . . . . 17
↾s ↾s |
43 | 30 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
↾s
↾s ↾s |
44 | 42, 43 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
↾s ↾s ↾s |
45 | 27, 44 | syl 17 |
. . . . . . . . . . . . . . 15
oRing
↾s ↾s ↾s
↾s |
46 | 45, 3 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
oRing
↾s ↾s
↾s |
47 | 29 | issubg 17594 |
. . . . . . . . . . . . . 14
↾s SubGrp
↾s
↾s ↾s |
48 | 41, 33, 46, 47 | syl3anbrc 1246 |
. . . . . . . . . . . . 13
oRing
↾s ↾s SubGrp |
49 | | eqid 2622 |
. . . . . . . . . . . . . 14
↾s ↾s
↾s ↾s |
50 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
51 | 49, 50 | subg0 17600 |
. . . . . . . . . . . . 13
↾s SubGrp ↾s ↾s |
52 | 48, 51 | syl 17 |
. . . . . . . . . . . 12
oRing
↾s ↾s ↾s |
53 | 45 | fveq2d 6195 |
. . . . . . . . . . . 12
oRing
↾s
↾s ↾s ↾s |
54 | 52, 53 | eqtr4d 2659 |
. . . . . . . . . . 11
oRing
↾s ↾s |
55 | 54 | ad2antrr 762 |
. . . . . . . . . 10
oRing
↾s ↾s
↾s ↾s |
56 | 27 | ad2antrr 762 |
. . . . . . . . . . 11
oRing
↾s ↾s
↾s |
57 | | eqid 2622 |
. . . . . . . . . . . 12
|
58 | 28, 57 | ressle 16059 |
. . . . . . . . . . 11
↾s |
59 | 56, 58 | syl 17 |
. . . . . . . . . 10
oRing
↾s ↾s
↾s ↾s |
60 | | eqidd 2623 |
. . . . . . . . . 10
oRing
↾s ↾s
↾s |
61 | 55, 59, 60 | breq123d 4667 |
. . . . . . . . 9
oRing
↾s ↾s
↾s
↾s ↾s |
62 | 61 | adantr 481 |
. . . . . . . 8
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
↾s ↾s |
63 | 37, 62 | mpbird 247 |
. . . . . . 7
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
|
64 | | simplr 792 |
. . . . . . . 8
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
↾s |
65 | 34, 64 | sseldd 3604 |
. . . . . . 7
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
|
66 | | simprr 796 |
. . . . . . . 8
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
↾s ↾s |
67 | | eqidd 2623 |
. . . . . . . . . 10
oRing
↾s ↾s
↾s |
68 | 55, 59, 67 | breq123d 4667 |
. . . . . . . . 9
oRing
↾s ↾s
↾s
↾s ↾s |
69 | 68 | adantr 481 |
. . . . . . . 8
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
↾s ↾s |
70 | 66, 69 | mpbird 247 |
. . . . . . 7
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
|
71 | | eqid 2622 |
. . . . . . . 8
|
72 | 29, 57, 50, 71 | orngmul 29803 |
. . . . . . 7
oRing
|
73 | 13, 36, 63, 65, 70, 72 | syl122anc 1335 |
. . . . . 6
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
|
74 | 55 | adantr 481 |
. . . . . . 7
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
↾s |
75 | 59 | adantr 481 |
. . . . . . 7
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
↾s |
76 | 56 | adantr 481 |
. . . . . . . . 9
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
|
77 | 28, 71 | ressmulr 16006 |
. . . . . . . . 9
↾s |
78 | 76, 77 | syl 17 |
. . . . . . . 8
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
↾s |
79 | 78 | oveqd 6667 |
. . . . . . 7
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
↾s |
80 | 74, 75, 79 | breq123d 4667 |
. . . . . 6
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
↾s ↾s ↾s |
81 | 73, 80 | mpbid 222 |
. . . . 5
oRing
↾s
↾s ↾s ↾s
↾s
↾s ↾s
↾s ↾s ↾s |
82 | 81 | ex 450 |
. . . 4
oRing
↾s ↾s
↾s ↾s ↾s ↾s
↾s
↾s ↾s ↾s |
83 | 82 | anasss 679 |
. . 3
oRing ↾s ↾s
↾s
↾s ↾s ↾s ↾s ↾s ↾s ↾s |
84 | 83 | ralrimivva 2971 |
. 2
oRing
↾s ↾s ↾s
↾s ↾s ↾s ↾s ↾s ↾s ↾s |
85 | | eqid 2622 |
. . 3
↾s ↾s |
86 | | eqid 2622 |
. . 3
↾s ↾s |
87 | | eqid 2622 |
. . 3
↾s ↾s |
88 | 20, 85, 86, 87 | isorng 29799 |
. 2
↾s oRing
↾s
↾s oGrp
↾s
↾s
↾s ↾s ↾s ↾s ↾s ↾s ↾s |
89 | 1, 12, 84, 88 | syl3anbrc 1246 |
1
oRing
↾s ↾s oRing |