Step | Hyp | Ref
| Expression |
1 | | elply 23755 |
. . . . 5
⊢ (𝑓 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0})
↑𝑚 ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
2 | 1 | simprbi 479 |
. . . 4
⊢ (𝑓 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0})
↑𝑚 ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
3 | | eqid 2610 |
. . . . . . . . 9
⊢
(ℂfld ↑s ℂ) =
(ℂfld ↑s ℂ) |
4 | | cnfldbas 19571 |
. . . . . . . . 9
⊢ ℂ =
(Base‘ℂfld) |
5 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘(ℂfld ↑s
ℂ)) = (0g‘(ℂfld
↑s ℂ)) |
6 | | cnex 9896 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
7 | 6 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → ℂ ∈ V) |
8 | | fzfid 12634 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (0...𝑛) ∈ Fin) |
9 | | cnring 19587 |
. . . . . . . . . 10
⊢
ℂfld ∈ Ring |
10 | | ringcmn 18404 |
. . . . . . . . . 10
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
11 | 9, 10 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → ℂfld ∈
CMnd) |
12 | 4 | subrgss 18604 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 ⊆ ℂ) |
13 | 12 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ⊆ ℂ) |
14 | | elmapi 7765 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0) → 𝑎:ℕ0⟶(𝑆 ∪ {0})) |
15 | 14 | ad2antll 761 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → 𝑎:ℕ0⟶(𝑆 ∪ {0})) |
16 | | subrgsubg 18609 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 ∈
(SubGrp‘ℂfld)) |
17 | | cnfld0 19589 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 =
(0g‘ℂfld) |
18 | 17 | subg0cl 17425 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 ∈
(SubGrp‘ℂfld) → 0 ∈ 𝑆) |
19 | 16, 18 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 0 ∈ 𝑆) |
20 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → 0 ∈ 𝑆) |
21 | 20 | snssd 4281 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → {0} ⊆ 𝑆) |
22 | | ssequn2 3748 |
. . . . . . . . . . . . . . . 16
⊢ ({0}
⊆ 𝑆 ↔ (𝑆 ∪ {0}) = 𝑆) |
23 | 21, 22 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝑆 ∪ {0}) = 𝑆) |
24 | 23 | feq3d 5945 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝑎:ℕ0⟶(𝑆 ∪ {0}) ↔ 𝑎:ℕ0⟶𝑆)) |
25 | 15, 24 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → 𝑎:ℕ0⟶𝑆) |
26 | | elfznn0 12302 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...𝑛) → 𝑘 ∈ ℕ0) |
27 | | ffvelrn 6265 |
. . . . . . . . . . . . 13
⊢ ((𝑎:ℕ0⟶𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑎‘𝑘) ∈ 𝑆) |
28 | 25, 26, 27 | syl2an 493 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) ∈ 𝑆) |
29 | 13, 28 | sseldd 3569 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) ∈ ℂ) |
30 | 29 | adantrl 748 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑎‘𝑘) ∈ ℂ) |
31 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑧 ∈ ℂ) |
32 | 26 | ad2antll 761 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑘 ∈ ℕ0) |
33 | | expcl 12740 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑧↑𝑘) ∈
ℂ) |
34 | 31, 32, 33 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑧↑𝑘) ∈ ℂ) |
35 | 30, 34 | mulcld 9939 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → ((𝑎‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
36 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) = (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) |
37 | 6 | mptex 6390 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ V |
38 | 37 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ V) |
39 | | fvex 6113 |
. . . . . . . . . . 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 8169 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) finSupp
(0g‘(ℂfld ↑s
ℂ))) |
42 | 3, 4, 5, 7, 8, 11,
35, 41 | pwsgsum 18201 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → ((ℂfld ↑s
ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦
(ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))))) |
43 | | fzfid 12634 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑧 ∈ ℂ) → (0...𝑛) ∈ Fin) |
44 | 35 | anassrs 678 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑛)) → ((𝑎‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
45 | 43, 44 | gsumfsum 19632 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑧 ∈ ℂ) →
(ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) |
46 | 45 | mpteq2dva 4672 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝑧 ∈ ℂ ↦
(ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
47 | 42, 46 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → ((ℂfld ↑s
ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
48 | 3 | pwsring 18438 |
. . . . . . . . . 10
⊢
((ℂfld ∈ Ring ∧ ℂ ∈ V) →
(ℂfld ↑s ℂ) ∈
Ring) |
49 | 9, 6, 48 | mp2an 704 |
. . . . . . . . 9
⊢
(ℂfld ↑s ℂ) ∈
Ring |
50 | | ringcmn 18404 |
. . . . . . . . 9
⊢
((ℂfld ↑s ℂ) ∈ Ring
→ (ℂfld ↑s ℂ) ∈
CMnd) |
51 | 49, 50 | mp1i 13 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (ℂfld ↑s
ℂ) ∈ CMnd) |
52 | | cncrng 19586 |
. . . . . . . . . . 11
⊢
ℂfld ∈ CRing |
53 | | plypf1.e |
. . . . . . . . . . . 12
⊢ 𝐸 =
(eval1‘ℂfld) |
54 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Poly1‘ℂfld) =
(Poly1‘ℂfld) |
55 | 53, 54, 3, 4 | evl1rhm 19517 |
. . . . . . . . . . 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 19424 |
. . . . . . . . . . 11
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝐴 ∈
(SubRing‘(Poly1‘ℂfld))) |
61 | 60 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → 𝐴 ∈
(SubRing‘(Poly1‘ℂfld))) |
62 | | rhmima 18634 |
. . . . . . . . . 10
⊢ ((𝐸 ∈
((Poly1‘ℂfld) RingHom (ℂfld
↑s ℂ)) ∧ 𝐴 ∈
(SubRing‘(Poly1‘ℂfld))) → (𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s
ℂ))) |
63 | 56, 61, 62 | sylancr 694 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s
ℂ))) |
64 | | subrgsubg 18609 |
. . . . . . . . 9
⊢ ((𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s ℂ))
→ (𝐸 “ 𝐴) ∈
(SubGrp‘(ℂfld ↑s
ℂ))) |
65 | | subgsubm 17439 |
. . . . . . . . 9
⊢ ((𝐸 “ 𝐴) ∈
(SubGrp‘(ℂfld ↑s ℂ)) →
(𝐸 “ 𝐴) ∈
(SubMnd‘(ℂfld ↑s
ℂ))) |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝐸 “ 𝐴) ∈
(SubMnd‘(ℂfld ↑s
ℂ))) |
67 | | eqid 2610 |
. . . . . . . . . . . 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 6007 |
. . . . . . . . . . . . . 14
⊢ ((𝑎‘𝑘) ∈ ℂ → (ℂ ×
{(𝑎‘𝑘)}):ℂ⟶ℂ) |
71 | 29, 70 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ) |
72 | 3, 4, 67 | pwselbasb 15971 |
. . . . . . . . . . . . . 14
⊢
((ℂfld ∈ Ring ∧ ℂ ∈ V) →
((ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld
↑s ℂ)) ↔ (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)) |
73 | 9, 6, 72 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ ((ℂ
× {(𝑎‘𝑘)}) ∈
(Base‘(ℂfld ↑s ℂ)) ↔
(ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ) |
74 | 71, 73 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld
↑s ℂ))) |
75 | 34 | anass1rs 845 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑧↑𝑘) ∈ ℂ) |
76 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) |
77 | 75, 76 | fmptd 6292 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ) |
78 | 3, 4, 67 | pwselbasb 15971 |
. . . . . . . . . . . . . 14
⊢
((ℂfld ∈ Ring ∧ ℂ ∈ V) →
((𝑧 ∈ ℂ ↦
(𝑧↑𝑘)) ∈ (Base‘(ℂfld
↑s ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ)) |
79 | 9, 6, 78 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld
↑s ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ) |
80 | 77, 79 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld
↑s ℂ))) |
81 | | cnfldmul 19573 |
. . . . . . . . . . . 12
⊢ ·
= (.r‘ℂfld) |
82 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(.r‘(ℂfld ↑s
ℂ)) = (.r‘(ℂfld
↑s ℂ)) |
83 | 3, 67, 68, 69, 74, 80, 81, 82 | pwsmulrval 15974 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld
↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = ((ℂ × {(𝑎‘𝑘)}) ∘𝑓 ·
(𝑧 ∈ ℂ ↦
(𝑧↑𝑘)))) |
84 | 29 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑎‘𝑘) ∈ ℂ) |
85 | | fconstmpt 5085 |
. . . . . . . . . . . . 13
⊢ (ℂ
× {(𝑎‘𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎‘𝑘)) |
86 | 85 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎‘𝑘))) |
87 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) |
88 | 69, 84, 75, 86, 87 | offval2 6812 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)}) ∘𝑓 ·
(𝑧 ∈ ℂ ↦
(𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) |
89 | 83, 88 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld
↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) |
90 | 63 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s
ℂ))) |
91 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(algSc‘(Poly1‘ℂfld)) =
(algSc‘(Poly1‘ℂfld)) |
92 | 53, 54, 4, 91 | evl1sca 19519 |
. . . . . . . . . . . . 13
⊢
((ℂfld ∈ CRing ∧ (𝑎‘𝑘) ∈ ℂ) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) =
(ℂ × {(𝑎‘𝑘)})) |
93 | 52, 29, 92 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) =
(ℂ × {(𝑎‘𝑘)})) |
94 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘(Poly1‘ℂfld)) =
(Base‘(Poly1‘ℂfld)) |
95 | 94, 67 | rhmf 18549 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 ∈
((Poly1‘ℂfld) RingHom (ℂfld
↑s ℂ)) → 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld
↑s ℂ))) |
96 | 56, 95 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld
↑s ℂ)) |
97 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢ (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld
↑s ℂ)) → 𝐸 Fn
(Base‘(Poly1‘ℂfld))) |
98 | 96, 97 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐸 Fn
(Base‘(Poly1‘ℂfld))) |
99 | 94 | subrgss 18604 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈
(SubRing‘(Poly1‘ℂfld)) → 𝐴 ⊆
(Base‘(Poly1‘ℂfld))) |
100 | 60, 99 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝐴 ⊆
(Base‘(Poly1‘ℂfld))) |
101 | 100 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ⊆
(Base‘(Poly1‘ℂfld))) |
102 | | simpll 786 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ∈
(SubRing‘ℂfld)) |
103 | 54, 91, 57, 58, 102, 59, 4, 29 | subrg1asclcl 19451 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) →
(((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴 ↔ (𝑎‘𝑘) ∈ 𝑆)) |
104 | 28, 103 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) →
((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴) |
105 | | fnfvima 6400 |
. . . . . . . . . . . . 13
⊢ ((𝐸 Fn
(Base‘(Poly1‘ℂfld)) ∧ 𝐴 ⊆
(Base‘(Poly1‘ℂfld)) ∧
((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)))
∈ (𝐸 “ 𝐴)) |
106 | 98, 101, 104, 105 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)))
∈ (𝐸 “ 𝐴)) |
107 | 93, 106 | eqeltrrd 2689 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) ∈ (𝐸 “ 𝐴)) |
108 | 67 | subrgss 18604 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s ℂ))
→ (𝐸 “ 𝐴) ⊆
(Base‘(ℂfld ↑s
ℂ))) |
109 | 90, 108 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸 “ 𝐴) ⊆ (Base‘(ℂfld
↑s ℂ))) |
110 | 60 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈
(SubRing‘(Poly1‘ℂfld))) |
111 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(mulGrp‘(Poly1‘ℂfld)) =
(mulGrp‘(Poly1‘ℂfld)) |
112 | 111 | subrgsubm 18616 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈
(SubRing‘(Poly1‘ℂfld)) → 𝐴 ∈
(SubMnd‘(mulGrp‘(Poly1‘ℂfld)))) |
113 | 110, 112 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈
(SubMnd‘(mulGrp‘(Poly1‘ℂfld)))) |
114 | 26 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑘 ∈ ℕ0) |
115 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(var1‘ℂfld) =
(var1‘ℂfld) |
116 | 115, 102,
57, 58, 59 | subrgvr1cl 19453 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) →
(var1‘ℂfld) ∈ 𝐴) |
117 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(.g‘(mulGrp‘(Poly1‘ℂfld)))
=
(.g‘(mulGrp‘(Poly1‘ℂfld))) |
118 | 117 | submmulgcl 17408 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
(SubMnd‘(mulGrp‘(Poly1‘ℂfld)))
∧ 𝑘 ∈
ℕ0 ∧ (var1‘ℂfld) ∈
𝐴) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ 𝐴) |
119 | 113, 114,
116, 118 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ 𝐴) |
120 | | fnfvima 6400 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸 Fn
(Base‘(Poly1‘ℂfld)) ∧ 𝐴 ⊆
(Base‘(Poly1‘ℂfld)) ∧ (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ 𝐴) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
∈ (𝐸 “ 𝐴)) |
121 | 98, 101, 119, 120 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
∈ (𝐸 “ 𝐴)) |
122 | 109, 121 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
∈ (Base‘(ℂfld ↑s ℂ))) |
123 | 3, 4, 67, 68, 69, 122 | pwselbas 15972 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))):ℂ⟶ℂ) |
124 | 123 | feqmptd 6159 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
= (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧))) |
125 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ℂfld
∈ CRing) |
126 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ) |
127 | 53, 115, 4, 54, 94, 125, 126 | evl1vard 19522 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) →
((var1‘ℂfld) ∈
(Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧)) |
128 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(.g‘(mulGrp‘ℂfld)) =
(.g‘(mulGrp‘ℂfld)) |
129 | 114 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0) |
130 | 53, 54, 4, 94, 125, 126, 127, 117, 128, 129 | evl1expd 19530 |
. . . . . . . . . . . . . . . 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))𝑧))) |
131 | 130 | simprd 478 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧)) |
132 | | cnfldexp 19598 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘)) |
133 | 126, 129,
132 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘)) |
134 | 131, 133 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘)) |
135 | 134 | mpteq2dva 4672 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) |
136 | 124, 135 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
= (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) |
137 | 136, 121 | eqeltrrd 2689 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (𝐸 “ 𝐴)) |
138 | 82 | subrgmcl 18615 |
. . . . . . . . . . 11
⊢ (((𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s ℂ)) ∧
(ℂ × {(𝑎‘𝑘)}) ∈ (𝐸 “ 𝐴) ∧ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (𝐸 “ 𝐴)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld
↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)) |
139 | 90, 107, 137, 138 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld
↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)) |
140 | 89, 139 | eqeltrrd 2689 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)) |
141 | 140, 36 | fmptd 6292 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))):(0...𝑛)⟶(𝐸 “ 𝐴)) |
142 | 36, 8, 140, 40 | fsuppmptdm 8169 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) finSupp
(0g‘(ℂfld ↑s
ℂ))) |
143 | 5, 51, 8, 66, 141, 142 | gsumsubmcl 18142 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → ((ℂfld ↑s
ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) ∈ (𝐸 “ 𝐴)) |
144 | 47, 143 | eqeltrrd 2689 |
. . . . . 6
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)) |
145 | | eleq1 2676 |
. . . . . 6
⊢ (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → (𝑓 ∈ (𝐸 “ 𝐴) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))) |
146 | 144, 145 | syl5ibrcom 236 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → 𝑓 ∈ (𝐸 “ 𝐴))) |
147 | 146 | rexlimdvva 3020 |
. . . 4
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0)𝑓 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → 𝑓 ∈ (𝐸 “ 𝐴))) |
148 | 2, 147 | syl5 33 |
. . 3
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) → 𝑓 ∈ (𝐸 “ 𝐴))) |
149 | | ffun 5961 |
. . . . . 6
⊢ (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld
↑s ℂ)) → Fun 𝐸) |
150 | 96, 149 | ax-mp 5 |
. . . . 5
⊢ Fun 𝐸 |
151 | | fvelima 6158 |
. . . . 5
⊢ ((Fun
𝐸 ∧ 𝑓 ∈ (𝐸 “ 𝐴)) → ∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓) |
152 | 150, 151 | mpan 702 |
. . . 4
⊢ (𝑓 ∈ (𝐸 “ 𝐴) → ∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓) |
153 | 100 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈
(Base‘(Poly1‘ℂfld))) |
154 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (
·𝑠
‘(Poly1‘ℂfld)) = (
·𝑠
‘(Poly1‘ℂfld)) |
155 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(coe1‘𝑎) = (coe1‘𝑎) |
156 | 54, 115, 94, 154, 111, 117, 155 | ply1coe 19487 |
. . . . . . . . . . 11
⊢
((ℂfld ∈ Ring ∧ 𝑎 ∈
(Base‘(Poly1‘ℂfld))) → 𝑎 =
((Poly1‘ℂfld) Σg
(𝑘 ∈
ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))) |
157 | 9, 153, 156 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑎 =
((Poly1‘ℂfld) Σg
(𝑘 ∈
ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))) |
158 | 157 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = (𝐸‘((Poly1‘ℂfld)
Σg (𝑘 ∈
ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))) |
159 | | eqid 2610 |
. . . . . . . . . 10
⊢
(0g‘(Poly1‘ℂfld)) =
(0g‘(Poly1‘ℂfld)) |
160 | 54 | ply1ring 19439 |
. . . . . . . . . . . 12
⊢
(ℂfld ∈ Ring →
(Poly1‘ℂfld) ∈ Ring) |
161 | 9, 160 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(Poly1‘ℂfld) ∈
Ring |
162 | | ringcmn 18404 |
. . . . . . . . . . 11
⊢
((Poly1‘ℂfld) ∈ Ring →
(Poly1‘ℂfld) ∈ CMnd) |
163 | 161, 162 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) →
(Poly1‘ℂfld) ∈ CMnd) |
164 | | ringmnd 18379 |
. . . . . . . . . . 11
⊢
((ℂfld ↑s ℂ) ∈ Ring
→ (ℂfld ↑s ℂ) ∈
Mnd) |
165 | 49, 164 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (ℂfld
↑s ℂ) ∈ Mnd) |
166 | | nn0ex 11175 |
. . . . . . . . . . 11
⊢
ℕ0 ∈ V |
167 | 166 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℕ0 ∈
V) |
168 | | rhmghm 18548 |
. . . . . . . . . . . 12
⊢ (𝐸 ∈
((Poly1‘ℂfld) RingHom (ℂfld
↑s ℂ)) → 𝐸 ∈
((Poly1‘ℂfld) GrpHom (ℂfld
↑s ℂ))) |
169 | 56, 168 | ax-mp 5 |
. . . . . . . . . . 11
⊢ 𝐸 ∈
((Poly1‘ℂfld) GrpHom (ℂfld
↑s ℂ)) |
170 | | ghmmhm 17493 |
. . . . . . . . . . 11
⊢ (𝐸 ∈
((Poly1‘ℂfld) GrpHom (ℂfld
↑s ℂ)) → 𝐸 ∈
((Poly1‘ℂfld) MndHom (ℂfld
↑s ℂ))) |
171 | 169, 170 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝐸 ∈
((Poly1‘ℂfld) MndHom (ℂfld
↑s ℂ))) |
172 | 54 | ply1lmod 19443 |
. . . . . . . . . . . . 13
⊢
(ℂfld ∈ Ring →
(Poly1‘ℂfld) ∈ LMod) |
173 | 9, 172 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
(Poly1‘ℂfld) ∈ LMod) |
174 | 12 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑆 ⊆
ℂ) |
175 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝑅) =
(Base‘𝑅) |
176 | 155, 59, 58, 175 | coe1f 19402 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ 𝐴 → (coe1‘𝑎):ℕ0⟶(Base‘𝑅)) |
177 | 57 | subrgbas 18612 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 = (Base‘𝑅)) |
178 | 177 | feq3d 5945 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∈
(SubRing‘ℂfld) → ((coe1‘𝑎):ℕ0⟶𝑆 ↔
(coe1‘𝑎):ℕ0⟶(Base‘𝑅))) |
179 | 176, 178 | syl5ibr 235 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (𝑎 ∈ 𝐴 → (coe1‘𝑎):ℕ0⟶𝑆)) |
180 | 179 | imp 444 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎):ℕ0⟶𝑆) |
181 | 180 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑎)‘𝑘) ∈ 𝑆) |
182 | 174, 181 | sseldd 3569 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑎)‘𝑘) ∈ ℂ) |
183 | 111 | ringmgp 18376 |
. . . . . . . . . . . . . 14
⊢
((Poly1‘ℂfld) ∈ Ring →
(mulGrp‘(Poly1‘ℂfld)) ∈
Mnd) |
184 | 161, 183 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
(mulGrp‘(Poly1‘ℂfld)) ∈
Mnd) |
185 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
186 | 115, 54, 94 | vr1cl 19408 |
. . . . . . . . . . . . . 14
⊢
(ℂfld ∈ Ring →
(var1‘ℂfld) ∈
(Base‘(Poly1‘ℂfld))) |
187 | 9, 186 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
(var1‘ℂfld) ∈
(Base‘(Poly1‘ℂfld))) |
188 | 111, 94 | mgpbas 18318 |
. . . . . . . . . . . . . 14
⊢
(Base‘(Poly1‘ℂfld)) =
(Base‘(mulGrp‘(Poly1‘ℂfld))) |
189 | 188, 117 | mulgnn0cl 17381 |
. . . . . . . . . . . . 13
⊢
(((mulGrp‘(Poly1‘ℂfld)) ∈
Mnd ∧ 𝑘 ∈
ℕ0 ∧ (var1‘ℂfld) ∈
(Base‘(Poly1‘ℂfld))) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ (Base‘(Poly1‘ℂfld))) |
190 | 184, 185,
187, 189 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ (Base‘(Poly1‘ℂfld))) |
191 | 54 | ply1sca 19444 |
. . . . . . . . . . . . . 14
⊢
(ℂfld ∈ Ring → ℂfld =
(Scalar‘(Poly1‘ℂfld))) |
192 | 9, 191 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
ℂfld =
(Scalar‘(Poly1‘ℂfld)) |
193 | 94, 192, 154, 4 | lmodvscl 18703 |
. . . . . . . . . . . 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))) |
194 | 173, 182,
190, 193 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
∈ (Base‘(Poly1‘ℂfld))) |
195 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
= (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) |
196 | 194, 195 | fmptd 6292 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℕ0⟶(Base‘(Poly1‘ℂfld))) |
197 | 166 | mptex 6390 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
∈ V |
198 | | funmpt 5840 |
. . . . . . . . . . . . 13
⊢ Fun
(𝑘 ∈
ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) |
199 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢
(0g‘(Poly1‘ℂfld))
∈ V |
200 | 197, 198,
199 | 3pm3.2i 1232 |
. . . . . . . . . . . 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) |
201 | 200 | 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)) |
202 | 155, 94, 54, 17 | coe1sfi 19404 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈
(Base‘(Poly1‘ℂfld)) →
(coe1‘𝑎)
finSupp 0) |
203 | 153, 202 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎) finSupp 0) |
204 | 203 | fsuppimpd 8165 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((coe1‘𝑎) supp 0) ∈
Fin) |
205 | 180 | feqmptd 6159 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎) = (𝑘 ∈ ℕ0 ↦
((coe1‘𝑎)‘𝑘))) |
206 | 205 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((coe1‘𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦
((coe1‘𝑎)‘𝑘)) supp 0)) |
207 | | eqimss2 3621 |
. . . . . . . . . . . . 13
⊢
(((coe1‘𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦
((coe1‘𝑎)‘𝑘)) supp 0) → ((𝑘 ∈ ℕ0 ↦
((coe1‘𝑎)‘𝑘)) supp 0) ⊆
((coe1‘𝑎)
supp 0)) |
208 | 206, 207 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦
((coe1‘𝑎)‘𝑘)) supp 0) ⊆
((coe1‘𝑎)
supp 0)) |
209 | 9, 172 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) →
(Poly1‘ℂfld) ∈ LMod) |
210 | 94, 192, 154, 17, 159 | lmod0vs 18719 |
. . . . . . . . . . . . 13
⊢
(((Poly1‘ℂfld) ∈ LMod ∧ 𝑥 ∈
(Base‘(Poly1‘ℂfld))) → (0(
·𝑠
‘(Poly1‘ℂfld))𝑥) =
(0g‘(Poly1‘ℂfld))) |
211 | 209, 210 | sylan 487 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈
(Base‘(Poly1‘ℂfld))) → (0(
·𝑠
‘(Poly1‘ℂfld))𝑥) =
(0g‘(Poly1‘ℂfld))) |
212 | | c0ex 9913 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
213 | 212 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 0 ∈ V) |
214 | 208, 211,
181, 190, 213 | suppssov1 7214 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
supp (0g‘(Poly1‘ℂfld))) ⊆ ((coe1‘𝑎)
supp 0)) |
215 | | suppssfifsupp 8173 |
. . . . . . . . . . 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))) |
216 | 201, 204,
214, 215 | syl12anc 1316 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
finSupp (0g‘(Poly1‘ℂfld))) |
217 | 94, 159, 163, 165, 167, 171, 196, 216 | gsummhm 18161 |
. . . . . . . . 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))))))) |
218 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
= (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) |
219 | 96 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld
↑s ℂ))) |
220 | 219 | feqmptd 6159 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝐸 = (𝑥 ∈
(Base‘(Poly1‘ℂfld)) ↦ (𝐸‘𝑥))) |
221 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 =
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
→ (𝐸‘𝑥) = (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) |
222 | 194, 218,
220, 221 | fmptco 6303 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))
= (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))) |
223 | 9 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
ℂfld ∈ Ring) |
224 | 6 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → ℂ
∈ V) |
225 | 96 | ffvelrni 6266 |
. . . . . . . . . . . . . . . 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 ℂ))) |
226 | 194, 225 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
∈ (Base‘(ℂfld ↑s ℂ))) |
227 | 3, 4, 67, 223, 224, 226 | pwselbas 15972 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℂ⟶ℂ) |
228 | 227 | feqmptd 6159 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
= (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧))) |
229 | 52 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) →
ℂfld ∈ CRing) |
230 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈
ℂ) |
231 | 53, 115, 4, 54, 94, 229, 230 | evl1vard 19522 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) →
((var1‘ℂfld) ∈
(Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧)) |
232 | 185 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈
ℕ0) |
233 | 53, 54, 4, 94, 229, 230, 231, 117, 128, 232 | evl1expd 19530 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧))) |
234 | 230, 232,
132 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘)) |
235 | 234 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧) ↔ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘))) |
236 | 235 | anbi2d 736 |
. . . . . . . . . . . . . . . . 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)))‘𝑧) = (𝑧↑𝑘)))) |
237 | 233, 236 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘))) |
238 | 182 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) →
((coe1‘𝑎)‘𝑘) ∈ ℂ) |
239 | 53, 54, 4, 94, 229, 230, 237, 238, 154, 81 | evl1vsd 19529 |
. . . . . . . . . . . . . . 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‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
240 | 239 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧) = (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) |
241 | 240 | mpteq2dva 4672 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧)) = (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
242 | 228, 241 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
= (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
243 | 242 | mpteq2dva 4672 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))
= (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) |
244 | 222, 243 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))
= (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) |
245 | 244 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((ℂfld
↑s ℂ) Σg (𝐸 ∘ (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
= ((ℂfld ↑s ℂ) Σg (𝑘 ∈
ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))) |
246 | 158, 217,
245 | 3eqtr2d 2650 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = ((ℂfld
↑s ℂ) Σg (𝑘 ∈ ℕ0
↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))) |
247 | 6 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℂ ∈ V) |
248 | 9, 10 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℂfld ∈
CMnd) |
249 | 182 | adantlr 747 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑎)‘𝑘) ∈ ℂ) |
250 | 33 | adantll 746 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ) |
251 | 249, 250 | mulcld 9939 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) →
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
252 | 251 | anasss 677 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)) →
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
253 | 166 | mptex 6390 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V |
254 | | funmpt 5840 |
. . . . . . . . . . . 12
⊢ Fun
(𝑘 ∈
ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
255 | 253, 254,
39 | 3pm3.2i 1232 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ0
↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∧
(0g‘(ℂfld ↑s ℂ))
∈ V) |
256 | 255 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∧
(0g‘(ℂfld ↑s ℂ))
∈ V)) |
257 | | fzfid 12634 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ∈ Fin) |
258 | | eldifn 3695 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (ℕ0
∖ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) → ¬ 𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
259 | 258 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → ¬ 𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
260 | 153 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → 𝑎 ∈
(Base‘(Poly1‘ℂfld))) |
261 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ (ℕ0
∖ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) → 𝑘 ∈ ℕ0) |
262 | 261 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℕ0) |
263 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (
deg1 ‘ℂfld) = ( deg1
‘ℂfld) |
264 | 263, 54, 94, 17, 155 | deg1ge 23662 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈
(Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0
∧ ((coe1‘𝑎)‘𝑘) ≠ 0) → 𝑘 ≤ (( deg1
‘ℂfld)‘𝑎)) |
265 | 264 | 3expia 1259 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈
(Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0)
→ (((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ (( deg1
‘ℂfld)‘𝑎))) |
266 | 260, 262,
265 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ (( deg1
‘ℂfld)‘𝑎))) |
267 | | 0xr 9965 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℝ* |
268 | 263, 54, 94 | deg1xrcl 23646 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈
(Base‘(Poly1‘ℂfld)) → ((
deg1 ‘ℂfld)‘𝑎) ∈
ℝ*) |
269 | 153, 268 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (( deg1
‘ℂfld)‘𝑎) ∈
ℝ*) |
270 | 269 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (( deg1
‘ℂfld)‘𝑎) ∈
ℝ*) |
271 | | xrmax2 11881 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((0
∈ ℝ* ∧ (( deg1
‘ℂfld)‘𝑎) ∈ ℝ*) → ((
deg1 ‘ℂfld)‘𝑎) ≤ if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) |
272 | 267, 270,
271 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (( deg1
‘ℂfld)‘𝑎) ≤ if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) |
273 | 262 | nn0red 11229 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ) |
274 | 273 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ*) |
275 | | ifcl 4080 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((
deg1 ‘ℂfld)‘𝑎) ∈ ℝ* ∧ 0 ∈
ℝ*) → if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℝ*) |
276 | 270, 267,
275 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℝ*) |
277 | | xrletr 11865 |
. . . . . . . . . . . . . . . . . . . . . . 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))) |
278 | 274, 270,
276, 277 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . 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))) |
279 | 272, 278 | mpan2d 706 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (𝑘 ≤ (( deg1
‘ℂfld)‘𝑎) → 𝑘 ≤ if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
280 | 266, 279 | syld 46 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
281 | 280, 262 | jctild 564 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) ≠ 0 → (𝑘 ∈ ℕ0 ∧ 𝑘 ≤ if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) |
282 | 263, 54, 94 | deg1cl 23647 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 ∈
(Base‘(Poly1‘ℂfld)) → ((
deg1 ‘ℂfld)‘𝑎) ∈ (ℕ0 ∪
{-∞})) |
283 | 153, 282 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (( deg1
‘ℂfld)‘𝑎) ∈ (ℕ0 ∪
{-∞})) |
284 | | elun 3715 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ (ℕ0 ∪
{-∞}) ↔ ((( deg1
‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞})) |
285 | 283, 284 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((( deg1
‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞})) |
286 | | nn0ge0 11195 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → 0 ≤ ((
deg1 ‘ℂfld)‘𝑎)) |
287 | 286 | iftrued 4044 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤
(( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) = (( deg1
‘ℂfld)‘𝑎)) |
288 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → ((
deg1 ‘ℂfld)‘𝑎) ∈
ℕ0) |
289 | 287, 288 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤
(( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℕ0) |
290 | | mnflt0 11835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ -∞
< 0 |
291 | | mnfxr 9975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ -∞
∈ ℝ* |
292 | | xrltnle 9984 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((-∞ ∈ ℝ* ∧ 0 ∈
ℝ*) → (-∞ < 0 ↔ ¬ 0 ≤
-∞)) |
293 | 291, 267,
292 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (-∞
< 0 ↔ ¬ 0 ≤ -∞) |
294 | 290, 293 | mpbi 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ¬ 0
≤ -∞ |
295 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → (( deg1
‘ℂfld)‘𝑎) = -∞) |
296 | 295 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → (0 ≤ ((
deg1 ‘ℂfld)‘𝑎) ↔ 0 ≤ -∞)) |
297 | 294, 296 | mtbiri 316 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → ¬ 0 ≤ ((
deg1 ‘ℂfld)‘𝑎)) |
298 | 297 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) = 0) |
299 | | 0nn0 11184 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
ℕ0 |
300 | 298, 299 | syl6eqel 2696 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℕ0) |
301 | 289, 300 | jaoi 393 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((
deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞}) → if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℕ0) |
302 | 285, 301 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℕ0) |
303 | 302 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℕ0) |
304 | | fznn0 12301 |
. . . . . . . . . . . . . . . . . . . 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)))) |
305 | 303, 304 | 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)))) |
306 | 281, 305 | sylibrd 248 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) |
307 | 306 | necon1bd 2800 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (¬ 𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) → ((coe1‘𝑎)‘𝑘) = 0)) |
308 | 259, 307 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → ((coe1‘𝑎)‘𝑘) = 0) |
309 | 308 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘))) |
310 | 261, 250 | sylan2 490 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (𝑧↑𝑘) ∈ ℂ) |
311 | 310 | mul02d 10113 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (0 · (𝑧↑𝑘)) = 0) |
312 | 309, 311 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = 0) |
313 | 312 | an32s 842 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) ∧ 𝑧 ∈ ℂ) →
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = 0) |
314 | 313 | mpteq2dva 4672 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ 0)) |
315 | | fconstmpt 5085 |
. . . . . . . . . . . . 13
⊢ (ℂ
× {0}) = (𝑧 ∈
ℂ ↦ 0) |
316 | | ringmnd 18379 |
. . . . . . . . . . . . . . 15
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
317 | 9, 316 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
ℂfld ∈ Mnd |
318 | 3, 17 | pws0g 17149 |
. . . . . . . . . . . . . 14
⊢
((ℂfld ∈ Mnd ∧ ℂ ∈ V) →
(ℂ × {0}) = (0g‘(ℂfld
↑s ℂ))) |
319 | 317, 6, 318 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (ℂ
× {0}) = (0g‘(ℂfld
↑s ℂ)) |
320 | 315, 319 | eqtr3i 2634 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℂ ↦ 0) =
(0g‘(ℂfld ↑s
ℂ)) |
321 | 314, 320 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) =
(0g‘(ℂfld ↑s
ℂ))) |
322 | 321, 167 | suppss2 7216 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) supp
(0g‘(ℂfld ↑s
ℂ))) ⊆ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
323 | | suppssfifsupp 8173 |
. . . . . . . . . 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
ℂ))) |
324 | 256, 257,
322, 323 | syl12anc 1316 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) finSupp
(0g‘(ℂfld ↑s
ℂ))) |
325 | 3, 4, 5, 247, 167, 248, 252, 324 | pwsgsum 18201 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((ℂfld
↑s ℂ) Σg (𝑘 ∈ ℕ0
↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦
(ℂfld Σg (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))) |
326 | | fz0ssnn0 12304 |
. . . . . . . . . . . 12
⊢ (0...if(0
≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ⊆
ℕ0 |
327 | | resmpt 5369 |
. . . . . . . . . . . 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‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
328 | 326, 327 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) = (𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) |
329 | 328 | oveq2i 6560 |
. . . . . . . . . 10
⊢
(ℂfld Σg ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) = (ℂfld
Σg (𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
330 | 9, 10 | mp1i 13 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ℂfld
∈ CMnd) |
331 | 166 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ℕ0
∈ V) |
332 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) = (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) |
333 | 251, 332 | fmptd 6292 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))):ℕ0⟶ℂ) |
334 | 312, 331 | suppss2 7216 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) supp 0) ⊆ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
335 | 166 | mptex 6390 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V |
336 | | funmpt 5840 |
. . . . . . . . . . . . . 14
⊢ Fun
(𝑘 ∈
ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) |
337 | 335, 336,
212 | 3pm3.2i 1232 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∧ 0 ∈ V) |
338 | 337 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∧ 0 ∈ V)) |
339 | | fzfid 12634 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ∈ Fin) |
340 | | suppssfifsupp 8173 |
. . . . . . . . . . . 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) |
341 | 338, 339,
334, 340 | syl12anc 1316 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) finSupp 0) |
342 | 4, 17, 330, 331, 333, 334, 341 | gsumres 18137 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) →
(ℂfld Σg ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) = (ℂfld
Σg (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) |
343 | | elfznn0 12302 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) → 𝑘 ∈ ℕ0) |
344 | 343, 251 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
345 | 339, 344 | gsumfsum 19632 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) →
(ℂfld Σg (𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) |
346 | 329, 342,
345 | 3eqtr3a 2668 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) →
(ℂfld Σg (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) |
347 | 346 | mpteq2dva 4672 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑧 ∈ ℂ ↦
(ℂfld Σg (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
348 | 246, 325,
347 | 3eqtrd 2648 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
349 | 12 | adantr 480 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑆 ⊆ ℂ) |
350 | | elplyr 23761 |
. . . . . . . 8
⊢ ((𝑆 ⊆ ℂ ∧ if(0 ≤
(( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈ ℕ0 ∧
(coe1‘𝑎):ℕ0⟶𝑆) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆)) |
351 | 349, 302,
180, 350 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆)) |
352 | 348, 351 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) ∈ (Poly‘𝑆)) |
353 | | eleq1 2676 |
. . . . . 6
⊢ ((𝐸‘𝑎) = 𝑓 → ((𝐸‘𝑎) ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (Poly‘𝑆))) |
354 | 352, 353 | syl5ibcom 234 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝐸‘𝑎) = 𝑓 → 𝑓 ∈ (Poly‘𝑆))) |
355 | 354 | rexlimdva 3013 |
. . . 4
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓 → 𝑓 ∈ (Poly‘𝑆))) |
356 | 152, 355 | syl5 33 |
. . 3
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (𝑓 ∈ (𝐸 “ 𝐴) → 𝑓 ∈ (Poly‘𝑆))) |
357 | 148, 356 | impbid 201 |
. 2
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (𝐸 “ 𝐴))) |
358 | 357 | eqrdv 2608 |
1
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (Poly‘𝑆) = (𝐸 “ 𝐴)) |