Step | Hyp | Ref
| Expression |
1 | | elply 24399 |
. . . . 5
⊢ (𝑓 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0})
↑𝑚 ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
2 | 1 | simprbi 492 |
. . . 4
⊢ (𝑓 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0})
↑𝑚 ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
3 | | eqid 2778 |
. . . . . . . . 9
⊢
(ℂfld ↑s ℂ) =
(ℂfld ↑s ℂ) |
4 | | cnfldbas 20157 |
. . . . . . . . 9
⊢ ℂ =
(Base‘ℂfld) |
5 | | eqid 2778 |
. . . . . . . . 9
⊢
(0g‘(ℂfld ↑s
ℂ)) = (0g‘(ℂfld
↑s ℂ)) |
6 | | cnex 10355 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
7 | 6 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → ℂ ∈ V) |
8 | | fzfid 13096 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (0...𝑛) ∈ Fin) |
9 | | cnring 20175 |
. . . . . . . . . 10
⊢
ℂfld ∈ Ring |
10 | | ringcmn 18979 |
. . . . . . . . . 10
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
11 | 9, 10 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → ℂfld ∈
CMnd) |
12 | 4 | subrgss 19184 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 ⊆ ℂ) |
13 | 12 | ad2antrr 716 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ⊆ ℂ) |
14 | | elmapi 8164 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0) → 𝑎:ℕ0⟶(𝑆 ∪ {0})) |
15 | 14 | ad2antll 719 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → 𝑎:ℕ0⟶(𝑆 ∪ {0})) |
16 | | subrgsubg 19189 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 ∈
(SubGrp‘ℂfld)) |
17 | | cnfld0 20177 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 =
(0g‘ℂfld) |
18 | 17 | subg0cl 17997 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 ∈
(SubGrp‘ℂfld) → 0 ∈ 𝑆) |
19 | 16, 18 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 0 ∈ 𝑆) |
20 | 19 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → 0 ∈ 𝑆) |
21 | 20 | snssd 4573 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → {0} ⊆ 𝑆) |
22 | | ssequn2 4009 |
. . . . . . . . . . . . . . . 16
⊢ ({0}
⊆ 𝑆 ↔ (𝑆 ∪ {0}) = 𝑆) |
23 | 21, 22 | sylib 210 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝑆 ∪ {0}) = 𝑆) |
24 | 23 | feq3d 6280 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝑎:ℕ0⟶(𝑆 ∪ {0}) ↔ 𝑎:ℕ0⟶𝑆)) |
25 | 15, 24 | mpbid 224 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → 𝑎:ℕ0⟶𝑆) |
26 | | elfznn0 12756 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...𝑛) → 𝑘 ∈ ℕ0) |
27 | | ffvelrn 6623 |
. . . . . . . . . . . . 13
⊢ ((𝑎:ℕ0⟶𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑎‘𝑘) ∈ 𝑆) |
28 | 25, 26, 27 | syl2an 589 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) ∈ 𝑆) |
29 | 13, 28 | sseldd 3822 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) ∈ ℂ) |
30 | 29 | adantrl 706 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑎‘𝑘) ∈ ℂ) |
31 | | simprl 761 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑧 ∈ ℂ) |
32 | 26 | ad2antll 719 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑘 ∈ ℕ0) |
33 | | expcl 13201 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑧↑𝑘) ∈
ℂ) |
34 | 31, 32, 33 | syl2anc 579 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑧↑𝑘) ∈ ℂ) |
35 | 30, 34 | mulcld 10399 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → ((𝑎‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
36 | | eqid 2778 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) = (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) |
37 | 6 | mptex 6760 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ V |
38 | 37 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ V) |
39 | | fvex 6461 |
. . . . . . . . . . 11
⊢
(0g‘(ℂfld ↑s
ℂ)) ∈ V |
40 | 39 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (0g‘(ℂfld
↑s ℂ)) ∈ V) |
41 | 36, 8, 38, 40 | fsuppmptdm 8576 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) finSupp
(0g‘(ℂfld ↑s
ℂ))) |
42 | 3, 4, 5, 7, 8, 11,
35, 41 | pwsgsum 18775 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → ((ℂfld ↑s
ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦
(ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))))) |
43 | | fzfid 13096 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑧 ∈ ℂ) → (0...𝑛) ∈ Fin) |
44 | 35 | anassrs 461 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑛)) → ((𝑎‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
45 | 43, 44 | gsumfsum 20220 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑧 ∈ ℂ) →
(ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) |
46 | 45 | mpteq2dva 4981 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝑧 ∈ ℂ ↦
(ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
47 | 42, 46 | eqtrd 2814 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → ((ℂfld ↑s
ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
48 | 3 | pwsring 19013 |
. . . . . . . . . 10
⊢
((ℂfld ∈ Ring ∧ ℂ ∈ V) →
(ℂfld ↑s ℂ) ∈
Ring) |
49 | 9, 6, 48 | mp2an 682 |
. . . . . . . . 9
⊢
(ℂfld ↑s ℂ) ∈
Ring |
50 | | ringcmn 18979 |
. . . . . . . . 9
⊢
((ℂfld ↑s ℂ) ∈ Ring
→ (ℂfld ↑s ℂ) ∈
CMnd) |
51 | 49, 50 | mp1i 13 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (ℂfld ↑s
ℂ) ∈ CMnd) |
52 | | cncrng 20174 |
. . . . . . . . . . 11
⊢
ℂfld ∈ CRing |
53 | | plypf1.e |
. . . . . . . . . . . 12
⊢ 𝐸 =
(eval1‘ℂfld) |
54 | | eqid 2778 |
. . . . . . . . . . . 12
⊢
(Poly1‘ℂfld) =
(Poly1‘ℂfld) |
55 | 53, 54, 3, 4 | evl1rhm 20103 |
. . . . . . . . . . 11
⊢
(ℂfld ∈ CRing → 𝐸 ∈
((Poly1‘ℂfld) RingHom (ℂfld
↑s ℂ))) |
56 | 52, 55 | ax-mp 5 |
. . . . . . . . . 10
⊢ 𝐸 ∈
((Poly1‘ℂfld) RingHom (ℂfld
↑s ℂ)) |
57 | | plypf1.r |
. . . . . . . . . . . 12
⊢ 𝑅 = (ℂfld
↾s 𝑆) |
58 | | plypf1.p |
. . . . . . . . . . . 12
⊢ 𝑃 = (Poly1‘𝑅) |
59 | | plypf1.a |
. . . . . . . . . . . 12
⊢ 𝐴 = (Base‘𝑃) |
60 | 54, 57, 58, 59 | subrgply1 20010 |
. . . . . . . . . . 11
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝐴 ∈
(SubRing‘(Poly1‘ℂfld))) |
61 | 60 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → 𝐴 ∈
(SubRing‘(Poly1‘ℂfld))) |
62 | | rhmima 19214 |
. . . . . . . . . 10
⊢ ((𝐸 ∈
((Poly1‘ℂfld) RingHom (ℂfld
↑s ℂ)) ∧ 𝐴 ∈
(SubRing‘(Poly1‘ℂfld))) → (𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s
ℂ))) |
63 | 56, 61, 62 | sylancr 581 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s
ℂ))) |
64 | | subrgsubg 19189 |
. . . . . . . . 9
⊢ ((𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s ℂ))
→ (𝐸 “ 𝐴) ∈
(SubGrp‘(ℂfld ↑s
ℂ))) |
65 | | subgsubm 18011 |
. . . . . . . . 9
⊢ ((𝐸 “ 𝐴) ∈
(SubGrp‘(ℂfld ↑s ℂ)) →
(𝐸 “ 𝐴) ∈
(SubMnd‘(ℂfld ↑s
ℂ))) |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝐸 “ 𝐴) ∈
(SubMnd‘(ℂfld ↑s
ℂ))) |
67 | | eqid 2778 |
. . . . . . . . . . . 12
⊢
(Base‘(ℂfld ↑s ℂ)) =
(Base‘(ℂfld ↑s
ℂ)) |
68 | 9 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ℂfld ∈
Ring) |
69 | 6 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ℂ ∈ V) |
70 | | fconst6g 6346 |
. . . . . . . . . . . . . 14
⊢ ((𝑎‘𝑘) ∈ ℂ → (ℂ ×
{(𝑎‘𝑘)}):ℂ⟶ℂ) |
71 | 29, 70 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ) |
72 | 3, 4, 67 | pwselbasb 16545 |
. . . . . . . . . . . . . 14
⊢
((ℂfld ∈ Ring ∧ ℂ ∈ V) →
((ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld
↑s ℂ)) ↔ (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)) |
73 | 9, 6, 72 | mp2an 682 |
. . . . . . . . . . . . 13
⊢ ((ℂ
× {(𝑎‘𝑘)}) ∈
(Base‘(ℂfld ↑s ℂ)) ↔
(ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ) |
74 | 71, 73 | sylibr 226 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld
↑s ℂ))) |
75 | 34 | anass1rs 645 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑧↑𝑘) ∈ ℂ) |
76 | 75 | fmpttd 6651 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ) |
77 | 3, 4, 67 | pwselbasb 16545 |
. . . . . . . . . . . . . 14
⊢
((ℂfld ∈ Ring ∧ ℂ ∈ V) →
((𝑧 ∈ ℂ ↦
(𝑧↑𝑘)) ∈ (Base‘(ℂfld
↑s ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ)) |
78 | 9, 6, 77 | mp2an 682 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld
↑s ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ) |
79 | 76, 78 | sylibr 226 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld
↑s ℂ))) |
80 | | cnfldmul 20159 |
. . . . . . . . . . . 12
⊢ ·
= (.r‘ℂfld) |
81 | | eqid 2778 |
. . . . . . . . . . . 12
⊢
(.r‘(ℂfld ↑s
ℂ)) = (.r‘(ℂfld
↑s ℂ)) |
82 | 3, 67, 68, 69, 74, 79, 80, 81 | pwsmulrval 16548 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld
↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = ((ℂ × {(𝑎‘𝑘)}) ∘𝑓 ·
(𝑧 ∈ ℂ ↦
(𝑧↑𝑘)))) |
83 | 29 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑎‘𝑘) ∈ ℂ) |
84 | | fconstmpt 5413 |
. . . . . . . . . . . . 13
⊢ (ℂ
× {(𝑎‘𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎‘𝑘)) |
85 | 84 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎‘𝑘))) |
86 | | eqidd 2779 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) |
87 | 69, 83, 75, 85, 86 | offval2 7193 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)}) ∘𝑓 ·
(𝑧 ∈ ℂ ↦
(𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) |
88 | 82, 87 | eqtrd 2814 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld
↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) |
89 | 63 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s
ℂ))) |
90 | | eqid 2778 |
. . . . . . . . . . . . . 14
⊢
(algSc‘(Poly1‘ℂfld)) =
(algSc‘(Poly1‘ℂfld)) |
91 | 53, 54, 4, 90 | evl1sca 20105 |
. . . . . . . . . . . . 13
⊢
((ℂfld ∈ CRing ∧ (𝑎‘𝑘) ∈ ℂ) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) =
(ℂ × {(𝑎‘𝑘)})) |
92 | 52, 29, 91 | sylancr 581 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) =
(ℂ × {(𝑎‘𝑘)})) |
93 | | eqid 2778 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘(Poly1‘ℂfld)) =
(Base‘(Poly1‘ℂfld)) |
94 | 93, 67 | rhmf 19126 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 ∈
((Poly1‘ℂfld) RingHom (ℂfld
↑s ℂ)) → 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld
↑s ℂ))) |
95 | 56, 94 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld
↑s ℂ)) |
96 | | ffn 6293 |
. . . . . . . . . . . . . 14
⊢ (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld
↑s ℂ)) → 𝐸 Fn
(Base‘(Poly1‘ℂfld))) |
97 | 95, 96 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐸 Fn
(Base‘(Poly1‘ℂfld))) |
98 | 93 | subrgss 19184 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈
(SubRing‘(Poly1‘ℂfld)) → 𝐴 ⊆
(Base‘(Poly1‘ℂfld))) |
99 | 60, 98 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝐴 ⊆
(Base‘(Poly1‘ℂfld))) |
100 | 99 | ad2antrr 716 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ⊆
(Base‘(Poly1‘ℂfld))) |
101 | | simpll 757 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ∈
(SubRing‘ℂfld)) |
102 | 54, 90, 57, 58, 101, 59, 4, 29 | subrg1asclcl 20037 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) →
(((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴 ↔ (𝑎‘𝑘) ∈ 𝑆)) |
103 | 28, 102 | mpbird 249 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) →
((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴) |
104 | | fnfvima 6771 |
. . . . . . . . . . . . 13
⊢ ((𝐸 Fn
(Base‘(Poly1‘ℂfld)) ∧ 𝐴 ⊆
(Base‘(Poly1‘ℂfld)) ∧
((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)))
∈ (𝐸 “ 𝐴)) |
105 | 97, 100, 103, 104 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)))
∈ (𝐸 “ 𝐴)) |
106 | 92, 105 | eqeltrrd 2860 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) ∈ (𝐸 “ 𝐴)) |
107 | 67 | subrgss 19184 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s ℂ))
→ (𝐸 “ 𝐴) ⊆
(Base‘(ℂfld ↑s
ℂ))) |
108 | 89, 107 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸 “ 𝐴) ⊆ (Base‘(ℂfld
↑s ℂ))) |
109 | 60 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈
(SubRing‘(Poly1‘ℂfld))) |
110 | | eqid 2778 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(mulGrp‘(Poly1‘ℂfld)) =
(mulGrp‘(Poly1‘ℂfld)) |
111 | 110 | subrgsubm 19196 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈
(SubRing‘(Poly1‘ℂfld)) → 𝐴 ∈
(SubMnd‘(mulGrp‘(Poly1‘ℂfld)))) |
112 | 109, 111 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈
(SubMnd‘(mulGrp‘(Poly1‘ℂfld)))) |
113 | 26 | adantl 475 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑘 ∈ ℕ0) |
114 | | eqid 2778 |
. . . . . . . . . . . . . . . . . . 19
⊢
(var1‘ℂfld) =
(var1‘ℂfld) |
115 | 114, 101,
57, 58, 59 | subrgvr1cl 20039 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) →
(var1‘ℂfld) ∈ 𝐴) |
116 | | eqid 2778 |
. . . . . . . . . . . . . . . . . . 19
⊢
(.g‘(mulGrp‘(Poly1‘ℂfld)))
=
(.g‘(mulGrp‘(Poly1‘ℂfld))) |
117 | 116 | submmulgcl 17980 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
(SubMnd‘(mulGrp‘(Poly1‘ℂfld)))
∧ 𝑘 ∈
ℕ0 ∧ (var1‘ℂfld) ∈
𝐴) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ 𝐴) |
118 | 112, 113,
115, 117 | syl3anc 1439 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ 𝐴) |
119 | | fnfvima 6771 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸 Fn
(Base‘(Poly1‘ℂfld)) ∧ 𝐴 ⊆
(Base‘(Poly1‘ℂfld)) ∧ (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ 𝐴) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
∈ (𝐸 “ 𝐴)) |
120 | 97, 100, 118, 119 | syl3anc 1439 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
∈ (𝐸 “ 𝐴)) |
121 | 108, 120 | sseldd 3822 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
∈ (Base‘(ℂfld ↑s ℂ))) |
122 | 3, 4, 67, 68, 69, 121 | pwselbas 16546 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))):ℂ⟶ℂ) |
123 | 122 | feqmptd 6511 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
= (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧))) |
124 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ℂfld
∈ CRing) |
125 | | simpr 479 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ) |
126 | 53, 114, 4, 54, 93, 124, 125 | evl1vard 20108 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) →
((var1‘ℂfld) ∈
(Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧)) |
127 | | eqid 2778 |
. . . . . . . . . . . . . . . . 17
⊢
(.g‘(mulGrp‘ℂfld)) =
(.g‘(mulGrp‘ℂfld)) |
128 | 113 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0) |
129 | 53, 54, 4, 93, 124, 125, 126, 116, 127, 128 | evl1expd 20116 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧))) |
130 | 129 | simprd 491 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧)) |
131 | | cnfldexp 20186 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘)) |
132 | 125, 128,
131 | syl2anc 579 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘)) |
133 | 130, 132 | eqtrd 2814 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘)) |
134 | 133 | mpteq2dva 4981 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) |
135 | 123, 134 | eqtrd 2814 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
= (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) |
136 | 135, 120 | eqeltrrd 2860 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (𝐸 “ 𝐴)) |
137 | 81 | subrgmcl 19195 |
. . . . . . . . . . 11
⊢ (((𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s ℂ)) ∧
(ℂ × {(𝑎‘𝑘)}) ∈ (𝐸 “ 𝐴) ∧ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (𝐸 “ 𝐴)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld
↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)) |
138 | 89, 106, 136, 137 | syl3anc 1439 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld
↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)) |
139 | 88, 138 | eqeltrrd 2860 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)) |
140 | 139 | fmpttd 6651 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))):(0...𝑛)⟶(𝐸 “ 𝐴)) |
141 | 36, 8, 139, 40 | fsuppmptdm 8576 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) finSupp
(0g‘(ℂfld ↑s
ℂ))) |
142 | 5, 51, 8, 66, 140, 141 | gsumsubmcl 18716 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → ((ℂfld ↑s
ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) ∈ (𝐸 “ 𝐴)) |
143 | 47, 142 | eqeltrrd 2860 |
. . . . . 6
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)) |
144 | | eleq1 2847 |
. . . . . 6
⊢ (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → (𝑓 ∈ (𝐸 “ 𝐴) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))) |
145 | 143, 144 | syl5ibrcom 239 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → 𝑓 ∈ (𝐸 “ 𝐴))) |
146 | 145 | rexlimdvva 3221 |
. . . 4
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0)𝑓 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → 𝑓 ∈ (𝐸 “ 𝐴))) |
147 | 2, 146 | syl5 34 |
. . 3
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) → 𝑓 ∈ (𝐸 “ 𝐴))) |
148 | | ffun 6296 |
. . . . . 6
⊢ (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld
↑s ℂ)) → Fun 𝐸) |
149 | 95, 148 | ax-mp 5 |
. . . . 5
⊢ Fun 𝐸 |
150 | | fvelima 6510 |
. . . . 5
⊢ ((Fun
𝐸 ∧ 𝑓 ∈ (𝐸 “ 𝐴)) → ∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓) |
151 | 149, 150 | mpan 680 |
. . . 4
⊢ (𝑓 ∈ (𝐸 “ 𝐴) → ∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓) |
152 | 99 | sselda 3821 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈
(Base‘(Poly1‘ℂfld))) |
153 | | eqid 2778 |
. . . . . . . . . . . 12
⊢ (
·𝑠
‘(Poly1‘ℂfld)) = (
·𝑠
‘(Poly1‘ℂfld)) |
154 | | eqid 2778 |
. . . . . . . . . . . 12
⊢
(coe1‘𝑎) = (coe1‘𝑎) |
155 | 54, 114, 93, 153, 110, 116, 154 | ply1coe 20073 |
. . . . . . . . . . 11
⊢
((ℂfld ∈ Ring ∧ 𝑎 ∈
(Base‘(Poly1‘ℂfld))) → 𝑎 =
((Poly1‘ℂfld) Σg
(𝑘 ∈
ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))) |
156 | 9, 152, 155 | sylancr 581 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑎 =
((Poly1‘ℂfld) Σg
(𝑘 ∈
ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))) |
157 | 156 | fveq2d 6452 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = (𝐸‘((Poly1‘ℂfld)
Σg (𝑘 ∈
ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))) |
158 | | eqid 2778 |
. . . . . . . . . 10
⊢
(0g‘(Poly1‘ℂfld)) =
(0g‘(Poly1‘ℂfld)) |
159 | 54 | ply1ring 20025 |
. . . . . . . . . . . 12
⊢
(ℂfld ∈ Ring →
(Poly1‘ℂfld) ∈ Ring) |
160 | 9, 159 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(Poly1‘ℂfld) ∈
Ring |
161 | | ringcmn 18979 |
. . . . . . . . . . 11
⊢
((Poly1‘ℂfld) ∈ Ring →
(Poly1‘ℂfld) ∈ CMnd) |
162 | 160, 161 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) →
(Poly1‘ℂfld) ∈ CMnd) |
163 | | ringmnd 18954 |
. . . . . . . . . . 11
⊢
((ℂfld ↑s ℂ) ∈ Ring
→ (ℂfld ↑s ℂ) ∈
Mnd) |
164 | 49, 163 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (ℂfld
↑s ℂ) ∈ Mnd) |
165 | | nn0ex 11654 |
. . . . . . . . . . 11
⊢
ℕ0 ∈ V |
166 | 165 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℕ0 ∈
V) |
167 | | rhmghm 19125 |
. . . . . . . . . . . 12
⊢ (𝐸 ∈
((Poly1‘ℂfld) RingHom (ℂfld
↑s ℂ)) → 𝐸 ∈
((Poly1‘ℂfld) GrpHom (ℂfld
↑s ℂ))) |
168 | 56, 167 | ax-mp 5 |
. . . . . . . . . . 11
⊢ 𝐸 ∈
((Poly1‘ℂfld) GrpHom (ℂfld
↑s ℂ)) |
169 | | ghmmhm 18065 |
. . . . . . . . . . 11
⊢ (𝐸 ∈
((Poly1‘ℂfld) GrpHom (ℂfld
↑s ℂ)) → 𝐸 ∈
((Poly1‘ℂfld) MndHom (ℂfld
↑s ℂ))) |
170 | 168, 169 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝐸 ∈
((Poly1‘ℂfld) MndHom (ℂfld
↑s ℂ))) |
171 | 54 | ply1lmod 20029 |
. . . . . . . . . . . . 13
⊢
(ℂfld ∈ Ring →
(Poly1‘ℂfld) ∈ LMod) |
172 | 9, 171 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
(Poly1‘ℂfld) ∈ LMod) |
173 | 12 | ad2antrr 716 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑆 ⊆
ℂ) |
174 | | eqid 2778 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝑅) =
(Base‘𝑅) |
175 | 154, 59, 58, 174 | coe1f 19988 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ 𝐴 → (coe1‘𝑎):ℕ0⟶(Base‘𝑅)) |
176 | 57 | subrgbas 19192 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 = (Base‘𝑅)) |
177 | 176 | feq3d 6280 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∈
(SubRing‘ℂfld) → ((coe1‘𝑎):ℕ0⟶𝑆 ↔
(coe1‘𝑎):ℕ0⟶(Base‘𝑅))) |
178 | 175, 177 | syl5ibr 238 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (𝑎 ∈ 𝐴 → (coe1‘𝑎):ℕ0⟶𝑆)) |
179 | 178 | imp 397 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎):ℕ0⟶𝑆) |
180 | 179 | ffvelrnda 6625 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑎)‘𝑘) ∈ 𝑆) |
181 | 173, 180 | sseldd 3822 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑎)‘𝑘) ∈ ℂ) |
182 | 110 | ringmgp 18951 |
. . . . . . . . . . . . . 14
⊢
((Poly1‘ℂfld) ∈ Ring →
(mulGrp‘(Poly1‘ℂfld)) ∈
Mnd) |
183 | 160, 182 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
(mulGrp‘(Poly1‘ℂfld)) ∈
Mnd) |
184 | | simpr 479 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
185 | 114, 54, 93 | vr1cl 19994 |
. . . . . . . . . . . . . 14
⊢
(ℂfld ∈ Ring →
(var1‘ℂfld) ∈
(Base‘(Poly1‘ℂfld))) |
186 | 9, 185 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
(var1‘ℂfld) ∈
(Base‘(Poly1‘ℂfld))) |
187 | 110, 93 | mgpbas 18893 |
. . . . . . . . . . . . . 14
⊢
(Base‘(Poly1‘ℂfld)) =
(Base‘(mulGrp‘(Poly1‘ℂfld))) |
188 | 187, 116 | mulgnn0cl 17955 |
. . . . . . . . . . . . 13
⊢
(((mulGrp‘(Poly1‘ℂfld)) ∈
Mnd ∧ 𝑘 ∈
ℕ0 ∧ (var1‘ℂfld) ∈
(Base‘(Poly1‘ℂfld))) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ (Base‘(Poly1‘ℂfld))) |
189 | 183, 184,
186, 188 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ (Base‘(Poly1‘ℂfld))) |
190 | 54 | ply1sca 20030 |
. . . . . . . . . . . . . 14
⊢
(ℂfld ∈ Ring → ℂfld =
(Scalar‘(Poly1‘ℂfld))) |
191 | 9, 190 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
ℂfld =
(Scalar‘(Poly1‘ℂfld)) |
192 | 93, 191, 153, 4 | lmodvscl 19283 |
. . . . . . . . . . . 12
⊢
(((Poly1‘ℂfld) ∈ LMod ∧
((coe1‘𝑎)‘𝑘) ∈ ℂ ∧ (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ (Base‘(Poly1‘ℂfld))) → (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
∈ (Base‘(Poly1‘ℂfld))) |
193 | 172, 181,
189, 192 | syl3anc 1439 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
∈ (Base‘(Poly1‘ℂfld))) |
194 | 193 | fmpttd 6651 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℕ0⟶(Base‘(Poly1‘ℂfld))) |
195 | 165 | mptex 6760 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
∈ V |
196 | | funmpt 6175 |
. . . . . . . . . . . . 13
⊢ Fun
(𝑘 ∈
ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) |
197 | | fvex 6461 |
. . . . . . . . . . . . 13
⊢
(0g‘(Poly1‘ℂfld))
∈ V |
198 | 195, 196,
197 | 3pm3.2i 1395 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
∧ (0g‘(Poly1‘ℂfld)) ∈ V) |
199 | 198 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
∧ (0g‘(Poly1‘ℂfld)) ∈ V)) |
200 | 154, 93, 54, 17 | coe1sfi 19990 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈
(Base‘(Poly1‘ℂfld)) →
(coe1‘𝑎)
finSupp 0) |
201 | 152, 200 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎) finSupp 0) |
202 | 201 | fsuppimpd 8572 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((coe1‘𝑎) supp 0) ∈
Fin) |
203 | 179 | feqmptd 6511 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎) = (𝑘 ∈ ℕ0 ↦
((coe1‘𝑎)‘𝑘))) |
204 | 203 | oveq1d 6939 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((coe1‘𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦
((coe1‘𝑎)‘𝑘)) supp 0)) |
205 | | eqimss2 3877 |
. . . . . . . . . . . . 13
⊢
(((coe1‘𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦
((coe1‘𝑎)‘𝑘)) supp 0) → ((𝑘 ∈ ℕ0 ↦
((coe1‘𝑎)‘𝑘)) supp 0) ⊆
((coe1‘𝑎)
supp 0)) |
206 | 204, 205 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦
((coe1‘𝑎)‘𝑘)) supp 0) ⊆
((coe1‘𝑎)
supp 0)) |
207 | 9, 171 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) →
(Poly1‘ℂfld) ∈ LMod) |
208 | 93, 191, 153, 17, 158 | lmod0vs 19299 |
. . . . . . . . . . . . 13
⊢
(((Poly1‘ℂfld) ∈ LMod ∧ 𝑥 ∈
(Base‘(Poly1‘ℂfld))) → (0(
·𝑠
‘(Poly1‘ℂfld))𝑥) =
(0g‘(Poly1‘ℂfld))) |
209 | 207, 208 | sylan 575 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈
(Base‘(Poly1‘ℂfld))) → (0(
·𝑠
‘(Poly1‘ℂfld))𝑥) =
(0g‘(Poly1‘ℂfld))) |
210 | | c0ex 10372 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
211 | 210 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 0 ∈ V) |
212 | 206, 209,
180, 189, 211 | suppssov1 7611 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
supp (0g‘(Poly1‘ℂfld))) ⊆ ((coe1‘𝑎)
supp 0)) |
213 | | suppssfifsupp 8580 |
. . . . . . . . . . 11
⊢ ((((𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
∧ (0g‘(Poly1‘ℂfld)) ∈ V) ∧ (((coe1‘𝑎) supp 0) ∈ Fin ∧ ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)(
·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
supp (0g‘(Poly1‘ℂfld))) ⊆ ((coe1‘𝑎)
supp 0))) → (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
finSupp (0g‘(Poly1‘ℂfld))) |
214 | 199, 202,
212, 213 | syl12anc 827 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
finSupp (0g‘(Poly1‘ℂfld))) |
215 | 93, 158, 162, 164, 166, 170, 194, 214 | gsummhm 18735 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((ℂfld
↑s ℂ) Σg (𝐸 ∘ (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
= (𝐸‘((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))) |
216 | | eqidd 2779 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
= (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) |
217 | 95 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld
↑s ℂ))) |
218 | 217 | feqmptd 6511 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝐸 = (𝑥 ∈
(Base‘(Poly1‘ℂfld)) ↦ (𝐸‘𝑥))) |
219 | | fveq2 6448 |
. . . . . . . . . . . 12
⊢ (𝑥 =
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
→ (𝐸‘𝑥) = (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) |
220 | 193, 216,
218, 219 | fmptco 6663 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))
= (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))) |
221 | 9 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
ℂfld ∈ Ring) |
222 | 6 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → ℂ
∈ V) |
223 | 95 | ffvelrni 6624 |
. . . . . . . . . . . . . . . 16
⊢
((((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
∈ (Base‘(Poly1‘ℂfld)) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
∈ (Base‘(ℂfld ↑s ℂ))) |
224 | 193, 223 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
∈ (Base‘(ℂfld ↑s ℂ))) |
225 | 3, 4, 67, 221, 222, 224 | pwselbas 16546 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℂ⟶ℂ) |
226 | 225 | feqmptd 6511 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
= (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧))) |
227 | 52 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) →
ℂfld ∈ CRing) |
228 | | simpr 479 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈
ℂ) |
229 | 53, 114, 4, 54, 93, 227, 228 | evl1vard 20108 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) →
((var1‘ℂfld) ∈
(Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧)) |
230 | 184 | adantr 474 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈
ℕ0) |
231 | 53, 54, 4, 93, 227, 228, 229, 116, 127, 230 | evl1expd 20116 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧))) |
232 | 228, 230,
131 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘)) |
233 | 232 | eqeq2d 2788 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧) ↔ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘))) |
234 | 233 | anbi2d 622 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧)) ↔ ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈
(Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘)))) |
235 | 231, 234 | mpbid 224 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘))) |
236 | 181 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) →
((coe1‘𝑎)‘𝑘) ∈ ℂ) |
237 | 53, 54, 4, 93, 227, 228, 235, 236, 153, 80 | evl1vsd 20115 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) →
((((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧) = (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
238 | 237 | simprd 491 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧) = (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) |
239 | 238 | mpteq2dva 4981 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧)) = (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
240 | 226, 239 | eqtrd 2814 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
= (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
241 | 240 | mpteq2dva 4981 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))
= (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) |
242 | 220, 241 | eqtrd 2814 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))
= (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) |
243 | 242 | oveq2d 6940 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((ℂfld
↑s ℂ) Σg (𝐸 ∘ (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
= ((ℂfld ↑s ℂ) Σg (𝑘 ∈
ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))) |
244 | 157, 215,
243 | 3eqtr2d 2820 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = ((ℂfld
↑s ℂ) Σg (𝑘 ∈ ℕ0
↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))) |
245 | 6 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℂ ∈ V) |
246 | 9, 10 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℂfld ∈
CMnd) |
247 | 181 | adantlr 705 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑎)‘𝑘) ∈ ℂ) |
248 | 33 | adantll 704 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ) |
249 | 247, 248 | mulcld 10399 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) →
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
250 | 249 | anasss 460 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)) →
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
251 | 165 | mptex 6760 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V |
252 | | funmpt 6175 |
. . . . . . . . . . . 12
⊢ Fun
(𝑘 ∈
ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
253 | 251, 252,
39 | 3pm3.2i 1395 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ0
↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∧
(0g‘(ℂfld ↑s ℂ))
∈ V) |
254 | 253 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∧
(0g‘(ℂfld ↑s ℂ))
∈ V)) |
255 | | fzfid 13096 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ∈ Fin) |
256 | | eldifn 3956 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (ℕ0
∖ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) → ¬ 𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
257 | 256 | adantl 475 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → ¬ 𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
258 | 152 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → 𝑎 ∈
(Base‘(Poly1‘ℂfld))) |
259 | | eldifi 3955 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ (ℕ0
∖ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) → 𝑘 ∈ ℕ0) |
260 | 259 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℕ0) |
261 | | eqid 2778 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (
deg1 ‘ℂfld) = ( deg1
‘ℂfld) |
262 | 261, 54, 93, 17, 154 | deg1ge 24306 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈
(Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0
∧ ((coe1‘𝑎)‘𝑘) ≠ 0) → 𝑘 ≤ (( deg1
‘ℂfld)‘𝑎)) |
263 | 262 | 3expia 1111 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈
(Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0)
→ (((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ (( deg1
‘ℂfld)‘𝑎))) |
264 | 258, 260,
263 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ (( deg1
‘ℂfld)‘𝑎))) |
265 | | 0xr 10425 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℝ* |
266 | 261, 54, 93 | deg1xrcl 24290 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈
(Base‘(Poly1‘ℂfld)) → ((
deg1 ‘ℂfld)‘𝑎) ∈
ℝ*) |
267 | 152, 266 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (( deg1
‘ℂfld)‘𝑎) ∈
ℝ*) |
268 | 267 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (( deg1
‘ℂfld)‘𝑎) ∈
ℝ*) |
269 | | xrmax2 12324 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((0
∈ ℝ* ∧ (( deg1
‘ℂfld)‘𝑎) ∈ ℝ*) → ((
deg1 ‘ℂfld)‘𝑎) ≤ if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) |
270 | 265, 268,
269 | sylancr 581 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (( deg1
‘ℂfld)‘𝑎) ≤ if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) |
271 | 260 | nn0red 11708 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ) |
272 | 271 | rexrd 10428 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ*) |
273 | | ifcl 4351 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((
deg1 ‘ℂfld)‘𝑎) ∈ ℝ* ∧ 0 ∈
ℝ*) → if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℝ*) |
274 | 268, 265,
273 | sylancl 580 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℝ*) |
275 | | xrletr 12306 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℝ*
∧ (( deg1 ‘ℂfld)‘𝑎) ∈ ℝ* ∧ if(0 ≤
(( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈ ℝ*) →
((𝑘 ≤ (( deg1
‘ℂfld)‘𝑎) ∧ (( deg1
‘ℂfld)‘𝑎) ≤ if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) → 𝑘 ≤ if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
276 | 272, 268,
274, 275 | syl3anc 1439 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → ((𝑘 ≤ (( deg1
‘ℂfld)‘𝑎) ∧ (( deg1
‘ℂfld)‘𝑎) ≤ if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) → 𝑘 ≤ if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
277 | 270, 276 | mpan2d 684 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (𝑘 ≤ (( deg1
‘ℂfld)‘𝑎) → 𝑘 ≤ if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
278 | 264, 277 | syld 47 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
279 | 278, 260 | jctild 521 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) ≠ 0 → (𝑘 ∈ ℕ0 ∧ 𝑘 ≤ if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) |
280 | 261, 54, 93 | deg1cl 24291 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 ∈
(Base‘(Poly1‘ℂfld)) → ((
deg1 ‘ℂfld)‘𝑎) ∈ (ℕ0 ∪
{-∞})) |
281 | 152, 280 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (( deg1
‘ℂfld)‘𝑎) ∈ (ℕ0 ∪
{-∞})) |
282 | | elun 3976 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ (ℕ0 ∪
{-∞}) ↔ ((( deg1
‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞})) |
283 | 281, 282 | sylib 210 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((( deg1
‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞})) |
284 | | nn0ge0 11674 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → 0 ≤ ((
deg1 ‘ℂfld)‘𝑎)) |
285 | 284 | iftrued 4315 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤
(( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) = (( deg1
‘ℂfld)‘𝑎)) |
286 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → ((
deg1 ‘ℂfld)‘𝑎) ∈
ℕ0) |
287 | 285, 286 | eqeltrd 2859 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤
(( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℕ0) |
288 | | mnflt0 12275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ -∞
< 0 |
289 | | mnfxr 10436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ -∞
∈ ℝ* |
290 | | xrltnle 10446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((-∞ ∈ ℝ* ∧ 0 ∈
ℝ*) → (-∞ < 0 ↔ ¬ 0 ≤
-∞)) |
291 | 289, 265,
290 | mp2an 682 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (-∞
< 0 ↔ ¬ 0 ≤ -∞) |
292 | 288, 291 | mpbi 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ¬ 0
≤ -∞ |
293 | | elsni 4415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → (( deg1
‘ℂfld)‘𝑎) = -∞) |
294 | 293 | breq2d 4900 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → (0 ≤ ((
deg1 ‘ℂfld)‘𝑎) ↔ 0 ≤ -∞)) |
295 | 292, 294 | mtbiri 319 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → ¬ 0 ≤ ((
deg1 ‘ℂfld)‘𝑎)) |
296 | 295 | iffalsed 4318 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) = 0) |
297 | | 0nn0 11664 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
ℕ0 |
298 | 296, 297 | syl6eqel 2867 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℕ0) |
299 | 287, 298 | jaoi 846 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((
deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞}) → if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℕ0) |
300 | 283, 299 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℕ0) |
301 | 300 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℕ0) |
302 | | fznn0 12755 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (if(0
≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈ ℕ0 →
(𝑘 ∈ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ↔ (𝑘 ∈ ℕ0 ∧ 𝑘 ≤ if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) |
303 | 301, 302 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ↔ (𝑘 ∈ ℕ0 ∧ 𝑘 ≤ if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) |
304 | 279, 303 | sylibrd 251 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) |
305 | 304 | necon1bd 2987 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (¬ 𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) → ((coe1‘𝑎)‘𝑘) = 0)) |
306 | 257, 305 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → ((coe1‘𝑎)‘𝑘) = 0) |
307 | 306 | oveq1d 6939 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘))) |
308 | 259, 248 | sylan2 586 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (𝑧↑𝑘) ∈ ℂ) |
309 | 308 | mul02d 10576 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (0 · (𝑧↑𝑘)) = 0) |
310 | 307, 309 | eqtrd 2814 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = 0) |
311 | 310 | an32s 642 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) ∧ 𝑧 ∈ ℂ) →
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = 0) |
312 | 311 | mpteq2dva 4981 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ 0)) |
313 | | fconstmpt 5413 |
. . . . . . . . . . . . 13
⊢ (ℂ
× {0}) = (𝑧 ∈
ℂ ↦ 0) |
314 | | ringmnd 18954 |
. . . . . . . . . . . . . . 15
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
315 | 9, 314 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
ℂfld ∈ Mnd |
316 | 3, 17 | pws0g 17723 |
. . . . . . . . . . . . . 14
⊢
((ℂfld ∈ Mnd ∧ ℂ ∈ V) →
(ℂ × {0}) = (0g‘(ℂfld
↑s ℂ))) |
317 | 315, 6, 316 | mp2an 682 |
. . . . . . . . . . . . 13
⊢ (ℂ
× {0}) = (0g‘(ℂfld
↑s ℂ)) |
318 | 313, 317 | eqtr3i 2804 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℂ ↦ 0) =
(0g‘(ℂfld ↑s
ℂ)) |
319 | 312, 318 | syl6eq 2830 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) =
(0g‘(ℂfld ↑s
ℂ))) |
320 | 319, 166 | suppss2 7613 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) supp
(0g‘(ℂfld ↑s
ℂ))) ⊆ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
321 | | suppssfifsupp 8580 |
. . . . . . . . . 10
⊢ ((((𝑘 ∈ ℕ0
↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∧
(0g‘(ℂfld ↑s ℂ))
∈ V) ∧ ((0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ∈ Fin ∧ ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) supp
(0g‘(ℂfld ↑s
ℂ))) ⊆ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) finSupp
(0g‘(ℂfld ↑s
ℂ))) |
322 | 254, 255,
320, 321 | syl12anc 827 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) finSupp
(0g‘(ℂfld ↑s
ℂ))) |
323 | 3, 4, 5, 245, 166, 246, 250, 322 | pwsgsum 18775 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((ℂfld
↑s ℂ) Σg (𝑘 ∈ ℕ0
↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦
(ℂfld Σg (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))) |
324 | | fz0ssnn0 12758 |
. . . . . . . . . . . 12
⊢ (0...if(0
≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ⊆
ℕ0 |
325 | | resmpt 5701 |
. . . . . . . . . . . 12
⊢
((0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ⊆ ℕ0 →
((𝑘 ∈
ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) = (𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
326 | 324, 325 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) = (𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) |
327 | 326 | oveq2i 6935 |
. . . . . . . . . 10
⊢
(ℂfld Σg ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) = (ℂfld
Σg (𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
328 | 9, 10 | mp1i 13 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ℂfld
∈ CMnd) |
329 | 165 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ℕ0
∈ V) |
330 | 249 | fmpttd 6651 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))):ℕ0⟶ℂ) |
331 | 310, 329 | suppss2 7613 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) supp 0) ⊆ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
332 | 165 | mptex 6760 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V |
333 | | funmpt 6175 |
. . . . . . . . . . . . . 14
⊢ Fun
(𝑘 ∈
ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) |
334 | 332, 333,
210 | 3pm3.2i 1395 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∧ 0 ∈ V) |
335 | 334 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∧ 0 ∈ V)) |
336 | | fzfid 13096 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ∈ Fin) |
337 | | suppssfifsupp 8580 |
. . . . . . . . . . . 12
⊢ ((((𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∧ 0 ∈ V) ∧ ((0...if(0 ≤
(( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ∈ Fin ∧ ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) supp 0) ⊆ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) finSupp 0) |
338 | 335, 336,
331, 337 | syl12anc 827 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) finSupp 0) |
339 | 4, 17, 328, 329, 330, 331, 338 | gsumres 18711 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) →
(ℂfld Σg ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) = (ℂfld
Σg (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) |
340 | | elfznn0 12756 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) → 𝑘 ∈ ℕ0) |
341 | 340, 249 | sylan2 586 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
342 | 336, 341 | gsumfsum 20220 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) →
(ℂfld Σg (𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) |
343 | 327, 339,
342 | 3eqtr3a 2838 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) →
(ℂfld Σg (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) |
344 | 343 | mpteq2dva 4981 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑧 ∈ ℂ ↦
(ℂfld Σg (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
345 | 244, 323,
344 | 3eqtrd 2818 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
346 | 12 | adantr 474 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑆 ⊆ ℂ) |
347 | | elplyr 24405 |
. . . . . . . 8
⊢ ((𝑆 ⊆ ℂ ∧ if(0 ≤
(( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈ ℕ0 ∧
(coe1‘𝑎):ℕ0⟶𝑆) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆)) |
348 | 346, 300,
179, 347 | syl3anc 1439 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆)) |
349 | 345, 348 | eqeltrd 2859 |
. . . . . 6
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) ∈ (Poly‘𝑆)) |
350 | | eleq1 2847 |
. . . . . 6
⊢ ((𝐸‘𝑎) = 𝑓 → ((𝐸‘𝑎) ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (Poly‘𝑆))) |
351 | 349, 350 | syl5ibcom 237 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝐸‘𝑎) = 𝑓 → 𝑓 ∈ (Poly‘𝑆))) |
352 | 351 | rexlimdva 3213 |
. . . 4
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓 → 𝑓 ∈ (Poly‘𝑆))) |
353 | 151, 352 | syl5 34 |
. . 3
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (𝑓 ∈ (𝐸 “ 𝐴) → 𝑓 ∈ (Poly‘𝑆))) |
354 | 147, 353 | impbid 204 |
. 2
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (𝐸 “ 𝐴))) |
355 | 354 | eqrdv 2776 |
1
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (Poly‘𝑆) = (𝐸 “ 𝐴)) |