Metamath Proof Explorer

Theorem pm2mpghmlem2

Description: Lemma 2 for pm2mpghm . (Contributed by AV, 15-Oct-2019) (Revised by AV, 4-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 pm2mpfo.p 
 |-  P = ( Poly1 ` R )
2 pm2mpfo.c 
 |-  C = ( N Mat P )
3 pm2mpfo.b 
 |-  B = ( Base ` C )
4 pm2mpfo.m 
 |-  .* = ( .s ` Q )
5 pm2mpfo.e 
 |-  .^ = ( .g ` ( mulGrp ` Q ) )
6 pm2mpfo.x 
 |-  X = ( var1 ` A )
7 pm2mpfo.a 
 |-  A = ( N Mat R )
8 pm2mpfo.q 
 |-  Q = ( Poly1 ` A )
9 nn0ex 
 |-  NN0 e. _V
10 9 a1i 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> NN0 e. _V )
11 7 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
12 11 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> A e. Ring )
13 8 ply1lmod 
 |-  ( A e. Ring -> Q e. LMod )
14 12 13 syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> Q e. LMod )
15 8 ply1sca 
 |-  ( A e. Ring -> A = ( Scalar ` Q ) )
16 12 15 syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> A = ( Scalar ` Q ) )
17 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
18 simpl2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ k e. NN0 ) -> R e. Ring )
19 simpl3 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ k e. NN0 ) -> M e. B )
20 simpr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ k e. NN0 ) -> k e. NN0 )
21 eqid 
 |-  ( Base ` A ) = ( Base ` A )
22 1 2 3 7 21 decpmatcl 
 |-  ( ( R e. Ring /\ M e. B /\ k e. NN0 ) -> ( M decompPMat k ) e. ( Base ` A ) )
23 18 19 20 22 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ k e. NN0 ) -> ( M decompPMat k ) e. ( Base ` A ) )
24 eqid 
 |-  ( mulGrp ` Q ) = ( mulGrp ` Q )
25 8 6 24 5 17 ply1moncl 
 |-  ( ( A e. Ring /\ k e. NN0 ) -> ( k .^ X ) e. ( Base ` Q ) )
26 12 25 sylan 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ k e. NN0 ) -> ( k .^ X ) e. ( Base ` Q ) )
27 eqid 
 |-  ( 0g ` Q ) = ( 0g ` Q )
28 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
29 1 2 3 7 28 decpmatfsupp 
 |-  ( ( R e. Ring /\ M e. B ) -> ( k e. NN0 |-> ( M decompPMat k ) ) finSupp ( 0g ` A ) )
30 29 3adant1 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( k e. NN0 |-> ( M decompPMat k ) ) finSupp ( 0g ` A ) )
31 10 14 16 17 23 26 27 28 4 30 mptscmfsupp0 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( k e. NN0 |-> ( ( M decompPMat k ) .* ( k .^ X ) ) ) finSupp ( 0g ` Q ) )