Step |
Hyp |
Ref |
Expression |
1 |
|
ply1lpir.p |
|- P = ( Poly1 ` R ) |
2 |
|
drngring |
|- ( R e. DivRing -> R e. Ring ) |
3 |
1
|
ply1ring |
|- ( R e. Ring -> P e. Ring ) |
4 |
2 3
|
syl |
|- ( R e. DivRing -> P e. Ring ) |
5 |
|
eqid |
|- ( Base ` P ) = ( Base ` P ) |
6 |
|
eqid |
|- ( LIdeal ` P ) = ( LIdeal ` P ) |
7 |
5 6
|
lidlss |
|- ( i e. ( LIdeal ` P ) -> i C_ ( Base ` P ) ) |
8 |
7
|
adantl |
|- ( ( R e. DivRing /\ i e. ( LIdeal ` P ) ) -> i C_ ( Base ` P ) ) |
9 |
|
eqid |
|- ( idlGen1p ` R ) = ( idlGen1p ` R ) |
10 |
1 9 6
|
ig1pcl |
|- ( ( R e. DivRing /\ i e. ( LIdeal ` P ) ) -> ( ( idlGen1p ` R ) ` i ) e. i ) |
11 |
8 10
|
sseldd |
|- ( ( R e. DivRing /\ i e. ( LIdeal ` P ) ) -> ( ( idlGen1p ` R ) ` i ) e. ( Base ` P ) ) |
12 |
|
eqid |
|- ( RSpan ` P ) = ( RSpan ` P ) |
13 |
1 9 6 12
|
ig1prsp |
|- ( ( R e. DivRing /\ i e. ( LIdeal ` P ) ) -> i = ( ( RSpan ` P ) ` { ( ( idlGen1p ` R ) ` i ) } ) ) |
14 |
|
sneq |
|- ( j = ( ( idlGen1p ` R ) ` i ) -> { j } = { ( ( idlGen1p ` R ) ` i ) } ) |
15 |
14
|
fveq2d |
|- ( j = ( ( idlGen1p ` R ) ` i ) -> ( ( RSpan ` P ) ` { j } ) = ( ( RSpan ` P ) ` { ( ( idlGen1p ` R ) ` i ) } ) ) |
16 |
15
|
rspceeqv |
|- ( ( ( ( idlGen1p ` R ) ` i ) e. ( Base ` P ) /\ i = ( ( RSpan ` P ) ` { ( ( idlGen1p ` R ) ` i ) } ) ) -> E. j e. ( Base ` P ) i = ( ( RSpan ` P ) ` { j } ) ) |
17 |
11 13 16
|
syl2anc |
|- ( ( R e. DivRing /\ i e. ( LIdeal ` P ) ) -> E. j e. ( Base ` P ) i = ( ( RSpan ` P ) ` { j } ) ) |
18 |
4
|
adantr |
|- ( ( R e. DivRing /\ i e. ( LIdeal ` P ) ) -> P e. Ring ) |
19 |
|
eqid |
|- ( LPIdeal ` P ) = ( LPIdeal ` P ) |
20 |
19 12 5
|
islpidl |
|- ( P e. Ring -> ( i e. ( LPIdeal ` P ) <-> E. j e. ( Base ` P ) i = ( ( RSpan ` P ) ` { j } ) ) ) |
21 |
18 20
|
syl |
|- ( ( R e. DivRing /\ i e. ( LIdeal ` P ) ) -> ( i e. ( LPIdeal ` P ) <-> E. j e. ( Base ` P ) i = ( ( RSpan ` P ) ` { j } ) ) ) |
22 |
17 21
|
mpbird |
|- ( ( R e. DivRing /\ i e. ( LIdeal ` P ) ) -> i e. ( LPIdeal ` P ) ) |
23 |
22
|
ex |
|- ( R e. DivRing -> ( i e. ( LIdeal ` P ) -> i e. ( LPIdeal ` P ) ) ) |
24 |
23
|
ssrdv |
|- ( R e. DivRing -> ( LIdeal ` P ) C_ ( LPIdeal ` P ) ) |
25 |
19 6
|
islpir2 |
|- ( P e. LPIR <-> ( P e. Ring /\ ( LIdeal ` P ) C_ ( LPIdeal ` P ) ) ) |
26 |
4 24 25
|
sylanbrc |
|- ( R e. DivRing -> P e. LPIR ) |