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 22228

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 2737	. . 3 ⊢ (PwSer₁‘𝑅) = (PwSer₁‘𝑅)
2	1	psr1lmod 22225	. 2 ⊢ (𝑅 ∈ Ring → (PwSer₁‘𝑅) ∈ LMod)
3		eqid 2737	. . . 4 ⊢ (Poly₁‘𝑅) = (Poly₁‘𝑅)
4		eqid 2737	. . . 4 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(Poly₁‘𝑅))
5	3, 4	ply1bas 22171	. . 3 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(1_o mPoly 𝑅))
6	3, 1, 4	ply1lss 22173	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘(Poly₁‘𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
7	5, 6	eqeltrrid 2842	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
8		ply1lmod.p	. . . 4 ⊢ 𝑃 = (Poly₁‘𝑅)
9	8, 1	ply1val 22170	. . 3 ⊢ 𝑃 = ((PwSer₁‘𝑅) ↾_s (Base‘(1_o mPoly 𝑅)))
10		eqid 2737	. . 3 ⊢ (LSubSp‘(PwSer₁‘𝑅)) = (LSubSp‘(PwSer₁‘𝑅))
11	9, 10	lsslmod 20949	. 2 ⊢ (((PwSer₁‘𝑅) ∈ LMod ∧ (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅))) → 𝑃 ∈ LMod)
12	2, 7, 11	syl2anc 585	1 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 ‘cfv 6493 (class class class)co 7361 1_oc1o 8392 Basecbs 17173 Ringcrg 20208 LModclmod 20849 LSubSpclss 20920 mPoly cmpl 21899 PwSer₁cps1 22151 Poly₁cpl1 22153

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-of 7625 df-om 7812 df-1st 7936 df-2nd 7937 df-supp 8105 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-er 8637 df-map 8769 df-ixp 8840 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-fsupp 9269 df-sup 9349 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-nn 12169 df-2 12238 df-3 12239 df-4 12240 df-5 12241 df-6 12242 df-7 12243 df-8 12244 df-9 12245 df-n0 12432 df-z 12519 df-dec 12639 df-uz 12783 df-fz 13456 df-struct 17111 df-sets 17128 df-slot 17146 df-ndx 17158 df-base 17174 df-ress 17195 df-plusg 17227 df-mulr 17228 df-sca 17230 df-vsca 17231 df-ip 17232 df-tset 17233 df-ple 17234 df-ds 17236 df-hom 17238 df-cco 17239 df-0g 17398 df-prds 17404 df-pws 17406 df-mgm 18602 df-sgrp 18681 df-mnd 18697 df-grp 18906 df-minusg 18907 df-sbg 18908 df-subg 19093 df-cmn 19751 df-abl 19752 df-mgp 20116 df-rng 20128 df-ur 20157 df-ring 20210 df-lmod 20851 df-lss 20921 df-psr 21902 df-mpl 21904 df-opsr 21906 df-psr1 22156 df-ply1 22158

This theorem is referenced by: ply1ascl0 22231 ply1ascl1 22232 ply10s0 22234 ply1tmcl 22250 coe1pwmul 22257 ply1sclf 22263 ply1scl0 22268 ply1scl1 22270 ply1idvr1OLD 22273 ply1coefsupp 22275 ply1coe 22276 cply1coe0bi 22280 gsumsmonply1 22285 gsummoncoe1 22286 lply1binomsc 22289 evls1sca 22301 evl1scvarpw 22341 evl1gsummon 22343 evls1fpws 22347 evls1vsca 22351 asclply1subcl 22352 evls1maplmhm 22355 cpmatacl 22694 cpmatinvcl 22695 mat2pmatbas 22704 mat2pmatghm 22708 mat2pmatmul 22709 decpmatid 22748 pmatcollpwscmatlem1 22767 pm2mpcl 22775 idpm2idmp 22779 mply1topmatcllem 22781 mply1topmatcl 22783 mp2pm2mplem4 22787 mp2pm2mplem5 22788 pm2mpghmlem2 22790 pm2mpghm 22794 pm2mpmhmlem1 22796 pm2mpmhmlem2 22797 monmat2matmon 22802 chpscmat 22820 chpscmatgsumbin 22822 chpscmatgsummon 22823 deg1invg 26084 deg1pwle 26098 deg1pw 26099 ply1remlem 26143 plypf1 26190 ply1lvec 33637 ressasclcl 33649 coe1mon 33665 ply1coedeg 33667 deg1vr 33670 ply1degltlss 33674 gsummoncoe1fzo 33675 q1pvsca 33682 r1pvsca 33683 r1p0 33684 r1plmhm 33688 vietalem 33741 irngnzply1lem 33853 extdgfialglem2 33856 2sqr3minply 33943 cos9thpiminplylem6 33950 cos9thpiminply 33951 aks5lem2 42643 ply1vr1smo 48874 ply1mulgsumlem4 48880 ply1mulgsum 48881

W3C validator