![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ply1tmcl | Structured version Visualization version GIF version |
Description: Closure of the expression for a univariate polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 25-Nov-2019.) |
Ref | Expression |
---|---|
ply1tmcl.k | ⊢ 𝐾 = (Base‘𝑅) |
ply1tmcl.p | ⊢ 𝑃 = (Poly1‘𝑅) |
ply1tmcl.x | ⊢ 𝑋 = (var1‘𝑅) |
ply1tmcl.m | ⊢ · = ( ·𝑠 ‘𝑃) |
ply1tmcl.n | ⊢ 𝑁 = (mulGrp‘𝑃) |
ply1tmcl.e | ⊢ ↑ = (.g‘𝑁) |
ply1tmcl.b | ⊢ 𝐵 = (Base‘𝑃) |
Ref | Expression |
---|---|
ply1tmcl | ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐶 · (𝐷 ↑ 𝑋)) ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ply1tmcl.p | . . . 4 ⊢ 𝑃 = (Poly1‘𝑅) | |
2 | 1 | ply1lmod 20139 | . . 3 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
3 | 2 | 3ad2ant1 1114 | . 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → 𝑃 ∈ LMod) |
4 | simp2 1118 | . 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → 𝐶 ∈ 𝐾) | |
5 | ply1tmcl.x | . . . 4 ⊢ 𝑋 = (var1‘𝑅) | |
6 | ply1tmcl.n | . . . 4 ⊢ 𝑁 = (mulGrp‘𝑃) | |
7 | ply1tmcl.e | . . . 4 ⊢ ↑ = (.g‘𝑁) | |
8 | ply1tmcl.b | . . . 4 ⊢ 𝐵 = (Base‘𝑃) | |
9 | 1, 5, 6, 7, 8 | ply1moncl 20158 | . . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐷 ∈ ℕ0) → (𝐷 ↑ 𝑋) ∈ 𝐵) |
10 | 9 | 3adant2 1112 | . 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐷 ↑ 𝑋) ∈ 𝐵) |
11 | 1 | ply1sca2 20141 | . . 3 ⊢ ( I ‘𝑅) = (Scalar‘𝑃) |
12 | ply1tmcl.m | . . 3 ⊢ · = ( ·𝑠 ‘𝑃) | |
13 | df-base 16344 | . . . 4 ⊢ Base = Slot 1 | |
14 | ply1tmcl.k | . . . 4 ⊢ 𝐾 = (Base‘𝑅) | |
15 | 13, 14 | strfvi 16392 | . . 3 ⊢ 𝐾 = (Base‘( I ‘𝑅)) |
16 | 8, 11, 12, 15 | lmodvscl 19386 | . 2 ⊢ ((𝑃 ∈ LMod ∧ 𝐶 ∈ 𝐾 ∧ (𝐷 ↑ 𝑋) ∈ 𝐵) → (𝐶 · (𝐷 ↑ 𝑋)) ∈ 𝐵) |
17 | 3, 4, 10, 16 | syl3anc 1352 | 1 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐶 · (𝐷 ↑ 𝑋)) ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1069 = wceq 1508 ∈ wcel 2051 I cid 5308 ‘cfv 6186 (class class class)co 6975 1c1 10335 ℕ0cn0 11706 Basecbs 16338 ·𝑠 cvsca 16424 .gcmg 18024 mulGrpcmgp 18975 Ringcrg 19033 LModclmod 19369 var1cv1 20063 Poly1cpl1 20064 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2745 ax-rep 5046 ax-sep 5057 ax-nul 5064 ax-pow 5116 ax-pr 5183 ax-un 7278 ax-cnex 10390 ax-resscn 10391 ax-1cn 10392 ax-icn 10393 ax-addcl 10394 ax-addrcl 10395 ax-mulcl 10396 ax-mulrcl 10397 ax-mulcom 10398 ax-addass 10399 ax-mulass 10400 ax-distr 10401 ax-i2m1 10402 ax-1ne0 10403 ax-1rid 10404 ax-rnegex 10405 ax-rrecex 10406 ax-cnre 10407 ax-pre-lttri 10408 ax-pre-lttrn 10409 ax-pre-ltadd 10410 ax-pre-mulgt0 10411 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ne 2963 df-nel 3069 df-ral 3088 df-rex 3089 df-reu 3090 df-rmo 3091 df-rab 3092 df-v 3412 df-sbc 3677 df-csb 3782 df-dif 3827 df-un 3829 df-in 3831 df-ss 3838 df-pss 3840 df-nul 4174 df-if 4346 df-pw 4419 df-sn 4437 df-pr 4439 df-tp 4441 df-op 4443 df-uni 4710 df-int 4747 df-iun 4791 df-iin 4792 df-br 4927 df-opab 4989 df-mpt 5006 df-tr 5028 df-id 5309 df-eprel 5314 df-po 5323 df-so 5324 df-fr 5363 df-se 5364 df-we 5365 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-rn 5415 df-res 5416 df-ima 5417 df-pred 5984 df-ord 6030 df-on 6031 df-lim 6032 df-suc 6033 df-iota 6150 df-fun 6188 df-fn 6189 df-f 6190 df-f1 6191 df-fo 6192 df-f1o 6193 df-fv 6194 df-isom 6195 df-riota 6936 df-ov 6978 df-oprab 6979 df-mpo 6980 df-of 7226 df-ofr 7227 df-om 7396 df-1st 7500 df-2nd 7501 df-supp 7633 df-wrecs 7749 df-recs 7811 df-rdg 7849 df-1o 7904 df-2o 7905 df-oadd 7908 df-er 8088 df-map 8207 df-pm 8208 df-ixp 8259 df-en 8306 df-dom 8307 df-sdom 8308 df-fin 8309 df-fsupp 8628 df-oi 8768 df-card 9161 df-pnf 10475 df-mnf 10476 df-xr 10477 df-ltxr 10478 df-le 10479 df-sub 10671 df-neg 10672 df-nn 11439 df-2 11502 df-3 11503 df-4 11504 df-5 11505 df-6 11506 df-7 11507 df-8 11508 df-9 11509 df-n0 11707 df-z 11793 df-dec 11911 df-uz 12058 df-fz 12708 df-fzo 12849 df-seq 13184 df-hash 13505 df-struct 16340 df-ndx 16341 df-slot 16342 df-base 16344 df-sets 16345 df-ress 16346 df-plusg 16433 df-mulr 16434 df-sca 16436 df-vsca 16437 df-tset 16439 df-ple 16440 df-0g 16570 df-gsum 16571 df-mre 16728 df-mrc 16729 df-acs 16731 df-mgm 17723 df-sgrp 17765 df-mnd 17776 df-mhm 17816 df-submnd 17817 df-grp 17907 df-minusg 17908 df-sbg 17909 df-mulg 18025 df-subg 18073 df-ghm 18140 df-cntz 18231 df-cmn 18681 df-abl 18682 df-mgp 18976 df-ur 18988 df-ring 19035 df-subrg 19269 df-lmod 19371 df-lss 19439 df-psr 19863 df-mvr 19864 df-mpl 19865 df-opsr 19867 df-psr1 20067 df-vr1 20068 df-ply1 20069 |
This theorem is referenced by: coe1tm 20160 coe1tmmul2 20163 coe1tmmul 20164 gsumsmonply1 20190 gsummoncoe1 20191 pmatcollpw1 21104 pmatcollpw2 21106 pmatcollpw 21109 pmatcollpwscmatlem2 21118 pm2mpcl 21125 mp2pm2mplem2 21135 mp2pm2mplem4 21137 mp2pm2mp 21139 pm2mpghmlem1 21141 deg1tmle 24430 deg1tm 24431 ply1divex 24449 |
Copyright terms: Public domain | W3C validator |