![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mvrcl | Structured version Visualization version GIF version |
Description: A power series variable is a polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.) |
Ref | Expression |
---|---|
mvrcl.s | ⊢ 𝑃 = (𝐼 mPoly 𝑅) |
mvrcl.v | ⊢ 𝑉 = (𝐼 mVar 𝑅) |
mvrcl.b | ⊢ 𝐵 = (Base‘𝑃) |
mvrcl.i | ⊢ (𝜑 → 𝐼 ∈ 𝑊) |
mvrcl.r | ⊢ (𝜑 → 𝑅 ∈ Ring) |
mvrcl.x | ⊢ (𝜑 → 𝑋 ∈ 𝐼) |
Ref | Expression |
---|---|
mvrcl | ⊢ (𝜑 → (𝑉‘𝑋) ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2795 | . . 3 ⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅) | |
2 | mvrcl.v | . . 3 ⊢ 𝑉 = (𝐼 mVar 𝑅) | |
3 | eqid 2795 | . . 3 ⊢ (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅)) | |
4 | mvrcl.i | . . 3 ⊢ (𝜑 → 𝐼 ∈ 𝑊) | |
5 | mvrcl.r | . . 3 ⊢ (𝜑 → 𝑅 ∈ Ring) | |
6 | mvrcl.x | . . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐼) | |
7 | 1, 2, 3, 4, 5, 6 | mvrcl2 19894 | . 2 ⊢ (𝜑 → (𝑉‘𝑋) ∈ (Base‘(𝐼 mPwSer 𝑅))) |
8 | fvexd 6553 | . . 3 ⊢ (𝜑 → (𝑉‘𝑋) ∈ V) | |
9 | eqid 2795 | . . . . 5 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
10 | eqid 2795 | . . . . 5 ⊢ {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} | |
11 | 1, 9, 10, 3, 7 | psrelbas 19847 | . . . 4 ⊢ (𝜑 → (𝑉‘𝑋):{𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}⟶(Base‘𝑅)) |
12 | 11 | ffund 6386 | . . 3 ⊢ (𝜑 → Fun (𝑉‘𝑋)) |
13 | fvexd 6553 | . . 3 ⊢ (𝜑 → (0g‘𝑅) ∈ V) | |
14 | snfi 8442 | . . . 4 ⊢ {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))} ∈ Fin | |
15 | 14 | a1i 11 | . . 3 ⊢ (𝜑 → {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))} ∈ Fin) |
16 | eqid 2795 | . . . . . 6 ⊢ (0g‘𝑅) = (0g‘𝑅) | |
17 | eqid 2795 | . . . . . 6 ⊢ (1r‘𝑅) = (1r‘𝑅) | |
18 | 4 | adantr 481 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))})) → 𝐼 ∈ 𝑊) |
19 | 5 | adantr 481 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))})) → 𝑅 ∈ Ring) |
20 | 6 | adantr 481 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))})) → 𝑋 ∈ 𝐼) |
21 | simpr 485 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))})) → 𝑥 ∈ ({𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))})) | |
22 | eldifsn 4626 | . . . . . . . 8 ⊢ (𝑥 ∈ ({𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))}) ↔ (𝑥 ∈ {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∧ 𝑥 ≠ (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) | |
23 | 21, 22 | sylib 219 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))})) → (𝑥 ∈ {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∧ 𝑥 ≠ (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) |
24 | 23 | simpld 495 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))})) → 𝑥 ∈ {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) |
25 | 2, 10, 16, 17, 18, 19, 20, 24 | mvrval2 19890 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))})) → ((𝑉‘𝑋)‘𝑥) = if(𝑥 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)), (1r‘𝑅), (0g‘𝑅))) |
26 | 23 | simprd 496 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))})) → 𝑥 ≠ (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) |
27 | 26 | neneqd 2989 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))})) → ¬ 𝑥 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) |
28 | 27 | iffalsed 4392 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))})) → if(𝑥 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)), (1r‘𝑅), (0g‘𝑅)) = (0g‘𝑅)) |
29 | 25, 28 | eqtrd 2831 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))})) → ((𝑉‘𝑋)‘𝑥) = (0g‘𝑅)) |
30 | 11, 29 | suppss 7711 | . . 3 ⊢ (𝜑 → ((𝑉‘𝑋) supp (0g‘𝑅)) ⊆ {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))}) |
31 | suppssfifsupp 8694 | . . 3 ⊢ ((((𝑉‘𝑋) ∈ V ∧ Fun (𝑉‘𝑋) ∧ (0g‘𝑅) ∈ V) ∧ ({(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))} ∈ Fin ∧ ((𝑉‘𝑋) supp (0g‘𝑅)) ⊆ {(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))})) → (𝑉‘𝑋) finSupp (0g‘𝑅)) | |
32 | 8, 12, 13, 15, 30, 31 | syl32anc 1371 | . 2 ⊢ (𝜑 → (𝑉‘𝑋) finSupp (0g‘𝑅)) |
33 | mvrcl.s | . . 3 ⊢ 𝑃 = (𝐼 mPoly 𝑅) | |
34 | mvrcl.b | . . 3 ⊢ 𝐵 = (Base‘𝑃) | |
35 | 33, 1, 3, 16, 34 | mplelbas 19898 | . 2 ⊢ ((𝑉‘𝑋) ∈ 𝐵 ↔ ((𝑉‘𝑋) ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ (𝑉‘𝑋) finSupp (0g‘𝑅))) |
36 | 7, 32, 35 | sylanbrc 583 | 1 ⊢ (𝜑 → (𝑉‘𝑋) ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1522 ∈ wcel 2081 ≠ wne 2984 {crab 3109 Vcvv 3437 ∖ cdif 3856 ⊆ wss 3859 ifcif 4381 {csn 4472 class class class wbr 4962 ↦ cmpt 5041 ◡ccnv 5442 “ cima 5446 Fun wfun 6219 ‘cfv 6225 (class class class)co 7016 supp csupp 7681 ↑𝑚 cmap 8256 Fincfn 8357 finSupp cfsupp 8679 0cc0 10383 1c1 10384 ℕcn 11486 ℕ0cn0 11745 Basecbs 16312 0gc0g 16542 1rcur 18941 Ringcrg 18987 mPwSer cmps 19819 mVar cmvr 19820 mPoly cmpl 19821 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5081 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 ax-cnex 10439 ax-resscn 10440 ax-1cn 10441 ax-icn 10442 ax-addcl 10443 ax-addrcl 10444 ax-mulcl 10445 ax-mulrcl 10446 ax-mulcom 10447 ax-addass 10448 ax-mulass 10449 ax-distr 10450 ax-i2m1 10451 ax-1ne0 10452 ax-1rid 10453 ax-rnegex 10454 ax-rrecex 10455 ax-cnre 10456 ax-pre-lttri 10457 ax-pre-lttrn 10458 ax-pre-ltadd 10459 ax-pre-mulgt0 10460 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-reu 3112 df-rmo 3113 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-pss 3876 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-tp 4477 df-op 4479 df-uni 4746 df-int 4783 df-iun 4827 df-br 4963 df-opab 5025 df-mpt 5042 df-tr 5064 df-id 5348 df-eprel 5353 df-po 5362 df-so 5363 df-fr 5402 df-we 5404 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-pred 6023 df-ord 6069 df-on 6070 df-lim 6071 df-suc 6072 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-riota 6977 df-ov 7019 df-oprab 7020 df-mpo 7021 df-of 7267 df-om 7437 df-1st 7545 df-2nd 7546 df-supp 7682 df-wrecs 7798 df-recs 7860 df-rdg 7898 df-1o 7953 df-oadd 7957 df-er 8139 df-map 8258 df-en 8358 df-dom 8359 df-sdom 8360 df-fin 8361 df-fsupp 8680 df-pnf 10523 df-mnf 10524 df-xr 10525 df-ltxr 10526 df-le 10527 df-sub 10719 df-neg 10720 df-nn 11487 df-2 11548 df-3 11549 df-4 11550 df-5 11551 df-6 11552 df-7 11553 df-8 11554 df-9 11555 df-n0 11746 df-z 11830 df-uz 12094 df-fz 12743 df-struct 16314 df-ndx 16315 df-slot 16316 df-base 16318 df-sets 16319 df-ress 16320 df-plusg 16407 df-mulr 16408 df-sca 16410 df-vsca 16411 df-tset 16413 df-0g 16544 df-mgm 17681 df-sgrp 17723 df-mnd 17734 df-grp 17864 df-mgp 18930 df-ur 18942 df-ring 18989 df-psr 19824 df-mvr 19825 df-mpl 19826 |
This theorem is referenced by: subrgmvrf 19930 mplcoe3 19934 mplcoe5lem 19935 mplcoe5 19936 mplcoe2 19937 mplbas2 19938 mvrf2 19959 mpfproj 19998 mpfind 20003 vr1cl 20068 |
Copyright terms: Public domain | W3C validator |