ply1lmod - Metamath Proof Explorer

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

Theorem ply1lmod 22569

Description: Univariate polynomials form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.)

**Hypothesis**
Ref	Expression
ply1lmod.p	⊢ 𝑃 = (Poly₁‘𝑅)

**Assertion**
Ref	Expression
ply1lmod	⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)

**Proof of Theorem ply1lmod**
Step	Hyp	Ref	Expression
1		eqid 2761	. . 3 ⊢ (PwSer₁‘𝑅) = (PwSer₁‘𝑅)
2	1	psr1lmod 22566	. 2 ⊢ (𝑅 ∈ Ring → (PwSer₁‘𝑅) ∈ LMod)
3		eqid 2761	. . . 4 ⊢ (Poly₁‘𝑅) = (Poly₁‘𝑅)
4		eqid 2761	. . . 4 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(Poly₁‘𝑅))
5	3, 4	ply1bas 22513	. . 3 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(1_o mPoly 𝑅))
6	3, 1, 4	ply1lss 22514	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘(Poly₁‘𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
7	5, 6	eqeltrrid 2866	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
8		ply1lmod.p	. . . 4 ⊢ 𝑃 = (Poly₁‘𝑅)
9	8, 1	ply1val 22512	. . 3 ⊢ 𝑃 = ((PwSer₁‘𝑅) ↾_s (Base‘(1_o mPoly 𝑅)))
10		eqid 2761	. . 3 ⊢ (LSubSp‘(PwSer₁‘𝑅)) = (LSubSp‘(PwSer₁‘𝑅))
11	9, 10	lsslmod 21235	. 2 ⊢ (((PwSer₁‘𝑅) ∈ LMod ∧ (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅))) → 𝑃 ∈ LMod)
12	2, 7, 11	syl2anc 596	1 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1570 ∈ wcel 2145 ‘cfv 6538 (class class class)co 7420 1_oc1o 8469 Basecbs 17387 Ringcrg 20459 LModclmod 21135 LSubSpclss 21206 mPoly cmpl 22214 PwSer₁cps1 22493 Poly₁cpl1 22495

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8178 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-er 8717 df-map 8849 df-ixp 8926 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-fsupp 9354 df-sup 9434 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-5 12408 df-6 12409 df-7 12410 df-8 12411 df-9 12412 df-n0 12607 df-z 12694 df-dec 12815 df-uz 12966 df-fz 13640 df-struct 17325 df-sets 17342 df-slot 17360 df-ndx 17372 df-base 17388 df-ress 17409 df-plusg 17441 df-mulr 17442 df-sca 17444 df-vsca 17445 df-ip 17446 df-tset 17447 df-ple 17448 df-ds 17450 df-hom 17452 df-cco 17453 df-0g 17612 df-prds 17618 df-pws 17620 df-mgm 18816 df-sgrp 18908 df-mnd 18924 df-grp 19147 df-minusg 19148 df-sbg 19149 df-subg 19333 df-cmn 19996 df-abl 19997 df-mgp 20361 df-rng 20375 df-ur 20408 df-ring 20461 df-lmod 21137 df-lss 21207 df-psr 22217 df-mpl 22219 df-opsr 22221 df-psr1 22498 df-ply1 22500

This theorem is used by: ply1ascl0 22572 ply1ascl1 22573 ply10s0 22575 ply1tmcl 22591 coe1pwmul 22598 ply1sclf 22604 ply1scl0 22609 ply1scl1 22611 ply1coefsupp 22615 ply1coe 22616 cply1coe0bi 22620 gsumsmonply1 22625 gsummoncoe1 22626 lply1binomsc 22629 evls1sca 22641 evl1scvarpw 22681 evl1gsummon 22683 evls1fpws 22687 evls1vsca 22691 asclply1subcl 22692 evls1maplmhm 22695 cpmatacl 23034 cpmatinvcl 23035 mat2pmatbas 23044 mat2pmatghm 23048 mat2pmatmul 23049 decpmatid 23088 pmatcollpwscmatlem1 23107 pm2mpcl 23115 idpm2idmp 23119 mply1topmatcllem 23121 mply1topmatcl 23123 mp2pm2mplem4 23127 mp2pm2mplem5 23128 pm2mpghmlem2 23130 pm2mpghm 23134 pm2mpmhmlem1 23136 pm2mpmhmlem2 23137 monmat2matmon 23142 chpscmat 23160 chpscmatgsumbin 23162 chpscmatgsummon 23163 deg1invg 26424 deg1pwle 26438 deg1pw 26439 ply1remlem 26483 plypf1 26531 ply1lvec 34091 ressasclcl 34103 coe1mon 34119 ply1coedeg 34121 deg1vr 34124 ply1degltlss 34128 gsummoncoe1fzo 34129 q1pvsca 34136 r1pvsca 34137 r1p0 34138 r1plmhm 34141 vietalem 34211 irngnzply1lem 34322 extdgfialglem2 34325 2sqr3minply 34412 cos9thpiminplylem6 34419 cos9thpiminply 34420 aks5lem2 43237 ply1vr1smo 49494 ply1mulgsumlem4 49500 ply1mulgsum 49501

W3C validator