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 22463

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 2765	. . 3 ⊢ (PwSer₁‘𝑅) = (PwSer₁‘𝑅)
2	1	psr1lmod 22460	. 2 ⊢ (𝑅 ∈ Ring → (PwSer₁‘𝑅) ∈ LMod)
3		eqid 2765	. . . 4 ⊢ (Poly₁‘𝑅) = (Poly₁‘𝑅)
4		eqid 2765	. . . 4 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(Poly₁‘𝑅))
5	3, 4	ply1bas 22407	. . 3 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(1_o mPoly 𝑅))
6	3, 1, 4	ply1lss 22408	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘(Poly₁‘𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
7	5, 6	eqeltrrid 2870	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
8		ply1lmod.p	. . . 4 ⊢ 𝑃 = (Poly₁‘𝑅)
9	8, 1	ply1val 22406	. . 3 ⊢ 𝑃 = ((PwSer₁‘𝑅) ↾_s (Base‘(1_o mPoly 𝑅)))
10		eqid 2765	. . 3 ⊢ (LSubSp‘(PwSer₁‘𝑅)) = (LSubSp‘(PwSer₁‘𝑅))
11	9, 10	lsslmod 21133	. 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 2146 ‘cfv 6540 (class class class)co 7419 1_oc1o 8452 Basecbs 17293 Ringcrg 20361 LModclmod 21033 LSubSpclss 21104 mPoly cmpl 22108 PwSer₁cps1 22387 Poly₁cpl1 22389

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-cnex 11173 ax-resscn 11174 ax-1cn 11175 ax-icn 11176 ax-addcl 11177 ax-addrcl 11178 ax-mulcl 11179 ax-mulrcl 11180 ax-mulcom 11181 ax-addass 11182 ax-mulass 11183 ax-distr 11184 ax-i2m1 11185 ax-1ne0 11186 ax-1rid 11187 ax-rnegex 11188 ax-rrecex 11189 ax-cnre 11190 ax-pre-lttri 11191 ax-pre-lttrn 11192 ax-pre-ltadd 11193 ax-pre-mulgt0 11194

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 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-of 7684 df-om 7869 df-1st 7992 df-2nd 7993 df-supp 8163 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-er 8700 df-map 8832 df-ixp 8902 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-fsupp 9329 df-sup 9409 df-pnf 11262 df-mnf 11263 df-xr 11264 df-ltxr 11265 df-le 11266 df-sub 11460 df-neg 11461 df-nn 12251 df-2 12320 df-3 12321 df-4 12322 df-5 12323 df-6 12324 df-7 12325 df-8 12326 df-9 12327 df-n0 12522 df-z 12609 df-dec 12730 df-uz 12881 df-fz 13554 df-struct 17231 df-sets 17248 df-slot 17266 df-ndx 17278 df-base 17294 df-ress 17315 df-plusg 17347 df-mulr 17348 df-sca 17350 df-vsca 17351 df-ip 17352 df-tset 17353 df-ple 17354 df-ds 17356 df-hom 17358 df-cco 17359 df-0g 17518 df-prds 17524 df-pws 17526 df-mgm 18722 df-sgrp 18811 df-mnd 18827 df-grp 19049 df-minusg 19050 df-sbg 19051 df-subg 19235 df-cmn 19898 df-abl 19899 df-mgp 20263 df-rng 20277 df-ur 20310 df-ring 20363 df-lmod 21035 df-lss 21105 df-psr 22111 df-mpl 22113 df-opsr 22115 df-psr1 22392 df-ply1 22394

This theorem is used by: ply1ascl0 22466 ply1ascl1 22467 ply10s0 22469 ply1tmcl 22485 coe1pwmul 22492 ply1sclf 22498 ply1scl0 22503 ply1scl1 22505 ply1coefsupp 22509 ply1coe 22510 cply1coe0bi 22514 gsumsmonply1 22519 gsummoncoe1 22520 lply1binomsc 22523 evls1sca 22535 evl1scvarpw 22575 evl1gsummon 22577 evls1fpws 22581 evls1vsca 22585 asclply1subcl 22586 evls1maplmhm 22589 cpmatacl 22925 cpmatinvcl 22926 mat2pmatbas 22935 mat2pmatghm 22939 mat2pmatmul 22940 decpmatid 22979 pmatcollpwscmatlem1 22998 pm2mpcl 23006 idpm2idmp 23010 mply1topmatcllem 23012 mply1topmatcl 23014 mp2pm2mplem4 23018 mp2pm2mplem5 23019 pm2mpghmlem2 23021 pm2mpghm 23025 pm2mpmhmlem1 23027 pm2mpmhmlem2 23028 monmat2matmon 23033 chpscmat 23051 chpscmatgsumbin 23053 chpscmatgsummon 23054 deg1invg 26316 deg1pwle 26330 deg1pw 26331 ply1remlem 26375 plypf1 26422 ply1lvec 33915 ressasclcl 33927 coe1mon 33943 ply1coedeg 33945 deg1vr 33948 ply1degltlss 33952 gsummoncoe1fzo 33953 q1pvsca 33960 r1pvsca 33961 r1p0 33962 r1plmhm 33965 vietalem 34035 irngnzply1lem 34146 extdgfialglem2 34149 2sqr3minply 34236 cos9thpiminplylem6 34243 cos9thpiminply 34244 aks5lem2 43014 ply1vr1smo 49222 ply1mulgsumlem4 49228 ply1mulgsum 49229

W3C validator