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

Theorem cpmatpmat 21293
Description: A constant polynomial matrix is a polynomial matrix. (Contributed by AV, 16-Nov-2019.)
Hypotheses
Ref Expression
cpmat.s 𝑆 = (𝑁 ConstPolyMat 𝑅)
cpmat.p 𝑃 = (Poly1𝑅)
cpmat.c 𝐶 = (𝑁 Mat 𝑃)
cpmat.b 𝐵 = (Base‘𝐶)
Assertion
Ref Expression
cpmatpmat ((𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆) → 𝑀𝐵)

Proof of Theorem cpmatpmat
Dummy variables 𝑚 𝑖 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cpmat.s . . . . 5 𝑆 = (𝑁 ConstPolyMat 𝑅)
2 cpmat.p . . . . 5 𝑃 = (Poly1𝑅)
3 cpmat.c . . . . 5 𝐶 = (𝑁 Mat 𝑃)
4 cpmat.b . . . . 5 𝐵 = (Base‘𝐶)
51, 2, 3, 4cpmat 21292 . . . 4 ((𝑁 ∈ Fin ∧ 𝑅𝑉) → 𝑆 = {𝑚𝐵 ∣ ∀𝑖𝑁𝑗𝑁𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑅)})
65eleq2d 2897 . . 3 ((𝑁 ∈ Fin ∧ 𝑅𝑉) → (𝑀𝑆𝑀 ∈ {𝑚𝐵 ∣ ∀𝑖𝑁𝑗𝑁𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑅)}))
7 elrabi 3652 . . 3 (𝑀 ∈ {𝑚𝐵 ∣ ∀𝑖𝑁𝑗𝑁𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑅)} → 𝑀𝐵)
86, 7syl6bi 256 . 2 ((𝑁 ∈ Fin ∧ 𝑅𝑉) → (𝑀𝑆𝑀𝐵))
983impia 1114 1 ((𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆) → 𝑀𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084   = wceq 1538  wcel 2115  wral 3126  {crab 3130  cfv 6328  (class class class)co 7130  Fincfn 8484  cn 11615  Basecbs 16461  0gc0g 16691  Poly1cpl1 20320  coe1cco1 20321   Mat cmat 20991   ConstPolyMat ccpmat 21286
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pr 5303
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ral 3131  df-rex 3132  df-rab 3135  df-v 3473  df-sbc 3750  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-opab 5102  df-id 5433  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-iota 6287  df-fun 6330  df-fv 6336  df-ov 7133  df-oprab 7134  df-mpo 7135  df-cpmat 21289
This theorem is referenced by:  cpmatelimp  21295  cpmatelimp2  21297  cpmatacl  21299  cpmatinvcl  21300  cpmatmcl  21302  cpm2mf  21335  m2cpminvid2lem  21337  m2cpminvid2  21338  m2cpmfo  21339  m2cpmrngiso  21341
  Copyright terms: Public domain W3C validator