Step | Hyp | Ref
| Expression |
1 | | subrgpsr.s |
. . 3
β’ π = (πΌ mPwSer π
) |
2 | | simpl 484 |
. . 3
β’ ((πΌ β π β§ π β (SubRingβπ
)) β πΌ β π) |
3 | | subrgrcl 20269 |
. . . 4
β’ (π β (SubRingβπ
) β π
β Ring) |
4 | 3 | adantl 483 |
. . 3
β’ ((πΌ β π β§ π β (SubRingβπ
)) β π
β Ring) |
5 | 1, 2, 4 | psrring 21403 |
. 2
β’ ((πΌ β π β§ π β (SubRingβπ
)) β π β Ring) |
6 | | subrgpsr.u |
. . . 4
β’ π = (πΌ mPwSer π») |
7 | | subrgpsr.h |
. . . . . 6
β’ π» = (π
βΎs π) |
8 | 7 | subrgring 20267 |
. . . . 5
β’ (π β (SubRingβπ
) β π» β Ring) |
9 | 8 | adantl 483 |
. . . 4
β’ ((πΌ β π β§ π β (SubRingβπ
)) β π» β Ring) |
10 | 6, 2, 9 | psrring 21403 |
. . 3
β’ ((πΌ β π β§ π β (SubRingβπ
)) β π β Ring) |
11 | | subrgpsr.b |
. . . . 5
β’ π΅ = (Baseβπ) |
12 | 11 | a1i 11 |
. . . 4
β’ ((πΌ β π β§ π β (SubRingβπ
)) β π΅ = (Baseβπ)) |
13 | | eqid 2733 |
. . . . 5
β’ (π βΎs π΅) = (π βΎs π΅) |
14 | | simpr 486 |
. . . . 5
β’ ((πΌ β π β§ π β (SubRingβπ
)) β π β (SubRingβπ
)) |
15 | 1, 7, 6, 11, 13, 14 | resspsrbas 21407 |
. . . 4
β’ ((πΌ β π β§ π β (SubRingβπ
)) β π΅ = (Baseβ(π βΎs π΅))) |
16 | 1, 7, 6, 11, 13, 14 | resspsradd 21408 |
. . . 4
β’ (((πΌ β π β§ π β (SubRingβπ
)) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπ)π¦) = (π₯(+gβ(π βΎs π΅))π¦)) |
17 | 1, 7, 6, 11, 13, 14 | resspsrmul 21409 |
. . . 4
β’ (((πΌ β π β§ π β (SubRingβπ
)) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπ)π¦) = (π₯(.rβ(π βΎs π΅))π¦)) |
18 | 12, 15, 16, 17 | ringpropd 20014 |
. . 3
β’ ((πΌ β π β§ π β (SubRingβπ
)) β (π β Ring β (π βΎs π΅) β Ring)) |
19 | 10, 18 | mpbid 231 |
. 2
β’ ((πΌ β π β§ π β (SubRingβπ
)) β (π βΎs π΅) β Ring) |
20 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
21 | 13, 20 | ressbasss 17129 |
. . . 4
β’
(Baseβ(π
βΎs π΅))
β (Baseβπ) |
22 | 15, 21 | eqsstrdi 4002 |
. . 3
β’ ((πΌ β π β§ π β (SubRingβπ
)) β π΅ β (Baseβπ)) |
23 | | eqid 2733 |
. . . . . . 7
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
24 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ
) = (0gβπ
) |
25 | | eqid 2733 |
. . . . . . 7
β’
(1rβπ
) = (1rβπ
) |
26 | | eqid 2733 |
. . . . . . 7
β’
(1rβπ) = (1rβπ) |
27 | 1, 2, 4, 23, 24, 25, 26 | psr1 21404 |
. . . . . 6
β’ ((πΌ β π β§ π β (SubRingβπ
)) β (1rβπ) = (π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π₯ = (πΌ Γ {0}), (1rβπ
), (0gβπ
)))) |
28 | 25 | subrg1cl 20272 |
. . . . . . . . . 10
β’ (π β (SubRingβπ
) β
(1rβπ
)
β π) |
29 | | subrgsubg 20270 |
. . . . . . . . . . 11
β’ (π β (SubRingβπ
) β π β (SubGrpβπ
)) |
30 | 24 | subg0cl 18944 |
. . . . . . . . . . 11
β’ (π β (SubGrpβπ
) β
(0gβπ
)
β π) |
31 | 29, 30 | syl 17 |
. . . . . . . . . 10
β’ (π β (SubRingβπ
) β
(0gβπ
)
β π) |
32 | 28, 31 | ifcld 4536 |
. . . . . . . . 9
β’ (π β (SubRingβπ
) β if(π₯ = (πΌ Γ {0}), (1rβπ
), (0gβπ
)) β π) |
33 | 32 | adantl 483 |
. . . . . . . 8
β’ ((πΌ β π β§ π β (SubRingβπ
)) β if(π₯ = (πΌ Γ {0}), (1rβπ
), (0gβπ
)) β π) |
34 | 7 | subrgbas 20273 |
. . . . . . . . 9
β’ (π β (SubRingβπ
) β π = (Baseβπ»)) |
35 | 34 | adantl 483 |
. . . . . . . 8
β’ ((πΌ β π β§ π β (SubRingβπ
)) β π = (Baseβπ»)) |
36 | 33, 35 | eleqtrd 2836 |
. . . . . . 7
β’ ((πΌ β π β§ π β (SubRingβπ
)) β if(π₯ = (πΌ Γ {0}), (1rβπ
), (0gβπ
)) β (Baseβπ»)) |
37 | 36 | adantr 482 |
. . . . . 6
β’ (((πΌ β π β§ π β (SubRingβπ
)) β§ π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
if(π₯ = (πΌ Γ {0}), (1rβπ
), (0gβπ
)) β (Baseβπ»)) |
38 | 27, 37 | fmpt3d 7068 |
. . . . 5
β’ ((πΌ β π β§ π β (SubRingβπ
)) β (1rβπ):{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ»)) |
39 | | fvex 6859 |
. . . . . 6
β’
(Baseβπ»)
β V |
40 | | ovex 7394 |
. . . . . . 7
β’
(β0 βm πΌ) β V |
41 | 40 | rabex 5293 |
. . . . . 6
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β
V |
42 | 39, 41 | elmap 8815 |
. . . . 5
β’
((1rβπ) β ((Baseβπ») βm {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
(1rβπ):{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ»)) |
43 | 38, 42 | sylibr 233 |
. . . 4
β’ ((πΌ β π β§ π β (SubRingβπ
)) β (1rβπ) β ((Baseβπ») βm {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin})) |
44 | | eqid 2733 |
. . . . 5
β’
(Baseβπ») =
(Baseβπ») |
45 | 6, 44, 23, 11, 2 | psrbas 21369 |
. . . 4
β’ ((πΌ β π β§ π β (SubRingβπ
)) β π΅ = ((Baseβπ») βm {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin})) |
46 | 43, 45 | eleqtrrd 2837 |
. . 3
β’ ((πΌ β π β§ π β (SubRingβπ
)) β (1rβπ) β π΅) |
47 | 22, 46 | jca 513 |
. 2
β’ ((πΌ β π β§ π β (SubRingβπ
)) β (π΅ β (Baseβπ) β§ (1rβπ) β π΅)) |
48 | 20, 26 | issubrg 20264 |
. 2
β’ (π΅ β (SubRingβπ) β ((π β Ring β§ (π βΎs π΅) β Ring) β§ (π΅ β (Baseβπ) β§ (1rβπ) β π΅))) |
49 | 5, 19, 47, 48 | syl21anbrc 1345 |
1
β’ ((πΌ β π β§ π β (SubRingβπ
)) β π΅ β (SubRingβπ)) |