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 20094 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑌 = (((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵)) |
6 | 1, 2, 5 | syl2anc 693 |
. . 3
⊢ (𝜑 → 𝑌 = (((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵)) |
7 | 6 | oveq1d 6665 |
. 2
⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = ((((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵) Σg
(𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))) |
8 | | eqid 2622 |
. . 3
⊢
(Base‘((ringLMod‘𝑅) ↑s 𝐼)) =
(Base‘((ringLMod‘𝑅) ↑s 𝐼)) |
9 | | eqid 2622 |
. . 3
⊢
(+g‘((ringLMod‘𝑅) ↑s 𝐼)) =
(+g‘((ringLMod‘𝑅) ↑s 𝐼)) |
10 | | eqid 2622 |
. . 3
⊢
(((ringLMod‘𝑅)
↑s 𝐼) ↾s 𝐵) = (((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵) |
11 | | ovexd 6680 |
. . 3
⊢ (𝜑 → ((ringLMod‘𝑅) ↑s
𝐼) ∈
V) |
12 | | frlmgsum.j |
. . 3
⊢ (𝜑 → 𝐽 ∈ 𝑊) |
13 | | eqid 2622 |
. . . . . 6
⊢
(LSubSp‘((ringLMod‘𝑅) ↑s 𝐼)) =
(LSubSp‘((ringLMod‘𝑅) ↑s 𝐼)) |
14 | 3, 4, 13 | frlmlss 20095 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝐵 ∈ (LSubSp‘((ringLMod‘𝑅) ↑s
𝐼))) |
15 | 1, 2, 14 | syl2anc 693 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ (LSubSp‘((ringLMod‘𝑅) ↑s
𝐼))) |
16 | 8, 13 | lssss 18937 |
. . . 4
⊢ (𝐵 ∈
(LSubSp‘((ringLMod‘𝑅) ↑s 𝐼)) → 𝐵 ⊆ (Base‘((ringLMod‘𝑅) ↑s
𝐼))) |
17 | 15, 16 | syl 17 |
. . 3
⊢ (𝜑 → 𝐵 ⊆ (Base‘((ringLMod‘𝑅) ↑s
𝐼))) |
18 | | frlmgsum.f |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝐼 ↦ 𝑈) ∈ 𝐵) |
19 | | eqid 2622 |
. . . 4
⊢ (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) = (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) |
20 | 18, 19 | fmptd 6385 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)):𝐽⟶𝐵) |
21 | | rlmlmod 19205 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(ringLMod‘𝑅) ∈
LMod) |
22 | 1, 21 | syl 17 |
. . . . 5
⊢ (𝜑 → (ringLMod‘𝑅) ∈ LMod) |
23 | | eqid 2622 |
. . . . . 6
⊢
((ringLMod‘𝑅)
↑s 𝐼) = ((ringLMod‘𝑅) ↑s 𝐼) |
24 | 23 | pwslmod 18970 |
. . . . 5
⊢
(((ringLMod‘𝑅)
∈ LMod ∧ 𝐼 ∈
𝑉) →
((ringLMod‘𝑅)
↑s 𝐼) ∈ LMod) |
25 | 22, 2, 24 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ((ringLMod‘𝑅) ↑s
𝐼) ∈
LMod) |
26 | | eqid 2622 |
. . . . 5
⊢
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) =
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) |
27 | 26, 13 | lss0cl 18947 |
. . . 4
⊢
((((ringLMod‘𝑅) ↑s 𝐼) ∈ LMod ∧ 𝐵 ∈
(LSubSp‘((ringLMod‘𝑅) ↑s 𝐼))) →
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) ∈ 𝐵) |
28 | 25, 15, 27 | syl2anc 693 |
. . 3
⊢ (𝜑 →
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) ∈ 𝐵) |
29 | | lmodcmn 18911 |
. . . . . . 7
⊢
((ringLMod‘𝑅)
∈ LMod → (ringLMod‘𝑅) ∈ CMnd) |
30 | 22, 29 | syl 17 |
. . . . . 6
⊢ (𝜑 → (ringLMod‘𝑅) ∈ CMnd) |
31 | | cmnmnd 18208 |
. . . . . 6
⊢
((ringLMod‘𝑅)
∈ CMnd → (ringLMod‘𝑅) ∈ Mnd) |
32 | 30, 31 | syl 17 |
. . . . 5
⊢ (𝜑 → (ringLMod‘𝑅) ∈ Mnd) |
33 | 23 | pwsmnd 17325 |
. . . . 5
⊢
(((ringLMod‘𝑅)
∈ Mnd ∧ 𝐼 ∈
𝑉) →
((ringLMod‘𝑅)
↑s 𝐼) ∈ Mnd) |
34 | 32, 2, 33 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ((ringLMod‘𝑅) ↑s
𝐼) ∈
Mnd) |
35 | 8, 9, 26 | mndlrid 17310 |
. . . 4
⊢
((((ringLMod‘𝑅) ↑s 𝐼) ∈ Mnd ∧ 𝑥 ∈
(Base‘((ringLMod‘𝑅) ↑s 𝐼))) →
(((0g‘((ringLMod‘𝑅) ↑s 𝐼))(+g‘((ringLMod‘𝑅) ↑s 𝐼))𝑥) = 𝑥 ∧ (𝑥(+g‘((ringLMod‘𝑅) ↑s 𝐼))(0g‘((ringLMod‘𝑅) ↑s 𝐼))) = 𝑥)) |
36 | 34, 35 | sylan 488 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘((ringLMod‘𝑅) ↑s
𝐼))) →
(((0g‘((ringLMod‘𝑅) ↑s 𝐼))(+g‘((ringLMod‘𝑅) ↑s 𝐼))𝑥) = 𝑥 ∧ (𝑥(+g‘((ringLMod‘𝑅) ↑s 𝐼))(0g‘((ringLMod‘𝑅) ↑s 𝐼))) = 𝑥)) |
37 | 8, 9, 10, 11, 12, 17, 20, 28, 36 | gsumress 17276 |
. 2
⊢ (𝜑 → (((ringLMod‘𝑅) ↑s
𝐼)
Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = ((((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵) Σg
(𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))) |
38 | | rlmbas 19195 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘(ringLMod‘𝑅)) |
39 | 2 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝐼 ∈ 𝑉) |
40 | | eqid 2622 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
41 | 3, 40, 4 | frlmbasf 20104 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝐼 ↦ 𝑈) ∈ 𝐵) → (𝑥 ∈ 𝐼 ↦ 𝑈):𝐼⟶(Base‘𝑅)) |
42 | 39, 18, 41 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝐼 ↦ 𝑈):𝐼⟶(Base‘𝑅)) |
43 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐼 ↦ 𝑈) = (𝑥 ∈ 𝐼 ↦ 𝑈) |
44 | 43 | fmpt 6381 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐼 𝑈 ∈ (Base‘𝑅) ↔ (𝑥 ∈ 𝐼 ↦ 𝑈):𝐼⟶(Base‘𝑅)) |
45 | 42, 44 | sylibr 224 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → ∀𝑥 ∈ 𝐼 𝑈 ∈ (Base‘𝑅)) |
46 | 45 | r19.21bi 2932 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑥 ∈ 𝐼) → 𝑈 ∈ (Base‘𝑅)) |
47 | 46 | an32s 846 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐽) → 𝑈 ∈ (Base‘𝑅)) |
48 | 47 | anasss 679 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ (Base‘𝑅)) |
49 | | frlmgsum.w |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 0 ) |
50 | | frlmgsum.z |
. . . . . 6
⊢ 0 =
(0g‘𝑌) |
51 | 6 | fveq2d 6195 |
. . . . . . 7
⊢ (𝜑 → (0g‘𝑌) =
(0g‘(((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵))) |
52 | 13 | lsssubg 18957 |
. . . . . . . . 9
⊢
((((ringLMod‘𝑅) ↑s 𝐼) ∈ LMod ∧ 𝐵 ∈
(LSubSp‘((ringLMod‘𝑅) ↑s 𝐼))) → 𝐵 ∈ (SubGrp‘((ringLMod‘𝑅) ↑s
𝐼))) |
53 | 25, 15, 52 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ (SubGrp‘((ringLMod‘𝑅) ↑s
𝐼))) |
54 | 10, 26 | subg0 17600 |
. . . . . . . 8
⊢ (𝐵 ∈
(SubGrp‘((ringLMod‘𝑅) ↑s 𝐼)) →
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) =
(0g‘(((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵))) |
55 | 53, 54 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) =
(0g‘(((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵))) |
56 | 51, 55 | eqtr4d 2659 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑌) =
(0g‘((ringLMod‘𝑅) ↑s 𝐼))) |
57 | 50, 56 | syl5eq 2668 |
. . . . 5
⊢ (𝜑 → 0 =
(0g‘((ringLMod‘𝑅) ↑s 𝐼))) |
58 | 49, 57 | breqtrd 4679 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp
(0g‘((ringLMod‘𝑅) ↑s 𝐼))) |
59 | 23, 38, 26, 2, 12, 30, 48, 58 | pwsgsum 18378 |
. . 3
⊢ (𝜑 → (((ringLMod‘𝑅) ↑s
𝐼)
Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ ((ringLMod‘𝑅) Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |
60 | | mptexg 6484 |
. . . . . 6
⊢ (𝐽 ∈ 𝑊 → (𝑦 ∈ 𝐽 ↦ 𝑈) ∈ V) |
61 | 12, 60 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ 𝑈) ∈ V) |
62 | | fvexd 6203 |
. . . . 5
⊢ (𝜑 → (ringLMod‘𝑅) ∈ V) |
63 | 38 | a1i 11 |
. . . . 5
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(ringLMod‘𝑅))) |
64 | | rlmplusg 19196 |
. . . . . 6
⊢
(+g‘𝑅) =
(+g‘(ringLMod‘𝑅)) |
65 | 64 | a1i 11 |
. . . . 5
⊢ (𝜑 → (+g‘𝑅) =
(+g‘(ringLMod‘𝑅))) |
66 | 61, 1, 62, 63, 65 | gsumpropd 17272 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)) = ((ringLMod‘𝑅) Σg (𝑦 ∈ 𝐽 ↦ 𝑈))) |
67 | 66 | mpteq2dv 4745 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ ((ringLMod‘𝑅) Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |
68 | 59, 67 | eqtr4d 2659 |
. 2
⊢ (𝜑 → (((ringLMod‘𝑅) ↑s
𝐼)
Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |
69 | 7, 37, 68 | 3eqtr2d 2662 |
1
⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |