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 22624

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 22621	. 2 ⊢ (𝑅 ∈ Ring → (PwSer₁‘𝑅) ∈ LMod)
3		eqid 2763	. . . 4 ⊢ (Poly₁‘𝑅) = (Poly₁‘𝑅)
4		eqid 2763	. . . 4 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(Poly₁‘𝑅))
5	3, 4	ply1bas 22568	. . 3 ⊢ (Base‘(Poly₁‘𝑅)) = (Base‘(1_o mPoly 𝑅))
6	3, 1, 4	ply1lss 22569	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘(Poly₁‘𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
7	5, 6	eqeltrrid 2869	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1_o mPoly 𝑅)) ∈ (LSubSp‘(PwSer₁‘𝑅)))
8		ply1lmod.p	. . . 4 ⊢ 𝑃 = (Poly₁‘𝑅)
9	8, 1	ply1val 22567	. . 3 ⊢ 𝑃 = ((PwSer₁‘𝑅) ↾_s (Base‘(1_o mPoly 𝑅)))
10		eqid 2763	. . 3 ⊢ (LSubSp‘(PwSer₁‘𝑅)) = (LSubSp‘(PwSer₁‘𝑅))
11	9, 10	lsslmod 21286	. 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 2147 ‘cfv 6566 (class class class)co 7451 1_oc1o 8507 Basecbs 17431 Ringcrg 20510 LModclmod 21186 LSubSpclss 21257 mPoly cmpl 22269 PwSer₁cps1 22548 Poly₁cpl1 22550

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4841 df-uni 4873 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-of 7725 df-om 7912 df-1st 8035 df-2nd 8036 df-supp 8215 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-er 8755 df-map 8887 df-ixp 8964 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-fsupp 9392 df-sup 9471 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-nn 12376 df-2 12445 df-3 12446 df-4 12447 df-5 12448 df-6 12449 df-7 12450 df-8 12451 df-9 12452 df-n0 12647 df-z 12734 df-dec 12855 df-uz 13006 df-fz 13680 df-struct 17369 df-sets 17386 df-slot 17404 df-ndx 17416 df-base 17432 df-ress 17453 df-plusg 17486 df-mulr 17487 df-sca 17489 df-vsca 17490 df-ip 17491 df-tset 17492 df-ple 17493 df-ds 17495 df-hom 17497 df-cco 17498 df-0g 17662 df-prds 17668 df-pws 17670 df-mgm 18866 df-sgrp 18958 df-mnd 18974 df-grp 19197 df-minusg 19198 df-sbg 19199 df-subg 19383 df-cmn 20047 df-abl 20048 df-mgp 20412 df-rng 20426 df-ur 20459 df-ring 20512 df-lmod 21188 df-lss 21258 df-psr 22272 df-mpl 22274 df-opsr 22276 df-psr1 22553 df-ply1 22555

This theorem is used by: ply1ascl0 22627 ply1ascl1 22628 ply10s0 22630 ply1tmcl 22646 coe1pwmul 22653 ply1sclf 22659 ply1scl0 22664 ply1scl1 22666 ply1coefsupp 22670 ply1coe 22671 cply1coe0bi 22675 gsumsmonply1 22680 gsummoncoe1 22681 lply1binomsc 22684 evls1sca 22696 evl1scvarpw 22736 evl1gsummon 22738 evls1fpws 22742 evls1vsca 22746 asclply1subcl 22747 evls1maplmhm 22750 cpmatacl 23089 cpmatinvcl 23090 mat2pmatbas 23099 mat2pmatghm 23103 mat2pmatmul 23104 decpmatid 23143 pmatcollpwscmatlem1 23162 pm2mpcl 23170 idpm2idmp 23174 mply1topmatcllem 23176 mply1topmatcl 23178 mp2pm2mplem4 23182 mp2pm2mplem5 23183 pm2mpghmlem2 23185 pm2mpghm 23189 pm2mpmhmlem1 23191 pm2mpmhmlem2 23192 monmat2matmon 23197 chpscmat 23215 chpscmatgsumbin 23217 chpscmatgsummon 23218 deg1invg 26479 deg1pwle 26493 deg1pw 26494 ply1remlem 26538 plypf1 26586 ply1lvec 34194 ressasclcl 34206 coe1mon 34222 ply1coedeg 34224 deg1vr 34227 ply1degltlss 34231 gsummoncoe1fzo 34232 q1pvsca 34241 r1pvsca 34242 r1p0 34243 r1plmhm 34246 rngunsnply1chr2lem1 34250 rngunsnply1chr2lem2 34251 rngunsnply1chr2lem3 34252 vietalem 34322 irngnzply1lem 34433 extdgfialglem2 34436 2sqr3minply 34523 cos9thpiminplylem6 34530 cos9thpiminply 34531 aks5lem2 43503 ply1vr1smo 49826 ply1mulgsumlem4 49832 ply1mulgsum 49833

W3C validator