Metamath Proof Explorer

Theorem mp2pm2mplem3

Description: Lemma 3 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 )
Assertion mp2pm2mplem3 
|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( ( I ` O ) decompPMat K ) = ( i e. N , j e. N |-> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) ) )

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 1 2 3 4 5 6 7 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 ) ) ) ) ) )
10 9 oveq1d 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( ( I ` O ) decompPMat K ) = ( ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) decompPMat K ) )
11 10 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( ( I ` O ) decompPMat K ) = ( ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) decompPMat K ) )
12 eqid 
 |-  ( N Mat P ) = ( N Mat P )
13 eqid 
 |-  ( Base ` ( N Mat P ) ) = ( Base ` ( N Mat P ) )
14 1 2 3 4 5 6 7 8 12 13 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. ( Base ` ( N Mat P ) ) )
15 12 13 decpmatval 
 |-  ( ( ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) e. ( Base ` ( N Mat P ) ) /\ K e. NN0 ) -> ( ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) decompPMat K ) = ( a e. N , b e. N |-> ( ( coe1 ` ( a ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) b ) ) ` K ) ) )
16 14 15 sylan 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) decompPMat K ) = ( a e. N , b e. N |-> ( ( coe1 ` ( a ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) b ) ) ` K ) ) )
17 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ a e. N /\ b e. N ) -> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` 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 ) ) ) ) ) )
18 oveq12 
 |-  ( ( i = a /\ j = b ) -> ( i ( ( coe1 ` O ) ` k ) j ) = ( a ( ( coe1 ` O ) ` k ) b ) )
19 18 oveq1d 
 |-  ( ( i = a /\ j = b ) -> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) = ( ( a ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) )
20 19 mpteq2dv 
 |-  ( ( i = a /\ j = b ) -> ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) = ( k e. NN0 |-> ( ( a ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) )
21 20 oveq2d 
 |-  ( ( i = a /\ j = b ) -> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) = ( P gsum ( k e. NN0 |-> ( ( a ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) )
22 21 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ a e. N /\ b e. N ) /\ ( i = a /\ j = b ) ) -> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) = ( P gsum ( k e. NN0 |-> ( ( a ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) )
23 simp2 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ a e. N /\ b e. N ) -> a e. N )
24 simp3 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ a e. N /\ b e. N ) -> b e. N )
25 ovexd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ a e. N /\ b e. N ) -> ( P gsum ( k e. NN0 |-> ( ( a ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) e. _V )
26 17 22 23 24 25 ovmpod 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ a e. N /\ b e. N ) -> ( a ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) b ) = ( P gsum ( k e. NN0 |-> ( ( a ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) )
27 26 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ a e. N /\ b e. N ) -> ( coe1 ` ( a ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) b ) ) = ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( a ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) ) )
28 27 fveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ a e. N /\ b e. N ) -> ( ( coe1 ` ( a ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) b ) ) ` K ) = ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( a ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) ) ` K ) )
29 28 mpoeq3dva 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( a e. N , b e. N |-> ( ( coe1 ` ( a ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) b ) ) ` K ) ) = ( a e. N , b e. N |-> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( a ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) ) ` K ) ) )
30 oveq1 
 |-  ( a = i -> ( a ( ( coe1 ` O ) ` k ) b ) = ( i ( ( coe1 ` O ) ` k ) b ) )
31 30 oveq1d 
 |-  ( a = i -> ( ( a ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) = ( ( i ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) )
32 31 mpteq2dv 
 |-  ( a = i -> ( k e. NN0 |-> ( ( a ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) = ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) )
33 32 oveq2d 
 |-  ( a = i -> ( P gsum ( k e. NN0 |-> ( ( a ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) = ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) )
34 33 fveq2d 
 |-  ( a = i -> ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( a ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) ) = ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) ) )
35 34 fveq1d 
 |-  ( a = i -> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( a ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) ) ` K ) = ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) ) ` K ) )
36 simpl 
 |-  ( ( b = j /\ k e. NN0 ) -> b = j )
37 36 oveq2d 
 |-  ( ( b = j /\ k e. NN0 ) -> ( i ( ( coe1 ` O ) ` k ) b ) = ( i ( ( coe1 ` O ) ` k ) j ) )
38 37 oveq1d 
 |-  ( ( b = j /\ k e. NN0 ) -> ( ( i ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) = ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) )
39 38 mpteq2dva 
 |-  ( b = j -> ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) = ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) )
40 39 oveq2d 
 |-  ( b = j -> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) = ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) )
41 40 fveq2d 
 |-  ( b = j -> ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) ) = ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
42 41 fveq1d 
 |-  ( b = j -> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) ) ` K ) = ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) )
43 35 42 cbvmpov 
 |-  ( a e. N , b e. N |-> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( a ( ( coe1 ` O ) ` k ) b ) .x. ( k E Y ) ) ) ) ) ` K ) ) = ( i e. N , j e. N |-> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) )
44 29 43 eqtrdi 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( a e. N , b e. N |-> ( ( coe1 ` ( a ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) b ) ) ` K ) ) = ( i e. N , j e. N |-> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) ) )
45 11 16 44 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( ( I ` O ) decompPMat K ) = ( i e. N , j e. N |-> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) ) )