Step | Hyp | Ref
| Expression |
1 | | evlslem1.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ CRing) |
2 | | crngring 18381 |
. . . . . 6
⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ Ring) |
4 | 3 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ Ring) |
5 | | evlslem1.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
6 | | evlslem1.k |
. . . . . . . 8
⊢ 𝐾 = (Base‘𝑅) |
7 | | evlslem1.c |
. . . . . . . 8
⊢ 𝐶 = (Base‘𝑆) |
8 | 6, 7 | rhmf 18549 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐾⟶𝐶) |
9 | 5, 8 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐾⟶𝐶) |
10 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐹:𝐾⟶𝐶) |
11 | | evlslem1.p |
. . . . . . 7
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
12 | | evlslem1.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑃) |
13 | | evlslem1.d |
. . . . . . 7
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} |
14 | | evlslem6.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
15 | 11, 6, 12, 13, 14 | mplelf 19254 |
. . . . . 6
⊢ (𝜑 → 𝑌:𝐷⟶𝐾) |
16 | 15 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑌‘𝑏) ∈ 𝐾) |
17 | 10, 16 | ffvelrnd 6268 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑌‘𝑏)) ∈ 𝐶) |
18 | | evlslem1.t |
. . . . . 6
⊢ 𝑇 = (mulGrp‘𝑆) |
19 | 18, 7 | mgpbas 18318 |
. . . . 5
⊢ 𝐶 = (Base‘𝑇) |
20 | | evlslem1.x |
. . . . 5
⊢ ↑ =
(.g‘𝑇) |
21 | | eqid 2610 |
. . . . 5
⊢
(0g‘𝑇) = (0g‘𝑇) |
22 | 18 | crngmgp 18378 |
. . . . . . 7
⊢ (𝑆 ∈ CRing → 𝑇 ∈ CMnd) |
23 | 1, 22 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ CMnd) |
24 | 23 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑇 ∈ CMnd) |
25 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷) |
26 | | evlslem1.g |
. . . . . 6
⊢ (𝜑 → 𝐺:𝐼⟶𝐶) |
27 | 26 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐺:𝐼⟶𝐶) |
28 | | evlslem1.i |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ V) |
29 | 28 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐼 ∈ V) |
30 | 13, 19, 20, 21, 24, 25, 27, 29 | psrbagev2 19332 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)) ∈ 𝐶) |
31 | | evlslem1.m |
. . . . 5
⊢ · =
(.r‘𝑆) |
32 | 7, 31 | ringcl 18384 |
. . . 4
⊢ ((𝑆 ∈ Ring ∧ (𝐹‘(𝑌‘𝑏)) ∈ 𝐶 ∧ (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)) ∈ 𝐶) → ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) ∈ 𝐶) |
33 | 4, 17, 30, 32 | syl3anc 1318 |
. . 3
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) ∈ 𝐶) |
34 | | eqid 2610 |
. . 3
⊢ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) |
35 | 33, 34 | fmptd 6292 |
. 2
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))):𝐷⟶𝐶) |
36 | | ovex 6577 |
. . . . . 6
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
37 | 36 | a1i 11 |
. . . . 5
⊢ (𝜑 → (ℕ0
↑𝑚 𝐼) ∈ V) |
38 | 13, 37 | rabexd 4741 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ V) |
39 | | mptexg 6389 |
. . . 4
⊢ (𝐷 ∈ V → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) ∈
V) |
40 | 38, 39 | syl 17 |
. . 3
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) ∈
V) |
41 | | funmpt 5840 |
. . . 4
⊢ Fun
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) |
42 | 41 | a1i 11 |
. . 3
⊢ (𝜑 → Fun (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
43 | | fvex 6113 |
. . . 4
⊢
(0g‘𝑆) ∈ V |
44 | 43 | a1i 11 |
. . 3
⊢ (𝜑 → (0g‘𝑆) ∈ V) |
45 | | eqid 2610 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
46 | | evlslem1.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) |
47 | 11, 12, 45, 14, 46 | mplelsfi 19312 |
. . . 4
⊢ (𝜑 → 𝑌 finSupp (0g‘𝑅)) |
48 | 47 | fsuppimpd 8165 |
. . 3
⊢ (𝜑 → (𝑌 supp (0g‘𝑅)) ∈ Fin) |
49 | 15 | feqmptd 6159 |
. . . . . . 7
⊢ (𝜑 → 𝑌 = (𝑏 ∈ 𝐷 ↦ (𝑌‘𝑏))) |
50 | 49 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → (𝑌 supp (0g‘𝑅)) = ((𝑏 ∈ 𝐷 ↦ (𝑌‘𝑏)) supp (0g‘𝑅))) |
51 | | eqimss2 3621 |
. . . . . 6
⊢ ((𝑌 supp (0g‘𝑅)) = ((𝑏 ∈ 𝐷 ↦ (𝑌‘𝑏)) supp (0g‘𝑅)) → ((𝑏 ∈ 𝐷 ↦ (𝑌‘𝑏)) supp (0g‘𝑅)) ⊆ (𝑌 supp (0g‘𝑅))) |
52 | 50, 51 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ (𝑌‘𝑏)) supp (0g‘𝑅)) ⊆ (𝑌 supp (0g‘𝑅))) |
53 | | rhmghm 18548 |
. . . . . 6
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
54 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝑆) = (0g‘𝑆) |
55 | 45, 54 | ghmid 17489 |
. . . . . 6
⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹‘(0g‘𝑅)) = (0g‘𝑆)) |
56 | 5, 53, 55 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (𝐹‘(0g‘𝑅)) = (0g‘𝑆)) |
57 | | fvex 6113 |
. . . . . 6
⊢ (𝑌‘𝑏) ∈ V |
58 | 57 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑌‘𝑏) ∈ V) |
59 | | fvex 6113 |
. . . . . 6
⊢
(0g‘𝑅) ∈ V |
60 | 59 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
61 | 52, 56, 58, 60 | suppssfv 7218 |
. . . 4
⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ (𝐹‘(𝑌‘𝑏))) supp (0g‘𝑆)) ⊆ (𝑌 supp (0g‘𝑅))) |
62 | 7, 31, 54 | ringlz 18410 |
. . . . 5
⊢ ((𝑆 ∈ Ring ∧ 𝑥 ∈ 𝐶) → ((0g‘𝑆) · 𝑥) = (0g‘𝑆)) |
63 | 3, 62 | sylan 487 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((0g‘𝑆) · 𝑥) = (0g‘𝑆)) |
64 | | fvex 6113 |
. . . . 5
⊢ (𝐹‘(𝑌‘𝑏)) ∈ V |
65 | 64 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑌‘𝑏)) ∈ V) |
66 | 61, 63, 65, 30, 44 | suppssov1 7214 |
. . 3
⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) supp
(0g‘𝑆))
⊆ (𝑌 supp
(0g‘𝑅))) |
67 | | suppssfifsupp 8173 |
. . 3
⊢ ((((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) ∈ V ∧ Fun
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) ∧
(0g‘𝑆)
∈ V) ∧ ((𝑌 supp
(0g‘𝑅))
∈ Fin ∧ ((𝑏 ∈
𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) supp
(0g‘𝑆))
⊆ (𝑌 supp
(0g‘𝑅))))
→ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) finSupp
(0g‘𝑆)) |
68 | 40, 42, 44, 48, 66, 67 | syl32anc 1326 |
. 2
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) finSupp
(0g‘𝑆)) |
69 | 35, 68 | jca 553 |
1
⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) finSupp
(0g‘𝑆))) |