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 22581

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 2763	. . 3 ⊢ (PwSer₁‘𝑅) = (PwSer₁‘𝑅)
2	1	psr1lmod 22578	. 2 ⊢ (𝑅 ∈ Ring → (PwSer₁‘𝑅) ∈ LMod)
3		eqid 2763	. . . 4 ⊢ (Poly₁‘𝑅) = (Poly₁‘𝑅)
4		eqid 2763	. . . 4 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(Poly₁‘𝑅))
5	3, 4	ply1bas 22525	. . 3 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(1_o mPoly 𝑅))
6	3, 1, 4	ply1lss 22526	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘(Poly₁‘𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
7	5, 6	eqeltrrid 2868	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
8		ply1lmod.p	. . . 4 ⊢ 𝑃 = (Poly₁‘𝑅)
9	8, 1	ply1val 22524	. . 3 ⊢ 𝑃 = ((PwSer₁‘𝑅) ↾_s (Base‘(1_o mPoly 𝑅)))
10		eqid 2763	. . 3 ⊢ (LSubSp‘(PwSer₁‘𝑅)) = (LSubSp‘(PwSer₁‘𝑅))
11	9, 10	lsslmod 21247	. 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 1569 ∈ wcel 2146 ‘cfv 6546 (class class class)co 7427 1_oc1o 8480 Basecbs 17399 Ringcrg 20471 LModclmod 21147 LSubSpclss 21218 mPoly cmpl 22226 PwSer₁cps1 22505 Poly₁cpl1 22507

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2196 ax-12 2215 ax-ext 2735 ax-rep 5234 ax-sep 5251 ax-nul 5262 ax-pow 5330 ax-pr 5394 ax-un 7758 ax-cnex 11266 ax-resscn 11267 ax-1cn 11268 ax-icn 11269 ax-addcl 11270 ax-addrcl 11271 ax-mulcl 11272 ax-mulrcl 11273 ax-mulcom 11274 ax-addass 11275 ax-mulass 11276 ax-distr 11277 ax-i2m1 11278 ax-1ne0 11279 ax-1rid 11280 ax-rnegex 11281 ax-rrecex 11282 ax-cnre 11283 ax-pre-lttri 11284 ax-pre-lttrn 11285 ax-pre-ltadd 11286 ax-pre-mulgt0 11287

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2101 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3455 df-sbc 3742 df-csb 3851 df-ss 3900 df-pss 4016 df-dif 4049 df-in 4093 df-un 4153 df-nul 4281 df-if 4485 df-pw 4561 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4838 df-uni 4870 df-iun 4955 df-br 5106 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5549 df-eprel 5554 df-po 5562 df-so 5563 df-fr 5607 df-we 5609 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6310 df-ord 6371 df-on 6372 df-lim 6373 df-suc 6374 df-iota 6500 df-fun 6548 df-fn 6549 df-f 6550 df-f1 6551 df-fo 6552 df-f1o 6553 df-fv 6554 df-riota 7384 df-ov 7430 df-oprab 7431 df-mpo 7432 df-of 7700 df-om 7885 df-1st 8008 df-2nd 8009 df-supp 8188 df-frecs 8310 df-wrecs 8341 df-recs 8390 df-rdg 8429 df-1o 8487 df-er 8728 df-map 8860 df-ixp 8937 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-fsupp 9365 df-sup 9444 df-pnf 11355 df-mnf 11356 df-xr 11357 df-ltxr 11358 df-le 11359 df-sub 11553 df-neg 11554 df-nn 12346 df-2 12415 df-3 12416 df-4 12417 df-5 12418 df-6 12419 df-7 12420 df-8 12421 df-9 12422 df-n0 12617 df-z 12704 df-dec 12825 df-uz 12976 df-fz 13650 df-struct 17337 df-sets 17354 df-slot 17372 df-ndx 17384 df-base 17400 df-ress 17421 df-plusg 17453 df-mulr 17454 df-sca 17456 df-vsca 17457 df-ip 17458 df-tset 17459 df-ple 17460 df-ds 17462 df-hom 17464 df-cco 17465 df-0g 17624 df-prds 17630 df-pws 17632 df-mgm 18828 df-sgrp 18920 df-mnd 18936 df-grp 19159 df-minusg 19160 df-sbg 19161 df-subg 19345 df-cmn 20008 df-abl 20009 df-mgp 20373 df-rng 20387 df-ur 20420 df-ring 20473 df-lmod 21149 df-lss 21219 df-psr 22229 df-mpl 22231 df-opsr 22233 df-psr1 22510 df-ply1 22512

This theorem is used by: ply1ascl0 22584 ply1ascl1 22585 ply10s0 22587 ply1tmcl 22603 coe1pwmul 22610 ply1sclf 22616 ply1scl0 22621 ply1scl1 22623 ply1coefsupp 22627 ply1coe 22628 cply1coe0bi 22632 gsumsmonply1 22637 gsummoncoe1 22638 lply1binomsc 22641 evls1sca 22653 evl1scvarpw 22693 evl1gsummon 22695 evls1fpws 22699 evls1vsca 22703 asclply1subcl 22704 evls1maplmhm 22707 cpmatacl 23046 cpmatinvcl 23047 mat2pmatbas 23056 mat2pmatghm 23060 mat2pmatmul 23061 decpmatid 23100 pmatcollpwscmatlem1 23119 pm2mpcl 23127 idpm2idmp 23131 mply1topmatcllem 23133 mply1topmatcl 23135 mp2pm2mplem4 23139 mp2pm2mplem5 23140 pm2mpghmlem2 23142 pm2mpghm 23146 pm2mpmhmlem1 23148 pm2mpmhmlem2 23149 monmat2matmon 23154 chpscmat 23172 chpscmatgsumbin 23174 chpscmatgsummon 23175 deg1invg 26436 deg1pwle 26450 deg1pw 26451 ply1remlem 26495 plypf1 26543 ply1lvec 34144 ressasclcl 34156 coe1mon 34172 ply1coedeg 34174 deg1vr 34177 ply1degltlss 34181 gsummoncoe1fzo 34182 q1pvsca 34189 r1pvsca 34190 r1p0 34191 r1plmhm 34194 vietalem 34264 irngnzply1lem 34375 extdgfialglem2 34378 2sqr3minply 34465 cos9thpiminplylem6 34472 cos9thpiminply 34473 aks5lem2 43377 ply1vr1smo 49634 ply1mulgsumlem4 49640 ply1mulgsum 49641

W3C validator