Step | Hyp | Ref
| Expression |
1 | | lnrring 37682 |
. . 3
LNoeR |
2 | | hbt.p |
. . . 4
Poly1 |
3 | 2 | ply1ring 19618 |
. . 3
|
4 | 1, 3 | syl 17 |
. 2
LNoeR |
5 | | eqid 2622 |
. . . . . . . 8
|
6 | | eqid 2622 |
. . . . . . . 8
LIdeal LIdeal |
7 | 5, 6 | islnr3 37685 |
. . . . . . 7
LNoeR LIdeal NoeACS |
8 | 7 | simprbi 480 |
. . . . . 6
LNoeR LIdeal NoeACS |
9 | 8 | adantr 481 |
. . . . 5
LNoeR
LIdeal
LIdeal NoeACS |
10 | | eqid 2622 |
. . . . . . 7
LIdeal LIdeal |
11 | | eqid 2622 |
. . . . . . 7
ldgIdlSeq ldgIdlSeq |
12 | 2, 10, 11, 6 | hbtlem7 37695 |
. . . . . 6
LIdeal
ldgIdlSeqLIdeal |
13 | 1, 12 | sylan 488 |
. . . . 5
LNoeR
LIdeal
ldgIdlSeqLIdeal |
14 | 1 | ad2antrr 762 |
. . . . . . 7
LNoeR LIdeal
|
15 | | simplr 792 |
. . . . . . 7
LNoeR LIdeal
LIdeal |
16 | | simpr 477 |
. . . . . . 7
LNoeR LIdeal
|
17 | | peano2nn0 11333 |
. . . . . . . 8
|
18 | 17 | adantl 482 |
. . . . . . 7
LNoeR LIdeal
|
19 | | nn0re 11301 |
. . . . . . . . 9
|
20 | 19 | lep1d 10955 |
. . . . . . . 8
|
21 | 20 | adantl 482 |
. . . . . . 7
LNoeR LIdeal
|
22 | 2, 10, 11, 14, 15, 16, 18, 21 | hbtlem4 37696 |
. . . . . 6
LNoeR LIdeal
ldgIdlSeq
ldgIdlSeq |
23 | 22 | ralrimiva 2966 |
. . . . 5
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq |
24 | | nacsfix 37275 |
. . . . 5
LIdeal NoeACS ldgIdlSeqLIdeal
ldgIdlSeq
ldgIdlSeq ldgIdlSeq ldgIdlSeq |
25 | 9, 13, 23, 24 | syl3anc 1326 |
. . . 4
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq |
26 | | fzfi 12771 |
. . . . . . 7
|
27 | | eqid 2622 |
. . . . . . . . 9
RSpan RSpan |
28 | | simpll 790 |
. . . . . . . . 9
LNoeR LIdeal
LNoeR |
29 | | simplr 792 |
. . . . . . . . 9
LNoeR LIdeal
LIdeal |
30 | | elfznn0 12433 |
. . . . . . . . . 10
|
31 | 30 | adantl 482 |
. . . . . . . . 9
LNoeR LIdeal
|
32 | 2, 10, 11, 27, 28, 29, 31 | hbtlem6 37699 |
. . . . . . . 8
LNoeR LIdeal
ldgIdlSeq
ldgIdlSeqRSpan |
33 | 32 | ralrimiva 2966 |
. . . . . . 7
LNoeR
LIdeal
ldgIdlSeq
ldgIdlSeqRSpan |
34 | | fveq2 6191 |
. . . . . . . . . . 11
RSpan RSpan |
35 | 34 | fveq2d 6195 |
. . . . . . . . . 10
ldgIdlSeqRSpan ldgIdlSeqRSpan |
36 | 35 | fveq1d 6193 |
. . . . . . . . 9
ldgIdlSeqRSpan ldgIdlSeqRSpan |
37 | 36 | sseq2d 3633 |
. . . . . . . 8
ldgIdlSeq ldgIdlSeqRSpan ldgIdlSeq ldgIdlSeqRSpan |
38 | 37 | ac6sfi 8204 |
. . . . . . 7
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeq ldgIdlSeqRSpan |
39 | 26, 33, 38 | sylancr 695 |
. . . . . 6
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeqRSpan |
40 | 39 | adantr 481 |
. . . . 5
LNoeR LIdeal
ldgIdlSeq ldgIdlSeq ldgIdlSeq ldgIdlSeqRSpan |
41 | | frn 6053 |
. . . . . . . . . . . . 13
|
42 | 41 | ad2antrl 764 |
. . . . . . . . . . . 12
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
43 | | inss1 3833 |
. . . . . . . . . . . 12
|
44 | 42, 43 | syl6ss 3615 |
. . . . . . . . . . 11
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
45 | 44 | unissd 4462 |
. . . . . . . . . 10
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
46 | | unipw 4918 |
. . . . . . . . . 10
|
47 | 45, 46 | syl6sseq 3651 |
. . . . . . . . 9
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
48 | | simpllr 799 |
. . . . . . . . . 10
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
LIdeal |
49 | | eqid 2622 |
. . . . . . . . . . 11
|
50 | 49, 10 | lidlss 19210 |
. . . . . . . . . 10
LIdeal
|
51 | 48, 50 | syl 17 |
. . . . . . . . 9
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
52 | 47, 51 | sstrd 3613 |
. . . . . . . 8
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
53 | | fvex 6201 |
. . . . . . . . 9
|
54 | 53 | elpw2 4828 |
. . . . . . . 8
|
55 | 52, 54 | sylibr 224 |
. . . . . . 7
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
56 | | simprl 794 |
. . . . . . . . 9
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
57 | | ffn 6045 |
. . . . . . . . 9
|
58 | | fniunfv 6505 |
. . . . . . . . 9
|
59 | 56, 57, 58 | 3syl 18 |
. . . . . . . 8
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
60 | | inss2 3834 |
. . . . . . . . . . 11
|
61 | 56 | ffvelrnda 6359 |
. . . . . . . . . . 11
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan |
62 | 60, 61 | sseldi 3601 |
. . . . . . . . . 10
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan |
63 | 62 | ralrimiva 2966 |
. . . . . . . . 9
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
64 | | iunfi 8254 |
. . . . . . . . 9
|
65 | 26, 63, 64 | sylancr 695 |
. . . . . . . 8
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
66 | 59, 65 | eqeltrrd 2702 |
. . . . . . 7
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
67 | 55, 66 | elind 3798 |
. . . . . 6
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
68 | 1 | ad3antrrr 766 |
. . . . . . . 8
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
69 | 4 | ad3antrrr 766 |
. . . . . . . . 9
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
70 | 27, 49, 10 | rspcl 19222 |
. . . . . . . . 9
RSpan LIdeal |
71 | 69, 52, 70 | syl2anc 693 |
. . . . . . . 8
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
RSpan LIdeal |
72 | 27, 10 | rspssp 19226 |
. . . . . . . . 9
LIdeal RSpan |
73 | 69, 48, 47, 72 | syl3anc 1326 |
. . . . . . . 8
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
RSpan |
74 | | nn0re 11301 |
. . . . . . . . . . 11
|
75 | 74 | adantl 482 |
. . . . . . . . . 10
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan |
76 | | simplrl 800 |
. . . . . . . . . . . 12
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
77 | 76 | adantr 481 |
. . . . . . . . . . 11
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan |
78 | 77 | nn0red 11352 |
. . . . . . . . . 10
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan |
79 | | simprl 794 |
. . . . . . . . . . . . . 14
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
80 | | simprr 796 |
. . . . . . . . . . . . . 14
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
81 | 76 | adantr 481 |
. . . . . . . . . . . . . . 15
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
82 | | fznn0 12432 |
. . . . . . . . . . . . . . 15
|
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . 14
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
84 | 79, 80, 83 | mpbir2and 957 |
. . . . . . . . . . . . 13
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
85 | | simplrr 801 |
. . . . . . . . . . . . 13
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeq ldgIdlSeqRSpan |
86 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
ldgIdlSeq ldgIdlSeq |
87 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
88 | 87 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
RSpan RSpan |
89 | 88 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
ldgIdlSeqRSpan ldgIdlSeqRSpan |
90 | | id 22 |
. . . . . . . . . . . . . . . 16
|
91 | 89, 90 | fveq12d 6197 |
. . . . . . . . . . . . . . 15
ldgIdlSeqRSpan ldgIdlSeqRSpan |
92 | 86, 91 | sseq12d 3634 |
. . . . . . . . . . . . . 14
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeq
ldgIdlSeqRSpan |
93 | 92 | rspcva 3307 |
. . . . . . . . . . . . 13
ldgIdlSeq ldgIdlSeqRSpan ldgIdlSeq ldgIdlSeqRSpan |
94 | 84, 85, 93 | syl2anc 693 |
. . . . . . . . . . . 12
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeq ldgIdlSeqRSpan |
95 | 68 | adantr 481 |
. . . . . . . . . . . . 13
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
96 | | fvssunirn 6217 |
. . . . . . . . . . . . . . . 16
|
97 | 96, 52 | syl5ss 3614 |
. . . . . . . . . . . . . . 15
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
98 | 27, 49, 10 | rspcl 19222 |
. . . . . . . . . . . . . . 15
RSpan LIdeal |
99 | 69, 97, 98 | syl2anc 693 |
. . . . . . . . . . . . . 14
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
RSpan LIdeal |
100 | 99 | adantr 481 |
. . . . . . . . . . . . 13
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
RSpan LIdeal |
101 | 71 | adantr 481 |
. . . . . . . . . . . . 13
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
RSpan LIdeal |
102 | 68, 3 | syl 17 |
. . . . . . . . . . . . . . 15
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
103 | 102 | adantr 481 |
. . . . . . . . . . . . . 14
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
104 | 27, 49 | rspssid 19223 |
. . . . . . . . . . . . . . . . 17
RSpan |
105 | 69, 52, 104 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
RSpan |
106 | 105 | adantr 481 |
. . . . . . . . . . . . . . 15
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
RSpan |
107 | 96, 106 | syl5ss 3614 |
. . . . . . . . . . . . . 14
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
RSpan |
108 | 27, 10 | rspssp 19226 |
. . . . . . . . . . . . . 14
RSpan LIdeal
RSpan
RSpan
RSpan |
109 | 103, 101,
107, 108 | syl3anc 1326 |
. . . . . . . . . . . . 13
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
RSpan RSpan |
110 | 2, 10, 11, 95, 100, 101, 109, 79 | hbtlem3 37697 |
. . . . . . . . . . . 12
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeqRSpan
ldgIdlSeqRSpan |
111 | 94, 110 | sstrd 3613 |
. . . . . . . . . . 11
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeq ldgIdlSeqRSpan |
112 | 111 | anassrs 680 |
. . . . . . . . . 10
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan ldgIdlSeq
ldgIdlSeqRSpan |
113 | | nn0z 11400 |
. . . . . . . . . . . . . . . 16
|
114 | 113 | adantr 481 |
. . . . . . . . . . . . . . 15
|
115 | | nn0z 11400 |
. . . . . . . . . . . . . . . 16
|
116 | 115 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
|
117 | | simprr 796 |
. . . . . . . . . . . . . . 15
|
118 | | eluz2 11693 |
. . . . . . . . . . . . . . 15
|
119 | 114, 116,
117, 118 | syl3anbrc 1246 |
. . . . . . . . . . . . . 14
|
120 | 76, 119 | sylan 488 |
. . . . . . . . . . . . 13
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
121 | | simprr 796 |
. . . . . . . . . . . . . 14
LNoeR LIdeal
ldgIdlSeq ldgIdlSeq ldgIdlSeq ldgIdlSeq |
122 | 121 | ad2antrr 762 |
. . . . . . . . . . . . 13
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeq ldgIdlSeq |
123 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
ldgIdlSeq ldgIdlSeq |
124 | 123 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeq |
125 | 124 | rspcva 3307 |
. . . . . . . . . . . . 13
ldgIdlSeq ldgIdlSeq ldgIdlSeq ldgIdlSeq |
126 | 120, 122,
125 | syl2anc 693 |
. . . . . . . . . . . 12
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeq ldgIdlSeq |
127 | 76 | nn0red 11352 |
. . . . . . . . . . . . . . . 16
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
128 | 127 | leidd 10594 |
. . . . . . . . . . . . . . 15
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
129 | 111 | expr 643 |
. . . . . . . . . . . . . . . . 17
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeq ldgIdlSeqRSpan |
130 | 129 | ralrimiva 2966 |
. . . . . . . . . . . . . . . 16
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeq
ldgIdlSeqRSpan |
131 | | breq1 4656 |
. . . . . . . . . . . . . . . . . 18
|
132 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
ldgIdlSeq ldgIdlSeq |
133 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
ldgIdlSeqRSpan ldgIdlSeqRSpan |
134 | 132, 133 | sseq12d 3634 |
. . . . . . . . . . . . . . . . . 18
ldgIdlSeq ldgIdlSeqRSpan ldgIdlSeq ldgIdlSeqRSpan |
135 | 131, 134 | imbi12d 334 |
. . . . . . . . . . . . . . . . 17
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeq
ldgIdlSeqRSpan |
136 | 135 | rspcva 3307 |
. . . . . . . . . . . . . . . 16
ldgIdlSeq ldgIdlSeqRSpan ldgIdlSeq ldgIdlSeqRSpan |
137 | 76, 130, 136 | syl2anc 693 |
. . . . . . . . . . . . . . 15
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeq
ldgIdlSeqRSpan |
138 | 128, 137 | mpd 15 |
. . . . . . . . . . . . . 14
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeq
ldgIdlSeqRSpan |
139 | 138 | adantr 481 |
. . . . . . . . . . . . 13
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeq ldgIdlSeqRSpan |
140 | 68 | adantr 481 |
. . . . . . . . . . . . . 14
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
141 | 71 | adantr 481 |
. . . . . . . . . . . . . 14
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
RSpan LIdeal |
142 | 76 | adantr 481 |
. . . . . . . . . . . . . 14
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
143 | | simprl 794 |
. . . . . . . . . . . . . 14
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
144 | | simprr 796 |
. . . . . . . . . . . . . 14
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
|
145 | 2, 10, 11, 140, 141, 142, 143, 144 | hbtlem4 37696 |
. . . . . . . . . . . . 13
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeqRSpan ldgIdlSeqRSpan |
146 | 139, 145 | sstrd 3613 |
. . . . . . . . . . . 12
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeq ldgIdlSeqRSpan |
147 | 126, 146 | eqsstrd 3639 |
. . . . . . . . . . 11
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeq ldgIdlSeqRSpan |
148 | 147 | anassrs 680 |
. . . . . . . . . 10
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan ldgIdlSeq
ldgIdlSeqRSpan |
149 | 75, 78, 112, 148 | lecasei 10143 |
. . . . . . . . 9
LNoeR
LIdeal
ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan ldgIdlSeq
ldgIdlSeqRSpan |
150 | 149 | ralrimiva 2966 |
. . . . . . . 8
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
ldgIdlSeq ldgIdlSeqRSpan |
151 | 2, 10, 11, 68, 71, 48, 73, 150 | hbtlem5 37698 |
. . . . . . 7
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
RSpan |
152 | 151 | eqcomd 2628 |
. . . . . 6
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
RSpan |
153 | | fveq2 6191 |
. . . . . . . 8
RSpan RSpan |
154 | 153 | eqeq2d 2632 |
. . . . . . 7
RSpan
RSpan |
155 | 154 | rspcev 3309 |
. . . . . 6
RSpan
RSpan |
156 | 67, 152, 155 | syl2anc 693 |
. . . . 5
LNoeR
LIdeal ldgIdlSeq ldgIdlSeq
ldgIdlSeq ldgIdlSeqRSpan
RSpan |
157 | 40, 156 | exlimddv 1863 |
. . . 4
LNoeR LIdeal
ldgIdlSeq ldgIdlSeq
RSpan |
158 | 25, 157 | rexlimddv 3035 |
. . 3
LNoeR
LIdeal
RSpan |
159 | 158 | ralrimiva 2966 |
. 2
LNoeR LIdeal RSpan |
160 | 49, 10, 27 | islnr2 37684 |
. 2
LNoeR LIdeal RSpan |
161 | 4, 159, 160 | sylanbrc 698 |
1
LNoeR LNoeR |