Step | Hyp | Ref
| Expression |
1 | | simpr 484 |
. . . . 5
β’
(((((π β§ π β (πΌ Γ πΈ)) β§ π β πΌ) β§ π β πΈ) β§ π = (π(.rβπ
)π)) β π = (π(.rβπ
)π)) |
2 | | ringlsmss1.1 |
. . . . . . . . . 10
β’ (π β π
β CRing) |
3 | 2 | ad2antrr 723 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ π β πΈ) β π
β CRing) |
4 | | ringlsmss1.2 |
. . . . . . . . . . 11
β’ (π β πΈ β π΅) |
5 | 4 | sselda 3977 |
. . . . . . . . . 10
β’ ((π β§ π β πΈ) β π β π΅) |
6 | 5 | adantlr 712 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ π β πΈ) β π β π΅) |
7 | | ringlsmss1.3 |
. . . . . . . . . . . 12
β’ (π β πΌ β (LIdealβπ
)) |
8 | | ringlsmss.1 |
. . . . . . . . . . . . 13
β’ π΅ = (Baseβπ
) |
9 | | eqid 2726 |
. . . . . . . . . . . . 13
β’
(LIdealβπ
) =
(LIdealβπ
) |
10 | 8, 9 | lidlss 21071 |
. . . . . . . . . . . 12
β’ (πΌ β (LIdealβπ
) β πΌ β π΅) |
11 | 7, 10 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΌ β π΅) |
12 | 11 | sselda 3977 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β π β π΅) |
13 | 12 | adantr 480 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ π β πΈ) β π β π΅) |
14 | | eqid 2726 |
. . . . . . . . . 10
β’
(.rβπ
) = (.rβπ
) |
15 | 8, 14 | crngcom 20156 |
. . . . . . . . 9
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β (π(.rβπ
)π) = (π(.rβπ
)π)) |
16 | 3, 6, 13, 15 | syl3anc 1368 |
. . . . . . . 8
β’ (((π β§ π β πΌ) β§ π β πΈ) β (π(.rβπ
)π) = (π(.rβπ
)π)) |
17 | | crngring 20150 |
. . . . . . . . . . 11
β’ (π
β CRing β π
β Ring) |
18 | 2, 17 | syl 17 |
. . . . . . . . . 10
β’ (π β π
β Ring) |
19 | 18 | ad2antrr 723 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ π β πΈ) β π
β Ring) |
20 | 7 | ad2antrr 723 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ π β πΈ) β πΌ β (LIdealβπ
)) |
21 | | simplr 766 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ π β πΈ) β π β πΌ) |
22 | 9, 8, 14 | lidlmcl 21084 |
. . . . . . . . 9
β’ (((π
β Ring β§ πΌ β (LIdealβπ
)) β§ (π β π΅ β§ π β πΌ)) β (π(.rβπ
)π) β πΌ) |
23 | 19, 20, 6, 21, 22 | syl22anc 836 |
. . . . . . . 8
β’ (((π β§ π β πΌ) β§ π β πΈ) β (π(.rβπ
)π) β πΌ) |
24 | 16, 23 | eqeltrrd 2828 |
. . . . . . 7
β’ (((π β§ π β πΌ) β§ π β πΈ) β (π(.rβπ
)π) β πΌ) |
25 | 24 | adantllr 716 |
. . . . . 6
β’ ((((π β§ π β (πΌ Γ πΈ)) β§ π β πΌ) β§ π β πΈ) β (π(.rβπ
)π) β πΌ) |
26 | 25 | adantr 480 |
. . . . 5
β’
(((((π β§ π β (πΌ Γ πΈ)) β§ π β πΌ) β§ π β πΈ) β§ π = (π(.rβπ
)π)) β (π(.rβπ
)π) β πΌ) |
27 | 1, 26 | eqeltrd 2827 |
. . . 4
β’
(((((π β§ π β (πΌ Γ πΈ)) β§ π β πΌ) β§ π β πΈ) β§ π = (π(.rβπ
)π)) β π β πΌ) |
28 | | ringlsmss.2 |
. . . . . 6
β’ πΊ = (mulGrpβπ
) |
29 | | ringlsmss.3 |
. . . . . 6
β’ Γ =
(LSSumβπΊ) |
30 | 8, 14, 28, 29, 11, 4 | elringlsm 33009 |
. . . . 5
β’ (π β (π β (πΌ Γ πΈ) β βπ β πΌ βπ β πΈ π = (π(.rβπ
)π))) |
31 | 30 | biimpa 476 |
. . . 4
β’ ((π β§ π β (πΌ Γ πΈ)) β βπ β πΌ βπ β πΈ π = (π(.rβπ
)π)) |
32 | 27, 31 | r19.29vva 3207 |
. . 3
β’ ((π β§ π β (πΌ Γ πΈ)) β π β πΌ) |
33 | 32 | ex 412 |
. 2
β’ (π β (π β (πΌ Γ πΈ) β π β πΌ)) |
34 | 33 | ssrdv 3983 |
1
β’ (π β (πΌ Γ πΈ) β πΌ) |