Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm2mpfval | Structured version Visualization version GIF version |
Description: A polynomial matrix transformed into a polynomial over matrices. (Contributed by AV, 4-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 𝑅) |
Ref | Expression |
---|---|
pm2mpfval | ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2mpval.p | . . . 4 ⊢ 𝑃 = (Poly1‘𝑅) | |
2 | pm2mpval.c | . . . 4 ⊢ 𝐶 = (𝑁 Mat 𝑃) | |
3 | pm2mpval.b | . . . 4 ⊢ 𝐵 = (Base‘𝐶) | |
4 | pm2mpval.m | . . . 4 ⊢ ∗ = ( ·𝑠 ‘𝑄) | |
5 | pm2mpval.e | . . . 4 ⊢ ↑ = (.g‘(mulGrp‘𝑄)) | |
6 | pm2mpval.x | . . . 4 ⊢ 𝑋 = (var1‘𝐴) | |
7 | pm2mpval.a | . . . 4 ⊢ 𝐴 = (𝑁 Mat 𝑅) | |
8 | pm2mpval.q | . . . 4 ⊢ 𝑄 = (Poly1‘𝐴) | |
9 | pm2mpval.t | . . . 4 ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) | |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | pm2mpval 21664 | . . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑇 = (𝑚 ∈ 𝐵 ↦ (𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))))) |
11 | 10 | 3adant3 1134 | . 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → 𝑇 = (𝑚 ∈ 𝐵 ↦ (𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))))) |
12 | oveq1 7209 | . . . . . 6 ⊢ (𝑚 = 𝑀 → (𝑚 decompPMat 𝑘) = (𝑀 decompPMat 𝑘)) | |
13 | 12 | oveq1d 7217 | . . . . 5 ⊢ (𝑚 = 𝑀 → ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)) = ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))) |
14 | 13 | mpteq2dv 5140 | . . . 4 ⊢ (𝑚 = 𝑀 → (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))) = (𝑘 ∈ ℕ0 ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))) |
15 | 14 | oveq2d 7218 | . . 3 ⊢ (𝑚 = 𝑀 → (𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))) = (𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))) |
16 | 15 | adantl 485 | . 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) ∧ 𝑚 = 𝑀) → (𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))) = (𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))) |
17 | simp3 1140 | . 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ 𝐵) | |
18 | ovexd 7237 | . 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))) ∈ V) | |
19 | 11, 16, 17, 18 | fvmptd 6814 | 1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1089 = wceq 1543 ∈ wcel 2110 Vcvv 3401 ↦ cmpt 5124 ‘cfv 6369 (class class class)co 7202 Fincfn 8615 ℕ0cn0 12073 Basecbs 16684 ·𝑠 cvsca 16771 Σg cgsu 16917 .gcmg 18460 mulGrpcmgp 19476 var1cv1 21069 Poly1cpl1 21070 Mat cmat 21276 decompPMat cdecpmat 21631 pMatToMatPoly cpm2mp 21661 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-rep 5168 ax-sep 5181 ax-nul 5188 ax-pr 5311 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ne 2936 df-ral 3059 df-rex 3060 df-reu 3061 df-rab 3063 df-v 3403 df-sbc 3688 df-csb 3803 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-nul 4228 df-if 4430 df-sn 4532 df-pr 4534 df-op 4538 df-uni 4810 df-iun 4896 df-br 5044 df-opab 5106 df-mpt 5125 df-id 5444 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-rn 5551 df-res 5552 df-ima 5553 df-iota 6327 df-fun 6371 df-fn 6372 df-f 6373 df-f1 6374 df-fo 6375 df-f1o 6376 df-fv 6377 df-ov 7205 df-oprab 7206 df-mpo 7207 df-pm2mp 21662 |
This theorem is referenced by: pm2mpcl 21666 pm2mpf1 21668 pm2mpcoe1 21669 idpm2idmp 21670 mp2pm2mp 21680 pm2mpghm 21685 pm2mpmhmlem2 21688 monmat2matmon 21693 |
Copyright terms: Public domain | W3C validator |