MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mat2pmatfval Structured version   Visualization version   GIF version

Theorem mat2pmatfval 22024
Description: Value of the matrix transformation. (Contributed by AV, 31-Jul-2019.)
Hypotheses
Ref Expression
mat2pmatfval.t 𝑇 = (𝑁 matToPolyMat 𝑅)
mat2pmatfval.a 𝐴 = (𝑁 Mat 𝑅)
mat2pmatfval.b 𝐡 = (Baseβ€˜π΄)
mat2pmatfval.p 𝑃 = (Poly1β€˜π‘…)
mat2pmatfval.s 𝑆 = (algScβ€˜π‘ƒ)
Assertion
Ref Expression
mat2pmatfval ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) β†’ 𝑇 = (π‘š ∈ 𝐡 ↦ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (π‘†β€˜(π‘₯π‘šπ‘¦)))))
Distinct variable groups:   𝐡,π‘š   π‘₯,π‘š,𝑦,𝑁   𝑅,π‘š,π‘₯,𝑦
Allowed substitution hints:   𝐴(π‘₯,𝑦,π‘š)   𝐡(π‘₯,𝑦)   𝑃(π‘₯,𝑦,π‘š)   𝑆(π‘₯,𝑦,π‘š)   𝑇(π‘₯,𝑦,π‘š)   𝑉(π‘₯,𝑦,π‘š)

