Step | Hyp | Ref
| Expression |
1 | | mplsubg.s |
. . 3
β’ π = (πΌ mPwSer π
) |
2 | | mplsubg.p |
. . 3
β’ π = (πΌ mPoly π
) |
3 | | mplsubg.u |
. . 3
β’ π = (Baseβπ) |
4 | | mplsubg.i |
. . 3
β’ (π β πΌ β π) |
5 | | mpllss.r |
. . . 4
β’ (π β π
β Ring) |
6 | | ringgrp 19976 |
. . . 4
β’ (π
β Ring β π
β Grp) |
7 | 5, 6 | syl 17 |
. . 3
β’ (π β π
β Grp) |
8 | 1, 2, 3, 4, 7 | mplsubg 21424 |
. 2
β’ (π β π β (SubGrpβπ)) |
9 | 1, 4, 5 | psrring 21396 |
. . . 4
β’ (π β π β Ring) |
10 | | eqid 2737 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
11 | | eqid 2737 |
. . . . 5
β’
(1rβπ) = (1rβπ) |
12 | 10, 11 | ringidcl 19996 |
. . . 4
β’ (π β Ring β
(1rβπ)
β (Baseβπ)) |
13 | 9, 12 | syl 17 |
. . 3
β’ (π β (1rβπ) β (Baseβπ)) |
14 | | eqid 2737 |
. . . . 5
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
15 | | eqid 2737 |
. . . . 5
β’
(0gβπ
) = (0gβπ
) |
16 | | eqid 2737 |
. . . . 5
β’
(1rβπ
) = (1rβπ
) |
17 | 1, 4, 5, 14, 15, 16, 11 | psr1 21397 |
. . . 4
β’ (π β (1rβπ) = (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π = (πΌ Γ {0}), (1rβπ
), (0gβπ
)))) |
18 | | ovex 7395 |
. . . . . . . 8
β’
(β0 βm πΌ) β V |
19 | 18 | mptrabex 7180 |
. . . . . . 7
β’ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π = (πΌ Γ {0}), (1rβπ
), (0gβπ
))) β V |
20 | | funmpt 6544 |
. . . . . . 7
β’ Fun
(π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π = (πΌ Γ {0}), (1rβπ
), (0gβπ
))) |
21 | | fvex 6860 |
. . . . . . 7
β’
(0gβπ
) β V |
22 | 19, 20, 21 | 3pm3.2i 1340 |
. . . . . 6
β’ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π = (πΌ Γ {0}), (1rβπ
), (0gβπ
))) β V β§ Fun (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π = (πΌ Γ {0}), (1rβπ
), (0gβπ
))) β§
(0gβπ
)
β V) |
23 | 22 | a1i 11 |
. . . . 5
β’ (π β ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π = (πΌ Γ {0}), (1rβπ
), (0gβπ
))) β V β§ Fun (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π = (πΌ Γ {0}), (1rβπ
), (0gβπ
))) β§
(0gβπ
)
β V)) |
24 | | snfi 8995 |
. . . . . 6
β’ {(πΌ Γ {0})} β
Fin |
25 | 24 | a1i 11 |
. . . . 5
β’ (π β {(πΌ Γ {0})} β Fin) |
26 | | eldifsni 4755 |
. . . . . . . 8
β’ (π β ({π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β {(πΌ Γ {0})}) β π β (πΌ Γ {0})) |
27 | 26 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β ({π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β {(πΌ Γ {0})})) β π β (πΌ Γ {0})) |
28 | | ifnefalse 4503 |
. . . . . . 7
β’ (π β (πΌ Γ {0}) β if(π = (πΌ Γ {0}), (1rβπ
), (0gβπ
)) = (0gβπ
)) |
29 | 27, 28 | syl 17 |
. . . . . 6
β’ ((π β§ π β ({π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β {(πΌ Γ {0})})) β if(π = (πΌ Γ {0}), (1rβπ
), (0gβπ
)) = (0gβπ
)) |
30 | 18 | rabex 5294 |
. . . . . . 7
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β
V |
31 | 30 | a1i 11 |
. . . . . 6
β’ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β
V) |
32 | 29, 31 | suppss2 8136 |
. . . . 5
β’ (π β ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π = (πΌ Γ {0}), (1rβπ
), (0gβπ
))) supp
(0gβπ
))
β {(πΌ Γ
{0})}) |
33 | | suppssfifsupp 9327 |
. . . . 5
β’ ((((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π = (πΌ Γ {0}), (1rβπ
), (0gβπ
))) β V β§ Fun (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π = (πΌ Γ {0}), (1rβπ
), (0gβπ
))) β§
(0gβπ
)
β V) β§ ({(πΌ
Γ {0})} β Fin β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π = (πΌ Γ {0}), (1rβπ
), (0gβπ
))) supp
(0gβπ
))
β {(πΌ Γ {0})}))
β (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π = (πΌ Γ {0}), (1rβπ
), (0gβπ
))) finSupp
(0gβπ
)) |
34 | 23, 25, 32, 33 | syl12anc 836 |
. . . 4
β’ (π β (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π = (πΌ Γ {0}), (1rβπ
), (0gβπ
))) finSupp
(0gβπ
)) |
35 | 17, 34 | eqbrtrd 5132 |
. . 3
β’ (π β (1rβπ) finSupp
(0gβπ
)) |
36 | 2, 1, 10, 15, 3 | mplelbas 21415 |
. . 3
β’
((1rβπ) β π β ((1rβπ) β (Baseβπ) β§
(1rβπ)
finSupp (0gβπ
))) |
37 | 13, 35, 36 | sylanbrc 584 |
. 2
β’ (π β (1rβπ) β π) |
38 | 4 | adantr 482 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π)) β πΌ β π) |
39 | 5 | adantr 482 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π
β Ring) |
40 | | eqid 2737 |
. . . 4
β’ (
βf + β ((π₯ supp (0gβπ
)) Γ (π¦ supp (0gβπ
)))) = ( βf + β
((π₯ supp
(0gβπ
))
Γ (π¦ supp
(0gβπ
)))) |
41 | | eqid 2737 |
. . . 4
β’
(.rβπ
) = (.rβπ
) |
42 | | simprl 770 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π₯ β π) |
43 | | simprr 772 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π¦ β π) |
44 | 1, 2, 3, 38, 39, 14, 15, 40, 41, 42, 43 | mplsubrglem 21426 |
. . 3
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(.rβπ)π¦) β π) |
45 | 44 | ralrimivva 3198 |
. 2
β’ (π β βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π) |
46 | | eqid 2737 |
. . . 4
β’
(.rβπ) = (.rβπ) |
47 | 10, 11, 46 | issubrg2 20258 |
. . 3
β’ (π β Ring β (π β (SubRingβπ) β (π β (SubGrpβπ) β§ (1rβπ) β π β§ βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π))) |
48 | 9, 47 | syl 17 |
. 2
β’ (π β (π β (SubRingβπ) β (π β (SubGrpβπ) β§ (1rβπ) β π β§ βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π))) |
49 | 8, 37, 45, 48 | mpbir3and 1343 |
1
β’ (π β π β (SubRingβπ)) |