Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm2mpcl | Structured version Visualization version GIF version |
Description: The transformation of polynomial matrices into polynomials over matrices maps polynomial matrices to polynomials over matrices. (Contributed by AV, 5-Oct-2019.) (Revised by AV, 5-Dec-2019.) |
Ref | Expression |
---|---|
pm2mpval.p | ⊢ 𝑃 = (Poly1‘𝑅) |
pm2mpval.c | ⊢ 𝐶 = (𝑁 Mat 𝑃) |
pm2mpval.b | ⊢ 𝐵 = (Base‘𝐶) |
pm2mpval.m | ⊢ ∗ = ( ·𝑠 ‘𝑄) |
pm2mpval.e | ⊢ ↑ = (.g‘(mulGrp‘𝑄)) |
pm2mpval.x | ⊢ 𝑋 = (var1‘𝐴) |
pm2mpval.a | ⊢ 𝐴 = (𝑁 Mat 𝑅) |
pm2mpval.q | ⊢ 𝑄 = (Poly1‘𝐴) |
pm2mpval.t | ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) |
pm2mpcl.l | ⊢ 𝐿 = (Base‘𝑄) |
Ref | Expression |
---|---|
pm2mpcl | ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ 𝐿) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2mpval.p | . . 3 ⊢ 𝑃 = (Poly1‘𝑅) | |
2 | pm2mpval.c | . . 3 ⊢ 𝐶 = (𝑁 Mat 𝑃) | |
3 | pm2mpval.b | . . 3 ⊢ 𝐵 = (Base‘𝐶) | |
4 | pm2mpval.m | . . 3 ⊢ ∗ = ( ·𝑠 ‘𝑄) | |
5 | pm2mpval.e | . . 3 ⊢ ↑ = (.g‘(mulGrp‘𝑄)) | |
6 | pm2mpval.x | . . 3 ⊢ 𝑋 = (var1‘𝐴) | |
7 | pm2mpval.a | . . 3 ⊢ 𝐴 = (𝑁 Mat 𝑅) | |
8 | pm2mpval.q | . . 3 ⊢ 𝑄 = (Poly1‘𝐴) | |
9 | pm2mpval.t | . . 3 ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) | |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | pm2mpfval 21955 | . 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))) |
11 | pm2mpcl.l | . . 3 ⊢ 𝐿 = (Base‘𝑄) | |
12 | eqid 2738 | . . 3 ⊢ (0g‘𝑄) = (0g‘𝑄) | |
13 | 7 | matring 21602 | . . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
14 | 8 | ply1ring 21429 | . . . . 5 ⊢ (𝐴 ∈ Ring → 𝑄 ∈ Ring) |
15 | ringcmn 19830 | . . . . 5 ⊢ (𝑄 ∈ Ring → 𝑄 ∈ CMnd) | |
16 | 13, 14, 15 | 3syl 18 | . . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ CMnd) |
17 | 16 | 3adant3 1131 | . . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑄 ∈ CMnd) |
18 | nn0ex 12249 | . . . 4 ⊢ ℕ0 ∈ V | |
19 | 18 | a1i 11 | . . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ℕ0 ∈ V) |
20 | 13 | 3adant3 1131 | . . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝐴 ∈ Ring) |
21 | 20 | adantr 481 | . . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ Ring) |
22 | simpl2 1191 | . . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ Ring) | |
23 | simpl3 1192 | . . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈ 𝐵) | |
24 | simpr 485 | . . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0) | |
25 | eqid 2738 | . . . . . . 7 ⊢ (Base‘𝐴) = (Base‘𝐴) | |
26 | 1, 2, 3, 7, 25 | decpmatcl 21926 | . . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0) → (𝑀 decompPMat 𝑘) ∈ (Base‘𝐴)) |
27 | 22, 23, 24, 26 | syl3anc 1370 | . . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑀 decompPMat 𝑘) ∈ (Base‘𝐴)) |
28 | eqid 2738 | . . . . . 6 ⊢ (mulGrp‘𝑄) = (mulGrp‘𝑄) | |
29 | 25, 8, 6, 4, 28, 5, 11 | ply1tmcl 21453 | . . . . 5 ⊢ ((𝐴 ∈ Ring ∧ (𝑀 decompPMat 𝑘) ∈ (Base‘𝐴) ∧ 𝑘 ∈ ℕ0) → ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)) ∈ 𝐿) |
30 | 21, 27, 24, 29 | syl3anc 1370 | . . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)) ∈ 𝐿) |
31 | 30 | fmpttd 6981 | . . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))):ℕ0⟶𝐿) |
32 | 8 | ply1lmod 21433 | . . . . 5 ⊢ (𝐴 ∈ Ring → 𝑄 ∈ LMod) |
33 | 20, 32 | syl 17 | . . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑄 ∈ LMod) |
34 | eqidd 2739 | . . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (Scalar‘𝑄) = (Scalar‘𝑄)) | |
35 | 8, 6, 28, 5, 11 | ply1moncl 21452 | . . . . 5 ⊢ ((𝐴 ∈ Ring ∧ 𝑘 ∈ ℕ0) → (𝑘 ↑ 𝑋) ∈ 𝐿) |
36 | 20, 35 | sylan 580 | . . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑘 ↑ 𝑋) ∈ 𝐿) |
37 | eqid 2738 | . . . 4 ⊢ (0g‘(Scalar‘𝑄)) = (0g‘(Scalar‘𝑄)) | |
38 | eqid 2738 | . . . . . . 7 ⊢ (0g‘𝐴) = (0g‘𝐴) | |
39 | 1, 2, 3, 7, 38 | decpmatfsupp 21928 | . . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑀 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
40 | 39 | 3adant1 1129 | . . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑀 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
41 | 8 | ply1sca 21434 | . . . . . . . 8 ⊢ (𝐴 ∈ Ring → 𝐴 = (Scalar‘𝑄)) |
42 | 41 | eqcomd 2744 | . . . . . . 7 ⊢ (𝐴 ∈ Ring → (Scalar‘𝑄) = 𝐴) |
43 | 20, 42 | syl 17 | . . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (Scalar‘𝑄) = 𝐴) |
44 | 43 | fveq2d 6770 | . . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (0g‘(Scalar‘𝑄)) = (0g‘𝐴)) |
45 | 40, 44 | breqtrrd 5101 | . . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑀 decompPMat 𝑘)) finSupp (0g‘(Scalar‘𝑄))) |
46 | 19, 33, 34, 11, 27, 36, 12, 37, 4, 45 | mptscmfsupp0 20198 | . . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))) finSupp (0g‘𝑄)) |
47 | 11, 12, 17, 19, 31, 46 | gsumcl 19526 | . 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))) ∈ 𝐿) |
48 | 10, 47 | eqeltrd 2839 | 1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ 𝐿) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 Vcvv 3429 class class class wbr 5073 ↦ cmpt 5156 ‘cfv 6426 (class class class)co 7267 Fincfn 8720 finSupp cfsupp 9115 ℕ0cn0 12243 Basecbs 16922 Scalarcsca 16975 ·𝑠 cvsca 16976 0gc0g 17160 Σg cgsu 17161 .gcmg 18710 CMndccmn 19396 mulGrpcmgp 19730 Ringcrg 19793 LModclmod 20133 var1cv1 21357 Poly1cpl1 21358 Mat cmat 21564 decompPMat cdecpmat 21921 pMatToMatPoly cpm2mp 21951 |
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 5208 ax-sep 5221 ax-nul 5228 ax-pow 5286 ax-pr 5350 ax-un 7578 ax-cnex 10937 ax-resscn 10938 ax-1cn 10939 ax-icn 10940 ax-addcl 10941 ax-addrcl 10942 ax-mulcl 10943 ax-mulrcl 10944 ax-mulcom 10945 ax-addass 10946 ax-mulass 10947 ax-distr 10948 ax-i2m1 10949 ax-1ne0 10950 ax-1rid 10951 ax-rnegex 10952 ax-rrecex 10953 ax-cnre 10954 ax-pre-lttri 10955 ax-pre-lttrn 10956 ax-pre-ltadd 10957 ax-pre-mulgt0 10958 |
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-rmo 3072 df-rab 3073 df-v 3431 df-sbc 3716 df-csb 3832 df-dif 3889 df-un 3891 df-in 3893 df-ss 3903 df-pss 3905 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-ot 4570 df-uni 4840 df-int 4880 df-iun 4926 df-iin 4927 df-br 5074 df-opab 5136 df-mpt 5157 df-tr 5191 df-id 5484 df-eprel 5490 df-po 5498 df-so 5499 df-fr 5539 df-se 5540 df-we 5541 df-xp 5590 df-rel 5591 df-cnv 5592 df-co 5593 df-dm 5594 df-rn 5595 df-res 5596 df-ima 5597 df-pred 6195 df-ord 6262 df-on 6263 df-lim 6264 df-suc 6265 df-iota 6384 df-fun 6428 df-fn 6429 df-f 6430 df-f1 6431 df-fo 6432 df-f1o 6433 df-fv 6434 df-isom 6435 df-riota 7224 df-ov 7270 df-oprab 7271 df-mpo 7272 df-of 7523 df-ofr 7524 df-om 7703 df-1st 7820 df-2nd 7821 df-supp 7965 df-frecs 8084 df-wrecs 8115 df-recs 8189 df-rdg 8228 df-1o 8284 df-er 8485 df-map 8604 df-pm 8605 df-ixp 8673 df-en 8721 df-dom 8722 df-sdom 8723 df-fin 8724 df-fsupp 9116 df-sup 9188 df-oi 9256 df-card 9707 df-pnf 11021 df-mnf 11022 df-xr 11023 df-ltxr 11024 df-le 11025 df-sub 11217 df-neg 11218 df-nn 11984 df-2 12046 df-3 12047 df-4 12048 df-5 12049 df-6 12050 df-7 12051 df-8 12052 df-9 12053 df-n0 12244 df-z 12330 df-dec 12448 df-uz 12593 df-fz 13250 df-fzo 13393 df-seq 13732 df-hash 14055 df-struct 16858 df-sets 16875 df-slot 16893 df-ndx 16905 df-base 16923 df-ress 16952 df-plusg 16985 df-mulr 16986 df-sca 16988 df-vsca 16989 df-ip 16990 df-tset 16991 df-ple 16992 df-ds 16994 df-hom 16996 df-cco 16997 df-0g 17162 df-gsum 17163 df-prds 17168 df-pws 17170 df-mre 17305 df-mrc 17306 df-acs 17308 df-mgm 18336 df-sgrp 18385 df-mnd 18396 df-mhm 18440 df-submnd 18441 df-grp 18590 df-minusg 18591 df-sbg 18592 df-mulg 18711 df-subg 18762 df-ghm 18842 df-cntz 18933 df-cmn 19398 df-abl 19399 df-mgp 19731 df-ur 19748 df-ring 19795 df-subrg 20032 df-lmod 20135 df-lss 20204 df-sra 20444 df-rgmod 20445 df-dsmm 20949 df-frlm 20964 df-psr 21122 df-mvr 21123 df-mpl 21124 df-opsr 21126 df-psr1 21361 df-vr1 21362 df-ply1 21363 df-coe1 21364 df-mamu 21543 df-mat 21565 df-decpmat 21922 df-pm2mp 21952 |
This theorem is referenced by: pm2mpf 21957 pm2mpf1 21958 |
Copyright terms: Public domain | W3C validator |