Step | Hyp | Ref
| Expression |
1 | | frlmgsum.r |
. . . 4
β’ (π β π
β Ring) |
2 | | frlmgsum.i |
. . . 4
β’ (π β πΌ β π) |
3 | | frlmgsum.y |
. . . . 5
β’ π = (π
freeLMod πΌ) |
4 | | frlmgsum.b |
. . . . 5
β’ π΅ = (Baseβπ) |
5 | 3, 4 | frlmpws 21172 |
. . . 4
β’ ((π
β Ring β§ πΌ β π) β π = (((ringLModβπ
) βs πΌ) βΎs π΅)) |
6 | 1, 2, 5 | syl2anc 585 |
. . 3
β’ (π β π = (((ringLModβπ
) βs πΌ) βΎs π΅)) |
7 | 6 | oveq1d 7373 |
. 2
β’ (π β (π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π))) = ((((ringLModβπ
) βs πΌ) βΎs π΅) Ξ£g
(π¦ β π½ β¦ (π₯ β πΌ β¦ π)))) |
8 | | eqid 2733 |
. . 3
β’
(Baseβ((ringLModβπ
) βs πΌ)) =
(Baseβ((ringLModβπ
) βs πΌ)) |
9 | | eqid 2733 |
. . 3
β’
(+gβ((ringLModβπ
) βs πΌ)) =
(+gβ((ringLModβπ
) βs πΌ)) |
10 | | eqid 2733 |
. . 3
β’
(((ringLModβπ
)
βs πΌ) βΎs π΅) = (((ringLModβπ
) βs πΌ) βΎs π΅) |
11 | | ovexd 7393 |
. . 3
β’ (π β ((ringLModβπ
) βs
πΌ) β
V) |
12 | | frlmgsum.j |
. . 3
β’ (π β π½ β π) |
13 | | eqid 2733 |
. . . . . 6
β’
(LSubSpβ((ringLModβπ
) βs πΌ)) =
(LSubSpβ((ringLModβπ
) βs πΌ)) |
14 | 3, 4, 13 | frlmlss 21173 |
. . . . 5
β’ ((π
β Ring β§ πΌ β π) β π΅ β (LSubSpβ((ringLModβπ
) βs
πΌ))) |
15 | 1, 2, 14 | syl2anc 585 |
. . . 4
β’ (π β π΅ β (LSubSpβ((ringLModβπ
) βs
πΌ))) |
16 | 8, 13 | lssss 20412 |
. . . 4
β’ (π΅ β
(LSubSpβ((ringLModβπ
) βs πΌ)) β π΅ β (Baseβ((ringLModβπ
) βs
πΌ))) |
17 | 15, 16 | syl 17 |
. . 3
β’ (π β π΅ β (Baseβ((ringLModβπ
) βs
πΌ))) |
18 | | frlmgsum.f |
. . . 4
β’ ((π β§ π¦ β π½) β (π₯ β πΌ β¦ π) β π΅) |
19 | 18 | fmpttd 7064 |
. . 3
β’ (π β (π¦ β π½ β¦ (π₯ β πΌ β¦ π)):π½βΆπ΅) |
20 | | rlmlmod 20690 |
. . . . . 6
β’ (π
β Ring β
(ringLModβπ
) β
LMod) |
21 | 1, 20 | syl 17 |
. . . . 5
β’ (π β (ringLModβπ
) β LMod) |
22 | | eqid 2733 |
. . . . . 6
β’
((ringLModβπ
)
βs πΌ) = ((ringLModβπ
) βs πΌ) |
23 | 22 | pwslmod 20446 |
. . . . 5
β’
(((ringLModβπ
)
β LMod β§ πΌ β
π) β
((ringLModβπ
)
βs πΌ) β LMod) |
24 | 21, 2, 23 | syl2anc 585 |
. . . 4
β’ (π β ((ringLModβπ
) βs
πΌ) β
LMod) |
25 | | eqid 2733 |
. . . . 5
β’
(0gβ((ringLModβπ
) βs πΌ)) =
(0gβ((ringLModβπ
) βs πΌ)) |
26 | 25, 13 | lss0cl 20422 |
. . . 4
β’
((((ringLModβπ
) βs πΌ) β LMod β§ π΅ β
(LSubSpβ((ringLModβπ
) βs πΌ))) β
(0gβ((ringLModβπ
) βs πΌ)) β π΅) |
27 | 24, 15, 26 | syl2anc 585 |
. . 3
β’ (π β
(0gβ((ringLModβπ
) βs πΌ)) β π΅) |
28 | | lmodcmn 20385 |
. . . . . . 7
β’
((ringLModβπ
)
β LMod β (ringLModβπ
) β CMnd) |
29 | 21, 28 | syl 17 |
. . . . . 6
β’ (π β (ringLModβπ
) β CMnd) |
30 | | cmnmnd 19584 |
. . . . . 6
β’
((ringLModβπ
)
β CMnd β (ringLModβπ
) β Mnd) |
31 | 29, 30 | syl 17 |
. . . . 5
β’ (π β (ringLModβπ
) β Mnd) |
32 | 22 | pwsmnd 18596 |
. . . . 5
β’
(((ringLModβπ
)
β Mnd β§ πΌ β
π) β
((ringLModβπ
)
βs πΌ) β Mnd) |
33 | 31, 2, 32 | syl2anc 585 |
. . . 4
β’ (π β ((ringLModβπ
) βs
πΌ) β
Mnd) |
34 | 8, 9, 25 | mndlrid 18580 |
. . . 4
β’
((((ringLModβπ
) βs πΌ) β Mnd β§ π₯ β
(Baseβ((ringLModβπ
) βs πΌ))) β
(((0gβ((ringLModβπ
) βs πΌ))(+gβ((ringLModβπ
) βs πΌ))π₯) = π₯ β§ (π₯(+gβ((ringLModβπ
) βs πΌ))(0gβ((ringLModβπ
) βs πΌ))) = π₯)) |
35 | 33, 34 | sylan 581 |
. . 3
β’ ((π β§ π₯ β (Baseβ((ringLModβπ
) βs
πΌ))) β
(((0gβ((ringLModβπ
) βs πΌ))(+gβ((ringLModβπ
) βs πΌ))π₯) = π₯ β§ (π₯(+gβ((ringLModβπ
) βs πΌ))(0gβ((ringLModβπ
) βs πΌ))) = π₯)) |
36 | 8, 9, 10, 11, 12, 17, 19, 27, 35 | gsumress 18542 |
. 2
β’ (π β (((ringLModβπ
) βs
πΌ)
Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π))) = ((((ringLModβπ
) βs πΌ) βΎs π΅) Ξ£g
(π¦ β π½ β¦ (π₯ β πΌ β¦ π)))) |
37 | | rlmbas 20680 |
. . . 4
β’
(Baseβπ
) =
(Baseβ(ringLModβπ
)) |
38 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ
) =
(Baseβπ
) |
39 | 3, 38, 4 | frlmbasf 21182 |
. . . . . . . 8
β’ ((πΌ β π β§ (π₯ β πΌ β¦ π) β π΅) β (π₯ β πΌ β¦ π):πΌβΆ(Baseβπ
)) |
40 | 2, 18, 39 | syl2an2r 684 |
. . . . . . 7
β’ ((π β§ π¦ β π½) β (π₯ β πΌ β¦ π):πΌβΆ(Baseβπ
)) |
41 | 40 | fvmptelcdm 7062 |
. . . . . 6
β’ (((π β§ π¦ β π½) β§ π₯ β πΌ) β π β (Baseβπ
)) |
42 | 41 | an32s 651 |
. . . . 5
β’ (((π β§ π₯ β πΌ) β§ π¦ β π½) β π β (Baseβπ
)) |
43 | 42 | anasss 468 |
. . . 4
β’ ((π β§ (π₯ β πΌ β§ π¦ β π½)) β π β (Baseβπ
)) |
44 | | frlmgsum.w |
. . . . 5
β’ (π β (π¦ β π½ β¦ (π₯ β πΌ β¦ π)) finSupp 0 ) |
45 | | frlmgsum.z |
. . . . . 6
β’ 0 =
(0gβπ) |
46 | 6 | fveq2d 6847 |
. . . . . . 7
β’ (π β (0gβπ) =
(0gβ(((ringLModβπ
) βs πΌ) βΎs π΅))) |
47 | 13 | lsssubg 20433 |
. . . . . . . . 9
β’
((((ringLModβπ
) βs πΌ) β LMod β§ π΅ β
(LSubSpβ((ringLModβπ
) βs πΌ))) β π΅ β (SubGrpβ((ringLModβπ
) βs
πΌ))) |
48 | 24, 15, 47 | syl2anc 585 |
. . . . . . . 8
β’ (π β π΅ β (SubGrpβ((ringLModβπ
) βs
πΌ))) |
49 | 10, 25 | subg0 18939 |
. . . . . . . 8
β’ (π΅ β
(SubGrpβ((ringLModβπ
) βs πΌ)) β
(0gβ((ringLModβπ
) βs πΌ)) =
(0gβ(((ringLModβπ
) βs πΌ) βΎs π΅))) |
50 | 48, 49 | syl 17 |
. . . . . . 7
β’ (π β
(0gβ((ringLModβπ
) βs πΌ)) =
(0gβ(((ringLModβπ
) βs πΌ) βΎs π΅))) |
51 | 46, 50 | eqtr4d 2776 |
. . . . . 6
β’ (π β (0gβπ) =
(0gβ((ringLModβπ
) βs πΌ))) |
52 | 45, 51 | eqtrid 2785 |
. . . . 5
β’ (π β 0 =
(0gβ((ringLModβπ
) βs πΌ))) |
53 | 44, 52 | breqtrd 5132 |
. . . 4
β’ (π β (π¦ β π½ β¦ (π₯ β πΌ β¦ π)) finSupp
(0gβ((ringLModβπ
) βs πΌ))) |
54 | 22, 37, 25, 2, 12, 29, 43, 53 | pwsgsum 19764 |
. . 3
β’ (π β (((ringLModβπ
) βs
πΌ)
Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π))) = (π₯ β πΌ β¦ ((ringLModβπ
) Ξ£g (π¦ β π½ β¦ π)))) |
55 | 12 | mptexd 7175 |
. . . . 5
β’ (π β (π¦ β π½ β¦ π) β V) |
56 | | fvexd 6858 |
. . . . 5
β’ (π β (ringLModβπ
) β V) |
57 | 37 | a1i 11 |
. . . . 5
β’ (π β (Baseβπ
) =
(Baseβ(ringLModβπ
))) |
58 | | rlmplusg 20681 |
. . . . . 6
β’
(+gβπ
) =
(+gβ(ringLModβπ
)) |
59 | 58 | a1i 11 |
. . . . 5
β’ (π β (+gβπ
) =
(+gβ(ringLModβπ
))) |
60 | 55, 1, 56, 57, 59 | gsumpropd 18538 |
. . . 4
β’ (π β (π
Ξ£g (π¦ β π½ β¦ π)) = ((ringLModβπ
) Ξ£g (π¦ β π½ β¦ π))) |
61 | 60 | mpteq2dv 5208 |
. . 3
β’ (π β (π₯ β πΌ β¦ (π
Ξ£g (π¦ β π½ β¦ π))) = (π₯ β πΌ β¦ ((ringLModβπ
) Ξ£g (π¦ β π½ β¦ π)))) |
62 | 54, 61 | eqtr4d 2776 |
. 2
β’ (π β (((ringLModβπ
) βs
πΌ)
Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π))) = (π₯ β πΌ β¦ (π
Ξ£g (π¦ β π½ β¦ π)))) |
63 | 7, 36, 62 | 3eqtr2d 2779 |
1
β’ (π β (π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π))) = (π₯ β πΌ β¦ (π
Ξ£g (π¦ β π½ β¦ π)))) |