Metamath Proof Explorer

Theorem decpmatmullem

Description: Lemma for decpmatmul . (Contributed by AV, 20-Oct-2019) (Revised by AV, 3-Dec-2019)

Ref Expression
Hypotheses decpmatmul.p 
|- P = ( Poly1 ` R )
decpmatmul.c 
|- C = ( N Mat P )
decpmatmul.b 
|- B = ( Base ` C )
Assertion decpmatmullem 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( I ( ( U ( .r ` C ) W ) decompPMat K ) J ) = ( R gsum ( t e. N |-> ( R gsum ( l e. ( 0 ... K ) |-> ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( K - l ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 decpmatmul.p 
 |-  P = ( Poly1 ` R )
2 decpmatmul.c 
 |-  C = ( N Mat P )
3 decpmatmul.b 
 |-  B = ( Base ` C )
4 simpr 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Ring )
5 4 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> R e. Ring )
6 1 2 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
7 6 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) ) -> C e. Ring )
8 simpl 
 |-  ( ( U e. B /\ W e. B ) -> U e. B )
9 8 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) ) -> U e. B )
10 simpr 
 |-  ( ( U e. B /\ W e. B ) -> W e. B )
11 10 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) ) -> W e. B )
12 eqid 
 |-  ( .r ` C ) = ( .r ` C )
13 3 12 ringcl 
 |-  ( ( C e. Ring /\ U e. B /\ W e. B ) -> ( U ( .r ` C ) W ) e. B )
14 7 9 11 13 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) ) -> ( U ( .r ` C ) W ) e. B )
15 14 3adant3 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( U ( .r ` C ) W ) e. B )
16 simp33 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> K e. NN0 )
17 3simpa 
 |-  ( ( I e. N /\ J e. N /\ K e. NN0 ) -> ( I e. N /\ J e. N ) )
18 17 3ad2ant3 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( I e. N /\ J e. N ) )
19 1 2 3 decpmate 
 |-  ( ( ( R e. Ring /\ ( U ( .r ` C ) W ) e. B /\ K e. NN0 ) /\ ( I e. N /\ J e. N ) ) -> ( I ( ( U ( .r ` C ) W ) decompPMat K ) J ) = ( ( coe1 ` ( I ( U ( .r ` C ) W ) J ) ) ` K ) )
20 5 15 16 18 19 syl31anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( I ( ( U ( .r ` C ) W ) decompPMat K ) J ) = ( ( coe1 ` ( I ( U ( .r ` C ) W ) J ) ) ` K ) )
21 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
22 eqid 
 |-  ( P maMul <. N , N , N >. ) = ( P maMul <. N , N , N >. )
23 2 22 matmulr 
 |-  ( ( N e. Fin /\ P e. Ring ) -> ( P maMul <. N , N , N >. ) = ( .r ` C ) )
24 23 eqcomd 
 |-  ( ( N e. Fin /\ P e. Ring ) -> ( .r ` C ) = ( P maMul <. N , N , N >. ) )
25 21 24 sylan2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( .r ` C ) = ( P maMul <. N , N , N >. ) )
26 25 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( .r ` C ) = ( P maMul <. N , N , N >. ) )
27 26 oveqd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( U ( .r ` C ) W ) = ( U ( P maMul <. N , N , N >. ) W ) )
28 27 oveqd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( I ( U ( .r ` C ) W ) J ) = ( I ( U ( P maMul <. N , N , N >. ) W ) J ) )
29 eqid 
 |-  ( Base ` P ) = ( Base ` P )
30 eqid 
 |-  ( .r ` P ) = ( .r ` P )
31 21 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> P e. Ring )
32 31 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> P e. Ring )
33 simpl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> N e. Fin )
34 33 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> N e. Fin )
35 2 29 matbas2 
 |-  ( ( N e. Fin /\ P e. Ring ) -> ( ( Base ` P ) ^m ( N X. N ) ) = ( Base ` C ) )
36 3 35 eqtr4id 
 |-  ( ( N e. Fin /\ P e. Ring ) -> B = ( ( Base ` P ) ^m ( N X. N ) ) )