Proof of Theorem mat2pmatfval
Dummy variables 𝑛 π‘Ÿ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mat2pmatfval.t . 2 𝑇 = (𝑁 matToPolyMat 𝑅)
2 df-mat2pmat 22008 . . . 4 matToPolyMat = (𝑛 ∈ Fin, π‘Ÿ ∈ V ↦ (π‘š ∈ (Baseβ€˜(𝑛 Mat π‘Ÿ)) ↦ (π‘₯ ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algScβ€˜(Poly1β€˜π‘Ÿ))β€˜(π‘₯π‘šπ‘¦)))))
32a1i 11 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) β†’ matToPolyMat = (𝑛 ∈ Fin, π‘Ÿ ∈ V ↦ (π‘š ∈ (Baseβ€˜(𝑛 Mat π‘Ÿ)) ↦ (π‘₯ ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algScβ€˜(Poly1β€˜π‘Ÿ))β€˜(π‘₯π‘šπ‘¦))))))
4 oveq12 7360 . . . . . . 7 ((𝑛 = 𝑁 ∧ π‘Ÿ = 𝑅) β†’ (𝑛 Mat π‘Ÿ) = (𝑁 Mat 𝑅))
54fveq2d 6843 . . . . . 6 ((𝑛 = 𝑁 ∧ π‘Ÿ = 𝑅) β†’ (Baseβ€˜(𝑛 Mat π‘Ÿ)) = (Baseβ€˜(𝑁 Mat 𝑅)))
6 mat2pmatfval.b . . . . . . 7 𝐡 = (Baseβ€˜π΄)
7 mat2pmatfval.a . . . . . . . 8 𝐴 = (𝑁 Mat 𝑅)
87fveq2i 6842 . . . . . . 7 (Baseβ€˜π΄) = (Baseβ€˜(𝑁 Mat 𝑅))
96, 8eqtr2i 2766 . . . . . 6 (Baseβ€˜(𝑁 Mat 𝑅)) = 𝐡
105, 9eqtrdi 2793 . . . . 5 ((𝑛 = 𝑁 ∧ π‘Ÿ = 𝑅) β†’ (Baseβ€˜(𝑛 Mat π‘Ÿ)) = 𝐡)
11 simpl 483 . . . . . 6 ((𝑛 = 𝑁 ∧ π‘Ÿ = 𝑅) β†’ 𝑛 = 𝑁)
12 2fveq3 6844 . . . . . . . . 9 (π‘Ÿ = 𝑅 β†’ (algScβ€˜(Poly1β€˜π‘Ÿ)) = (algScβ€˜(Poly1β€˜π‘…)))
1312adantl 482 . . . . . . . 8 ((𝑛 = 𝑁 ∧ π‘Ÿ = 𝑅) β†’ (algScβ€˜(Poly1β€˜π‘Ÿ)) = (algScβ€˜(Poly1β€˜π‘…)))
14 mat2pmatfval.s . . . . . . . . 9 𝑆 = (algScβ€˜π‘ƒ)
15 mat2pmatfval.p . . . . . . . . . 10 𝑃 = (Poly1β€˜π‘…)
1615fveq2i 6842 . . . . . . . . 9 (algScβ€˜π‘ƒ) = (algScβ€˜(Poly1β€˜π‘…))
1714, 16eqtr2i 2766 . . . . . . . 8 (algScβ€˜(Poly1β€˜π‘…)) = 𝑆
1813, 17eqtrdi 2793 . . . . . . 7 ((𝑛 = 𝑁 ∧ π‘Ÿ = 𝑅) β†’ (algScβ€˜(Poly1β€˜π‘Ÿ)) = 𝑆)
1918fveq1d 6841 . . . . . 6 ((𝑛 = 𝑁 ∧ π‘Ÿ = 𝑅) β†’ ((algScβ€˜(Poly1β€˜π‘Ÿ))β€˜(π‘₯π‘šπ‘¦)) = (π‘†β€˜(π‘₯π‘šπ‘¦)))
2011, 11, 19mpoeq123dv 7426 . . . . 5 ((𝑛 = 𝑁 ∧ π‘Ÿ = 𝑅) β†’ (π‘₯ ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algScβ€˜(Poly1β€˜π‘Ÿ))β€˜(π‘₯π‘šπ‘¦))) = (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (π‘†β€˜(π‘₯π‘šπ‘¦))))
2110, 20mpteq12dv 5194 . . . 4 ((𝑛 = 𝑁 ∧ π‘Ÿ = 𝑅) β†’ (π‘š ∈ (Baseβ€˜(𝑛 Mat π‘Ÿ)) ↦ (π‘₯ ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algScβ€˜(Poly1β€˜π‘Ÿ))β€˜(π‘₯π‘šπ‘¦)))) = (π‘š ∈ 𝐡 ↦ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (π‘†β€˜(π‘₯π‘šπ‘¦)))))
2221adantl 482 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) ∧ (𝑛 = 𝑁 ∧ π‘Ÿ = 𝑅)) β†’ (π‘š ∈ (Baseβ€˜(𝑛 Mat π‘Ÿ)) ↦ (π‘₯ ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algScβ€˜(Poly1β€˜π‘Ÿ))β€˜(π‘₯π‘šπ‘¦)))) = (π‘š ∈ 𝐡 ↦ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (π‘†β€˜(π‘₯π‘šπ‘¦)))))
23 simpl 483 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) β†’ 𝑁 ∈ Fin)
24 elex 3461 . . . 4 (𝑅 ∈ 𝑉 β†’ 𝑅 ∈ V)
2524adantl 482 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) β†’ 𝑅 ∈ V)
266fvexi 6853 . . . 4 𝐡 ∈ V
27 mptexg 7167 . . . 4 (𝐡 ∈ V β†’ (π‘š ∈ 𝐡 ↦ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (π‘†β€˜(π‘₯π‘šπ‘¦)))) ∈ V)
2826, 27mp1i 13 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) β†’ (π‘š ∈ 𝐡 ↦ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (π‘†β€˜(π‘₯π‘šπ‘¦)))) ∈ V)
293, 22, 23, 25, 28ovmpod 7501 . 2 ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) β†’ (𝑁 matToPolyMat 𝑅) = (π‘š ∈ 𝐡 ↦ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (π‘†β€˜(π‘₯π‘šπ‘¦)))))
301, 29eqtrid 2789 1 ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) β†’ 𝑇 = (π‘š ∈ 𝐡 ↦ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (π‘†β€˜(π‘₯π‘šπ‘¦)))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Vcvv 3443   ↦ cmpt 5186  β€˜cfv 6493  (class class class)co 7351   ∈ cmpo 7353  Fincfn 8841  Basecbs 17043  algSccascl 21211  Poly1cpl1 21500   Mat cmat 21706   matToPolyMat cmat2pmat 22005
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pr 5382
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-id 5529  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7354  df-oprab 7355  df-mpo 7356  df-mat2pmat 22008
This theorem is referenced by:  mat2pmatval  22025  mat2pmatf  22029  m2cpmf  22043
  Copyright terms: Public domain W3C validator