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 22479

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 2760	. . 3 ⊢ (PwSer₁‘𝑅) = (PwSer₁‘𝑅)
2	1	psr1lmod 22476	. 2 ⊢ (𝑅 ∈ Ring → (PwSer₁‘𝑅) ∈ LMod)
3		eqid 2760	. . . 4 ⊢ (Poly₁‘𝑅) = (Poly₁‘𝑅)
4		eqid 2760	. . . 4 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(Poly₁‘𝑅))
5	3, 4	ply1bas 22423	. . 3 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(1_o mPoly 𝑅))
6	3, 1, 4	ply1lss 22424	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘(Poly₁‘𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
7	5, 6	eqeltrrid 2865	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
8		ply1lmod.p	. . . 4 ⊢ 𝑃 = (Poly₁‘𝑅)
9	8, 1	ply1val 22422	. . 3 ⊢ 𝑃 = ((PwSer₁‘𝑅) ↾_s (Base‘(1_o mPoly 𝑅)))
10		eqid 2760	. . 3 ⊢ (LSubSp‘(PwSer₁‘𝑅)) = (LSubSp‘(PwSer₁‘𝑅))
11	9, 10	lsslmod 21147	. 2 ⊢ (((PwSer₁‘𝑅) ∈ LMod ∧ (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅))) → 𝑃 ∈ LMod)
12	2, 7, 11	syl2anc 596	1 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1570 ∈ wcel 2145 ‘cfv 6533 (class class class)co 7414 1_oc1o 8451 Basecbs 17304 Ringcrg 20375 LModclmod 21047 LSubSpclss 21118 mPoly cmpl 22124 PwSer₁cps1 22403 Poly₁cpl1 22405

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-of 7679 df-om 7864 df-1st 7987 df-2nd 7988 df-supp 8160 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8458 df-er 8699 df-map 8831 df-ixp 8908 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-fsupp 9335 df-sup 9415 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-z 12619 df-dec 12740 df-uz 12891 df-fz 13565 df-struct 17242 df-sets 17259 df-slot 17277 df-ndx 17289 df-base 17305 df-ress 17326 df-plusg 17358 df-mulr 17359 df-sca 17361 df-vsca 17362 df-ip 17363 df-tset 17364 df-ple 17365 df-ds 17367 df-hom 17369 df-cco 17370 df-0g 17529 df-prds 17535 df-pws 17537 df-mgm 18733 df-sgrp 18824 df-mnd 18840 df-grp 19063 df-minusg 19064 df-sbg 19065 df-subg 19249 df-cmn 19912 df-abl 19913 df-mgp 20277 df-rng 20291 df-ur 20324 df-ring 20377 df-lmod 21049 df-lss 21119 df-psr 22127 df-mpl 22129 df-opsr 22131 df-psr1 22408 df-ply1 22410

This theorem is used by: ply1ascl0 22482 ply1ascl1 22483 ply10s0 22485 ply1tmcl 22501 coe1pwmul 22508 ply1sclf 22514 ply1scl0 22519 ply1scl1 22521 ply1coefsupp 22525 ply1coe 22526 cply1coe0bi 22530 gsumsmonply1 22535 gsummoncoe1 22536 lply1binomsc 22539 evls1sca 22551 evl1scvarpw 22591 evl1gsummon 22593 evls1fpws 22597 evls1vsca 22601 asclply1subcl 22602 evls1maplmhm 22605 cpmatacl 22944 cpmatinvcl 22945 mat2pmatbas 22954 mat2pmatghm 22958 mat2pmatmul 22959 decpmatid 22998 pmatcollpwscmatlem1 23017 pm2mpcl 23025 idpm2idmp 23029 mply1topmatcllem 23031 mply1topmatcl 23033 mp2pm2mplem4 23037 mp2pm2mplem5 23038 pm2mpghmlem2 23040 pm2mpghm 23044 pm2mpmhmlem1 23046 pm2mpmhmlem2 23047 monmat2matmon 23052 chpscmat 23070 chpscmatgsumbin 23072 chpscmatgsummon 23073 deg1invg 26334 deg1pwle 26348 deg1pw 26349 ply1remlem 26393 plypf1 26441 ply1lvec 33972 ressasclcl 33984 coe1mon 34000 ply1coedeg 34002 deg1vr 34005 ply1degltlss 34009 gsummoncoe1fzo 34010 q1pvsca 34017 r1pvsca 34018 r1p0 34019 r1plmhm 34022 vietalem 34092 irngnzply1lem 34203 extdgfialglem2 34206 2sqr3minply 34293 cos9thpiminplylem6 34300 cos9thpiminply 34301 aks5lem2 43056 ply1vr1smo 49316 ply1mulgsumlem4 49322 ply1mulgsum 49323

W3C validator