Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ply1coefsupp | Structured version Visualization version GIF version |
Description: The decomposition of a univariate polynomial is finitely supported. Formerly part of proof for ply1coe 21457. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 8-Aug-2019.) |
Ref | Expression |
---|---|
ply1coefsupp.p | ⊢ 𝑃 = (Poly1‘𝑅) |
ply1coefsupp.x | ⊢ 𝑋 = (var1‘𝑅) |
ply1coefsupp.b | ⊢ 𝐵 = (Base‘𝑃) |
ply1coefsupp.n | ⊢ · = ( ·𝑠 ‘𝑃) |
ply1coefsupp.m | ⊢ 𝑀 = (mulGrp‘𝑃) |
ply1coefsupp.e | ⊢ ↑ = (.g‘𝑀) |
ply1coefsupp.a | ⊢ 𝐴 = (coe1‘𝐾) |
Ref | Expression |
---|---|
ply1coefsupp | ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ply1coefsupp.b | . 2 ⊢ 𝐵 = (Base‘𝑃) | |
2 | eqid 2740 | . 2 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃) | |
3 | ply1coefsupp.n | . 2 ⊢ · = ( ·𝑠 ‘𝑃) | |
4 | ply1coefsupp.p | . . . 4 ⊢ 𝑃 = (Poly1‘𝑅) | |
5 | 4 | ply1lmod 21413 | . . 3 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
6 | 5 | adantr 481 | . 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝑃 ∈ LMod) |
7 | nn0ex 12231 | . . 3 ⊢ ℕ0 ∈ V | |
8 | 7 | a1i 11 | . 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ℕ0 ∈ V) |
9 | 4 | ply1ring 21409 | . . . . 5 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
10 | ply1coefsupp.m | . . . . . 6 ⊢ 𝑀 = (mulGrp‘𝑃) | |
11 | 10 | ringmgp 19779 | . . . . 5 ⊢ (𝑃 ∈ Ring → 𝑀 ∈ Mnd) |
12 | 9, 11 | syl 17 | . . . 4 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd) |
13 | 12 | ad2antrr 723 | . . 3 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈ Mnd) |
14 | simpr 485 | . . 3 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0) | |
15 | ply1coefsupp.x | . . . . 5 ⊢ 𝑋 = (var1‘𝑅) | |
16 | 15, 4, 1 | vr1cl 21378 | . . . 4 ⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵) |
17 | 16 | ad2antrr 723 | . . 3 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑋 ∈ 𝐵) |
18 | 10, 1 | mgpbas 19716 | . . . 4 ⊢ 𝐵 = (Base‘𝑀) |
19 | ply1coefsupp.e | . . . 4 ⊢ ↑ = (.g‘𝑀) | |
20 | 18, 19 | mulgnn0cl 18710 | . . 3 ⊢ ((𝑀 ∈ Mnd ∧ 𝑘 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (𝑘 ↑ 𝑋) ∈ 𝐵) |
21 | 13, 14, 17, 20 | syl3anc 1370 | . 2 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑘 ↑ 𝑋) ∈ 𝐵) |
22 | ply1coefsupp.a | . . . 4 ⊢ 𝐴 = (coe1‘𝐾) | |
23 | eqid 2740 | . . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
24 | 22, 1, 4, 23 | coe1f 21372 | . . 3 ⊢ (𝐾 ∈ 𝐵 → 𝐴:ℕ0⟶(Base‘𝑅)) |
25 | 24 | adantl 482 | . 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐴:ℕ0⟶(Base‘𝑅)) |
26 | eqid 2740 | . . . . 5 ⊢ (0g‘𝑅) = (0g‘𝑅) | |
27 | 22, 1, 4, 26 | coe1sfi 21374 | . . . 4 ⊢ (𝐾 ∈ 𝐵 → 𝐴 finSupp (0g‘𝑅)) |
28 | 27 | adantl 482 | . . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐴 finSupp (0g‘𝑅)) |
29 | 4 | ply1sca 21414 | . . . . . 6 ⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃)) |
30 | 29 | eqcomd 2746 | . . . . 5 ⊢ (𝑅 ∈ Ring → (Scalar‘𝑃) = 𝑅) |
31 | 30 | adantr 481 | . . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (Scalar‘𝑃) = 𝑅) |
32 | 31 | fveq2d 6773 | . . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (0g‘(Scalar‘𝑃)) = (0g‘𝑅)) |
33 | 28, 32 | breqtrrd 5107 | . 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐴 finSupp (0g‘(Scalar‘𝑃))) |
34 | 1, 2, 3, 6, 8, 21, 25, 33 | mptscmfsuppd 20179 | 1 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1542 ∈ wcel 2110 Vcvv 3431 class class class wbr 5079 ↦ cmpt 5162 ⟶wf 6427 ‘cfv 6431 (class class class)co 7269 finSupp cfsupp 9098 ℕ0cn0 12225 Basecbs 16902 Scalarcsca 16955 ·𝑠 cvsca 16956 0gc0g 17140 Mndcmnd 18375 .gcmg 18690 mulGrpcmgp 19710 Ringcrg 19773 LModclmod 20113 var1cv1 21337 Poly1cpl1 21338 coe1cco1 21339 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2711 ax-rep 5214 ax-sep 5227 ax-nul 5234 ax-pow 5292 ax-pr 5356 ax-un 7580 ax-cnex 10920 ax-resscn 10921 ax-1cn 10922 ax-icn 10923 ax-addcl 10924 ax-addrcl 10925 ax-mulcl 10926 ax-mulrcl 10927 ax-mulcom 10928 ax-addass 10929 ax-mulass 10930 ax-distr 10931 ax-i2m1 10932 ax-1ne0 10933 ax-1rid 10934 ax-rnegex 10935 ax-rrecex 10936 ax-cnre 10937 ax-pre-lttri 10938 ax-pre-lttrn 10939 ax-pre-ltadd 10940 ax-pre-mulgt0 10941 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2072 df-mo 2542 df-eu 2571 df-clab 2718 df-cleq 2732 df-clel 2818 df-nfc 2891 df-ne 2946 df-nel 3052 df-ral 3071 df-rex 3072 df-reu 3073 df-rmo 3074 df-rab 3075 df-v 3433 df-sbc 3721 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-pss 3911 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4846 df-int 4886 df-iun 4932 df-iin 4933 df-br 5080 df-opab 5142 df-mpt 5163 df-tr 5197 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-se 5545 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6200 df-ord 6267 df-on 6268 df-lim 6269 df-suc 6270 df-iota 6389 df-fun 6433 df-fn 6434 df-f 6435 df-f1 6436 df-fo 6437 df-f1o 6438 df-fv 6439 df-isom 6440 df-riota 7226 df-ov 7272 df-oprab 7273 df-mpo 7274 df-of 7525 df-ofr 7526 df-om 7702 df-1st 7818 df-2nd 7819 df-supp 7963 df-frecs 8082 df-wrecs 8113 df-recs 8187 df-rdg 8226 df-1o 8282 df-er 8473 df-map 8592 df-pm 8593 df-ixp 8661 df-en 8709 df-dom 8710 df-sdom 8711 df-fin 8712 df-fsupp 9099 df-oi 9239 df-card 9690 df-pnf 11004 df-mnf 11005 df-xr 11006 df-ltxr 11007 df-le 11008 df-sub 11199 df-neg 11200 df-nn 11966 df-2 12028 df-3 12029 df-4 12030 df-5 12031 df-6 12032 df-7 12033 df-8 12034 df-9 12035 df-n0 12226 df-z 12312 df-dec 12429 df-uz 12574 df-fz 13231 df-fzo 13374 df-seq 13712 df-hash 14035 df-struct 16838 df-sets 16855 df-slot 16873 df-ndx 16885 df-base 16903 df-ress 16932 df-plusg 16965 df-mulr 16966 df-sca 16968 df-vsca 16969 df-tset 16971 df-ple 16972 df-0g 17142 df-gsum 17143 df-mre 17285 df-mrc 17286 df-acs 17288 df-mgm 18316 df-sgrp 18365 df-mnd 18376 df-mhm 18420 df-submnd 18421 df-grp 18570 df-minusg 18571 df-sbg 18572 df-mulg 18691 df-subg 18742 df-ghm 18822 df-cntz 18913 df-cmn 19378 df-abl 19379 df-mgp 19711 df-ur 19728 df-ring 19775 df-subrg 20012 df-lmod 20115 df-lss 20184 df-psr 21102 df-mvr 21103 df-mpl 21104 df-opsr 21106 df-psr1 21341 df-vr1 21342 df-ply1 21343 df-coe1 21344 |
This theorem is referenced by: ply1coe 21457 |
Copyright terms: Public domain | W3C validator |