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 22207

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 2737	. . 3 ⊢ (PwSer₁‘𝑅) = (PwSer₁‘𝑅)
2	1	psr1lmod 22204	. 2 ⊢ (𝑅 ∈ Ring → (PwSer₁‘𝑅) ∈ LMod)
3		eqid 2737	. . . 4 ⊢ (Poly₁‘𝑅) = (Poly₁‘𝑅)
4		eqid 2737	. . . 4 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(Poly₁‘𝑅))
5	3, 4	ply1bas 22150	. . 3 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(1_o mPoly 𝑅))
6	3, 1, 4	ply1lss 22152	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘(Poly₁‘𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
7	5, 6	eqeltrrid 2842	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
8		ply1lmod.p	. . . 4 ⊢ 𝑃 = (Poly₁‘𝑅)
9	8, 1	ply1val 22149	. . 3 ⊢ 𝑃 = ((PwSer₁‘𝑅) ↾_s (Base‘(1_o mPoly 𝑅)))
10		eqid 2737	. . 3 ⊢ (LSubSp‘(PwSer₁‘𝑅)) = (LSubSp‘(PwSer₁‘𝑅))
11	9, 10	lsslmod 20926	. 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 6500 (class class class)co 7368 1_oc1o 8400 Basecbs 17148 Ringcrg 20183 LModclmod 20826 LSubSpclss 20897 mPoly cmpl 21877 PwSer₁cps1 22130 Poly₁cpl1 22132

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 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 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 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-of 7632 df-om 7819 df-1st 7943 df-2nd 7944 df-supp 8113 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-er 8645 df-map 8777 df-ixp 8848 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9277 df-sup 9357 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-nn 12158 df-2 12220 df-3 12221 df-4 12222 df-5 12223 df-6 12224 df-7 12225 df-8 12226 df-9 12227 df-n0 12414 df-z 12501 df-dec 12620 df-uz 12764 df-fz 13436 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17149 df-ress 17170 df-plusg 17202 df-mulr 17203 df-sca 17205 df-vsca 17206 df-ip 17207 df-tset 17208 df-ple 17209 df-ds 17211 df-hom 17213 df-cco 17214 df-0g 17373 df-prds 17379 df-pws 17381 df-mgm 18577 df-sgrp 18656 df-mnd 18672 df-grp 18881 df-minusg 18882 df-sbg 18883 df-subg 19068 df-cmn 19726 df-abl 19727 df-mgp 20091 df-rng 20103 df-ur 20132 df-ring 20185 df-lmod 20828 df-lss 20898 df-psr 21880 df-mpl 21882 df-opsr 21884 df-psr1 22135 df-ply1 22137

This theorem is referenced by: ply1ascl0 22210 ply1ascl1 22211 ply10s0 22213 ply1tmcl 22229 coe1pwmul 22236 ply1sclf 22242 ply1scl0 22247 ply1scl0OLD 22248 ply1scl1 22250 ply1scl1OLD 22251 ply1idvr1OLD 22254 ply1coefsupp 22256 ply1coe 22257 cply1coe0bi 22261 gsumsmonply1 22266 gsummoncoe1 22267 lply1binomsc 22270 evls1sca 22282 evl1scvarpw 22322 evl1gsummon 22324 evls1fpws 22328 evls1vsca 22332 asclply1subcl 22333 evls1maplmhm 22336 cpmatacl 22675 cpmatinvcl 22676 mat2pmatbas 22685 mat2pmatghm 22689 mat2pmatmul 22690 decpmatid 22729 pmatcollpwscmatlem1 22748 pm2mpcl 22756 idpm2idmp 22760 mply1topmatcllem 22762 mply1topmatcl 22764 mp2pm2mplem4 22768 mp2pm2mplem5 22769 pm2mpghmlem2 22771 pm2mpghm 22775 pm2mpmhmlem1 22777 pm2mpmhmlem2 22778 monmat2matmon 22783 chpscmat 22801 chpscmatgsumbin 22803 chpscmatgsummon 22804 deg1invg 26082 deg1pwle 26096 deg1pw 26097 ply1remlem 26141 plypf1 26188 ply1lvec 33656 ressasclcl 33668 coe1mon 33684 ply1coedeg 33686 deg1vr 33689 ply1degltlss 33693 gsummoncoe1fzo 33694 q1pvsca 33701 r1pvsca 33702 r1p0 33703 r1plmhm 33707 vietalem 33760 irngnzply1lem 33872 extdgfialglem2 33875 2sqr3minply 33962 cos9thpiminplylem6 33969 cos9thpiminply 33970 aks5lem2 42561 ply1vr1smo 48747 ply1mulgsumlem4 48753 ply1mulgsum 48754

W3C validator