Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mplsubglem2 | Structured version Visualization version GIF version |
Description: Lemma for mplsubg 21196 and mpllss 21197. (Contributed by AV, 16-Jul-2019.) |
Ref | Expression |
---|---|
mplsubg.s | ⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
mplsubg.p | ⊢ 𝑃 = (𝐼 mPoly 𝑅) |
mplsubg.u | ⊢ 𝑈 = (Base‘𝑃) |
mplsubg.i | ⊢ (𝜑 → 𝐼 ∈ 𝑊) |
Ref | Expression |
---|---|
mplsubglem2 | ⊢ (𝜑 → 𝑈 = {𝑔 ∈ (Base‘𝑆) ∣ (𝑔 supp (0g‘𝑅)) ∈ Fin}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mplsubg.p | . . 3 ⊢ 𝑃 = (𝐼 mPoly 𝑅) | |
2 | mplsubg.s | . . 3 ⊢ 𝑆 = (𝐼 mPwSer 𝑅) | |
3 | eqid 2738 | . . 3 ⊢ (Base‘𝑆) = (Base‘𝑆) | |
4 | eqid 2738 | . . 3 ⊢ (0g‘𝑅) = (0g‘𝑅) | |
5 | mplsubg.u | . . 3 ⊢ 𝑈 = (Base‘𝑃) | |
6 | 1, 2, 3, 4, 5 | mplbas 21186 | . 2 ⊢ 𝑈 = {𝑔 ∈ (Base‘𝑆) ∣ 𝑔 finSupp (0g‘𝑅)} |
7 | 2, 3 | psrelbasfun 21137 | . . . . 5 ⊢ (𝑔 ∈ (Base‘𝑆) → Fun 𝑔) |
8 | 7 | adantl 482 | . . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) → Fun 𝑔) |
9 | simpr 485 | . . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) → 𝑔 ∈ (Base‘𝑆)) | |
10 | fvexd 6782 | . . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) → (0g‘𝑅) ∈ V) | |
11 | funisfsupp 9121 | . . . 4 ⊢ ((Fun 𝑔 ∧ 𝑔 ∈ (Base‘𝑆) ∧ (0g‘𝑅) ∈ V) → (𝑔 finSupp (0g‘𝑅) ↔ (𝑔 supp (0g‘𝑅)) ∈ Fin)) | |
12 | 8, 9, 10, 11 | syl3anc 1370 | . . 3 ⊢ ((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) → (𝑔 finSupp (0g‘𝑅) ↔ (𝑔 supp (0g‘𝑅)) ∈ Fin)) |
13 | 12 | rabbidva 3411 | . 2 ⊢ (𝜑 → {𝑔 ∈ (Base‘𝑆) ∣ 𝑔 finSupp (0g‘𝑅)} = {𝑔 ∈ (Base‘𝑆) ∣ (𝑔 supp (0g‘𝑅)) ∈ Fin}) |
14 | 6, 13 | eqtrid 2790 | 1 ⊢ (𝜑 → 𝑈 = {𝑔 ∈ (Base‘𝑆) ∣ (𝑔 supp (0g‘𝑅)) ∈ Fin}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 ∈ wcel 2106 {crab 3068 Vcvv 3430 class class class wbr 5074 Fun wfun 6421 ‘cfv 6427 (class class class)co 7268 supp csupp 7965 Fincfn 8721 finSupp cfsupp 9116 Basecbs 16900 0gc0g 17138 mPwSer cmps 21095 mPoly cmpl 21097 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5222 ax-nul 5229 ax-pow 5287 ax-pr 5351 ax-un 7579 ax-cnex 10915 ax-resscn 10916 ax-1cn 10917 ax-icn 10918 ax-addcl 10919 ax-addrcl 10920 ax-mulcl 10921 ax-mulrcl 10922 ax-mulcom 10923 ax-addass 10924 ax-mulass 10925 ax-distr 10926 ax-i2m1 10927 ax-1ne0 10928 ax-1rid 10929 ax-rnegex 10930 ax-rrecex 10931 ax-cnre 10932 ax-pre-lttri 10933 ax-pre-lttrn 10934 ax-pre-ltadd 10935 ax-pre-mulgt0 10936 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rab 3073 df-v 3432 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4841 df-iun 4927 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5485 df-eprel 5491 df-po 5499 df-so 5500 df-fr 5540 df-we 5542 df-xp 5591 df-rel 5592 df-cnv 5593 df-co 5594 df-dm 5595 df-rn 5596 df-res 5597 df-ima 5598 df-pred 6196 df-ord 6263 df-on 6264 df-lim 6265 df-suc 6266 df-iota 6385 df-fun 6429 df-fn 6430 df-f 6431 df-f1 6432 df-fo 6433 df-f1o 6434 df-fv 6435 df-riota 7225 df-ov 7271 df-oprab 7272 df-mpo 7273 df-of 7524 df-om 7704 df-1st 7821 df-2nd 7822 df-supp 7966 df-frecs 8085 df-wrecs 8116 df-recs 8190 df-rdg 8229 df-1o 8285 df-er 8486 df-map 8605 df-en 8722 df-dom 8723 df-sdom 8724 df-fin 8725 df-fsupp 9117 df-pnf 10999 df-mnf 11000 df-xr 11001 df-ltxr 11002 df-le 11003 df-sub 11195 df-neg 11196 df-nn 11962 df-2 12024 df-3 12025 df-4 12026 df-5 12027 df-6 12028 df-7 12029 df-8 12030 df-9 12031 df-n0 12222 df-z 12308 df-uz 12571 df-fz 13228 df-struct 16836 df-sets 16853 df-slot 16871 df-ndx 16883 df-base 16901 df-ress 16930 df-plusg 16963 df-mulr 16964 df-sca 16966 df-vsca 16967 df-tset 16969 df-psr 21100 df-mpl 21102 |
This theorem is referenced by: mplsubg 21196 mpllss 21197 |
Copyright terms: Public domain | W3C validator |