| Step | Hyp | Ref
| Expression |
|---|
| 1 | | lpirring 21228 |
. 2
β’ (π
β LPIR β π
β Ring) |
| 2 | | eqid 2728 |
. . . . . . . 8
β’
(LPIdealβπ
) =
(LPIdealβπ
) |
| 3 | | eqid 2728 |
. . . . . . . 8
β’
(RSpanβπ
) =
(RSpanβπ
) |
| 4 | | eqid 2728 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ
) |
| 5 | 2, 3, 4 | islpidl 21222 |
. . . . . . 7
β’ (π
β Ring β (π β (LPIdealβπ
) β βπ β (Baseβπ
)π = ((RSpanβπ
)β{π}))) |
| 6 | 1, 5 | syl 17 |
. . . . . 6
β’ (π
β LPIR β (π β (LPIdealβπ
) β βπ β (Baseβπ
)π = ((RSpanβπ
)β{π}))) |
| 7 | 6 | biimpa 475 |
. . . . 5
β’ ((π
β LPIR β§ π β (LPIdealβπ
)) β βπ β (Baseβπ
)π = ((RSpanβπ
)β{π})) |
| 8 | | snelpwi 5449 |
. . . . . . . . . 10
β’ (π β (Baseβπ
) β {π} β π« (Baseβπ
)) |
| 9 | 8 | adantl 480 |
. . . . . . . . 9
β’ (((π
β LPIR β§ π β (LPIdealβπ
)) β§ π β (Baseβπ
)) β {π} β π« (Baseβπ
)) |
| 10 | | snfi 9075 |
. . . . . . . . . 10
β’ {π} β Fin |
| 11 | 10 | a1i 11 |
. . . . . . . . 9
β’ (((π
β LPIR β§ π β (LPIdealβπ
)) β§ π β (Baseβπ
)) β {π} β Fin) |
| 12 | 9, 11 | elind 4196 |
. . . . . . . 8
β’ (((π
β LPIR β§ π β (LPIdealβπ
)) β§ π β (Baseβπ
)) β {π} β (π« (Baseβπ
) β© Fin)) |
| 13 | | eqid 2728 |
. . . . . . . 8
β’
((RSpanβπ
)β{π}) = ((RSpanβπ
)β{π}) |
| 14 | | fveq2 6902 |
. . . . . . . . 9
β’ (π = {π} β ((RSpanβπ
)βπ) = ((RSpanβπ
)β{π})) |
| 15 | 14 | rspceeqv 3633 |
. . . . . . . 8
β’ (({π} β (π«
(Baseβπ
) β© Fin)
β§ ((RSpanβπ
)β{π}) = ((RSpanβπ
)β{π})) β βπ β (π« (Baseβπ
) β© Fin)((RSpanβπ
)β{π}) = ((RSpanβπ
)βπ)) |
| 16 | 12, 13, 15 | sylancl 584 |
. . . . . . 7
β’ (((π
β LPIR β§ π β (LPIdealβπ
)) β§ π β (Baseβπ
)) β βπ β (π« (Baseβπ
) β© Fin)((RSpanβπ
)β{π}) = ((RSpanβπ
)βπ)) |
| 17 | | eqeq1 2732 |
. . . . . . . 8
β’ (π = ((RSpanβπ
)β{π}) β (π = ((RSpanβπ
)βπ) β ((RSpanβπ
)β{π}) = ((RSpanβπ
)βπ))) |
| 18 | 17 | rexbidv 3176 |
. . . . . . 7
β’ (π = ((RSpanβπ
)β{π}) β (βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ) β βπ β (π« (Baseβπ
) β© Fin)((RSpanβπ
)β{π}) = ((RSpanβπ
)βπ))) |
| 19 | 16, 18 | syl5ibrcom 246 |
. . . . . 6
β’ (((π
β LPIR β§ π β (LPIdealβπ
)) β§ π β (Baseβπ
)) β (π = ((RSpanβπ
)β{π}) β βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ))) |
| 20 | 19 | rexlimdva 3152 |
. . . . 5
β’ ((π
β LPIR β§ π β (LPIdealβπ
)) β (βπ β (Baseβπ
)π = ((RSpanβπ
)β{π}) β βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ))) |
| 21 | 7, 20 | mpd 15 |
. . . 4
β’ ((π
β LPIR β§ π β (LPIdealβπ
)) β βπ β (π«
(Baseβπ
) β©
Fin)π = ((RSpanβπ
)βπ)) |
| 22 | 21 | ralrimiva 3143 |
. . 3
β’ (π
β LPIR β
βπ β
(LPIdealβπ
)βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ)) |
| 23 | | eqid 2728 |
. . . . . 6
β’
(LIdealβπ
) =
(LIdealβπ
) |
| 24 | 2, 23 | islpir 21225 |
. . . . 5
β’ (π
β LPIR β (π
β Ring β§
(LIdealβπ
) =
(LPIdealβπ
))) |
| 25 | 24 | simprbi 495 |
. . . 4
β’ (π
β LPIR β
(LIdealβπ
) =
(LPIdealβπ
)) |
| 26 | 25 | raleqdv 3323 |
. . 3
β’ (π
β LPIR β
(βπ β
(LIdealβπ
)βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ) β βπ β (LPIdealβπ
)βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ))) |
| 27 | 22, 26 | mpbird 256 |
. 2
β’ (π
β LPIR β
βπ β
(LIdealβπ
)βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ)) |
| 28 | 4, 23, 3 | islnr2 42569 |
. 2
β’ (π
β LNoeR β (π
β Ring β§ βπ β (LIdealβπ
)βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ))) |
| 29 | 1, 27, 28 | sylanbrc 581 |
1
β’ (π
β LPIR β π
β LNoeR) |
