| Step | Hyp | Ref
| Expression |
|---|
| 1 | | lpirring 21181 |
. 2
β’ (π
β LPIR β π
β Ring) |
| 2 | | eqid 2726 |
. . . . . . . 8
β’
(LPIdealβπ
) =
(LPIdealβπ
) |
| 3 | | eqid 2726 |
. . . . . . . 8
β’
(RSpanβπ
) =
(RSpanβπ
) |
| 4 | | eqid 2726 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ
) |
| 5 | 2, 3, 4 | islpidl 21175 |
. . . . . . 7
β’ (π
β Ring β (π β (LPIdealβπ
) β βπ β (Baseβπ
)π = ((RSpanβπ
)β{π}))) |
| 6 | 1, 5 | syl 17 |
. . . . . 6
β’ (π
β LPIR β (π β (LPIdealβπ
) β βπ β (Baseβπ
)π = ((RSpanβπ
)β{π}))) |
| 7 | 6 | biimpa 476 |
. . . . 5
β’ ((π
β LPIR β§ π β (LPIdealβπ
)) β βπ β (Baseβπ
)π = ((RSpanβπ
)β{π})) |
| 8 | | snelpwi 5436 |
. . . . . . . . . 10
β’ (π β (Baseβπ
) β {π} β π« (Baseβπ
)) |
| 9 | 8 | adantl 481 |
. . . . . . . . 9
β’ (((π
β LPIR β§ π β (LPIdealβπ
)) β§ π β (Baseβπ
)) β {π} β π« (Baseβπ
)) |
| 10 | | snfi 9043 |
. . . . . . . . . 10
β’ {π} β Fin |
| 11 | 10 | a1i 11 |
. . . . . . . . 9
β’ (((π
β LPIR β§ π β (LPIdealβπ
)) β§ π β (Baseβπ
)) β {π} β Fin) |
| 12 | 9, 11 | elind 4189 |
. . . . . . . 8
β’ (((π
β LPIR β§ π β (LPIdealβπ
)) β§ π β (Baseβπ
)) β {π} β (π« (Baseβπ
) β© Fin)) |
| 13 | | eqid 2726 |
. . . . . . . 8
β’
((RSpanβπ
)β{π}) = ((RSpanβπ
)β{π}) |
| 14 | | fveq2 6884 |
. . . . . . . . 9
β’ (π = {π} β ((RSpanβπ
)βπ) = ((RSpanβπ
)β{π})) |
| 15 | 14 | rspceeqv 3628 |
. . . . . . . 8
β’ (({π} β (π«
(Baseβπ
) β© Fin)
β§ ((RSpanβπ
)β{π}) = ((RSpanβπ
)β{π})) β βπ β (π« (Baseβπ
) β© Fin)((RSpanβπ
)β{π}) = ((RSpanβπ
)βπ)) |
| 16 | 12, 13, 15 | sylancl 585 |
. . . . . . 7
β’ (((π
β LPIR β§ π β (LPIdealβπ
)) β§ π β (Baseβπ
)) β βπ β (π« (Baseβπ
) β© Fin)((RSpanβπ
)β{π}) = ((RSpanβπ
)βπ)) |
| 17 | | eqeq1 2730 |
. . . . . . . 8
β’ (π = ((RSpanβπ
)β{π}) β (π = ((RSpanβπ
)βπ) β ((RSpanβπ
)β{π}) = ((RSpanβπ
)βπ))) |
| 18 | 17 | rexbidv 3172 |
. . . . . . 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 3149 |
. . . . 5
β’ ((π
β LPIR β§ π β (LPIdealβπ
)) β (βπ β (Baseβπ
)π = ((RSpanβπ
)β{π}) β βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ))) |
| 21 | 7, 20 | mpd 15 |
. . . 4
β’ ((π
β LPIR β§ π β (LPIdealβπ
)) β βπ β (π«
(Baseβπ
) β©
Fin)π = ((RSpanβπ
)βπ)) |
| 22 | 21 | ralrimiva 3140 |
. . 3
β’ (π
β LPIR β
βπ β
(LPIdealβπ
)βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ)) |
| 23 | | eqid 2726 |
. . . . . 6
β’
(LIdealβπ
) =
(LIdealβπ
) |
| 24 | 2, 23 | islpir 21178 |
. . . . 5
β’ (π
β LPIR β (π
β Ring β§
(LIdealβπ
) =
(LPIdealβπ
))) |
| 25 | 24 | simprbi 496 |
. . . 4
β’ (π
β LPIR β
(LIdealβπ
) =
(LPIdealβπ
)) |
| 26 | 25 | raleqdv 3319 |
. . 3
β’ (π
β LPIR β
(βπ β
(LIdealβπ
)βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ) β βπ β (LPIdealβπ
)βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ))) |
| 27 | 22, 26 | mpbird 257 |
. 2
β’ (π
β LPIR β
βπ β
(LIdealβπ
)βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ)) |
| 28 | 4, 23, 3 | islnr2 42416 |
. 2
β’ (π
β LNoeR β (π
β Ring β§ βπ β (LIdealβπ
)βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ))) |
| 29 | 1, 27, 28 | sylanbrc 582 |
1
β’ (π
β LPIR β π
β LNoeR) |
