Step | Hyp | Ref
| Expression |
1 | | lpirring 20738 |
. 2
β’ (π
β LPIR β π
β Ring) |
2 | | eqid 2737 |
. . . . . . . 8
β’
(LPIdealβπ
) =
(LPIdealβπ
) |
3 | | eqid 2737 |
. . . . . . . 8
β’
(RSpanβπ
) =
(RSpanβπ
) |
4 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ
) |
5 | 2, 3, 4 | islpidl 20732 |
. . . . . . 7
β’ (π
β Ring β (π β (LPIdealβπ
) β βπ β (Baseβπ
)π = ((RSpanβπ
)β{π}))) |
6 | 1, 5 | syl 17 |
. . . . . 6
β’ (π
β LPIR β (π β (LPIdealβπ
) β βπ β (Baseβπ
)π = ((RSpanβπ
)β{π}))) |
7 | 6 | biimpa 478 |
. . . . 5
β’ ((π
β LPIR β§ π β (LPIdealβπ
)) β βπ β (Baseβπ
)π = ((RSpanβπ
)β{π})) |
8 | | snelpwi 5405 |
. . . . . . . . . 10
β’ (π β (Baseβπ
) β {π} β π« (Baseβπ
)) |
9 | 8 | adantl 483 |
. . . . . . . . 9
β’ (((π
β LPIR β§ π β (LPIdealβπ
)) β§ π β (Baseβπ
)) β {π} β π« (Baseβπ
)) |
10 | | snfi 8995 |
. . . . . . . . . 10
β’ {π} β Fin |
11 | 10 | a1i 11 |
. . . . . . . . 9
β’ (((π
β LPIR β§ π β (LPIdealβπ
)) β§ π β (Baseβπ
)) β {π} β Fin) |
12 | 9, 11 | elind 4159 |
. . . . . . . 8
β’ (((π
β LPIR β§ π β (LPIdealβπ
)) β§ π β (Baseβπ
)) β {π} β (π« (Baseβπ
) β© Fin)) |
13 | | eqid 2737 |
. . . . . . . 8
β’
((RSpanβπ
)β{π}) = ((RSpanβπ
)β{π}) |
14 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = {π} β ((RSpanβπ
)βπ) = ((RSpanβπ
)β{π})) |
15 | 14 | rspceeqv 3600 |
. . . . . . . 8
β’ (({π} β (π«
(Baseβπ
) β© Fin)
β§ ((RSpanβπ
)β{π}) = ((RSpanβπ
)β{π})) β βπ β (π« (Baseβπ
) β© Fin)((RSpanβπ
)β{π}) = ((RSpanβπ
)βπ)) |
16 | 12, 13, 15 | sylancl 587 |
. . . . . . 7
β’ (((π
β LPIR β§ π β (LPIdealβπ
)) β§ π β (Baseβπ
)) β βπ β (π« (Baseβπ
) β© Fin)((RSpanβπ
)β{π}) = ((RSpanβπ
)βπ)) |
17 | | eqeq1 2741 |
. . . . . . . 8
β’ (π = ((RSpanβπ
)β{π}) β (π = ((RSpanβπ
)βπ) β ((RSpanβπ
)β{π}) = ((RSpanβπ
)βπ))) |
18 | 17 | rexbidv 3176 |
. . . . . . 7
β’ (π = ((RSpanβπ
)β{π}) β (βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ) β βπ β (π« (Baseβπ
) β© Fin)((RSpanβπ
)β{π}) = ((RSpanβπ
)βπ))) |
19 | 16, 18 | syl5ibrcom 247 |
. . . . . 6
β’ (((π
β LPIR β§ π β (LPIdealβπ
)) β§ π β (Baseβπ
)) β (π = ((RSpanβπ
)β{π}) β βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ))) |
20 | 19 | rexlimdva 3153 |
. . . . 5
β’ ((π
β LPIR β§ π β (LPIdealβπ
)) β (βπ β (Baseβπ
)π = ((RSpanβπ
)β{π}) β βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ))) |
21 | 7, 20 | mpd 15 |
. . . 4
β’ ((π
β LPIR β§ π β (LPIdealβπ
)) β βπ β (π«
(Baseβπ
) β©
Fin)π = ((RSpanβπ
)βπ)) |
22 | 21 | ralrimiva 3144 |
. . 3
β’ (π
β LPIR β
βπ β
(LPIdealβπ
)βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ)) |
23 | | eqid 2737 |
. . . . . 6
β’
(LIdealβπ
) =
(LIdealβπ
) |
24 | 2, 23 | islpir 20735 |
. . . . 5
β’ (π
β LPIR β (π
β Ring β§
(LIdealβπ
) =
(LPIdealβπ
))) |
25 | 24 | simprbi 498 |
. . . 4
β’ (π
β LPIR β
(LIdealβπ
) =
(LPIdealβπ
)) |
26 | 25 | raleqdv 3316 |
. . 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 41470 |
. 2
β’ (π
β LNoeR β (π
β Ring β§ βπ β (LIdealβπ
)βπ β (π« (Baseβπ
) β© Fin)π = ((RSpanβπ
)βπ))) |
29 | 1, 27, 28 | sylanbrc 584 |
1
β’ (π
β LPIR β π
β LNoeR) |