Step | Hyp | Ref
| Expression |
1 | | elply 25556 |
. . . . 5
⊢ (𝑓 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)𝑓 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
2 | 1 | simprbi 497 |
. . . 4
⊢ (𝑓 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)𝑓 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
3 | | eqid 2736 |
. . . . . . . . 9
⊢
(ℂfld ↑s ℂ) =
(ℂfld ↑s ℂ) |
4 | | cnfldbas 20800 |
. . . . . . . . 9
⊢ ℂ =
(Base‘ℂfld) |
5 | | eqid 2736 |
. . . . . . . . 9
⊢
(0g‘(ℂfld ↑s
ℂ)) = (0g‘(ℂfld
↑s ℂ)) |
6 | | cnex 11132 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
7 | 6 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → ℂ ∈ V) |
8 | | fzfid 13878 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → (0...𝑛) ∈ Fin) |
9 | | cnring 20819 |
. . . . . . . . . 10
⊢
ℂfld ∈ Ring |
10 | | ringcmn 20003 |
. . . . . . . . . 10
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
11 | 9, 10 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → ℂfld ∈
CMnd) |
12 | 4 | subrgss 20223 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 ⊆ ℂ) |
13 | 12 | ad2antrr 724 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ⊆ ℂ) |
14 | | elmapi 8787 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) → 𝑎:ℕ0⟶(𝑆 ∪ {0})) |
15 | 14 | ad2antll 727 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → 𝑎:ℕ0⟶(𝑆 ∪ {0})) |
16 | | subrgsubg 20228 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 ∈
(SubGrp‘ℂfld)) |
17 | | cnfld0 20821 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 =
(0g‘ℂfld) |
18 | 17 | subg0cl 18936 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 ∈
(SubGrp‘ℂfld) → 0 ∈ 𝑆) |
19 | 16, 18 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 0 ∈ 𝑆) |
20 | 19 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → 0 ∈ 𝑆) |
21 | 20 | snssd 4769 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → {0} ⊆ 𝑆) |
22 | | ssequn2 4143 |
. . . . . . . . . . . . . . . 16
⊢ ({0}
⊆ 𝑆 ↔ (𝑆 ∪ {0}) = 𝑆) |
23 | 21, 22 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → (𝑆 ∪ {0}) = 𝑆) |
24 | 23 | feq3d 6655 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → (𝑎:ℕ0⟶(𝑆 ∪ {0}) ↔ 𝑎:ℕ0⟶𝑆)) |
25 | 15, 24 | mpbid 231 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → 𝑎:ℕ0⟶𝑆) |
26 | | elfznn0 13534 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...𝑛) → 𝑘 ∈ ℕ0) |
27 | | ffvelcdm 7032 |
. . . . . . . . . . . . 13
⊢ ((𝑎:ℕ0⟶𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑎‘𝑘) ∈ 𝑆) |
28 | 25, 26, 27 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) ∈ 𝑆) |
29 | 13, 28 | sseldd 3945 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) ∈ ℂ) |
30 | 29 | adantrl 714 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑎‘𝑘) ∈ ℂ) |
31 | | simprl 769 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑧 ∈ ℂ) |
32 | 26 | ad2antll 727 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑘 ∈ ℕ0) |
33 | | expcl 13985 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑧↑𝑘) ∈
ℂ) |
34 | 31, 32, 33 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑧↑𝑘) ∈ ℂ) |
35 | 30, 34 | mulcld 11175 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → ((𝑎‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
36 | | eqid 2736 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) = (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) |
37 | 6 | mptex 7173 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ V |
38 | 37 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ V) |
39 | | fvex 6855 |
. . . . . . . . . . 11
⊢
(0g‘(ℂfld ↑s
ℂ)) ∈ V |
40 | 39 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → (0g‘(ℂfld
↑s ℂ)) ∈ V) |
41 | 36, 8, 38, 40 | fsuppmptdm 9316 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) finSupp
(0g‘(ℂfld ↑s
ℂ))) |
42 | 3, 4, 5, 7, 8, 11,
35, 41 | pwsgsum 19759 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → ((ℂfld ↑s
ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦
(ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))))) |
43 | | fzfid 13878 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑧 ∈ ℂ) → (0...𝑛) ∈ Fin) |
44 | 35 | anassrs 468 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑛)) → ((𝑎‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
45 | 43, 44 | gsumfsum 20864 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑧 ∈ ℂ) →
(ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) |
46 | 45 | mpteq2dva 5205 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → (𝑧 ∈ ℂ ↦
(ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
47 | 42, 46 | eqtrd 2776 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → ((ℂfld ↑s
ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
48 | 3 | pwsring 20039 |
. . . . . . . . . 10
⊢
((ℂfld ∈ Ring ∧ ℂ ∈ V) →
(ℂfld ↑s ℂ) ∈
Ring) |
49 | 9, 6, 48 | mp2an 690 |
. . . . . . . . 9
⊢
(ℂfld ↑s ℂ) ∈
Ring |
50 | | ringcmn 20003 |
. . . . . . . . 9
⊢
((ℂfld ↑s ℂ) ∈ Ring
→ (ℂfld ↑s ℂ) ∈
CMnd) |
51 | 49, 50 | mp1i 13 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → (ℂfld ↑s
ℂ) ∈ CMnd) |
52 | | cncrng 20818 |
. . . . . . . . . . 11
⊢
ℂfld ∈ CRing |
53 | | plypf1.e |
. . . . . . . . . . . 12
⊢ 𝐸 =
(eval1‘ℂfld) |
54 | | eqid 2736 |
. . . . . . . . . . . 12
⊢
(Poly1‘ℂfld) =
(Poly1‘ℂfld) |
55 | 53, 54, 3, 4 | evl1rhm 21698 |
. . . . . . . . . . 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 21604 |
. . . . . . . . . . 11
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝐴 ∈
(SubRing‘(Poly1‘ℂfld))) |
61 | 60 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → 𝐴 ∈
(SubRing‘(Poly1‘ℂfld))) |
62 | | rhmima 20253 |
. . . . . . . . . 10
⊢ ((𝐸 ∈
((Poly1‘ℂfld) RingHom (ℂfld
↑s ℂ)) ∧ 𝐴 ∈
(SubRing‘(Poly1‘ℂfld))) → (𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s
ℂ))) |
63 | 56, 61, 62 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → (𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s
ℂ))) |
64 | | subrgsubg 20228 |
. . . . . . . . 9
⊢ ((𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s ℂ))
→ (𝐸 “ 𝐴) ∈
(SubGrp‘(ℂfld ↑s
ℂ))) |
65 | | subgsubm 18950 |
. . . . . . . . 9
⊢ ((𝐸 “ 𝐴) ∈
(SubGrp‘(ℂfld ↑s ℂ)) →
(𝐸 “ 𝐴) ∈
(SubMnd‘(ℂfld ↑s
ℂ))) |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → (𝐸 “ 𝐴) ∈
(SubMnd‘(ℂfld ↑s
ℂ))) |
67 | | eqid 2736 |
. . . . . . . . . . . 12
⊢
(Base‘(ℂfld ↑s ℂ)) =
(Base‘(ℂfld ↑s
ℂ)) |
68 | 9 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ℂfld ∈
Ring) |
69 | 6 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ℂ ∈ V) |
70 | | fconst6g 6731 |
. . . . . . . . . . . . . 14
⊢ ((𝑎‘𝑘) ∈ ℂ → (ℂ ×
{(𝑎‘𝑘)}):ℂ⟶ℂ) |
71 | 29, 70 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ) |
72 | 3, 4, 67 | pwselbasb 17370 |
. . . . . . . . . . . . . 14
⊢
((ℂfld ∈ Ring ∧ ℂ ∈ V) →
((ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld
↑s ℂ)) ↔ (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)) |
73 | 9, 6, 72 | mp2an 690 |
. . . . . . . . . . . . 13
⊢ ((ℂ
× {(𝑎‘𝑘)}) ∈
(Base‘(ℂfld ↑s ℂ)) ↔
(ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ) |
74 | 71, 73 | sylibr 233 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld
↑s ℂ))) |
75 | 34 | anass1rs 653 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑧↑𝑘) ∈ ℂ) |
76 | 75 | fmpttd 7063 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ) |
77 | 3, 4, 67 | pwselbasb 17370 |
. . . . . . . . . . . . . 14
⊢
((ℂfld ∈ Ring ∧ ℂ ∈ V) →
((𝑧 ∈ ℂ ↦
(𝑧↑𝑘)) ∈ (Base‘(ℂfld
↑s ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ)) |
78 | 9, 6, 77 | mp2an 690 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld
↑s ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ) |
79 | 76, 78 | sylibr 233 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld
↑s ℂ))) |
80 | | cnfldmul 20802 |
. . . . . . . . . . . 12
⊢ ·
= (.r‘ℂfld) |
81 | | eqid 2736 |
. . . . . . . . . . . 12
⊢
(.r‘(ℂfld ↑s
ℂ)) = (.r‘(ℂfld
↑s ℂ)) |
82 | 3, 67, 68, 69, 74, 79, 80, 81 | pwsmulrval 17373 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld
↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = ((ℂ × {(𝑎‘𝑘)}) ∘f · (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)))) |
83 | 29 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑎‘𝑘) ∈ ℂ) |
84 | | fconstmpt 5694 |
. . . . . . . . . . . . 13
⊢ (ℂ
× {(𝑎‘𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎‘𝑘)) |
85 | 84 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎‘𝑘))) |
86 | | eqidd 2737 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) |
87 | 69, 83, 75, 85, 86 | offval2 7637 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)}) ∘f · (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) |
88 | 82, 87 | eqtrd 2776 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld
↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) |
89 | 63 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s
ℂ))) |
90 | | eqid 2736 |
. . . . . . . . . . . . . 14
⊢
(algSc‘(Poly1‘ℂfld)) =
(algSc‘(Poly1‘ℂfld)) |
91 | 53, 54, 4, 90 | evl1sca 21700 |
. . . . . . . . . . . . 13
⊢
((ℂfld ∈ CRing ∧ (𝑎‘𝑘) ∈ ℂ) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) =
(ℂ × {(𝑎‘𝑘)})) |
92 | 52, 29, 91 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) =
(ℂ × {(𝑎‘𝑘)})) |
93 | | eqid 2736 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘(Poly1‘ℂfld)) =
(Base‘(Poly1‘ℂfld)) |
94 | 93, 67 | rhmf 20158 |
. . . . . . . . . . . . . . 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 6668 |
. . . . . . . . . . . . . 14
⊢ (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld
↑s ℂ)) → 𝐸 Fn
(Base‘(Poly1‘ℂfld))) |
97 | 95, 96 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐸 Fn
(Base‘(Poly1‘ℂfld))) |
98 | 93 | subrgss 20223 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈
(SubRing‘(Poly1‘ℂfld)) → 𝐴 ⊆
(Base‘(Poly1‘ℂfld))) |
99 | 60, 98 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝐴 ⊆
(Base‘(Poly1‘ℂfld))) |
100 | 99 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ⊆
(Base‘(Poly1‘ℂfld))) |
101 | | simpll 765 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ∈
(SubRing‘ℂfld)) |
102 | 54, 90, 57, 58, 101, 59, 4, 29 | subrg1asclcl 21631 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) →
(((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴 ↔ (𝑎‘𝑘) ∈ 𝑆)) |
103 | 28, 102 | mpbird 256 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) →
((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴) |
104 | | fnfvima 7183 |
. . . . . . . . . . . . 13
⊢ ((𝐸 Fn
(Base‘(Poly1‘ℂfld)) ∧ 𝐴 ⊆
(Base‘(Poly1‘ℂfld)) ∧
((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)))
∈ (𝐸 “ 𝐴)) |
105 | 97, 100, 103, 104 | syl3anc 1371 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)))
∈ (𝐸 “ 𝐴)) |
106 | 92, 105 | eqeltrrd 2839 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) ∈ (𝐸 “ 𝐴)) |
107 | 67 | subrgss 20223 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s ℂ))
→ (𝐸 “ 𝐴) ⊆
(Base‘(ℂfld ↑s
ℂ))) |
108 | 89, 107 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸 “ 𝐴) ⊆ (Base‘(ℂfld
↑s ℂ))) |
109 | 60 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈
(SubRing‘(Poly1‘ℂfld))) |
110 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(mulGrp‘(Poly1‘ℂfld)) =
(mulGrp‘(Poly1‘ℂfld)) |
111 | 110 | subrgsubm 20235 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈
(SubRing‘(Poly1‘ℂfld)) → 𝐴 ∈
(SubMnd‘(mulGrp‘(Poly1‘ℂfld)))) |
112 | 109, 111 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈
(SubMnd‘(mulGrp‘(Poly1‘ℂfld)))) |
113 | 26 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑘 ∈ ℕ0) |
114 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . 19
⊢
(var1‘ℂfld) =
(var1‘ℂfld) |
115 | 114, 101,
57, 58, 59 | subrgvr1cl 21633 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) →
(var1‘ℂfld) ∈ 𝐴) |
116 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . 19
⊢
(.g‘(mulGrp‘(Poly1‘ℂfld)))
=
(.g‘(mulGrp‘(Poly1‘ℂfld))) |
117 | 116 | submmulgcl 18919 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
(SubMnd‘(mulGrp‘(Poly1‘ℂfld)))
∧ 𝑘 ∈
ℕ0 ∧ (var1‘ℂfld) ∈
𝐴) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ 𝐴) |
118 | 112, 113,
115, 117 | syl3anc 1371 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ 𝐴) |
119 | | fnfvima 7183 |
. . . . . . . . . . . . . . . . 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 1371 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
∈ (𝐸 “ 𝐴)) |
121 | 108, 120 | sseldd 3945 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
∈ (Base‘(ℂfld ↑s ℂ))) |
122 | 3, 4, 67, 68, 69, 121 | pwselbas 17371 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))):ℂ⟶ℂ) |
123 | 122 | feqmptd 6910 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
= (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧))) |
124 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ℂfld
∈ CRing) |
125 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ) |
126 | 53, 114, 4, 54, 93, 124, 125 | evl1vard 21703 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) →
((var1‘ℂfld) ∈
(Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧)) |
127 | | eqid 2736 |
. . . . . . . . . . . . . . . . 17
⊢
(.g‘(mulGrp‘ℂfld)) =
(.g‘(mulGrp‘ℂfld)) |
128 | 113 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0) |
129 | 53, 54, 4, 93, 124, 125, 126, 116, 127, 128 | evl1expd 21711 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧))) |
130 | 129 | simprd 496 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧)) |
131 | | cnfldexp 20830 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘)) |
132 | 125, 128,
131 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘)) |
133 | 130, 132 | eqtrd 2776 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘)) |
134 | 133 | mpteq2dva 5205 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) |
135 | 123, 134 | eqtrd 2776 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
= (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) |
136 | 135, 120 | eqeltrrd 2839 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (𝐸 “ 𝐴)) |
137 | 81 | subrgmcl 20234 |
. . . . . . . . . . 11
⊢ (((𝐸 “ 𝐴) ∈
(SubRing‘(ℂfld ↑s ℂ)) ∧
(ℂ × {(𝑎‘𝑘)}) ∈ (𝐸 “ 𝐴) ∧ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (𝐸 “ 𝐴)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld
↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)) |
138 | 89, 106, 136, 137 | syl3anc 1371 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld
↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)) |
139 | 88, 138 | eqeltrrd 2839 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)) |
140 | 139 | fmpttd 7063 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))):(0...𝑛)⟶(𝐸 “ 𝐴)) |
141 | 36, 8, 139, 40 | fsuppmptdm 9316 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) finSupp
(0g‘(ℂfld ↑s
ℂ))) |
142 | 5, 51, 8, 66, 140, 141 | gsumsubmcl 19696 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → ((ℂfld ↑s
ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) ∈ (𝐸 “ 𝐴)) |
143 | 47, 142 | eqeltrrd 2839 |
. . . . . 6
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)) |
144 | | eleq1 2825 |
. . . . . 6
⊢ (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → (𝑓 ∈ (𝐸 “ 𝐴) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))) |
145 | 143, 144 | syl5ibrcom 246 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0))) → (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → 𝑓 ∈ (𝐸 “ 𝐴))) |
146 | 145 | rexlimdvva 3205 |
. . . 4
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)𝑓 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → 𝑓 ∈ (𝐸 “ 𝐴))) |
147 | 2, 146 | syl5 34 |
. . 3
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) → 𝑓 ∈ (𝐸 “ 𝐴))) |
148 | | ffun 6671 |
. . . . . 6
⊢ (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld
↑s ℂ)) → Fun 𝐸) |
149 | 95, 148 | ax-mp 5 |
. . . . 5
⊢ Fun 𝐸 |
150 | | fvelima 6908 |
. . . . 5
⊢ ((Fun
𝐸 ∧ 𝑓 ∈ (𝐸 “ 𝐴)) → ∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓) |
151 | 149, 150 | mpan 688 |
. . . 4
⊢ (𝑓 ∈ (𝐸 “ 𝐴) → ∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓) |
152 | 99 | sselda 3944 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈
(Base‘(Poly1‘ℂfld))) |
153 | | eqid 2736 |
. . . . . . . . . . . 12
⊢ (
·𝑠
‘(Poly1‘ℂfld)) = (
·𝑠
‘(Poly1‘ℂfld)) |
154 | | eqid 2736 |
. . . . . . . . . . . 12
⊢
(coe1‘𝑎) = (coe1‘𝑎) |
155 | 54, 114, 93, 153, 110, 116, 154 | ply1coe 21667 |
. . . . . . . . . . 11
⊢
((ℂfld ∈ Ring ∧ 𝑎 ∈
(Base‘(Poly1‘ℂfld))) → 𝑎 =
((Poly1‘ℂfld) Σg
(𝑘 ∈
ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))) |
156 | 9, 152, 155 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑎 =
((Poly1‘ℂfld) Σg
(𝑘 ∈
ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))) |
157 | 156 | fveq2d 6846 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = (𝐸‘((Poly1‘ℂfld)
Σg (𝑘 ∈
ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))) |
158 | | eqid 2736 |
. . . . . . . . . 10
⊢
(0g‘(Poly1‘ℂfld)) =
(0g‘(Poly1‘ℂfld)) |
159 | 54 | ply1ring 21619 |
. . . . . . . . . . . 12
⊢
(ℂfld ∈ Ring →
(Poly1‘ℂfld) ∈ Ring) |
160 | 9, 159 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(Poly1‘ℂfld) ∈
Ring |
161 | | ringcmn 20003 |
. . . . . . . . . . 11
⊢
((Poly1‘ℂfld) ∈ Ring →
(Poly1‘ℂfld) ∈ CMnd) |
162 | 160, 161 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) →
(Poly1‘ℂfld) ∈ CMnd) |
163 | | ringmnd 19974 |
. . . . . . . . . . 11
⊢
((ℂfld ↑s ℂ) ∈ Ring
→ (ℂfld ↑s ℂ) ∈
Mnd) |
164 | 49, 163 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (ℂfld
↑s ℂ) ∈ Mnd) |
165 | | nn0ex 12419 |
. . . . . . . . . . 11
⊢
ℕ0 ∈ V |
166 | 165 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℕ0 ∈
V) |
167 | | rhmghm 20157 |
. . . . . . . . . . . 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 19018 |
. . . . . . . . . . 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 21623 |
. . . . . . . . . . . . 13
⊢
(ℂfld ∈ Ring →
(Poly1‘ℂfld) ∈ LMod) |
172 | 9, 171 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
(Poly1‘ℂfld) ∈ LMod) |
173 | 12 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑆 ⊆
ℂ) |
174 | | eqid 2736 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝑅) =
(Base‘𝑅) |
175 | 154, 59, 58, 174 | coe1f 21582 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ 𝐴 → (coe1‘𝑎):ℕ0⟶(Base‘𝑅)) |
176 | 57 | subrgbas 20231 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 = (Base‘𝑅)) |
177 | 176 | feq3d 6655 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∈
(SubRing‘ℂfld) → ((coe1‘𝑎):ℕ0⟶𝑆 ↔
(coe1‘𝑎):ℕ0⟶(Base‘𝑅))) |
178 | 175, 177 | syl5ibr 245 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (𝑎 ∈ 𝐴 → (coe1‘𝑎):ℕ0⟶𝑆)) |
179 | 178 | imp 407 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎):ℕ0⟶𝑆) |
180 | 179 | ffvelcdmda 7035 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑎)‘𝑘) ∈ 𝑆) |
181 | 173, 180 | sseldd 3945 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑎)‘𝑘) ∈ ℂ) |
182 | 110, 93 | mgpbas 19902 |
. . . . . . . . . . . . 13
⊢
(Base‘(Poly1‘ℂfld)) =
(Base‘(mulGrp‘(Poly1‘ℂfld))) |
183 | 110 | ringmgp 19970 |
. . . . . . . . . . . . . 14
⊢
((Poly1‘ℂfld) ∈ Ring →
(mulGrp‘(Poly1‘ℂfld)) ∈
Mnd) |
184 | 160, 183 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
(mulGrp‘(Poly1‘ℂfld)) ∈
Mnd) |
185 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
186 | 114, 54, 93 | vr1cl 21588 |
. . . . . . . . . . . . . 14
⊢
(ℂfld ∈ Ring →
(var1‘ℂfld) ∈
(Base‘(Poly1‘ℂfld))) |
187 | 9, 186 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
(var1‘ℂfld) ∈
(Base‘(Poly1‘ℂfld))) |
188 | 182, 116,
184, 185, 187 | mulgnn0cld 18897 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ (Base‘(Poly1‘ℂfld))) |
189 | 54 | ply1sca 21624 |
. . . . . . . . . . . . . 14
⊢
(ℂfld ∈ Ring → ℂfld =
(Scalar‘(Poly1‘ℂfld))) |
190 | 9, 189 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
ℂfld =
(Scalar‘(Poly1‘ℂfld)) |
191 | 93, 190, 153, 4 | lmodvscl 20339 |
. . . . . . . . . . . 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))) |
192 | 172, 181,
188, 191 | syl3anc 1371 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))
∈ (Base‘(Poly1‘ℂfld))) |
193 | 192 | fmpttd 7063 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℕ0⟶(Base‘(Poly1‘ℂfld))) |
194 | 165 | mptex 7173 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
∈ V |
195 | | funmpt 6539 |
. . . . . . . . . . . . 13
⊢ Fun
(𝑘 ∈
ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) |
196 | | fvex 6855 |
. . . . . . . . . . . . 13
⊢
(0g‘(Poly1‘ℂfld))
∈ V |
197 | 194, 195,
196 | 3pm3.2i 1339 |
. . . . . . . . . . . 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) |
198 | 197 | 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)) |
199 | 154, 93, 54, 17 | coe1sfi 21584 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈
(Base‘(Poly1‘ℂfld)) →
(coe1‘𝑎)
finSupp 0) |
200 | 152, 199 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎) finSupp 0) |
201 | 200 | fsuppimpd 9312 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((coe1‘𝑎) supp 0) ∈
Fin) |
202 | 179 | feqmptd 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎) = (𝑘 ∈ ℕ0 ↦
((coe1‘𝑎)‘𝑘))) |
203 | 202 | oveq1d 7372 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((coe1‘𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦
((coe1‘𝑎)‘𝑘)) supp 0)) |
204 | | eqimss2 4001 |
. . . . . . . . . . . . 13
⊢
(((coe1‘𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦
((coe1‘𝑎)‘𝑘)) supp 0) → ((𝑘 ∈ ℕ0 ↦
((coe1‘𝑎)‘𝑘)) supp 0) ⊆
((coe1‘𝑎)
supp 0)) |
205 | 203, 204 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦
((coe1‘𝑎)‘𝑘)) supp 0) ⊆
((coe1‘𝑎)
supp 0)) |
206 | 9, 171 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) →
(Poly1‘ℂfld) ∈ LMod) |
207 | 93, 190, 153, 17, 158 | lmod0vs 20355 |
. . . . . . . . . . . . 13
⊢
(((Poly1‘ℂfld) ∈ LMod ∧ 𝑥 ∈
(Base‘(Poly1‘ℂfld))) → (0(
·𝑠
‘(Poly1‘ℂfld))𝑥) =
(0g‘(Poly1‘ℂfld))) |
208 | 206, 207 | sylan 580 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈
(Base‘(Poly1‘ℂfld))) → (0(
·𝑠
‘(Poly1‘ℂfld))𝑥) =
(0g‘(Poly1‘ℂfld))) |
209 | | c0ex 11149 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
210 | 209 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 0 ∈ V) |
211 | 205, 208,
180, 188, 210 | suppssov1 8129 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
supp (0g‘(Poly1‘ℂfld))) ⊆ ((coe1‘𝑎)
supp 0)) |
212 | | suppssfifsupp 9320 |
. . . . . . . . . . 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))) |
213 | 198, 201,
211, 212 | syl12anc 835 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
finSupp (0g‘(Poly1‘ℂfld))) |
214 | 93, 158, 162, 164, 166, 170, 193, 213 | gsummhm 19715 |
. . . . . . . . 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))))))) |
215 | 95 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld
↑s ℂ))) |
216 | 215, 192 | cofmpt 7078 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))
= (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))) |
217 | 9 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) →
ℂfld ∈ Ring) |
218 | 6 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → ℂ
∈ V) |
219 | 95 | ffvelcdmi 7034 |
. . . . . . . . . . . . . . . 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 ℂ))) |
220 | 192, 219 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
∈ (Base‘(ℂfld ↑s ℂ))) |
221 | 3, 4, 67, 217, 218, 220 | pwselbas 17371 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℂ⟶ℂ) |
222 | 221 | feqmptd 6910 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
= (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧))) |
223 | 52 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) →
ℂfld ∈ CRing) |
224 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈
ℂ) |
225 | 53, 114, 4, 54, 93, 223, 224 | evl1vard 21703 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) →
((var1‘ℂfld) ∈
(Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧)) |
226 | 185 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈
ℕ0) |
227 | 53, 54, 4, 93, 223, 224, 225, 116, 127, 226 | evl1expd 21711 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧))) |
228 | 224, 226,
131 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘)) |
229 | 228 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧) ↔ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘))) |
230 | 229 | anbi2d 629 |
. . . . . . . . . . . . . . . . 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)))‘𝑧) = (𝑧↑𝑘)))) |
231 | 227, 230 | mpbid 231 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))
∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘))) |
232 | 181 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) →
((coe1‘𝑎)‘𝑘) ∈ ℂ) |
233 | 53, 54, 4, 93, 223, 224, 231, 232, 153, 80 | evl1vsd 21710 |
. . . . . . . . . . . . . . 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‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
234 | 233 | simprd 496 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧) = (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) |
235 | 234 | mpteq2dva 5205 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧)) = (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
236 | 222, 235 | eqtrd 2776 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
= (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
237 | 236 | mpteq2dva 5205 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))
= (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) |
238 | 216, 237 | eqtrd 2776 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))
= (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) |
239 | 238 | oveq2d 7373 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((ℂfld
↑s ℂ) Σg (𝐸 ∘ (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘)( ·𝑠
‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
= ((ℂfld ↑s ℂ) Σg (𝑘 ∈
ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))) |
240 | 157, 214,
239 | 3eqtr2d 2782 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = ((ℂfld
↑s ℂ) Σg (𝑘 ∈ ℕ0
↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))) |
241 | 6 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℂ ∈ V) |
242 | 9, 10 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℂfld ∈
CMnd) |
243 | 181 | adantlr 713 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑎)‘𝑘) ∈ ℂ) |
244 | 33 | adantll 712 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ) |
245 | 243, 244 | mulcld 11175 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) →
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
246 | 245 | anasss 467 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)) →
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
247 | 165 | mptex 7173 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V |
248 | | funmpt 6539 |
. . . . . . . . . . . 12
⊢ Fun
(𝑘 ∈
ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
249 | 247, 248,
39 | 3pm3.2i 1339 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ0
↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∧
(0g‘(ℂfld ↑s ℂ))
∈ V) |
250 | 249 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∧
(0g‘(ℂfld ↑s ℂ))
∈ V)) |
251 | | fzfid 13878 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ∈ Fin) |
252 | | eldifn 4087 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (ℕ0
∖ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) → ¬ 𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
253 | 252 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → ¬ 𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
254 | 152 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → 𝑎 ∈
(Base‘(Poly1‘ℂfld))) |
255 | | eldifi 4086 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ (ℕ0
∖ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) → 𝑘 ∈ ℕ0) |
256 | 255 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℕ0) |
257 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (
deg1 ‘ℂfld) = ( deg1
‘ℂfld) |
258 | 257, 54, 93, 17, 154 | deg1ge 25463 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈
(Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0
∧ ((coe1‘𝑎)‘𝑘) ≠ 0) → 𝑘 ≤ (( deg1
‘ℂfld)‘𝑎)) |
259 | 258 | 3expia 1121 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈
(Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0)
→ (((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ (( deg1
‘ℂfld)‘𝑎))) |
260 | 254, 256,
259 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ (( deg1
‘ℂfld)‘𝑎))) |
261 | | 0xr 11202 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℝ* |
262 | 257, 54, 93 | deg1xrcl 25447 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈
(Base‘(Poly1‘ℂfld)) → ((
deg1 ‘ℂfld)‘𝑎) ∈
ℝ*) |
263 | 152, 262 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (( deg1
‘ℂfld)‘𝑎) ∈
ℝ*) |
264 | 263 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (( deg1
‘ℂfld)‘𝑎) ∈
ℝ*) |
265 | | xrmax2 13095 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((0
∈ ℝ* ∧ (( deg1
‘ℂfld)‘𝑎) ∈ ℝ*) → ((
deg1 ‘ℂfld)‘𝑎) ≤ if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) |
266 | 261, 264,
265 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (( deg1
‘ℂfld)‘𝑎) ≤ if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) |
267 | 256 | nn0red 12474 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ) |
268 | 267 | rexrd 11205 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ*) |
269 | | ifcl 4531 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((
deg1 ‘ℂfld)‘𝑎) ∈ ℝ* ∧ 0 ∈
ℝ*) → if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℝ*) |
270 | 264, 261,
269 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℝ*) |
271 | | xrletr 13077 |
. . . . . . . . . . . . . . . . . . . . . . 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))) |
272 | 268, 264,
270, 271 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . 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))) |
273 | 266, 272 | mpan2d 692 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (𝑘 ≤ (( deg1
‘ℂfld)‘𝑎) → 𝑘 ≤ if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
274 | 260, 273 | syld 47 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
275 | 274, 256 | jctild 526 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) ≠ 0 → (𝑘 ∈ ℕ0 ∧ 𝑘 ≤ if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) |
276 | 257, 54, 93 | deg1cl 25448 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 ∈
(Base‘(Poly1‘ℂfld)) → ((
deg1 ‘ℂfld)‘𝑎) ∈ (ℕ0 ∪
{-∞})) |
277 | 152, 276 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (( deg1
‘ℂfld)‘𝑎) ∈ (ℕ0 ∪
{-∞})) |
278 | | elun 4108 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ (ℕ0 ∪
{-∞}) ↔ ((( deg1
‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞})) |
279 | 277, 278 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((( deg1
‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞})) |
280 | | nn0ge0 12438 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → 0 ≤ ((
deg1 ‘ℂfld)‘𝑎)) |
281 | 280 | iftrued 4494 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤
(( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) = (( deg1
‘ℂfld)‘𝑎)) |
282 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → ((
deg1 ‘ℂfld)‘𝑎) ∈
ℕ0) |
283 | 281, 282 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤
(( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℕ0) |
284 | | mnflt0 13046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ -∞
< 0 |
285 | | mnfxr 11212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ -∞
∈ ℝ* |
286 | | xrltnle 11222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((-∞ ∈ ℝ* ∧ 0 ∈
ℝ*) → (-∞ < 0 ↔ ¬ 0 ≤
-∞)) |
287 | 285, 261,
286 | mp2an 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (-∞
< 0 ↔ ¬ 0 ≤ -∞) |
288 | 284, 287 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ¬ 0
≤ -∞ |
289 | | elsni 4603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → (( deg1
‘ℂfld)‘𝑎) = -∞) |
290 | 289 | breq2d 5117 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → (0 ≤ ((
deg1 ‘ℂfld)‘𝑎) ↔ 0 ≤ -∞)) |
291 | 288, 290 | mtbiri 326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → ¬ 0 ≤ ((
deg1 ‘ℂfld)‘𝑎)) |
292 | 291 | iffalsed 4497 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) = 0) |
293 | | 0nn0 12428 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
ℕ0 |
294 | 292, 293 | eqeltrdi 2846 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℕ0) |
295 | 283, 294 | jaoi 855 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((
deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((
deg1 ‘ℂfld)‘𝑎) ∈ {-∞}) → if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℕ0) |
296 | 279, 295 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℕ0) |
297 | 296 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈
ℕ0) |
298 | | fznn0 13533 |
. . . . . . . . . . . . . . . . . . . 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)))) |
299 | 297, 298 | 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)))) |
300 | 275, 299 | sylibrd 258 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) |
301 | 300 | necon1bd 2961 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (¬ 𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) → ((coe1‘𝑎)‘𝑘) = 0)) |
302 | 253, 301 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → ((coe1‘𝑎)‘𝑘) = 0) |
303 | 302 | oveq1d 7372 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘))) |
304 | 255, 244 | sylan2 593 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (𝑧↑𝑘) ∈ ℂ) |
305 | 304 | mul02d 11353 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (0 · (𝑧↑𝑘)) = 0) |
306 | 303, 305 | eqtrd 2776 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) →
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = 0) |
307 | 306 | an32s 650 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) ∧ 𝑧 ∈ ℂ) →
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = 0) |
308 | 307 | mpteq2dva 5205 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ 0)) |
309 | | fconstmpt 5694 |
. . . . . . . . . . . . 13
⊢ (ℂ
× {0}) = (𝑧 ∈
ℂ ↦ 0) |
310 | | ringmnd 19974 |
. . . . . . . . . . . . . . 15
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
311 | 9, 310 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
ℂfld ∈ Mnd |
312 | 3, 17 | pws0g 18592 |
. . . . . . . . . . . . . 14
⊢
((ℂfld ∈ Mnd ∧ ℂ ∈ V) →
(ℂ × {0}) = (0g‘(ℂfld
↑s ℂ))) |
313 | 311, 6, 312 | mp2an 690 |
. . . . . . . . . . . . 13
⊢ (ℂ
× {0}) = (0g‘(ℂfld
↑s ℂ)) |
314 | 309, 313 | eqtr3i 2766 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℂ ↦ 0) =
(0g‘(ℂfld ↑s
ℂ)) |
315 | 308, 314 | eqtrdi 2792 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖
(0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) =
(0g‘(ℂfld ↑s
ℂ))) |
316 | 315, 166 | suppss2 8131 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) supp
(0g‘(ℂfld ↑s
ℂ))) ⊆ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
317 | | suppssfifsupp 9320 |
. . . . . . . . . 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
ℂ))) |
318 | 250, 251,
316, 317 | syl12anc 835 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) finSupp
(0g‘(ℂfld ↑s
ℂ))) |
319 | 3, 4, 5, 241, 166, 242, 246, 318 | pwsgsum 19759 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((ℂfld
↑s ℂ) Σg (𝑘 ∈ ℕ0
↦ (𝑧 ∈ ℂ
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦
(ℂfld Σg (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))) |
320 | | fz0ssnn0 13536 |
. . . . . . . . . . . 12
⊢ (0...if(0
≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ⊆
ℕ0 |
321 | | resmpt 5991 |
. . . . . . . . . . . 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‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
322 | 320, 321 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) = (𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) |
323 | 322 | oveq2i 7368 |
. . . . . . . . . 10
⊢
(ℂfld Σg ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) = (ℂfld
Σg (𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
324 | 9, 10 | mp1i 13 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ℂfld
∈ CMnd) |
325 | 165 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ℕ0
∈ V) |
326 | 245 | fmpttd 7063 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))):ℕ0⟶ℂ) |
327 | 306, 325 | suppss2 8131 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) supp 0) ⊆ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) |
328 | 165 | mptex 7173 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V |
329 | | funmpt 6539 |
. . . . . . . . . . . . . 14
⊢ Fun
(𝑘 ∈
ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) |
330 | 328, 329,
209 | 3pm3.2i 1339 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ0
↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∧ 0 ∈ V) |
331 | 330 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∧ 0 ∈ V)) |
332 | | fzfid 13878 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ∈ Fin) |
333 | | suppssfifsupp 9320 |
. . . . . . . . . . . 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) |
334 | 331, 332,
327, 333 | syl12anc 835 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) finSupp 0) |
335 | 4, 17, 324, 325, 326, 327, 334 | gsumres 19690 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) →
(ℂfld Σg ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)))) = (ℂfld
Σg (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) |
336 | | elfznn0 13534 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) → 𝑘 ∈ ℕ0) |
337 | 336, 245 | sylan2 593 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
338 | 332, 337 | gsumfsum 20864 |
. . . . . . . . . 10
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) →
(ℂfld Σg (𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0)) ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) |
339 | 323, 335,
338 | 3eqtr3a 2800 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) →
(ℂfld Σg (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ (( deg1
‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) |
340 | 339 | mpteq2dva 5205 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑧 ∈ ℂ ↦
(ℂfld Σg (𝑘 ∈ ℕ0 ↦
(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
341 | 240, 319,
340 | 3eqtrd 2780 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) |
342 | 12 | adantr 481 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑆 ⊆ ℂ) |
343 | | elplyr 25562 |
. . . . . . . 8
⊢ ((𝑆 ⊆ ℂ ∧ if(0 ≤
(( deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0) ∈ ℕ0 ∧
(coe1‘𝑎):ℕ0⟶𝑆) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆)) |
344 | 342, 296,
179, 343 | syl3anc 1371 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((
deg1 ‘ℂfld)‘𝑎), (( deg1
‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆)) |
345 | 341, 344 | eqeltrd 2838 |
. . . . . 6
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) ∈ (Poly‘𝑆)) |
346 | | eleq1 2825 |
. . . . . 6
⊢ ((𝐸‘𝑎) = 𝑓 → ((𝐸‘𝑎) ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (Poly‘𝑆))) |
347 | 345, 346 | syl5ibcom 244 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝐸‘𝑎) = 𝑓 → 𝑓 ∈ (Poly‘𝑆))) |
348 | 347 | rexlimdva 3152 |
. . . 4
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓 → 𝑓 ∈ (Poly‘𝑆))) |
349 | 151, 348 | syl5 34 |
. . 3
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (𝑓 ∈ (𝐸 “ 𝐴) → 𝑓 ∈ (Poly‘𝑆))) |
350 | 147, 349 | impbid 211 |
. 2
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (𝐸 “ 𝐴))) |
351 | 350 | eqrdv 2734 |
1
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (Poly‘𝑆) = (𝐸 “ 𝐴)) |