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 22164

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 2731	. . 3 ⊢ (PwSer₁‘𝑅) = (PwSer₁‘𝑅)
2	1	psr1lmod 22161	. 2 ⊢ (𝑅 ∈ Ring → (PwSer₁‘𝑅) ∈ LMod)
3		eqid 2731	. . . 4 ⊢ (Poly₁‘𝑅) = (Poly₁‘𝑅)
4		eqid 2731	. . . 4 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(Poly₁‘𝑅))
5	3, 4	ply1bas 22107	. . 3 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(1_o mPoly 𝑅))
6	3, 1, 4	ply1lss 22109	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘(Poly₁‘𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
7	5, 6	eqeltrrid 2836	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
8		ply1lmod.p	. . . 4 ⊢ 𝑃 = (Poly₁‘𝑅)
9	8, 1	ply1val 22106	. . 3 ⊢ 𝑃 = ((PwSer₁‘𝑅) ↾_s (Base‘(1_o mPoly 𝑅)))
10		eqid 2731	. . 3 ⊢ (LSubSp‘(PwSer₁‘𝑅)) = (LSubSp‘(PwSer₁‘𝑅))
11	9, 10	lsslmod 20893	. 2 ⊢ (((PwSer₁‘𝑅) ∈ LMod ∧ (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅))) → 𝑃 ∈ LMod)
12	2, 7, 11	syl2anc 584	1 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2111 ‘cfv 6481 (class class class)co 7346 1_oc1o 8378 Basecbs 17120 Ringcrg 20151 LModclmod 20793 LSubSpclss 20864 mPoly cmpl 21843 PwSer₁cps1 22087 Poly₁cpl1 22089

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-tp 4578 df-op 4580 df-uni 4857 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-of 7610 df-om 7797 df-1st 7921 df-2nd 7922 df-supp 8091 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-er 8622 df-map 8752 df-ixp 8822 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-fsupp 9246 df-sup 9326 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-nn 12126 df-2 12188 df-3 12189 df-4 12190 df-5 12191 df-6 12192 df-7 12193 df-8 12194 df-9 12195 df-n0 12382 df-z 12469 df-dec 12589 df-uz 12733 df-fz 13408 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-sca 17177 df-vsca 17178 df-ip 17179 df-tset 17180 df-ple 17181 df-ds 17183 df-hom 17185 df-cco 17186 df-0g 17345 df-prds 17351 df-pws 17353 df-mgm 18548 df-sgrp 18627 df-mnd 18643 df-grp 18849 df-minusg 18850 df-sbg 18851 df-subg 19036 df-cmn 19694 df-abl 19695 df-mgp 20059 df-rng 20071 df-ur 20100 df-ring 20153 df-lmod 20795 df-lss 20865 df-psr 21846 df-mpl 21848 df-opsr 21850 df-psr1 22092 df-ply1 22094

This theorem is referenced by: ply1ascl0 22167 ply1ascl1 22168 ply10s0 22170 ply1tmcl 22186 coe1pwmul 22193 ply1sclf 22199 ply1scl0 22204 ply1scl0OLD 22205 ply1scl1 22207 ply1scl1OLD 22208 ply1idvr1OLD 22210 ply1coefsupp 22212 ply1coe 22213 cply1coe0bi 22217 gsumsmonply1 22222 gsummoncoe1 22223 lply1binomsc 22226 evls1sca 22238 evl1scvarpw 22278 evl1gsummon 22280 evls1fpws 22284 evls1vsca 22288 asclply1subcl 22289 evls1maplmhm 22292 cpmatacl 22631 cpmatinvcl 22632 mat2pmatbas 22641 mat2pmatghm 22645 mat2pmatmul 22646 decpmatid 22685 pmatcollpwscmatlem1 22704 pm2mpcl 22712 idpm2idmp 22716 mply1topmatcllem 22718 mply1topmatcl 22720 mp2pm2mplem4 22724 mp2pm2mplem5 22725 pm2mpghmlem2 22727 pm2mpghm 22731 pm2mpmhmlem1 22733 pm2mpmhmlem2 22734 monmat2matmon 22739 chpscmat 22757 chpscmatgsumbin 22759 chpscmatgsummon 22760 deg1invg 26038 deg1pwle 26052 deg1pw 26053 ply1remlem 26097 plypf1 26144 ply1lvec 33522 ressasclcl 33534 coe1mon 33549 deg1vr 33553 ply1degltlss 33557 gsummoncoe1fzo 33558 q1pvsca 33564 r1pvsca 33565 r1p0 33566 r1plmhm 33570 irngnzply1lem 33703 extdgfialglem2 33706 2sqr3minply 33793 cos9thpiminplylem6 33800 cos9thpiminply 33801 aks5lem2 42290 ply1vr1smo 48493 ply1mulgsumlem4 48500 ply1mulgsum 48501

W3C validator