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 22380

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 2769	. . 3 ⊢ (PwSer₁‘𝑅) = (PwSer₁‘𝑅)
2	1	psr1lmod 22377	. 2 ⊢ (𝑅 ∈ Ring → (PwSer₁‘𝑅) ∈ LMod)
3		eqid 2769	. . . 4 ⊢ (Poly₁‘𝑅) = (Poly₁‘𝑅)
4		eqid 2769	. . . 4 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(Poly₁‘𝑅))
5	3, 4	ply1bas 22324	. . 3 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(1_o mPoly 𝑅))
6	3, 1, 4	ply1lss 22325	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘(Poly₁‘𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
7	5, 6	eqeltrrid 2874	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
8		ply1lmod.p	. . . 4 ⊢ 𝑃 = (Poly₁‘𝑅)
9	8, 1	ply1val 22323	. . 3 ⊢ 𝑃 = ((PwSer₁‘𝑅) ↾_s (Base‘(1_o mPoly 𝑅)))
10		eqid 2769	. . 3 ⊢ (LSubSp‘(PwSer₁‘𝑅)) = (LSubSp‘(PwSer₁‘𝑅))
11	9, 10	lsslmod 21059	. 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 1567 ∈ wcel 2149 ‘cfv 6537 (class class class)co 7411 1_oc1o 8446 Basecbs 17269 Ringcrg 20315 LModclmod 20959 LSubSpclss 21030 mPoly cmpl 22025 PwSer₁cps1 22304 Poly₁cpl1 22306

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7675 df-om 7863 df-1st 7986 df-2nd 7987 df-supp 8157 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-er 8694 df-map 8826 df-ixp 8896 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-fsupp 9322 df-sup 9402 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-nn 12234 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12505 df-z 12592 df-dec 12712 df-uz 12863 df-fz 13536 df-struct 17207 df-sets 17224 df-slot 17242 df-ndx 17254 df-base 17270 df-ress 17291 df-plusg 17323 df-mulr 17324 df-sca 17326 df-vsca 17327 df-ip 17328 df-tset 17329 df-ple 17330 df-ds 17332 df-hom 17334 df-cco 17335 df-0g 17494 df-prds 17500 df-pws 17502 df-mgm 18698 df-sgrp 18777 df-mnd 18793 df-grp 19003 df-minusg 19004 df-sbg 19005 df-subg 19189 df-cmn 19852 df-abl 19853 df-mgp 20217 df-rng 20231 df-ur 20264 df-ring 20317 df-lmod 20961 df-lss 21031 df-psr 22028 df-mpl 22030 df-opsr 22032 df-psr1 22309 df-ply1 22311

This theorem is referenced by: ply1ascl0 22383 ply1ascl1 22384 ply10s0 22386 ply1tmcl 22402 coe1pwmul 22409 ply1sclf 22415 ply1scl0 22420 ply1scl1 22422 ply1coefsupp 22426 ply1coe 22427 cply1coe0bi 22431 gsumsmonply1 22436 gsummoncoe1 22437 lply1binomsc 22440 evls1sca 22452 evl1scvarpw 22492 evl1gsummon 22494 evls1fpws 22498 evls1vsca 22502 asclply1subcl 22503 evls1maplmhm 22506 cpmatacl 22842 cpmatinvcl 22843 mat2pmatbas 22852 mat2pmatghm 22856 mat2pmatmul 22857 decpmatid 22896 pmatcollpwscmatlem1 22915 pm2mpcl 22923 idpm2idmp 22927 mply1topmatcllem 22929 mply1topmatcl 22931 mp2pm2mplem4 22935 mp2pm2mplem5 22936 pm2mpghmlem2 22938 pm2mpghm 22942 pm2mpmhmlem1 22944 pm2mpmhmlem2 22945 monmat2matmon 22950 chpscmat 22968 chpscmatgsumbin 22970 chpscmatgsummon 22971 deg1invg 26232 deg1pwle 26246 deg1pw 26247 ply1remlem 26291 plypf1 26338 ply1lvec 33794 ressasclcl 33806 coe1mon 33822 ply1coedeg 33824 deg1vr 33827 ply1degltlss 33831 gsummoncoe1fzo 33832 q1pvsca 33839 r1pvsca 33840 r1p0 33841 r1plmhm 33844 vietalem 33914 irngnzply1lem 34025 extdgfialglem2 34028 2sqr3minply 34115 cos9thpiminplylem6 34122 cos9thpiminply 34123 aks5lem2 42844 ply1vr1smo 49048 ply1mulgsumlem4 49054 ply1mulgsum 49055

W3C validator