Metamath Proof Explorer

Theorem pm2mpf1lem

Description: Lemma for pm2mpf1 . (Contributed by AV, 14-Oct-2019) (Revised by AV, 4-Dec-2019)

Ref Expression
Hypotheses pm2mpf1lem.p 
|- P = ( Poly1 ` R )
pm2mpf1lem.c 
|- C = ( N Mat P )
pm2mpf1lem.b 
|- B = ( Base ` C )
pm2mpf1lem.m 
|- .* = ( .s ` Q )
pm2mpf1lem.e 
|- .^ = ( .g ` ( mulGrp ` Q ) )
pm2mpf1lem.x 
|- X = ( var1 ` A )
pm2mpf1lem.a 
|- A = ( N Mat R )
pm2mpf1lem.q 
|- Q = ( Poly1 ` A )
Assertion pm2mpf1lem 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ K e. NN0 ) ) -> ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( U decompPMat k ) .* ( k .^ X ) ) ) ) ) ` K ) = ( U decompPMat K ) )

Proof

Step Hyp Ref Expression
1 pm2mpf1lem.p 
 |-  P = ( Poly1 ` R )
2 pm2mpf1lem.c 
 |-  C = ( N Mat P )
3 pm2mpf1lem.b 
 |-  B = ( Base ` C )
4 pm2mpf1lem.m 
 |-  .* = ( .s ` Q )
5 pm2mpf1lem.e 
 |-  .^ = ( .g ` ( mulGrp ` Q ) )
6 pm2mpf1lem.x 
 |-  X = ( var1 ` A )
7 pm2mpf1lem.a 
 |-  A = ( N Mat R )
8 pm2mpf1lem.q 
 |-  Q = ( Poly1 ` A )
9 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
10 7 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
11 10 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ K e. NN0 ) ) -> A e. Ring )
12 eqid 
 |-  ( Base ` A ) = ( Base ` A )
13 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
14 simpllr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ K e. NN0 ) ) /\ k e. NN0 ) -> R e. Ring )
15 simplrl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ K e. NN0 ) ) /\ k e. NN0 ) -> U e. B )
16 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ K e. NN0 ) ) /\ k e. NN0 ) -> k e. NN0 )
17 1 2 3 7 12 decpmatcl 
 |-  ( ( R e. Ring /\ U e. B /\ k e. NN0 ) -> ( U decompPMat k ) e. ( Base ` A ) )
18 14 15 16 17 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ K e. NN0 ) ) /\ k e. NN0 ) -> ( U decompPMat k ) e. ( Base ` A ) )
19 18 ralrimiva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ K e. NN0 ) ) -> A. k e. NN0 ( U decompPMat k ) e. ( Base ` A ) )
20 1 2 3 7 13 decpmatfsupp 
 |-  ( ( R e. Ring /\ U e. B ) -> ( k e. NN0 |-> ( U decompPMat k ) ) finSupp ( 0g ` A ) )
21 20 ad2ant2lr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ K e. NN0 ) ) -> ( k e. NN0 |-> ( U decompPMat k ) ) finSupp ( 0g ` A ) )
22 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ K e. NN0 ) ) -> K e. NN0 )
23 8 9 6 5 11 12 4 13 19 21 22 gsummoncoe1 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ K e. NN0 ) ) -> ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( U decompPMat k ) .* ( k .^ X ) ) ) ) ) ` K ) = [_ K / k ]_ ( U decompPMat k ) )
24 csbov2g 
 |-  ( K e. NN0 -> [_ K / k ]_ ( U decompPMat k ) = ( U decompPMat [_ K / k ]_ k ) )
25 24 ad2antll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ K e. NN0 ) ) -> [_ K / k ]_ ( U decompPMat k ) = ( U decompPMat [_ K / k ]_ k ) )
26 csbvarg 
 |-  ( K e. NN0 -> [_ K / k ]_ k = K )
27 26 ad2antll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ K e. NN0 ) ) -> [_ K / k ]_ k = K )
28 27 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ K e. NN0 ) ) -> ( U decompPMat [_ K / k ]_ k ) = ( U decompPMat K ) )
29 23 25 28 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ K e. NN0 ) ) -> ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( U decompPMat k ) .* ( k .^ X ) ) ) ) ) ` K ) = ( U decompPMat K ) )