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 22169

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 2729	. . 3 ⊢ (PwSer₁‘𝑅) = (PwSer₁‘𝑅)
2	1	psr1lmod 22166	. 2 ⊢ (𝑅 ∈ Ring → (PwSer₁‘𝑅) ∈ LMod)
3		eqid 2729	. . . 4 ⊢ (Poly₁‘𝑅) = (Poly₁‘𝑅)
4		eqid 2729	. . . 4 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(Poly₁‘𝑅))
5	3, 4	ply1bas 22112	. . 3 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(1_o mPoly 𝑅))
6	3, 1, 4	ply1lss 22114	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘(Poly₁‘𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
7	5, 6	eqeltrrid 2833	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
8		ply1lmod.p	. . . 4 ⊢ 𝑃 = (Poly₁‘𝑅)
9	8, 1	ply1val 22111	. . 3 ⊢ 𝑃 = ((PwSer₁‘𝑅) ↾_s (Base‘(1_o mPoly 𝑅)))
10		eqid 2729	. . 3 ⊢ (LSubSp‘(PwSer₁‘𝑅)) = (LSubSp‘(PwSer₁‘𝑅))
11	9, 10	lsslmod 20898	. 2 ⊢ (((PwSer₁‘𝑅) ∈ LMod ∧ (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅))) → 𝑃 ∈ LMod)
12	2, 7, 11	syl2anc 584	1 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2109 ‘cfv 6499 (class class class)co 7369 1_oc1o 8404 Basecbs 17155 Ringcrg 20153 LModclmod 20798 LSubSpclss 20869 mPoly cmpl 21848 PwSer₁cps1 22092 Poly₁cpl1 22094

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 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 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-of 7633 df-om 7823 df-1st 7947 df-2nd 7948 df-supp 8117 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-er 8648 df-map 8778 df-ixp 8848 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9289 df-sup 9369 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-nn 12163 df-2 12225 df-3 12226 df-4 12227 df-5 12228 df-6 12229 df-7 12230 df-8 12231 df-9 12232 df-n0 12419 df-z 12506 df-dec 12626 df-uz 12770 df-fz 13445 df-struct 17093 df-sets 17110 df-slot 17128 df-ndx 17140 df-base 17156 df-ress 17177 df-plusg 17209 df-mulr 17210 df-sca 17212 df-vsca 17213 df-ip 17214 df-tset 17215 df-ple 17216 df-ds 17218 df-hom 17220 df-cco 17221 df-0g 17380 df-prds 17386 df-pws 17388 df-mgm 18549 df-sgrp 18628 df-mnd 18644 df-grp 18850 df-minusg 18851 df-sbg 18852 df-subg 19037 df-cmn 19696 df-abl 19697 df-mgp 20061 df-rng 20073 df-ur 20102 df-ring 20155 df-lmod 20800 df-lss 20870 df-psr 21851 df-mpl 21853 df-opsr 21855 df-psr1 22097 df-ply1 22099

This theorem is referenced by: ply1ascl0 22172 ply1ascl1 22173 ply10s0 22175 ply1tmcl 22191 coe1pwmul 22198 ply1sclf 22204 ply1scl0 22209 ply1scl0OLD 22210 ply1scl1 22212 ply1scl1OLD 22213 ply1idvr1OLD 22215 ply1coefsupp 22217 ply1coe 22218 cply1coe0bi 22222 gsumsmonply1 22227 gsummoncoe1 22228 lply1binomsc 22231 evls1sca 22243 evl1scvarpw 22283 evl1gsummon 22285 evls1fpws 22289 evls1vsca 22293 asclply1subcl 22294 evls1maplmhm 22297 cpmatacl 22636 cpmatinvcl 22637 mat2pmatbas 22646 mat2pmatghm 22650 mat2pmatmul 22651 decpmatid 22690 pmatcollpwscmatlem1 22709 pm2mpcl 22717 idpm2idmp 22721 mply1topmatcllem 22723 mply1topmatcl 22725 mp2pm2mplem4 22729 mp2pm2mplem5 22730 pm2mpghmlem2 22732 pm2mpghm 22736 pm2mpmhmlem1 22738 pm2mpmhmlem2 22739 monmat2matmon 22744 chpscmat 22762 chpscmatgsumbin 22764 chpscmatgsummon 22765 deg1invg 26044 deg1pwle 26058 deg1pw 26059 ply1remlem 26103 plypf1 26150 ply1lvec 33521 ressasclcl 33533 coe1mon 33547 deg1vr 33551 ply1degltlss 33555 gsummoncoe1fzo 33556 q1pvsca 33562 r1pvsca 33563 r1p0 33564 r1plmhm 33568 irngnzply1lem 33678 2sqr3minply 33763 cos9thpiminplylem6 33770 cos9thpiminply 33771 aks5lem2 42168 ply1vr1smo 48364 ply1mulgsumlem4 48371 ply1mulgsum 48372

W3C validator