Proof of Theorem frlmgsum
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 20497 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑌 = (((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵)) |
6 | 1, 2, 5 | syl2anc 579 |
. . 3
⊢ (𝜑 → 𝑌 = (((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵)) |
7 | 6 | oveq1d 6939 |
. 2
⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = ((((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵) Σg
(𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))) |
8 | | eqid 2778 |
. . 3
⊢
(Base‘((ringLMod‘𝑅) ↑s 𝐼)) =
(Base‘((ringLMod‘𝑅) ↑s 𝐼)) |
9 | | eqid 2778 |
. . 3
⊢
(+g‘((ringLMod‘𝑅) ↑s 𝐼)) =
(+g‘((ringLMod‘𝑅) ↑s 𝐼)) |
10 | | eqid 2778 |
. . 3
⊢
(((ringLMod‘𝑅)
↑s 𝐼) ↾s 𝐵) = (((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵) |
11 | | ovexd 6958 |
. . 3
⊢ (𝜑 → ((ringLMod‘𝑅) ↑s
𝐼) ∈
V) |
12 | | frlmgsum.j |
. . 3
⊢ (𝜑 → 𝐽 ∈ 𝑊) |
13 | | eqid 2778 |
. . . . . 6
⊢
(LSubSp‘((ringLMod‘𝑅) ↑s 𝐼)) =
(LSubSp‘((ringLMod‘𝑅) ↑s 𝐼)) |
14 | 3, 4, 13 | frlmlss 20498 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝐵 ∈ (LSubSp‘((ringLMod‘𝑅) ↑s
𝐼))) |
15 | 1, 2, 14 | syl2anc 579 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ (LSubSp‘((ringLMod‘𝑅) ↑s
𝐼))) |
16 | 8, 13 | lssss 19333 |
. . . 4
⊢ (𝐵 ∈
(LSubSp‘((ringLMod‘𝑅) ↑s 𝐼)) → 𝐵 ⊆ (Base‘((ringLMod‘𝑅) ↑s
𝐼))) |
17 | 15, 16 | syl 17 |
. . 3
⊢ (𝜑 → 𝐵 ⊆ (Base‘((ringLMod‘𝑅) ↑s
𝐼))) |
18 | | frlmgsum.f |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝐼 ↦ 𝑈) ∈ 𝐵) |
19 | 18 | fmpttd 6651 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)):𝐽⟶𝐵) |
20 | | rlmlmod 19606 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(ringLMod‘𝑅) ∈
LMod) |
21 | 1, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → (ringLMod‘𝑅) ∈ LMod) |
22 | | eqid 2778 |
. . . . . 6
⊢
((ringLMod‘𝑅)
↑s 𝐼) = ((ringLMod‘𝑅) ↑s 𝐼) |
23 | 22 | pwslmod 19369 |
. . . . 5
⊢
(((ringLMod‘𝑅)
∈ LMod ∧ 𝐼 ∈
𝑉) →
((ringLMod‘𝑅)
↑s 𝐼) ∈ LMod) |
24 | 21, 2, 23 | syl2anc 579 |
. . . 4
⊢ (𝜑 → ((ringLMod‘𝑅) ↑s
𝐼) ∈
LMod) |
25 | | eqid 2778 |
. . . . 5
⊢
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) =
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) |
26 | 25, 13 | lss0cl 19343 |
. . . 4
⊢
((((ringLMod‘𝑅) ↑s 𝐼) ∈ LMod ∧ 𝐵 ∈
(LSubSp‘((ringLMod‘𝑅) ↑s 𝐼))) →
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) ∈ 𝐵) |
27 | 24, 15, 26 | syl2anc 579 |
. . 3
⊢ (𝜑 →
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) ∈ 𝐵) |
28 | | lmodcmn 19307 |
. . . . . . 7
⊢
((ringLMod‘𝑅)
∈ LMod → (ringLMod‘𝑅) ∈ CMnd) |
29 | 21, 28 | syl 17 |
. . . . . 6
⊢ (𝜑 → (ringLMod‘𝑅) ∈ CMnd) |
30 | | cmnmnd 18598 |
. . . . . 6
⊢
((ringLMod‘𝑅)
∈ CMnd → (ringLMod‘𝑅) ∈ Mnd) |
31 | 29, 30 | syl 17 |
. . . . 5
⊢ (𝜑 → (ringLMod‘𝑅) ∈ Mnd) |
32 | 22 | pwsmnd 17715 |
. . . . 5
⊢
(((ringLMod‘𝑅)
∈ Mnd ∧ 𝐼 ∈
𝑉) →
((ringLMod‘𝑅)
↑s 𝐼) ∈ Mnd) |
33 | 31, 2, 32 | syl2anc 579 |
. . . 4
⊢ (𝜑 → ((ringLMod‘𝑅) ↑s
𝐼) ∈
Mnd) |
34 | 8, 9, 25 | mndlrid 17700 |
. . . 4
⊢
((((ringLMod‘𝑅) ↑s 𝐼) ∈ Mnd ∧ 𝑥 ∈
(Base‘((ringLMod‘𝑅) ↑s 𝐼))) →
(((0g‘((ringLMod‘𝑅) ↑s 𝐼))(+g‘((ringLMod‘𝑅) ↑s 𝐼))𝑥) = 𝑥 ∧ (𝑥(+g‘((ringLMod‘𝑅) ↑s 𝐼))(0g‘((ringLMod‘𝑅) ↑s 𝐼))) = 𝑥)) |
35 | 33, 34 | sylan 575 |
. . 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 17666 |
. 2
⊢ (𝜑 → (((ringLMod‘𝑅) ↑s
𝐼)
Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = ((((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵) Σg
(𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))) |
37 | | rlmbas 19596 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘(ringLMod‘𝑅)) |
38 | 2 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝐼 ∈ 𝑉) |
39 | | eqid 2778 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
40 | 3, 39, 4 | frlmbasf 20507 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝐼 ↦ 𝑈) ∈ 𝐵) → (𝑥 ∈ 𝐼 ↦ 𝑈):𝐼⟶(Base‘𝑅)) |
41 | 38, 18, 40 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝐼 ↦ 𝑈):𝐼⟶(Base‘𝑅)) |
42 | | eqid 2778 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐼 ↦ 𝑈) = (𝑥 ∈ 𝐼 ↦ 𝑈) |
43 | 42 | fmpt 6646 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐼 𝑈 ∈ (Base‘𝑅) ↔ (𝑥 ∈ 𝐼 ↦ 𝑈):𝐼⟶(Base‘𝑅)) |
44 | 41, 43 | sylibr 226 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → ∀𝑥 ∈ 𝐼 𝑈 ∈ (Base‘𝑅)) |
45 | 44 | r19.21bi 3114 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑥 ∈ 𝐼) → 𝑈 ∈ (Base‘𝑅)) |
46 | 45 | an32s 642 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐽) → 𝑈 ∈ (Base‘𝑅)) |
47 | 46 | anasss 460 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ (Base‘𝑅)) |
48 | | frlmgsum.w |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 0 ) |
49 | | frlmgsum.z |
. . . . . 6
⊢ 0 =
(0g‘𝑌) |
50 | 6 | fveq2d 6452 |
. . . . . . 7
⊢ (𝜑 → (0g‘𝑌) =
(0g‘(((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵))) |
51 | 13 | lsssubg 19356 |
. . . . . . . . 9
⊢
((((ringLMod‘𝑅) ↑s 𝐼) ∈ LMod ∧ 𝐵 ∈
(LSubSp‘((ringLMod‘𝑅) ↑s 𝐼))) → 𝐵 ∈ (SubGrp‘((ringLMod‘𝑅) ↑s
𝐼))) |
52 | 24, 15, 51 | syl2anc 579 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ (SubGrp‘((ringLMod‘𝑅) ↑s
𝐼))) |
53 | 10, 25 | subg0 17988 |
. . . . . . . 8
⊢ (𝐵 ∈
(SubGrp‘((ringLMod‘𝑅) ↑s 𝐼)) →
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) =
(0g‘(((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵))) |
54 | 52, 53 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) =
(0g‘(((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵))) |
55 | 50, 54 | eqtr4d 2817 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑌) =
(0g‘((ringLMod‘𝑅) ↑s 𝐼))) |
56 | 49, 55 | syl5eq 2826 |
. . . . 5
⊢ (𝜑 → 0 =
(0g‘((ringLMod‘𝑅) ↑s 𝐼))) |
57 | 48, 56 | breqtrd 4914 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp
(0g‘((ringLMod‘𝑅) ↑s 𝐼))) |
58 | 22, 37, 25, 2, 12, 29, 47, 57 | pwsgsum 18768 |
. . 3
⊢ (𝜑 → (((ringLMod‘𝑅) ↑s
𝐼)
Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ ((ringLMod‘𝑅) Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |
59 | | mptexg 6758 |
. . . . . 6
⊢ (𝐽 ∈ 𝑊 → (𝑦 ∈ 𝐽 ↦ 𝑈) ∈ V) |
60 | 12, 59 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ 𝑈) ∈ V) |
61 | | fvexd 6463 |
. . . . 5
⊢ (𝜑 → (ringLMod‘𝑅) ∈ V) |
62 | 37 | a1i 11 |
. . . . 5
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(ringLMod‘𝑅))) |
63 | | rlmplusg 19597 |
. . . . . 6
⊢
(+g‘𝑅) =
(+g‘(ringLMod‘𝑅)) |
64 | 63 | a1i 11 |
. . . . 5
⊢ (𝜑 → (+g‘𝑅) =
(+g‘(ringLMod‘𝑅))) |
65 | 60, 1, 61, 62, 64 | gsumpropd 17662 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)) = ((ringLMod‘𝑅) Σg (𝑦 ∈ 𝐽 ↦ 𝑈))) |
66 | 65 | mpteq2dv 4982 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ ((ringLMod‘𝑅) Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |
67 | 58, 66 | eqtr4d 2817 |
. 2
⊢ (𝜑 → (((ringLMod‘𝑅) ↑s
𝐼)
Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |
68 | 7, 36, 67 | 3eqtr2d 2820 |
1
⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |