Theorem mp2pm2mplem1

Description: Lemma 1 for mp2pm2mp . (Contributed by AV, 9-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 ) ) ) ) ) )
Assertion	mp2pm2mplem1	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( I ` O ) = ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )

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		fveq2	|- ( p = O -> ( coe1 ` p ) = ( coe1 ` O ) )
9	8	fveq1d	|- ( p = O -> ( ( coe1 ` p ) ` k ) = ( ( coe1 ` O ) ` k ) )
10	9	oveqd	|- ( p = O -> ( i ( ( coe1 ` p ) ` k ) j ) = ( i ( ( coe1 ` O ) ` k ) j ) )
11	10	oveq1d	|- ( p = O -> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) = ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) )
12	11	mpteq2dv	|- ( p = O -> ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) = ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) )
13	12	oveq2d	|- ( p = O -> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) = ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) )
14	13	mpoeq3dv	|- ( p = O -> ( 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 ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
15		simp3	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> O e. L )
16		simp1	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> N e. Fin )
17		mpoexga	|- ( ( N e. Fin /\ N e. Fin ) -> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) e. _V )
18	16 16 17	syl2anc	|- ( ( 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. _V )
19	7 14 15 18	fvmptd3	|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( I ` O ) = ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )