Theorem mp2pm2mplem2

Description: Lemma 2 for mp2pm2mp . (Contributed by AV, 10-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 )
	mp2pm2mplem2.c	|- C = ( N Mat P )
	mp2pm2mplem2.b	|- B = ( Base ` C )
Assertion	mp2pm2mplem2	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) e. B )

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		mp2pm2mplem2.c	|- C = ( N Mat P )
10		mp2pm2mplem2.b	|- B = ( Base ` C )
11		eqid	|- ( Base ` P ) = ( Base ` P )
12		simp1	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> N e. Fin )
13	8	ply1ring	|- ( R e. Ring -> P e. Ring )
14	13	3ad2ant2	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. Ring )
15		eqid	|- ( 0g ` P ) = ( 0g ` P )
16		ringcmn	|- ( P e. Ring -> P e. CMnd )
17	13 16	syl	|- ( R e. Ring -> P e. CMnd )
18	17	3ad2ant2	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. CMnd )
19	18	3ad2ant1	|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) -> P e. CMnd )
20		nn0ex	|- NN0 e. _V
21	20	a1i	|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) -> NN0 e. _V )
22		simpl12	|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> R e. Ring )
23		eqid	|- ( Base ` R ) = ( Base ` R )
24		eqid	|- ( Base ` A ) = ( Base ` A )
25		simpl2	|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> i e. N )
26		simpl3	|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> j e. N )
27		simp13	|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) -> O e. L )
28		eqid	|- ( coe1 ` O ) = ( coe1 ` O )
29	28 3 2 24	coe1fvalcl	|- ( ( O e. L /\ k e. NN0 ) -> ( ( coe1 ` O ) ` k ) e. ( Base ` A ) )
30	27 29	sylan	|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> ( ( coe1 ` O ) ` k ) e. ( Base ` A ) )
31	1 23 24 25 26 30	matecld	|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> ( i ( ( coe1 ` O ) ` k ) j ) e. ( Base ` R ) )
32		simpr	|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> k e. NN0 )
33		eqid	|- ( mulGrp ` P ) = ( mulGrp ` P )
34	23 8 6 4 33 5 11	ply1tmcl	|- ( ( R e. Ring /\ ( i ( ( coe1 ` O ) ` k ) j ) e. ( Base ` R ) /\ k e. NN0 ) -> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) e. ( Base ` P ) )
35	22 31 32 34	syl3anc	|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) e. ( Base ` P ) )
36	35	fmpttd	|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) -> ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) : NN0 --> ( Base ` P ) )
37	1 2 3 8 4 5 6	mply1topmatcllem	|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) -> ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) finSupp ( 0g ` P ) )
38	11 15 19 21 36 37	gsumcl	|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) -> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) e. ( Base ` P ) )
39	9 11 10 12 14 38	matbas2d	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) e. B )