37 21 36 sylan2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> B = ( ( Base ` P ) ^m ( N X. N ) ) )
38 37 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( U e. B <-> U e. ( ( Base ` P ) ^m ( N X. N ) ) ) )
39 38 biimpcd 
 |-  ( U e. B -> ( ( N e. Fin /\ R e. Ring ) -> U e. ( ( Base ` P ) ^m ( N X. N ) ) ) )
40 39 adantr 
 |-  ( ( U e. B /\ W e. B ) -> ( ( N e. Fin /\ R e. Ring ) -> U e. ( ( Base ` P ) ^m ( N X. N ) ) ) )
41 40 impcom 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) ) -> U e. ( ( Base ` P ) ^m ( N X. N ) ) )
42 41 3adant3 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> U e. ( ( Base ` P ) ^m ( N X. N ) ) )
43 21 35 sylan2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( Base ` P ) ^m ( N X. N ) ) = ( Base ` C ) )
44 3 43 eqtr4id 
 |-  ( ( N e. Fin /\ R e. Ring ) -> B = ( ( Base ` P ) ^m ( N X. N ) ) )
45 44 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( W e. B <-> W e. ( ( Base ` P ) ^m ( N X. N ) ) ) )
46 45 biimpcd 
 |-  ( W e. B -> ( ( N e. Fin /\ R e. Ring ) -> W e. ( ( Base ` P ) ^m ( N X. N ) ) ) )
47 46 adantl 
 |-  ( ( U e. B /\ W e. B ) -> ( ( N e. Fin /\ R e. Ring ) -> W e. ( ( Base ` P ) ^m ( N X. N ) ) ) )
