Theorem mp2pm2mplem5

Description: Lemma 5 for mp2pm2mp . (Contributed by AV, 12-Oct-2019) (Revised by AV, 5-Dec-2019)

	Ref	Expression
Hypotheses	mp2pm2mp.a	|- A = ( N Mat R )
	mp2pm2mp.q	|- Q = ( Poly1 ` A )
	mp2pm2mp.l	|- L = ( Base ` Q )
	mp2pm2mp.m	|- .x. = ( .s ` P )
	mp2pm2mp.e	|- E = ( .g ` ( mulGrp ` P ) )
	mp2pm2mp.y	|- Y = ( var1 ` R )
	mp2pm2mp.i	|- I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
	mp2pm2mplem2.p	|- P = ( Poly1 ` R )
	mp2pm2mplem5.m	|- .* = ( .s ` Q )
	mp2pm2mplem5.e	|- .^ = ( .g ` ( mulGrp ` Q ) )
	mp2pm2mplem5.x	|- X = ( var1 ` A )
Assertion	mp2pm2mplem5	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( k e. NN0 |-> ( ( ( I ` O ) decompPMat k ) .* ( k .^ X ) ) ) finSupp ( 0g ` Q ) )

Proof

Step	Hyp	Ref	Expression
1		mp2pm2mp.a	|- A = ( N Mat R )
2		mp2pm2mp.q	|- Q = ( Poly1 ` A )
3		mp2pm2mp.l	|- L = ( Base ` Q )
4		mp2pm2mp.m	|- .x. = ( .s ` P )
5		mp2pm2mp.e	|- E = ( .g ` ( mulGrp ` P ) )
6		mp2pm2mp.y	|- Y = ( var1 ` R )
7		mp2pm2mp.i	|- I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
8		mp2pm2mplem2.p	|- P = ( Poly1 ` R )
9		mp2pm2mplem5.m	|- .* = ( .s ` Q )
10		mp2pm2mplem5.e	|- .^ = ( .g ` ( mulGrp ` Q ) )
11		mp2pm2mplem5.x	|- X = ( var1 ` A )
12		nn0ex	|- NN0 e. _V
13	12	a1i	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> NN0 e. _V )
14	1	matring	|- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
15	2	ply1lmod	|- ( A e. Ring -> Q e. LMod )
16	14 15	syl	|- ( ( N e. Fin /\ R e. Ring ) -> Q e. LMod )
17	16	3adant3	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> Q e. LMod )
18	14	3adant3	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> A e. Ring )
19	2	ply1sca	|- ( A e. Ring -> A = ( Scalar ` Q ) )
20	18 19	syl	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> A = ( Scalar ` Q ) )
21		simpl2	|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ k e. NN0 ) -> R e. Ring )
22		eqid	|- ( N Mat P ) = ( N Mat P )
23		eqid	|- ( Base ` ( N Mat P ) ) = ( Base ` ( N Mat P ) )
24	1 2 3 8 4 5 6 7 22 23	mply1topmatcl	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( I ` O ) e. ( Base ` ( N Mat P ) ) )
25	24	adantr	|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ k e. NN0 ) -> ( I ` O ) e. ( Base ` ( N Mat P ) ) )
26		simpr	|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ k e. NN0 ) -> k e. NN0 )
27		eqid	|- ( Base ` A ) = ( Base ` A )
28	8 22 23 1 27	decpmatcl	|- ( ( R e. Ring /\ ( I ` O ) e. ( Base ` ( N Mat P ) ) /\ k e. NN0 ) -> ( ( I ` O ) decompPMat k ) e. ( Base ` A ) )
29	21 25 26 28	syl3anc	|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ k e. NN0 ) -> ( ( I ` O ) decompPMat k ) e. ( Base ` A ) )
30		eqid	|- ( mulGrp ` Q ) = ( mulGrp ` Q )
31	2 11 30 10 3	ply1moncl	|- ( ( A e. Ring /\ k e. NN0 ) -> ( k .^ X ) e. L )
32	18 31	sylan	|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ k e. NN0 ) -> ( k .^ X ) e. L )
33		eqid	|- ( 0g ` Q ) = ( 0g ` Q )
34		eqid	|- ( 0g ` A ) = ( 0g ` A )
35		fveq2	|- ( k = l -> ( ( coe1 ` p ) ` k ) = ( ( coe1 ` p ) ` l ) )
36	35	oveqd	|- ( k = l -> ( i ( ( coe1 ` p ) ` k ) j ) = ( i ( ( coe1 ` p ) ` l ) j ) )
37		oveq1	|- ( k = l -> ( k E Y ) = ( l E Y ) )
38	36 37	oveq12d	|- ( k = l -> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) = ( ( i ( ( coe1 ` p ) ` l ) j ) .x. ( l E Y ) ) )
39	38	cbvmptv	|- ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) = ( l e. NN0 |-> ( ( i ( ( coe1 ` p ) ` l ) j ) .x. ( l E Y ) ) )
40	39	oveq2i	|- ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) = ( P gsum ( l e. NN0 |-> ( ( i ( ( coe1 ` p ) ` l ) j ) .x. ( l E Y ) ) ) )
41	40	a1i	|- ( ( i e. N /\ j e. N ) -> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) = ( P gsum ( l e. NN0 |-> ( ( i ( ( coe1 ` p ) ` l ) j ) .x. ( l E Y ) ) ) ) )
42	41	mpoeq3ia	|- ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) = ( i e. N , j e. N |-> ( P gsum ( l e. NN0 |-> ( ( i ( ( coe1 ` p ) ` l ) j ) .x. ( l E Y ) ) ) ) )
43	42	mpteq2i	|- ( p e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ) = ( p e. L |-> ( i e. N , j e. N |-> ( P gsum ( l e. NN0 |-> ( ( i ( ( coe1 ` p ) ` l ) j ) .x. ( l E Y ) ) ) ) ) )
44	7 43	eqtri	|- I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsum ( l e. NN0 |-> ( ( i ( ( coe1 ` p ) ` l ) j ) .x. ( l E Y ) ) ) ) ) )
45	1 2 3 4 5 6 44 8	mp2pm2mplem4	|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ k e. NN0 ) -> ( ( I ` O ) decompPMat k ) = ( ( coe1 ` O ) ` k ) )
46	45	mpteq2dva	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( k e. NN0 |-> ( ( I ` O ) decompPMat k ) ) = ( k e. NN0 |-> ( ( coe1 ` O ) ` k ) ) )
47	2 3 34	mptcoe1fsupp	|- ( ( A e. Ring /\ O e. L ) -> ( k e. NN0 |-> ( ( coe1 ` O ) ` k ) ) finSupp ( 0g ` A ) )
48	14 47	stoic3	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( k e. NN0 |-> ( ( coe1 ` O ) ` k ) ) finSupp ( 0g ` A ) )
49	46 48	eqbrtrd	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( k e. NN0 |-> ( ( I ` O ) decompPMat k ) ) finSupp ( 0g ` A ) )
50	13 17 20 3 29 32 33 34 9 49	mptscmfsupp0	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( k e. NN0 |-> ( ( ( I ` O ) decompPMat k ) .* ( k .^ X ) ) ) finSupp ( 0g ` Q ) )