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 19913 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑌 = (((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵)) |
6 | 1, 2, 5 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝑌 = (((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵)) |
7 | 6 | oveq1d 6564 |
. 2
⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = ((((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵) Σg
(𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))) |
8 | | eqid 2610 |
. . 3
⊢
(Base‘((ringLMod‘𝑅) ↑s 𝐼)) =
(Base‘((ringLMod‘𝑅) ↑s 𝐼)) |
9 | | eqid 2610 |
. . 3
⊢
(+g‘((ringLMod‘𝑅) ↑s 𝐼)) =
(+g‘((ringLMod‘𝑅) ↑s 𝐼)) |
10 | | eqid 2610 |
. . 3
⊢
(((ringLMod‘𝑅)
↑s 𝐼) ↾s 𝐵) = (((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵) |
11 | | ovex 6577 |
. . . 4
⊢
((ringLMod‘𝑅)
↑s 𝐼) ∈ V |
12 | 11 | a1i 11 |
. . 3
⊢ (𝜑 → ((ringLMod‘𝑅) ↑s
𝐼) ∈
V) |
13 | | frlmgsum.j |
. . 3
⊢ (𝜑 → 𝐽 ∈ 𝑊) |
14 | | eqid 2610 |
. . . . . 6
⊢
(LSubSp‘((ringLMod‘𝑅) ↑s 𝐼)) =
(LSubSp‘((ringLMod‘𝑅) ↑s 𝐼)) |
15 | 3, 4, 14 | frlmlss 19914 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝐵 ∈ (LSubSp‘((ringLMod‘𝑅) ↑s
𝐼))) |
16 | 1, 2, 15 | syl2anc 691 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ (LSubSp‘((ringLMod‘𝑅) ↑s
𝐼))) |
17 | 8, 14 | lssss 18758 |
. . . 4
⊢ (𝐵 ∈
(LSubSp‘((ringLMod‘𝑅) ↑s 𝐼)) → 𝐵 ⊆ (Base‘((ringLMod‘𝑅) ↑s
𝐼))) |
18 | 16, 17 | syl 17 |
. . 3
⊢ (𝜑 → 𝐵 ⊆ (Base‘((ringLMod‘𝑅) ↑s
𝐼))) |
19 | | frlmgsum.f |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝐼 ↦ 𝑈) ∈ 𝐵) |
20 | | eqid 2610 |
. . . 4
⊢ (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) = (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) |
21 | 19, 20 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)):𝐽⟶𝐵) |
22 | | rlmlmod 19026 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(ringLMod‘𝑅) ∈
LMod) |
23 | 1, 22 | syl 17 |
. . . . 5
⊢ (𝜑 → (ringLMod‘𝑅) ∈ LMod) |
24 | | eqid 2610 |
. . . . . 6
⊢
((ringLMod‘𝑅)
↑s 𝐼) = ((ringLMod‘𝑅) ↑s 𝐼) |
25 | 24 | pwslmod 18791 |
. . . . 5
⊢
(((ringLMod‘𝑅)
∈ LMod ∧ 𝐼 ∈
𝑉) →
((ringLMod‘𝑅)
↑s 𝐼) ∈ LMod) |
26 | 23, 2, 25 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ((ringLMod‘𝑅) ↑s
𝐼) ∈
LMod) |
27 | | eqid 2610 |
. . . . 5
⊢
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) =
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) |
28 | 27, 14 | lss0cl 18768 |
. . . 4
⊢
((((ringLMod‘𝑅) ↑s 𝐼) ∈ LMod ∧ 𝐵 ∈
(LSubSp‘((ringLMod‘𝑅) ↑s 𝐼))) →
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) ∈ 𝐵) |
29 | 26, 16, 28 | syl2anc 691 |
. . 3
⊢ (𝜑 →
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) ∈ 𝐵) |
30 | | lmodcmn 18734 |
. . . . . . 7
⊢
((ringLMod‘𝑅)
∈ LMod → (ringLMod‘𝑅) ∈ CMnd) |
31 | 23, 30 | syl 17 |
. . . . . 6
⊢ (𝜑 → (ringLMod‘𝑅) ∈ CMnd) |
32 | | cmnmnd 18031 |
. . . . . 6
⊢
((ringLMod‘𝑅)
∈ CMnd → (ringLMod‘𝑅) ∈ Mnd) |
33 | 31, 32 | syl 17 |
. . . . 5
⊢ (𝜑 → (ringLMod‘𝑅) ∈ Mnd) |
34 | 24 | pwsmnd 17148 |
. . . . 5
⊢
(((ringLMod‘𝑅)
∈ Mnd ∧ 𝐼 ∈
𝑉) →
((ringLMod‘𝑅)
↑s 𝐼) ∈ Mnd) |
35 | 33, 2, 34 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ((ringLMod‘𝑅) ↑s
𝐼) ∈
Mnd) |
36 | 8, 9, 27 | mndlrid 17133 |
. . . 4
⊢
((((ringLMod‘𝑅) ↑s 𝐼) ∈ Mnd ∧ 𝑥 ∈
(Base‘((ringLMod‘𝑅) ↑s 𝐼))) →
(((0g‘((ringLMod‘𝑅) ↑s 𝐼))(+g‘((ringLMod‘𝑅) ↑s 𝐼))𝑥) = 𝑥 ∧ (𝑥(+g‘((ringLMod‘𝑅) ↑s 𝐼))(0g‘((ringLMod‘𝑅) ↑s 𝐼))) = 𝑥)) |
37 | 35, 36 | sylan 487 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘((ringLMod‘𝑅) ↑s
𝐼))) →
(((0g‘((ringLMod‘𝑅) ↑s 𝐼))(+g‘((ringLMod‘𝑅) ↑s 𝐼))𝑥) = 𝑥 ∧ (𝑥(+g‘((ringLMod‘𝑅) ↑s 𝐼))(0g‘((ringLMod‘𝑅) ↑s 𝐼))) = 𝑥)) |
38 | 8, 9, 10, 12, 13, 18, 21, 29, 37 | gsumress 17099 |
. 2
⊢ (𝜑 → (((ringLMod‘𝑅) ↑s
𝐼)
Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = ((((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵) Σg
(𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))) |
39 | | rlmbas 19016 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘(ringLMod‘𝑅)) |
40 | 2 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝐼 ∈ 𝑉) |
41 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
42 | 3, 41, 4 | frlmbasf 19923 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝐼 ↦ 𝑈) ∈ 𝐵) → (𝑥 ∈ 𝐼 ↦ 𝑈):𝐼⟶(Base‘𝑅)) |
43 | 40, 19, 42 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝐼 ↦ 𝑈):𝐼⟶(Base‘𝑅)) |
44 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐼 ↦ 𝑈) = (𝑥 ∈ 𝐼 ↦ 𝑈) |
45 | 44 | fmpt 6289 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐼 𝑈 ∈ (Base‘𝑅) ↔ (𝑥 ∈ 𝐼 ↦ 𝑈):𝐼⟶(Base‘𝑅)) |
46 | 43, 45 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → ∀𝑥 ∈ 𝐼 𝑈 ∈ (Base‘𝑅)) |
47 | 46 | r19.21bi 2916 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑥 ∈ 𝐼) → 𝑈 ∈ (Base‘𝑅)) |
48 | 47 | an32s 842 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐽) → 𝑈 ∈ (Base‘𝑅)) |
49 | 48 | anasss 677 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ (Base‘𝑅)) |
50 | | frlmgsum.w |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 0 ) |
51 | | frlmgsum.z |
. . . . . 6
⊢ 0 =
(0g‘𝑌) |
52 | 6 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → (0g‘𝑌) =
(0g‘(((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵))) |
53 | 14 | lsssubg 18778 |
. . . . . . . . 9
⊢
((((ringLMod‘𝑅) ↑s 𝐼) ∈ LMod ∧ 𝐵 ∈
(LSubSp‘((ringLMod‘𝑅) ↑s 𝐼))) → 𝐵 ∈ (SubGrp‘((ringLMod‘𝑅) ↑s
𝐼))) |
54 | 26, 16, 53 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ (SubGrp‘((ringLMod‘𝑅) ↑s
𝐼))) |
55 | 10, 27 | subg0 17423 |
. . . . . . . 8
⊢ (𝐵 ∈
(SubGrp‘((ringLMod‘𝑅) ↑s 𝐼)) →
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) =
(0g‘(((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵))) |
56 | 54, 55 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
(0g‘((ringLMod‘𝑅) ↑s 𝐼)) =
(0g‘(((ringLMod‘𝑅) ↑s 𝐼) ↾s 𝐵))) |
57 | 52, 56 | eqtr4d 2647 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑌) =
(0g‘((ringLMod‘𝑅) ↑s 𝐼))) |
58 | 51, 57 | syl5eq 2656 |
. . . . 5
⊢ (𝜑 → 0 =
(0g‘((ringLMod‘𝑅) ↑s 𝐼))) |
59 | 50, 58 | breqtrd 4609 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp
(0g‘((ringLMod‘𝑅) ↑s 𝐼))) |
60 | 24, 39, 27, 2, 13, 31, 49, 59 | pwsgsum 18201 |
. . 3
⊢ (𝜑 → (((ringLMod‘𝑅) ↑s
𝐼)
Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ ((ringLMod‘𝑅) Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |
61 | | mptexg 6389 |
. . . . . 6
⊢ (𝐽 ∈ 𝑊 → (𝑦 ∈ 𝐽 ↦ 𝑈) ∈ V) |
62 | 13, 61 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ 𝑈) ∈ V) |
63 | | fvex 6113 |
. . . . . 6
⊢
(ringLMod‘𝑅)
∈ V |
64 | 63 | a1i 11 |
. . . . 5
⊢ (𝜑 → (ringLMod‘𝑅) ∈ V) |
65 | 39 | a1i 11 |
. . . . 5
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(ringLMod‘𝑅))) |
66 | | rlmplusg 19017 |
. . . . . 6
⊢
(+g‘𝑅) =
(+g‘(ringLMod‘𝑅)) |
67 | 66 | a1i 11 |
. . . . 5
⊢ (𝜑 → (+g‘𝑅) =
(+g‘(ringLMod‘𝑅))) |
68 | 62, 1, 64, 65, 67 | gsumpropd 17095 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)) = ((ringLMod‘𝑅) Σg (𝑦 ∈ 𝐽 ↦ 𝑈))) |
69 | 68 | mpteq2dv 4673 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ ((ringLMod‘𝑅) Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |
70 | 60, 69 | eqtr4d 2647 |
. 2
⊢ (𝜑 → (((ringLMod‘𝑅) ↑s
𝐼)
Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |
71 | 7, 38, 70 | 3eqtr2d 2650 |
1
⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |