Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pmatcollpw1lem3 Structured version   Unicode version

Theorem pmatcollpw1lem3 31211
 Description: Lemma 3 for pmatcollpw1 31218: An entry of the matrix consisting of the coefficients in the polynomial entries of a given matrix is the corresponding coefficient in the polynomial entry of the given matrix. (Contributed by AV, 28-Sep-2019.)
Hypotheses
Ref Expression
pmatcollpw.p Poly1
pmatcollpw.c Mat
pmatcollpw.b
pmatcollpw.f coe1
Assertion
Ref Expression
pmatcollpw1lem3 coe1
Distinct variable groups:   ,,   ,,,,   ,,,,   ,,,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,,,)   (,,,)   (,)   (,,,)   (,)   (,)

Proof of Theorem pmatcollpw1lem3
StepHypRef Expression
1 simp1l 1012 . . . 4
2 simpl 457 . . . . 5
323ad2ant2 1010 . . . 4
4 simpr 461 . . . . 5
543ad2ant2 1010 . . . 4
6 pmatcollpw.p . . . . 5 Poly1
7 pmatcollpw.c . . . . 5 Mat
8 pmatcollpw.b . . . . 5
9 pmatcollpw.f . . . . 5 coe1
106, 7, 8, 9pmatcollpw1lem1 31209 . . . 4 coe1
111, 3, 5, 10syl3anc 1219 . . 3 coe1
12 oveq12 6185 . . . . . 6
1312fveq2d 5779 . . . . 5 coe1 coe1
1413fveq1d 5777 . . . 4 coe1 coe1
1514adantl 466 . . 3 coe1 coe1
16 simpl 457 . . . 4