| Step | Hyp | Ref
| Expression |
|---|
| 1 | | eqid 2728 |
. . . 4
β’
(Baseβπ
) =
(Baseβπ
) |
| 2 | | rnglidl0.z |
. . . 4
β’ 0 =
(0gβπ
) |
| 3 | 1, 2 | rng0cl 20117 |
. . 3
β’ (π
β Rng β 0 β
(Baseβπ
)) |
| 4 | 3 | snssd 4817 |
. 2
β’ (π
β Rng β { 0 } β
(Baseβπ
)) |
| 5 | 2 | fvexi 6916 |
. . . 4
β’ 0 β
V |
| 6 | 5 | a1i 11 |
. . 3
β’ (π
β Rng β 0 β
V) |
| 7 | 6 | snn0d 4784 |
. 2
β’ (π
β Rng β { 0 } β
β
) |
| 8 | | eqid 2728 |
. . . . . . . 8
β’
(.rβπ
) = (.rβπ
) |
| 9 | 1, 8, 2 | rngrz 20120 |
. . . . . . 7
β’ ((π
β Rng β§ π₯ β (Baseβπ
)) β (π₯(.rβπ
) 0 ) = 0 ) |
| 10 | 9 | oveq1d 7441 |
. . . . . 6
β’ ((π
β Rng β§ π₯ β (Baseβπ
)) β ((π₯(.rβπ
) 0
)(+gβπ
)
0 ) = (
0
(+gβπ
)
0
)) |
| 11 | | rnggrp 20112 |
. . . . . . . 8
β’ (π
β Rng β π
β Grp) |
| 12 | 1, 2 | grpidcl 18936 |
. . . . . . . 8
β’ (π
β Grp β 0 β
(Baseβπ
)) |
| 13 | | eqid 2728 |
. . . . . . . . 9
β’
(+gβπ
) = (+gβπ
) |
| 14 | 1, 13, 2 | grprid 18939 |
. . . . . . . 8
β’ ((π
β Grp β§ 0 β
(Baseβπ
)) β (
0
(+gβπ
)
0 ) =
0
) |
| 15 | 11, 12, 14 | syl2anc2 583 |
. . . . . . 7
β’ (π
β Rng β ( 0
(+gβπ
)
0 ) =
0
) |
| 16 | 15 | adantr 479 |
. . . . . 6
β’ ((π
β Rng β§ π₯ β (Baseβπ
)) β ( 0 (+gβπ
) 0 ) = 0 ) |
| 17 | 10, 16 | eqtrd 2768 |
. . . . 5
β’ ((π
β Rng β§ π₯ β (Baseβπ
)) β ((π₯(.rβπ
) 0
)(+gβπ
)
0 ) =
0
) |
| 18 | 5 | elsn2 4672 |
. . . . 5
β’ (((π₯(.rβπ
) 0
)(+gβπ
)
0 )
β { 0 } β ((π₯(.rβπ
) 0
)(+gβπ
)
0 ) =
0
) |
| 19 | 17, 18 | sylibr 233 |
. . . 4
β’ ((π
β Rng β§ π₯ β (Baseβπ
)) β ((π₯(.rβπ
) 0
)(+gβπ
)
0 )
β { 0 }) |
| 20 | | oveq2 7434 |
. . . . . . . . 9
β’ (π¦ = 0 β (π₯(.rβπ
)π¦) = (π₯(.rβπ
) 0 )) |
| 21 | 20 | oveq1d 7441 |
. . . . . . . 8
β’ (π¦ = 0 β ((π₯(.rβπ
)π¦)(+gβπ
)π§) = ((π₯(.rβπ
) 0
)(+gβπ
)π§)) |
| 22 | 21 | eleq1d 2814 |
. . . . . . 7
β’ (π¦ = 0 β (((π₯(.rβπ
)π¦)(+gβπ
)π§) β { 0 } β ((π₯(.rβπ
) 0
)(+gβπ
)π§) β { 0 })) |
| 23 | 22 | ralbidv 3175 |
. . . . . 6
β’ (π¦ = 0 β (βπ§ β { 0 } ((π₯(.rβπ
)π¦)(+gβπ
)π§) β { 0 } β βπ§ β { 0 } ((π₯(.rβπ
) 0
)(+gβπ
)π§) β { 0 })) |
| 24 | 5, 23 | ralsn 4690 |
. . . . 5
β’
(βπ¦ β {
0
}βπ§ β { 0 } ((π₯(.rβπ
)π¦)(+gβπ
)π§) β { 0 } β βπ§ β { 0 } ((π₯(.rβπ
) 0
)(+gβπ
)π§) β { 0 }) |
| 25 | | oveq2 7434 |
. . . . . . 7
β’ (π§ = 0 β ((π₯(.rβπ
) 0
)(+gβπ
)π§) = ((π₯(.rβπ
) 0
)(+gβπ
)
0
)) |
| 26 | 25 | eleq1d 2814 |
. . . . . 6
β’ (π§ = 0 β (((π₯(.rβπ
) 0
)(+gβπ
)π§) β { 0 } β ((π₯(.rβπ
) 0
)(+gβπ
)
0 )
β { 0 })) |
| 27 | 5, 26 | ralsn 4690 |
. . . . 5
β’
(βπ§ β {
0 }
((π₯(.rβπ
) 0
)(+gβπ
)π§) β { 0 } β ((π₯(.rβπ
) 0
)(+gβπ
)
0 )
β { 0 }) |
| 28 | 24, 27 | bitri 274 |
. . . 4
β’
(βπ¦ β {
0
}βπ§ β { 0 } ((π₯(.rβπ
)π¦)(+gβπ
)π§) β { 0 } β ((π₯(.rβπ
) 0
)(+gβπ
)
0 )
β { 0 }) |
| 29 | 19, 28 | sylibr 233 |
. . 3
β’ ((π
β Rng β§ π₯ β (Baseβπ
)) β βπ¦ β { 0 }βπ§ β { 0 } ((π₯(.rβπ
)π¦)(+gβπ
)π§) β { 0 }) |
| 30 | 29 | ralrimiva 3143 |
. 2
β’ (π
β Rng β βπ₯ β (Baseβπ
)βπ¦ β { 0 }βπ§ β { 0 } ((π₯(.rβπ
)π¦)(+gβπ
)π§) β { 0 }) |
| 31 | | rnglidl0.u |
. . 3
β’ π = (LIdealβπ
) |
| 32 | 31, 1, 13, 8 | islidl 21125 |
. 2
β’ ({ 0 } β
π β ({ 0 } β
(Baseβπ
) β§ {
0 } β
β
β§ βπ₯
β (Baseβπ
)βπ¦ β { 0 }βπ§ β { 0 } ((π₯(.rβπ
)π¦)(+gβπ
)π§) β { 0 })) |
| 33 | 4, 7, 30, 32 | syl3anbrc 1340 |
1
β’ (π
β Rng β { 0 } β
π) |
