Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > psrvscacl | Structured version Visualization version GIF version |
Description: Closure of the power series scalar multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.) |
Ref | Expression |
---|---|
psrvscacl.s | ⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
psrvscacl.n | ⊢ · = ( ·𝑠 ‘𝑆) |
psrvscacl.k | ⊢ 𝐾 = (Base‘𝑅) |
psrvscacl.b | ⊢ 𝐵 = (Base‘𝑆) |
psrvscacl.r | ⊢ (𝜑 → 𝑅 ∈ Ring) |
psrvscacl.x | ⊢ (𝜑 → 𝑋 ∈ 𝐾) |
psrvscacl.y | ⊢ (𝜑 → 𝐹 ∈ 𝐵) |
Ref | Expression |
---|---|
psrvscacl | ⊢ (𝜑 → (𝑋 · 𝐹) ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | psrvscacl.r | . . . . 5 ⊢ (𝜑 → 𝑅 ∈ Ring) | |
2 | psrvscacl.k | . . . . . . 7 ⊢ 𝐾 = (Base‘𝑅) | |
3 | eqid 2737 | . . . . . . 7 ⊢ (.r‘𝑅) = (.r‘𝑅) | |
4 | 2, 3 | ringcl 19867 | . . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐾) |
5 | 4 | 3expb 1119 | . . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐾) |
6 | 1, 5 | sylan 580 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐾) |
7 | psrvscacl.x | . . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐾) | |
8 | fconst6g 6698 | . . . . 5 ⊢ (𝑋 ∈ 𝐾 → ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑋}):{𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}⟶𝐾) | |
9 | 7, 8 | syl 17 | . . . 4 ⊢ (𝜑 → ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑋}):{𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}⟶𝐾) |
10 | psrvscacl.s | . . . . 5 ⊢ 𝑆 = (𝐼 mPwSer 𝑅) | |
11 | eqid 2737 | . . . . 5 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} | |
12 | psrvscacl.b | . . . . 5 ⊢ 𝐵 = (Base‘𝑆) | |
13 | psrvscacl.y | . . . . 5 ⊢ (𝜑 → 𝐹 ∈ 𝐵) | |
14 | 10, 2, 11, 12, 13 | psrelbas 21219 | . . . 4 ⊢ (𝜑 → 𝐹:{𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}⟶𝐾) |
15 | ovex 7346 | . . . . . 6 ⊢ (ℕ0 ↑m 𝐼) ∈ V | |
16 | 15 | rabex 5269 | . . . . 5 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∈ V |
17 | 16 | a1i 11 | . . . 4 ⊢ (𝜑 → {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∈ V) |
18 | inidm 4162 | . . . 4 ⊢ ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} | |
19 | 6, 9, 14, 17, 17, 18 | off 7589 | . . 3 ⊢ (𝜑 → (({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑋}) ∘f (.r‘𝑅)𝐹):{𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}⟶𝐾) |
20 | 2 | fvexi 6823 | . . . 4 ⊢ 𝐾 ∈ V |
21 | 20, 16 | elmap 8705 | . . 3 ⊢ ((({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑋}) ∘f (.r‘𝑅)𝐹) ∈ (𝐾 ↑m {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ↔ (({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑋}) ∘f (.r‘𝑅)𝐹):{𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}⟶𝐾) |
22 | 19, 21 | sylibr 233 | . 2 ⊢ (𝜑 → (({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑋}) ∘f (.r‘𝑅)𝐹) ∈ (𝐾 ↑m {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin})) |
23 | psrvscacl.n | . . 3 ⊢ · = ( ·𝑠 ‘𝑆) | |
24 | 10, 23, 2, 12, 3, 11, 7, 13 | psrvsca 21231 | . 2 ⊢ (𝜑 → (𝑋 · 𝐹) = (({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑋}) ∘f (.r‘𝑅)𝐹)) |
25 | reldmpsr 21188 | . . . . . 6 ⊢ Rel dom mPwSer | |
26 | 25, 10, 12 | elbasov 16986 | . . . . 5 ⊢ (𝐹 ∈ 𝐵 → (𝐼 ∈ V ∧ 𝑅 ∈ V)) |
27 | 13, 26 | syl 17 | . . . 4 ⊢ (𝜑 → (𝐼 ∈ V ∧ 𝑅 ∈ V)) |
28 | 27 | simpld 495 | . . 3 ⊢ (𝜑 → 𝐼 ∈ V) |
29 | 10, 2, 11, 12, 28 | psrbas 21218 | . 2 ⊢ (𝜑 → 𝐵 = (𝐾 ↑m {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin})) |
30 | 22, 24, 29 | 3eltr4d 2853 | 1 ⊢ (𝜑 → (𝑋 · 𝐹) ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1540 ∈ wcel 2105 {crab 3404 Vcvv 3441 {csn 4569 × cxp 5603 ◡ccnv 5604 “ cima 5608 ⟶wf 6459 ‘cfv 6463 (class class class)co 7313 ∘f cof 7569 ↑m cmap 8661 Fincfn 8779 ℕcn 12043 ℕ0cn0 12303 Basecbs 16979 .rcmulr 17030 ·𝑠 cvsca 17033 Ringcrg 19850 mPwSer cmps 21178 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2708 ax-rep 5222 ax-sep 5236 ax-nul 5243 ax-pow 5301 ax-pr 5365 ax-un 7626 ax-cnex 10997 ax-resscn 10998 ax-1cn 10999 ax-icn 11000 ax-addcl 11001 ax-addrcl 11002 ax-mulcl 11003 ax-mulrcl 11004 ax-mulcom 11005 ax-addass 11006 ax-mulass 11007 ax-distr 11008 ax-i2m1 11009 ax-1ne0 11010 ax-1rid 11011 ax-rnegex 11012 ax-rrecex 11013 ax-cnre 11014 ax-pre-lttri 11015 ax-pre-lttrn 11016 ax-pre-ltadd 11017 ax-pre-mulgt0 11018 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-reu 3351 df-rab 3405 df-v 3443 df-sbc 3726 df-csb 3842 df-dif 3899 df-un 3901 df-in 3903 df-ss 3913 df-pss 3915 df-nul 4267 df-if 4470 df-pw 4545 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4849 df-iun 4937 df-br 5086 df-opab 5148 df-mpt 5169 df-tr 5203 df-id 5505 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5560 df-we 5562 df-xp 5611 df-rel 5612 df-cnv 5613 df-co 5614 df-dm 5615 df-rn 5616 df-res 5617 df-ima 5618 df-pred 6222 df-ord 6289 df-on 6290 df-lim 6291 df-suc 6292 df-iota 6415 df-fun 6465 df-fn 6466 df-f 6467 df-f1 6468 df-fo 6469 df-f1o 6470 df-fv 6471 df-riota 7270 df-ov 7316 df-oprab 7317 df-mpo 7318 df-of 7571 df-om 7756 df-1st 7874 df-2nd 7875 df-supp 8023 df-frecs 8142 df-wrecs 8173 df-recs 8247 df-rdg 8286 df-1o 8342 df-er 8544 df-map 8663 df-en 8780 df-dom 8781 df-sdom 8782 df-fin 8783 df-fsupp 9197 df-pnf 11081 df-mnf 11082 df-xr 11083 df-ltxr 11084 df-le 11085 df-sub 11277 df-neg 11278 df-nn 12044 df-2 12106 df-3 12107 df-4 12108 df-5 12109 df-6 12110 df-7 12111 df-8 12112 df-9 12113 df-n0 12304 df-z 12390 df-uz 12653 df-fz 13310 df-struct 16915 df-sets 16932 df-slot 16950 df-ndx 16962 df-base 16980 df-plusg 17042 df-mulr 17043 df-sca 17045 df-vsca 17046 df-tset 17048 df-mgm 18393 df-sgrp 18442 df-mnd 18453 df-mgp 19788 df-ring 19852 df-psr 21183 |
This theorem is referenced by: psrlmod 21241 psrass23l 21248 psrass23 21250 mpllsslem 21277 |
Copyright terms: Public domain | W3C validator |