mplelf - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mplelf		Structured version Visualization version GIF version

Theorem mplelf 22049

Description: A polynomial is defined as a function on the coefficients. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)

**Hypotheses**
Ref	Expression
mplelf.p	⊢ 𝑃 = (𝐼 mPoly 𝑅)
mplelf.k	⊢ 𝐾 = (Base‘𝑅)
mplelf.b	⊢ 𝐵 = (Base‘𝑃)
mplelf.d	⊢ 𝐷 = {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}
mplelf.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)

**Assertion**
Ref	Expression
mplelf	⊢ (𝜑 → 𝑋:𝐷⟶𝐾)

Distinct variable group: 𝑓,𝐼 Allowed substitution hints: 𝜑(𝑓) 𝐵(𝑓) 𝐷(𝑓) 𝑃(𝑓) 𝑅(𝑓) 𝐾(𝑓) 𝑋(𝑓)

**Proof of Theorem mplelf**
Step	Hyp	Ref	Expression
1		eqid 2762	. 2 ⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅)
2		mplelf.k	. 2 ⊢ 𝐾 = (Base‘𝑅)
3		mplelf.d	. 2 ⊢ 𝐷 = {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}
4		eqid 2762	. 2 ⊢ (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅))
5		mplelf.p	. . . 4 ⊢ 𝑃 = (𝐼 mPoly 𝑅)
6		mplelf.b	. . . 4 ⊢ 𝐵 = (Base‘𝑃)
7	5, 1, 6, 4	mplbasss 22048	. . 3 ⊢ 𝐵 ⊆ (Base‘(𝐼 mPwSer 𝑅))
8		mplelf.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
9	7, 8	sselid 3934	. 2 ⊢ (𝜑 → 𝑋 ∈ (Base‘(𝐼 mPwSer 𝑅)))
10	1, 2, 3, 4, 9	psrelbas 21987	1 ⊢ (𝜑 → 𝑋:𝐷⟶𝐾)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1560 ∈ wcel 2142 {crab 3414 ^◡ccnv 5646 “ cima 5650 ⟶wf 6517 ‘cfv 6521 (class class class)co 7396 ↑_m cmap 8808 Fincfn 8927 ℕcn 12210 ℕ₀cn0 12481 Basecbs 17245 mPwSer cmps 21956 mPoly cmpl 21958

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-iun 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-of 7660 df-om 7847 df-1st 7970 df-2nd 7971 df-supp 8141 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-er 8678 df-map 8810 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-fsupp 9308 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-nn 12211 df-2 12280 df-3 12281 df-4 12282 df-5 12283 df-6 12284 df-7 12285 df-8 12286 df-9 12287 df-n0 12482 df-z 12569 df-uz 12840 df-fz 13513 df-struct 17183 df-sets 17200 df-slot 17218 df-ndx 17230 df-base 17246 df-ress 17267 df-plusg 17299 df-mulr 17300 df-sca 17302 df-vsca 17303 df-tset 17305 df-psr 21961 df-mpl 21963

This theorem is referenced by: mplsubrglem 22055 mplvscaval 22067 mplmonmul 22089 mplcoe1 22090 mplbas2 22095 mplcoe4 22124 evlslem2 22132 evlslem6 22134 evlslem1 22135 evlsvvvallem2 22145 evlsvvval 22146 mhmcompl 22174 mplmapghm 22175 mhmcoaddmpl 22176 rhmcomulmpl 22177 evlsevl 22185 selvvvval 22195 ismhp3 22207 mhpmulcl 22214 mhpaddcl 22216 mhpinvcl 22217 mhpvscacl 22219 psdmplcl 22227 ply1basf 22264 mdegfval 26122 mdegleb 26124 mdegldg 26126 mdegaddle 26134 mdegvsca 26136 mdegle0 26137 mdegmullem 26138 0mplrim 33811 selvply1rhmlema 33815 selvply1rhmlemb 33816 selvply1rhmlem1 33817 selvply1rhmlem4 33820 selvply1rhm0 33823 extvfvvcl 33832 extvfvcl 33833 mplmulmvr 33836 evlextv 33839 mplvrpmfgalem 33841 mplvrpmga 33842 mplvrpmmhm 33843 issply 33858 esplyind 33872 evlselv 43171 mhpind 43176 evlsmhpvvval 43177 mhphf 43179

W3C validator