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 22411

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 2763	. . 3 ⊢ (PwSer₁‘𝑅) = (PwSer₁‘𝑅)
2	1	psr1lmod 22408	. 2 ⊢ (𝑅 ∈ Ring → (PwSer₁‘𝑅) ∈ LMod)
3		eqid 2763	. . . 4 ⊢ (Poly₁‘𝑅) = (Poly₁‘𝑅)
4		eqid 2763	. . . 4 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(Poly₁‘𝑅))
5	3, 4	ply1bas 22355	. . 3 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(1_o mPoly 𝑅))
6	3, 1, 4	ply1lss 22356	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘(Poly₁‘𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
7	5, 6	eqeltrrid 2868	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
8		ply1lmod.p	. . . 4 ⊢ 𝑃 = (Poly₁‘𝑅)
9	8, 1	ply1val 22354	. . 3 ⊢ 𝑃 = ((PwSer₁‘𝑅) ↾_s (Base‘(1_o mPoly 𝑅)))
10		eqid 2763	. . 3 ⊢ (LSubSp‘(PwSer₁‘𝑅)) = (LSubSp‘(PwSer₁‘𝑅))
11	9, 10	lsslmod 21081	. 2 ⊢ (((PwSer₁‘𝑅) ∈ LMod ∧ (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅))) → 𝑃 ∈ LMod)
12	2, 7, 11	syl2anc 595	1 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1570 ∈ wcel 2143 ‘cfv 6536 (class class class)co 7410 1_oc1o 8442 Basecbs 17264 Ringcrg 20310 LModclmod 20981 LSubSpclss 21052 mPoly cmpl 22056 PwSer₁cps1 22335 Poly₁cpl1 22337

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4873 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-om 7859 df-1st 7982 df-2nd 7983 df-supp 8153 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-er 8690 df-map 8822 df-ixp 8892 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-fsupp 9318 df-sup 9398 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-nn 12229 df-2 12298 df-3 12299 df-4 12300 df-5 12301 df-6 12302 df-7 12303 df-8 12304 df-9 12305 df-n0 12500 df-z 12587 df-dec 12707 df-uz 12858 df-fz 13531 df-struct 17202 df-sets 17219 df-slot 17237 df-ndx 17249 df-base 17265 df-ress 17286 df-plusg 17318 df-mulr 17319 df-sca 17321 df-vsca 17322 df-ip 17323 df-tset 17324 df-ple 17325 df-ds 17327 df-hom 17329 df-cco 17330 df-0g 17489 df-prds 17495 df-pws 17497 df-mgm 18693 df-sgrp 18772 df-mnd 18788 df-grp 18998 df-minusg 18999 df-sbg 19000 df-subg 19184 df-cmn 19847 df-abl 19848 df-mgp 20212 df-rng 20226 df-ur 20259 df-ring 20312 df-lmod 20983 df-lss 21053 df-psr 22059 df-mpl 22061 df-opsr 22063 df-psr1 22340 df-ply1 22342

This theorem is referenced by: ply1ascl0 22414 ply1ascl1 22415 ply10s0 22417 ply1tmcl 22433 coe1pwmul 22440 ply1sclf 22446 ply1scl0 22451 ply1scl1 22453 ply1coefsupp 22457 ply1coe 22458 cply1coe0bi 22462 gsumsmonply1 22467 gsummoncoe1 22468 lply1binomsc 22471 evls1sca 22483 evl1scvarpw 22523 evl1gsummon 22525 evls1fpws 22529 evls1vsca 22533 asclply1subcl 22534 evls1maplmhm 22537 cpmatacl 22873 cpmatinvcl 22874 mat2pmatbas 22883 mat2pmatghm 22887 mat2pmatmul 22888 decpmatid 22927 pmatcollpwscmatlem1 22946 pm2mpcl 22954 idpm2idmp 22958 mply1topmatcllem 22960 mply1topmatcl 22962 mp2pm2mplem4 22966 mp2pm2mplem5 22967 pm2mpghmlem2 22969 pm2mpghm 22973 pm2mpmhmlem1 22975 pm2mpmhmlem2 22976 monmat2matmon 22981 chpscmat 22999 chpscmatgsumbin 23001 chpscmatgsummon 23002 deg1invg 26263 deg1pwle 26277 deg1pw 26278 ply1remlem 26322 plypf1 26369 ply1lvec 33849 ressasclcl 33861 coe1mon 33877 ply1coedeg 33879 deg1vr 33882 ply1degltlss 33886 gsummoncoe1fzo 33887 q1pvsca 33894 r1pvsca 33895 r1p0 33896 r1plmhm 33899 vietalem 33969 irngnzply1lem 34080 extdgfialglem2 34083 2sqr3minply 34170 cos9thpiminplylem6 34177 cos9thpiminply 34178 aks5lem2 42974 ply1vr1smo 49183 ply1mulgsumlem4 49189 ply1mulgsum 49190

W3C validator