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 22215

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 2736	. . 3 ⊢ (PwSer₁‘𝑅) = (PwSer₁‘𝑅)
2	1	psr1lmod 22212	. 2 ⊢ (𝑅 ∈ Ring → (PwSer₁‘𝑅) ∈ LMod)
3		eqid 2736	. . . 4 ⊢ (Poly₁‘𝑅) = (Poly₁‘𝑅)
4		eqid 2736	. . . 4 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(Poly₁‘𝑅))
5	3, 4	ply1bas 22158	. . 3 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(1_o mPoly 𝑅))
6	3, 1, 4	ply1lss 22160	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘(Poly₁‘𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
7	5, 6	eqeltrrid 2841	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
8		ply1lmod.p	. . . 4 ⊢ 𝑃 = (Poly₁‘𝑅)
9	8, 1	ply1val 22157	. . 3 ⊢ 𝑃 = ((PwSer₁‘𝑅) ↾_s (Base‘(1_o mPoly 𝑅)))
10		eqid 2736	. . 3 ⊢ (LSubSp‘(PwSer₁‘𝑅)) = (LSubSp‘(PwSer₁‘𝑅))
11	9, 10	lsslmod 20955	. 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 6498 (class class class)co 7367 1_oc1o 8398 Basecbs 17179 Ringcrg 20214 LModclmod 20855 LSubSpclss 20926 mPoly cmpl 21886 PwSer₁cps1 22138 Poly₁cpl1 22140

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 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

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 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4851 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-of 7631 df-om 7818 df-1st 7942 df-2nd 7943 df-supp 8111 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-er 8643 df-map 8775 df-ixp 8846 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-fsupp 9275 df-sup 9355 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-nn 12175 df-2 12244 df-3 12245 df-4 12246 df-5 12247 df-6 12248 df-7 12249 df-8 12250 df-9 12251 df-n0 12438 df-z 12525 df-dec 12645 df-uz 12789 df-fz 13462 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-hom 17244 df-cco 17245 df-0g 17404 df-prds 17410 df-pws 17412 df-mgm 18608 df-sgrp 18687 df-mnd 18703 df-grp 18912 df-minusg 18913 df-sbg 18914 df-subg 19099 df-cmn 19757 df-abl 19758 df-mgp 20122 df-rng 20134 df-ur 20163 df-ring 20216 df-lmod 20857 df-lss 20927 df-psr 21889 df-mpl 21891 df-opsr 21893 df-psr1 22143 df-ply1 22145

This theorem is referenced by: ply1ascl0 22218 ply1ascl1 22219 ply10s0 22221 ply1tmcl 22237 coe1pwmul 22244 ply1sclf 22250 ply1scl0 22255 ply1scl1 22257 ply1idvr1OLD 22260 ply1coefsupp 22262 ply1coe 22263 cply1coe0bi 22267 gsumsmonply1 22272 gsummoncoe1 22273 lply1binomsc 22276 evls1sca 22288 evl1scvarpw 22328 evl1gsummon 22330 evls1fpws 22334 evls1vsca 22338 asclply1subcl 22339 evls1maplmhm 22342 cpmatacl 22681 cpmatinvcl 22682 mat2pmatbas 22691 mat2pmatghm 22695 mat2pmatmul 22696 decpmatid 22735 pmatcollpwscmatlem1 22754 pm2mpcl 22762 idpm2idmp 22766 mply1topmatcllem 22768 mply1topmatcl 22770 mp2pm2mplem4 22774 mp2pm2mplem5 22775 pm2mpghmlem2 22777 pm2mpghm 22781 pm2mpmhmlem1 22783 pm2mpmhmlem2 22784 monmat2matmon 22789 chpscmat 22807 chpscmatgsumbin 22809 chpscmatgsummon 22810 deg1invg 26071 deg1pwle 26085 deg1pw 26086 ply1remlem 26130 plypf1 26177 ply1lvec 33619 ressasclcl 33631 coe1mon 33647 ply1coedeg 33649 deg1vr 33652 ply1degltlss 33656 gsummoncoe1fzo 33657 q1pvsca 33664 r1pvsca 33665 r1p0 33666 r1plmhm 33670 vietalem 33723 irngnzply1lem 33834 extdgfialglem2 33837 2sqr3minply 33924 cos9thpiminplylem6 33931 cos9thpiminply 33932 aks5lem2 42626 ply1vr1smo 48859 ply1mulgsumlem4 48865 ply1mulgsum 48866

W3C validator