48 47 impcom 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) ) -> W e. ( ( Base ` P ) ^m ( N X. N ) ) )
49 48 3adant3 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> W e. ( ( Base ` P ) ^m ( N X. N ) ) )
50 simp31 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> I e. N )
51 simp32 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> J e. N )
52 22 29 30 32 34 34 34 42 49 50 51 mamufv 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( I ( U ( P maMul <. N , N , N >. ) W ) J ) = ( P gsum ( t e. N |-> ( ( I U t ) ( .r ` P ) ( t W J ) ) ) ) )
53 28 52 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( I ( U ( .r ` C ) W ) J ) = ( P gsum ( t e. N |-> ( ( I U t ) ( .r ` P ) ( t W J ) ) ) ) )
54 53 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( coe1 ` ( I ( U ( .r ` C ) W ) J ) ) = ( coe1 ` ( P gsum ( t e. N |-> ( ( I U t ) ( .r ` P ) ( t W J ) ) ) ) ) )
55 54 fveq1d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( ( coe1 ` ( I ( U ( .r ` C ) W ) J ) ) ` K ) = ( ( coe1 ` ( P gsum ( t e. N |-> ( ( I U t ) ( .r ` P ) ( t W J ) ) ) ) ) ` K ) )
56 32 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) /\ t e. N ) -> P e. Ring )
57 50 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) /\ t e. N ) -> I e. N )
58 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) /\ t e. N ) -> t e. N )
59 simpl2l 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) /\ t e. N ) -> U e. B )
60 2 29 3 57 58 59 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) /\ t e. N ) -> ( I U t ) e. ( Base ` P ) )
61 51 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) /\ t e. N ) -> J e. N )
62 simpl2r 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) /\ t e. N ) -> W e. B )
63 2 29 3 58 61 62 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) /\ t e. N ) -> ( t W J ) e. ( Base ` P ) )
64 29 30 ringcl 
 |-  ( ( P e. Ring /\ ( I U t ) e. ( Base ` P ) /\ ( t W J ) e. ( Base ` P ) ) -> ( ( I U t ) ( .r ` P ) ( t W J ) ) e. ( Base ` P ) )
65 56 60 63 64 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) /\ t e. N ) -> ( ( I U t ) ( .r ` P ) ( t W J ) ) e. ( Base ` P ) )
66 65 ralrimiva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> A. t e. N ( ( I U t ) ( .r ` P ) ( t W J ) ) e. ( Base ` P ) )
67 1 29 5 16 66 34 coe1fzgsumd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( ( coe1 ` ( P gsum ( t e. N |-> ( ( I U t ) ( .r ` P ) ( t W J ) ) ) ) ) ` K ) = ( R gsum ( t e. N |-> ( ( coe1 ` ( ( I U t ) ( .r ` P ) ( t W J ) ) ) ` K ) ) ) )
68 simpl1r 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) /\ t e. N ) -> R e. Ring )
69 eqid 
 |-  ( .r ` R ) = ( .r ` R )
70 1 30 69 29 coe1mul 
 |-  ( ( R e. Ring /\ ( I U t ) e. ( Base ` P ) /\ ( t W J ) e. ( Base ` P ) ) -> ( coe1 ` ( ( I U t ) ( .r ` P ) ( t W J ) ) ) = ( k e. NN0 |-> ( R gsum ( l e. ( 0 ... k ) |-> ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( k - l ) ) ) ) ) ) )
71 68 60 63 70 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) /\ t e. N ) -> ( coe1 ` ( ( I U t ) ( .r ` P ) ( t W J ) ) ) = ( k e. NN0 |-> ( R gsum ( l e. ( 0 ... k ) |-> ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( k - l ) ) ) ) ) ) )
72 oveq2 
 |-  ( k = K -> ( 0 ... k ) = ( 0 ... K ) )
73 fvoveq1 
 |-  ( k = K -> ( ( coe1 ` ( t W J ) ) ` ( k - l ) ) = ( ( coe1 ` ( t W J ) ) ` ( K - l ) ) )
74 73 oveq2d 
 |-  ( k = K -> ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( k - l ) ) ) = ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( K - l ) ) ) )
75 72 74 mpteq12dv 
 |-  ( k = K -> ( l e. ( 0 ... k ) |-> ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( k - l ) ) ) ) = ( l e. ( 0 ... K ) |-> ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( K - l ) ) ) ) )
76 75 oveq2d 
 |-  ( k = K -> ( R gsum ( l e. ( 0 ... k ) |-> ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( k - l ) ) ) ) ) = ( R gsum ( l e. ( 0 ... K ) |-> ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( K - l ) ) ) ) ) )
77 76 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) /\ t e. N ) /\ k = K ) -> ( R gsum ( l e. ( 0 ... k ) |-> ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( k - l ) ) ) ) ) = ( R gsum ( l e. ( 0 ... K ) |-> ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( K - l ) ) ) ) ) )
78 16 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) /\ t e. N ) -> K e. NN0 )
79 ovexd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) /\ t e. N ) -> ( R gsum ( l e. ( 0 ... K ) |-> ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( K - l ) ) ) ) ) e. _V )
80 71 77 78 79 fvmptd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) /\ t e. N ) -> ( ( coe1 ` ( ( I U t ) ( .r ` P ) ( t W J ) ) ) ` K ) = ( R gsum ( l e. ( 0 ... K ) |-> ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( K - l ) ) ) ) ) )
81 80 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( t e. N |-> ( ( coe1 ` ( ( I U t ) ( .r ` P ) ( t W J ) ) ) ` K ) ) = ( t e. N |-> ( R gsum ( l e. ( 0 ... K ) |-> ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( K - l ) ) ) ) ) ) )
82 81 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( R gsum ( t e. N |-> ( ( coe1 ` ( ( I U t ) ( .r ` P ) ( t W J ) ) ) ` K ) ) ) = ( R gsum ( t e. N |-> ( R gsum ( l e. ( 0 ... K ) |-> ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( K - l ) ) ) ) ) ) ) )
83 67 82 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( ( coe1 ` ( P gsum ( t e. N |-> ( ( I U t ) ( .r ` P ) ( t W J ) ) ) ) ) ` K ) = ( R gsum ( t e. N |-> ( R gsum ( l e. ( 0 ... K ) |-> ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( K - l ) ) ) ) ) ) ) )
84 20 55 83 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( I ( ( U ( .r ` C ) W ) decompPMat K ) J ) = ( R gsum ( t e. N |-> ( R gsum ( l e. ( 0 ... K ) |-> ( ( ( coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( ( coe1 ` ( t W J ) ) ` ( K - l ) ) ) ) ) ) ) )