MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  decpmatmul Structured version   Unicode version

Theorem decpmatmul 19035
Description: The matrix consisting of the coefficients in the polynomial entries of the product of two polynomial matrices is a sum of products of the matrices consisting of the coefficients in the polynomial entries of the polynomial matrices for the same power (Contributed by AV, 21-Oct-2019.) (Revised by AV, 3-Dec-2019.)
Hypotheses
Ref Expression
decpmatmul.p  |-  P  =  (Poly1 `  R )
decpmatmul.c  |-  C  =  ( N Mat  P )
decpmatmul.b  |-  B  =  ( Base `  C
)
decpmatmul.a  |-  A  =  ( N Mat  R )
Assertion
Ref Expression
decpmatmul  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  ( ( U ( .r `  C
) W ) decompPMat  K )  =  ( A  gsumg  ( k  e.  ( 0 ... K )  |->  ( ( U decompPMat  k ) ( .r
`  A ) ( W decompPMat  ( K  -  k
) ) ) ) ) )
Distinct variable groups:    B, k    k, K    k, N    P, k    R, k    U, k   
k, W    A, k
Allowed substitution hint:    C( k)

Proof of Theorem decpmatmul
Dummy variables  t 
i  j  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqidd 2463 . . . . 5  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( x  e.  N ,  y  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) ) ) )  =  ( x  e.  N , 
y  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) ) ) ) )
2 oveq1 6284 . . . . . . . . . . 11  |-  ( x  =  i  ->  (
x ( U decompPMat  k ) t )  =  ( i ( U decompPMat  k ) t ) )
3 oveq2 6285 . . . . . . . . . . 11  |-  ( y  =  j  ->  (
t ( W decompPMat  ( K  -  k ) ) y )  =  ( t ( W decompPMat  ( K  -  k ) ) j ) )
42, 3oveqan12d 6296 . . . . . . . . . 10  |-  ( ( x  =  i  /\  y  =  j )  ->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) )  =  ( ( i ( U decompPMat  k ) t ) ( .r
`  R ) ( t ( W decompPMat  ( K  -  k ) ) j ) ) )
54mpteq2dv 4529 . . . . . . . . 9  |-  ( ( x  =  i  /\  y  =  j )  ->  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) )  =  ( t  e.  N  |->  ( ( i ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) j ) ) ) )
65oveq2d 6293 . . . . . . . 8  |-  ( ( x  =  i  /\  y  =  j )  ->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) )  =  ( R  gsumg  ( t  e.  N  |->  ( ( i ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) j ) ) ) ) )
76mpteq2dv 4529 . . . . . . 7  |-  ( ( x  =  i  /\  y  =  j )  ->  ( k  e.  ( 0 ... K ) 
|->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) )  =  ( k  e.  ( 0 ... K
)  |->  ( R  gsumg  ( t  e.  N  |->  ( ( i ( U decompPMat  k ) t ) ( .r
`  R ) ( t ( W decompPMat  ( K  -  k ) ) j ) ) ) ) ) )
87oveq2d 6293 . . . . . 6  |-  ( ( x  =  i  /\  y  =  j )  ->  ( R  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) ) )  =  ( R 
gsumg  ( k  e.  ( 0 ... K ) 
|->  ( R  gsumg  ( t  e.  N  |->  ( ( i ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) j ) ) ) ) ) ) )
98adantl 466 . . . . 5  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  ( x  =  i  /\  y  =  j ) )  ->  ( R  gsumg  ( k  e.  ( 0 ... K )  |->  ( R 
gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) ) )  =  ( R 
gsumg  ( k  e.  ( 0 ... K ) 
|->  ( R  gsumg  ( t  e.  N  |->  ( ( i ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) j ) ) ) ) ) ) )
10 simprl 755 . . . . 5  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
i  e.  N )
11 simprr 756 . . . . 5  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
j  e.  N )
12 ovex 6302 . . . . . 6  |-  ( R 
gsumg  ( k  e.  ( 0 ... K ) 
|->  ( R  gsumg  ( t  e.  N  |->  ( ( i ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) j ) ) ) ) ) )  e.  _V
1312a1i 11 . . . . 5  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( R  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( R  gsumg  ( t  e.  N  |->  ( ( i ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) j ) ) ) ) ) )  e.  _V )
141, 9, 10, 11, 13ovmpt2d 6407 . . . 4  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( i ( x  e.  N ,  y  e.  N  |->  ( R 
gsumg  ( k  e.  ( 0 ... K ) 
|->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) ) ) ) j )  =  ( R  gsumg  ( k  e.  ( 0 ... K )  |->  ( R 
gsumg  ( t  e.  N  |->  ( ( i ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) j ) ) ) ) ) ) )
15 decpmatmul.c . . . . . . . . . . . . . . . . . . . 20  |-  C  =  ( N Mat  P )
16 decpmatmul.b . . . . . . . . . . . . . . . . . . . 20  |-  B  =  ( Base `  C
)
1715, 16matrcl 18676 . . . . . . . . . . . . . . . . . . 19  |-  ( U  e.  B  ->  ( N  e.  Fin  /\  P  e.  _V ) )
1817simpld 459 . . . . . . . . . . . . . . . . . 18  |-  ( U  e.  B  ->  N  e.  Fin )
1918adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( U  e.  B  /\  W  e.  B )  ->  N  e.  Fin )
2019anim2i 569 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )
)  ->  ( R  e.  Ring  /\  N  e.  Fin ) )
2120ancomd 451 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )
)  ->  ( N  e.  Fin  /\  R  e. 
Ring ) )
22213adant3 1011 . . . . . . . . . . . . . 14  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  ( N  e. 
Fin  /\  R  e.  Ring ) )
23 decpmatmul.a . . . . . . . . . . . . . . 15  |-  A  =  ( N Mat  R )
24 eqid 2462 . . . . . . . . . . . . . . 15  |-  ( R maMul  <. N ,  N ,  N >. )  =  ( R maMul  <. N ,  N ,  N >. )
2523, 24matmulr 18702 . . . . . . . . . . . . . 14  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( R maMul  <. N ,  N ,  N >. )  =  ( .r `  A ) )
2622, 25syl 16 . . . . . . . . . . . . 13  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  ( R maMul  <. N ,  N ,  N >. )  =  ( .r `  A ) )
2726adantr 465 . . . . . . . . . . . 12  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( R maMul  <. N ,  N ,  N >. )  =  ( .r `  A ) )
2827adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  ( R maMul  <. N ,  N ,  N >. )  =  ( .r `  A ) )
2928eqcomd 2470 . . . . . . . . . 10  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  ( .r `  A )  =  ( R maMul  <. N ,  N ,  N >. ) )
3029oveqd 6294 . . . . . . . . 9  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  (
( U decompPMat  k ) ( .r `  A ) ( W decompPMat  ( K  -  k ) ) )  =  ( ( U decompPMat  k ) ( R maMul  <. N ,  N ,  N >. ) ( W decompPMat  ( K  -  k
) ) ) )
31 eqid 2462 . . . . . . . . . 10  |-  ( Base `  R )  =  (
Base `  R )
32 eqid 2462 . . . . . . . . . 10  |-  ( .r
`  R )  =  ( .r `  R
)
33 simp1 991 . . . . . . . . . . . 12  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  R  e.  Ring )
3433adantr 465 . . . . . . . . . . 11  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  ->  R  e.  Ring )
3534adantr 465 . . . . . . . . . 10  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  R  e.  Ring )
3622simpld 459 . . . . . . . . . . . 12  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  N  e.  Fin )
3736adantr 465 . . . . . . . . . . 11  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  ->  N  e.  Fin )
3837adantr 465 . . . . . . . . . 10  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  N  e.  Fin )
39 simpl2l 1044 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  ->  U  e.  B )
4039adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  U  e.  B )
41 elfznn0 11761 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... K )  ->  k  e.  NN0 )
4241adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  k  e.  NN0 )
4335, 40, 423jca 1171 . . . . . . . . . . . 12  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  ( R  e.  Ring  /\  U  e.  B  /\  k  e.  NN0 ) )
44 decpmatmul.p . . . . . . . . . . . . 13  |-  P  =  (Poly1 `  R )
45 eqid 2462 . . . . . . . . . . . . 13  |-  ( Base `  A )  =  (
Base `  A )
4644, 15, 16, 23, 45decpmatcl 19030 . . . . . . . . . . . 12  |-  ( ( R  e.  Ring  /\  U  e.  B  /\  k  e.  NN0 )  ->  ( U decompPMat  k )  e.  (
Base `  A )
)
4743, 46syl 16 . . . . . . . . . . 11  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  ( U decompPMat  k )  e.  (
Base `  A )
)
4823, 31, 45matbas2i 18686 . . . . . . . . . . 11  |-  ( ( U decompPMat  k )  e.  (
Base `  A )  ->  ( U decompPMat  k )  e.  ( ( Base `  R
)  ^m  ( N  X.  N ) ) )
4947, 48syl 16 . . . . . . . . . 10  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  ( U decompPMat  k )  e.  ( ( Base `  R
)  ^m  ( N  X.  N ) ) )
50 simpl2r 1045 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  ->  W  e.  B )
5150adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  W  e.  B )
52 fznn0sub 11707 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... K )  ->  ( K  -  k )  e.  NN0 )
5352adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  ( K  -  k )  e.  NN0 )
5435, 51, 533jca 1171 . . . . . . . . . . . 12  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  ( R  e.  Ring  /\  W  e.  B  /\  ( K  -  k )  e.  NN0 ) )
5544, 15, 16, 23, 45decpmatcl 19030 . . . . . . . . . . . 12  |-  ( ( R  e.  Ring  /\  W  e.  B  /\  ( K  -  k )  e.  NN0 )  ->  ( W decompPMat  ( K  -  k
) )  e.  (
Base `  A )
)
5654, 55syl 16 . . . . . . . . . . 11  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  ( W decompPMat  ( K  -  k
) )  e.  (
Base `  A )
)
5723, 31, 45matbas2i 18686 . . . . . . . . . . 11  |-  ( ( W decompPMat  ( K  -  k
) )  e.  (
Base `  A )  ->  ( W decompPMat  ( K  -  k ) )  e.  ( ( Base `  R )  ^m  ( N  X.  N ) ) )
5856, 57syl 16 . . . . . . . . . 10  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  ( W decompPMat  ( K  -  k
) )  e.  ( ( Base `  R
)  ^m  ( N  X.  N ) ) )
5924, 31, 32, 35, 38, 38, 38, 49, 58mamuval 18650 . . . . . . . . 9  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  (
( U decompPMat  k ) ( R maMul  <. N ,  N ,  N >. ) ( W decompPMat  ( K  -  k
) ) )  =  ( x  e.  N ,  y  e.  N  |->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) ) )
6030, 59eqtrd 2503 . . . . . . . 8  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  (
( U decompPMat  k ) ( .r `  A ) ( W decompPMat  ( K  -  k ) ) )  =  ( x  e.  N ,  y  e.  N  |->  ( R 
gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) ) )
6160mpteq2dva 4528 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( k  e.  ( 0 ... K ) 
|->  ( ( U decompPMat  k ) ( .r `  A
) ( W decompPMat  ( K  -  k ) ) ) )  =  ( k  e.  ( 0 ... K )  |->  ( x  e.  N , 
y  e.  N  |->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) ) ) )
6261oveq2d 6293 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( A  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( ( U decompPMat  k ) ( .r `  A
) ( W decompPMat  ( K  -  k ) ) ) ) )  =  ( A  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( x  e.  N ,  y  e.  N  |->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) ) ) ) )
63 eqid 2462 . . . . . . 7  |-  ( 0g
`  A )  =  ( 0g `  A
)
64 ovex 6302 . . . . . . . 8  |-  ( 0 ... K )  e. 
_V
6564a1i 11 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( 0 ... K
)  e.  _V )
66 rngcmn 17011 . . . . . . . . . . . . 13  |-  ( R  e.  Ring  ->  R  e. CMnd
)
6733, 66syl 16 . . . . . . . . . . . 12  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  R  e. CMnd )
6867adantr 465 . . . . . . . . . . 11  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  ->  R  e. CMnd )
6968adantr 465 . . . . . . . . . 10  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  R  e. CMnd )
70693ad2ant1 1012 . . . . . . . . 9  |-  ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  ->  R  e. CMnd )
71383ad2ant1 1012 . . . . . . . . 9  |-  ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  ->  N  e.  Fin )
72353ad2ant1 1012 . . . . . . . . . . . 12  |-  ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  ->  R  e.  Ring )
7372adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  /\  t  e.  N )  ->  R  e.  Ring )
74 simpl2 995 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  /\  t  e.  N )  ->  x  e.  N )
75 simpr 461 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  /\  t  e.  N )  ->  t  e.  N )
76433ad2ant1 1012 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  ->  ( R  e.  Ring  /\  U  e.  B  /\  k  e.  NN0 ) )
7776adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  /\  t  e.  N )  ->  ( R  e.  Ring  /\  U  e.  B  /\  k  e.  NN0 ) )
7877, 46syl 16 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  /\  t  e.  N )  ->  ( U decompPMat  k )  e.  (
Base `  A )
)
7923, 31, 45, 74, 75, 78matecld 18690 . . . . . . . . . . 11  |-  ( ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  /\  t  e.  N )  ->  (
x ( U decompPMat  k ) t )  e.  (
Base `  R )
)
80 simpl3 996 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  /\  t  e.  N )  ->  y  e.  N )
81563ad2ant1 1012 . . . . . . . . . . . . 13  |-  ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  ->  ( W decompPMat  ( K  -  k ) )  e.  ( Base `  A ) )
8281adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  /\  t  e.  N )  ->  ( W decompPMat  ( K  -  k
) )  e.  (
Base `  A )
)
8323, 31, 45, 75, 80, 82matecld 18690 . . . . . . . . . . 11  |-  ( ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  /\  t  e.  N )  ->  (
t ( W decompPMat  ( K  -  k ) ) y )  e.  (
Base `  R )
)
8431, 32rngcl 16994 . . . . . . . . . . 11  |-  ( ( R  e.  Ring  /\  (
x ( U decompPMat  k ) t )  e.  (
Base `  R )  /\  ( t ( W decompPMat  ( K  -  k
) ) y )  e.  ( Base `  R
) )  ->  (
( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) )  e.  ( Base `  R ) )
8573, 79, 83, 84syl3anc 1223 . . . . . . . . . 10  |-  ( ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  /\  t  e.  N )  ->  (
( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) )  e.  ( Base `  R ) )
8685ralrimiva 2873 . . . . . . . . 9  |-  ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  ->  A. t  e.  N  ( (
x ( U decompPMat  k ) t ) ( .r
`  R ) ( t ( W decompPMat  ( K  -  k ) ) y ) )  e.  ( Base `  R
) )
8731, 70, 71, 86gsummptcl 16780 . . . . . . . 8  |-  ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  x  e.  N  /\  y  e.  N
)  ->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) )  e.  ( Base `  R
) )
8823, 31, 45, 38, 35, 87matbas2d 18687 . . . . . . 7  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  (
x  e.  N , 
y  e.  N  |->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) )  e.  ( Base `  A
) )
89 eqid 2462 . . . . . . . 8  |-  ( k  e.  ( 0 ... K )  |->  ( x  e.  N ,  y  e.  N  |->  ( R 
gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) ) )  =  ( k  e.  ( 0 ... K )  |->  ( x  e.  N ,  y  e.  N  |->  ( R 
gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) ) )
90 fzfid 12041 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( 0 ... K
)  e.  Fin )
91 simpl 457 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  Fin  /\  P  e.  _V )  ->  N  e.  Fin )
9291, 91jca 532 . . . . . . . . . . . . . 14  |-  ( ( N  e.  Fin  /\  P  e.  _V )  ->  ( N  e.  Fin  /\  N  e.  Fin )
)
9317, 92syl 16 . . . . . . . . . . . . 13  |-  ( U  e.  B  ->  ( N  e.  Fin  /\  N  e.  Fin ) )
9493adantr 465 . . . . . . . . . . . 12  |-  ( ( U  e.  B  /\  W  e.  B )  ->  ( N  e.  Fin  /\  N  e.  Fin )
)
95943ad2ant2 1013 . . . . . . . . . . 11  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  ( N  e. 
Fin  /\  N  e.  Fin ) )
9695adantr 465 . . . . . . . . . 10  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( N  e.  Fin  /\  N  e.  Fin )
)
9796adantr 465 . . . . . . . . 9  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  ( N  e.  Fin  /\  N  e.  Fin ) )
98 mpt2exga 6851 . . . . . . . . 9  |-  ( ( N  e.  Fin  /\  N  e.  Fin )  ->  ( x  e.  N ,  y  e.  N  |->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) )  e.  _V )
9997, 98syl 16 . . . . . . . 8  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  (
x  e.  N , 
y  e.  N  |->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) )  e.  _V )
100 fvex 5869 . . . . . . . . 9  |-  ( 0g
`  A )  e. 
_V
101100a1i 11 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( 0g `  A
)  e.  _V )
10289, 90, 99, 101fsuppmptdm 7831 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( k  e.  ( 0 ... K ) 
|->  ( x  e.  N ,  y  e.  N  |->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) ) ) finSupp  ( 0g `  A ) )
10323, 45, 63, 37, 65, 34, 88, 102matgsum 18701 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( A  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( x  e.  N ,  y  e.  N  |->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) ) ) )  =  ( x  e.  N , 
y  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) ) ) ) )
10462, 103eqtrd 2503 . . . . 5  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( A  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( ( U decompPMat  k ) ( .r `  A
) ( W decompPMat  ( K  -  k ) ) ) ) )  =  ( x  e.  N ,  y  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) ) ) ) )
105104oveqd 6294 . . . 4  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( i ( A 
gsumg  ( k  e.  ( 0 ... K ) 
|->  ( ( U decompPMat  k ) ( .r `  A
) ( W decompPMat  ( K  -  k ) ) ) ) ) j )  =  ( i ( x  e.  N ,  y  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( R  gsumg  ( t  e.  N  |->  ( ( x ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) y ) ) ) ) ) ) ) j ) )
106 simpl2 995 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( U  e.  B  /\  W  e.  B
) )
107 simpl3 996 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  ->  K  e.  NN0 )
10844, 15, 16decpmatmullem 19034 . . . . . 6  |-  ( ( ( 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  gsumg  ( t  e.  N  |->  ( R 
gsumg  ( k  e.  ( 0 ... K ) 
|->  ( ( (coe1 `  (
i U t ) ) `  k ) ( .r `  R
) ( (coe1 `  (
t W j ) ) `  ( K  -  k ) ) ) ) ) ) ) )
10937, 34, 106, 10, 11, 107, 108syl213anc 1242 . . . . 5  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( i ( ( U ( .r `  C ) W ) decompPMat  K ) j )  =  ( R  gsumg  ( t  e.  N  |->  ( R 
gsumg  ( k  e.  ( 0 ... K ) 
|->  ( ( (coe1 `  (
i U t ) ) `  k ) ( .r `  R
) ( (coe1 `  (
t W j ) ) `  ( K  -  k ) ) ) ) ) ) ) )
110 simpll1 1030 . . . . . . 7  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  ( t  e.  N  /\  k  e.  ( 0 ... K
) ) )  ->  R  e.  Ring )
111 simplrl 759 . . . . . . . . 9  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  ( t  e.  N  /\  k  e.  ( 0 ... K
) ) )  -> 
i  e.  N )
112 simprl 755 . . . . . . . . 9  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  ( t  e.  N  /\  k  e.  ( 0 ... K
) ) )  -> 
t  e.  N )
11316eleq2i 2540 . . . . . . . . . . . . . 14  |-  ( U  e.  B  <->  U  e.  ( Base `  C )
)
114113biimpi 194 . . . . . . . . . . . . 13  |-  ( U  e.  B  ->  U  e.  ( Base `  C
) )
115114adantr 465 . . . . . . . . . . . 12  |-  ( ( U  e.  B  /\  W  e.  B )  ->  U  e.  ( Base `  C ) )
1161153ad2ant2 1013 . . . . . . . . . . 11  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  U  e.  (
Base `  C )
)
117116adantr 465 . . . . . . . . . 10  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  ->  U  e.  ( Base `  C ) )
118117adantr 465 . . . . . . . . 9  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  ( t  e.  N  /\  k  e.  ( 0 ... K
) ) )  ->  U  e.  ( Base `  C ) )
119 eqid 2462 . . . . . . . . . 10  |-  ( Base `  P )  =  (
Base `  P )
12015, 119matecl 18689 . . . . . . . . 9  |-  ( ( i  e.  N  /\  t  e.  N  /\  U  e.  ( Base `  C ) )  -> 
( i U t )  e.  ( Base `  P ) )
121111, 112, 118, 120syl3anc 1223 . . . . . . . 8  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  ( t  e.  N  /\  k  e.  ( 0 ... K
) ) )  -> 
( i U t )  e.  ( Base `  P ) )
12241ad2antll 728 . . . . . . . 8  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  ( t  e.  N  /\  k  e.  ( 0 ... K
) ) )  -> 
k  e.  NN0 )
123 eqid 2462 . . . . . . . . 9  |-  (coe1 `  (
i U t ) )  =  (coe1 `  (
i U t ) )
124123, 119, 44, 31coe1fvalcl 18017 . . . . . . . 8  |-  ( ( ( i U t )  e.  ( Base `  P )  /\  k  e.  NN0 )  ->  (
(coe1 `  ( i U t ) ) `  k )  e.  (
Base `  R )
)
125121, 122, 124syl2anc 661 . . . . . . 7  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  ( t  e.  N  /\  k  e.  ( 0 ... K
) ) )  -> 
( (coe1 `  ( i U t ) ) `  k )  e.  (
Base `  R )
)
126 simplrr 760 . . . . . . . . 9  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  ( t  e.  N  /\  k  e.  ( 0 ... K
) ) )  -> 
j  e.  N )
12750adantr 465 . . . . . . . . 9  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  ( t  e.  N  /\  k  e.  ( 0 ... K
) ) )  ->  W  e.  B )
12815, 119, 16, 112, 126, 127matecld 18690 . . . . . . . 8  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  ( t  e.  N  /\  k  e.  ( 0 ... K
) ) )  -> 
( t W j )  e.  ( Base `  P ) )
12952ad2antll 728 . . . . . . . 8  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  ( t  e.  N  /\  k  e.  ( 0 ... K
) ) )  -> 
( K  -  k
)  e.  NN0 )
130 eqid 2462 . . . . . . . . 9  |-  (coe1 `  (
t W j ) )  =  (coe1 `  (
t W j ) )
131130, 119, 44, 31coe1fvalcl 18017 . . . . . . . 8  |-  ( ( ( t W j )  e.  ( Base `  P )  /\  ( K  -  k )  e.  NN0 )  ->  (
(coe1 `  ( t W j ) ) `  ( K  -  k
) )  e.  (
Base `  R )
)
132128, 129, 131syl2anc 661 . . . . . . 7  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  ( t  e.  N  /\  k  e.  ( 0 ... K
) ) )  -> 
( (coe1 `  ( t W j ) ) `  ( K  -  k
) )  e.  (
Base `  R )
)
13331, 32rngcl 16994 . . . . . . 7  |-  ( ( R  e.  Ring  /\  (
(coe1 `  ( i U t ) ) `  k )  e.  (
Base `  R )  /\  ( (coe1 `  ( t W j ) ) `  ( K  -  k
) )  e.  (
Base `  R )
)  ->  ( (
(coe1 `  ( i U t ) ) `  k ) ( .r
`  R ) ( (coe1 `  ( t W j ) ) `  ( K  -  k
) ) )  e.  ( Base `  R
) )
134110, 125, 132, 133syl3anc 1223 . . . . . 6  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  ( t  e.  N  /\  k  e.  ( 0 ... K
) ) )  -> 
( ( (coe1 `  (
i U t ) ) `  k ) ( .r `  R
) ( (coe1 `  (
t W j ) ) `  ( K  -  k ) ) )  e.  ( Base `  R ) )
13531, 68, 37, 90, 134gsumcom3fi 18664 . . . . 5  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( R  gsumg  ( t  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( ( (coe1 `  (
i U t ) ) `  k ) ( .r `  R
) ( (coe1 `  (
t W j ) ) `  ( K  -  k ) ) ) ) ) ) )  =  ( R 
gsumg  ( k  e.  ( 0 ... K ) 
|->  ( R  gsumg  ( t  e.  N  |->  ( ( (coe1 `  (
i U t ) ) `  k ) ( .r `  R
) ( (coe1 `  (
t W j ) ) `  ( K  -  k ) ) ) ) ) ) ) )
13643adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  t  e.  N
)  ->  ( R  e.  Ring  /\  U  e.  B  /\  k  e.  NN0 ) )
13710adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  i  e.  N )
138137anim1i 568 . . . . . . . . . . . 12  |-  ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  t  e.  N
)  ->  ( i  e.  N  /\  t  e.  N ) )
13944, 15, 16decpmate 19029 . . . . . . . . . . . 12  |-  ( ( ( R  e.  Ring  /\  U  e.  B  /\  k  e.  NN0 )  /\  ( i  e.  N  /\  t  e.  N
) )  ->  (
i ( U decompPMat  k ) t )  =  ( (coe1 `  ( i U t ) ) `  k ) )
140136, 138, 139syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  t  e.  N
)  ->  ( i
( U decompPMat  k ) t )  =  ( (coe1 `  ( i U t ) ) `  k
) )
14154adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  t  e.  N
)  ->  ( R  e.  Ring  /\  W  e.  B  /\  ( K  -  k )  e.  NN0 ) )
142 simplrr 760 . . . . . . . . . . . . . 14  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  j  e.  N )
143142anim1i 568 . . . . . . . . . . . . 13  |-  ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  t  e.  N
)  ->  ( j  e.  N  /\  t  e.  N ) )
144143ancomd 451 . . . . . . . . . . . 12  |-  ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  t  e.  N
)  ->  ( t  e.  N  /\  j  e.  N ) )
14544, 15, 16decpmate 19029 . . . . . . . . . . . 12  |-  ( ( ( R  e.  Ring  /\  W  e.  B  /\  ( K  -  k
)  e.  NN0 )  /\  ( t  e.  N  /\  j  e.  N
) )  ->  (
t ( W decompPMat  ( K  -  k ) ) j )  =  ( (coe1 `  ( t W j ) ) `  ( K  -  k
) ) )
146141, 144, 145syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  t  e.  N
)  ->  ( t
( W decompPMat  ( K  -  k ) ) j )  =  ( (coe1 `  ( t W j ) ) `  ( K  -  k )
) )
147140, 146oveq12d 6295 . . . . . . . . . 10  |-  ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  t  e.  N
)  ->  ( (
i ( U decompPMat  k ) t ) ( .r
`  R ) ( t ( W decompPMat  ( K  -  k ) ) j ) )  =  ( ( (coe1 `  (
i U t ) ) `  k ) ( .r `  R
) ( (coe1 `  (
t W j ) ) `  ( K  -  k ) ) ) )
148147eqcomd 2470 . . . . . . . . 9  |-  ( ( ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  ( 0 ... K ) )  /\  t  e.  N
)  ->  ( (
(coe1 `  ( i U t ) ) `  k ) ( .r
`  R ) ( (coe1 `  ( t W j ) ) `  ( K  -  k
) ) )  =  ( ( i ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) j ) ) )
149148mpteq2dva 4528 . . . . . . . 8  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  (
t  e.  N  |->  ( ( (coe1 `  ( i U t ) ) `  k ) ( .r
`  R ) ( (coe1 `  ( t W j ) ) `  ( K  -  k
) ) ) )  =  ( t  e.  N  |->  ( ( i ( U decompPMat  k )
t ) ( .r
`  R ) ( t ( W decompPMat  ( K  -  k ) ) j ) ) ) )
150149oveq2d 6293 . . . . . . 7  |-  ( ( ( ( R  e. 
Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  k  e.  ( 0 ... K
) )  ->  ( R  gsumg  ( t  e.  N  |->  ( ( (coe1 `  (
i U t ) ) `  k ) ( .r `  R
) ( (coe1 `  (
t W j ) ) `  ( K  -  k ) ) ) ) )  =  ( R  gsumg  ( t  e.  N  |->  ( ( i ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) j ) ) ) ) )
151150mpteq2dva 4528 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( k  e.  ( 0 ... K ) 
|->  ( R  gsumg  ( t  e.  N  |->  ( ( (coe1 `  (
i U t ) ) `  k ) ( .r `  R
) ( (coe1 `  (
t W j ) ) `  ( K  -  k ) ) ) ) ) )  =  ( k  e.  ( 0 ... K
)  |->  ( R  gsumg  ( t  e.  N  |->  ( ( i ( U decompPMat  k ) t ) ( .r
`  R ) ( t ( W decompPMat  ( K  -  k ) ) j ) ) ) ) ) )
152151oveq2d 6293 . . . . 5  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( R  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( R  gsumg  ( t  e.  N  |->  ( ( (coe1 `  (
i U t ) ) `  k ) ( .r `  R
) ( (coe1 `  (
t W j ) ) `  ( K  -  k ) ) ) ) ) ) )  =  ( R 
gsumg  ( k  e.  ( 0 ... K ) 
|->  ( R  gsumg  ( t  e.  N  |->  ( ( i ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) j ) ) ) ) ) ) )
153109, 135, 1523eqtrd 2507 . . . 4  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( i ( ( U ( .r `  C ) W ) decompPMat  K ) j )  =  ( R  gsumg  ( k  e.  ( 0 ... K )  |->  ( R 
gsumg  ( t  e.  N  |->  ( ( i ( U decompPMat  k ) t ) ( .r `  R
) ( t ( W decompPMat  ( K  -  k
) ) j ) ) ) ) ) ) )
15414, 105, 1533eqtr4rd 2514 . . 3  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  ( i  e.  N  /\  j  e.  N ) )  -> 
( i ( ( U ( .r `  C ) W ) decompPMat  K ) j )  =  ( i ( A  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( ( U decompPMat  k ) ( .r `  A
) ( W decompPMat  ( K  -  k ) ) ) ) ) j ) )
155154ralrimivva 2880 . 2  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  A. i  e.  N  A. j  e.  N  ( i ( ( U ( .r `  C ) W ) decompPMat  K ) j )  =  ( i ( A  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( ( U decompPMat  k ) ( .r `  A
) ( W decompPMat  ( K  -  k ) ) ) ) ) j ) )
15644, 15pmatrng 18956 . . . . . . 7  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  C  e.  Ring )
15721, 156syl 16 . . . . . 6  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )
)  ->  C  e.  Ring )
158 simprl 755 . . . . . 6  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )
)  ->  U  e.  B )
159 simprr 756 . . . . . 6  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )
)  ->  W  e.  B )
160 eqid 2462 . . . . . . 7  |-  ( .r
`  C )  =  ( .r `  C
)
16116, 160rngcl 16994 . . . . . 6  |-  ( ( C  e.  Ring  /\  U  e.  B  /\  W  e.  B )  ->  ( U ( .r `  C ) W )  e.  B )
162157, 158, 159, 161syl3anc 1223 . . . . 5  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )
)  ->  ( U
( .r `  C
) W )  e.  B )
1631623adant3 1011 . . . 4  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  ( U ( .r `  C ) W )  e.  B
)
16444, 15, 16, 23, 45decpmatcl 19030 . . . 4  |-  ( ( R  e.  Ring  /\  ( U ( .r `  C ) W )  e.  B  /\  K  e.  NN0 )  ->  (
( U ( .r
`  C ) W ) decompPMat  K )  e.  (
Base `  A )
)
165163, 164syld3an2 1270 . . 3  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  ( ( U ( .r `  C
) W ) decompPMat  K )  e.  ( Base `  A
) )
16623matrng 18707 . . . . . 6  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  A  e.  Ring )
16722, 166syl 16 . . . . 5  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  A  e.  Ring )
168 rngcmn 17011 . . . . 5  |-  ( A  e.  Ring  ->  A  e. CMnd
)
169167, 168syl 16 . . . 4  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  A  e. CMnd )
170 fzfid 12041 . . . 4  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  ( 0 ... K )  e.  Fin )
171167adantr 465 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  k  e.  ( 0 ... K
) )  ->  A  e.  Ring )
17233adantr 465 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  k  e.  ( 0 ... K
) )  ->  R  e.  Ring )
173 simpl2l 1044 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  k  e.  ( 0 ... K
) )  ->  U  e.  B )
17441adantl 466 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  k  e.  ( 0 ... K
) )  ->  k  e.  NN0 )
175172, 173, 1743jca 1171 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  k  e.  ( 0 ... K
) )  ->  ( R  e.  Ring  /\  U  e.  B  /\  k  e.  NN0 ) )
176175, 46syl 16 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  k  e.  ( 0 ... K
) )  ->  ( U decompPMat  k )  e.  (
Base `  A )
)
177 simpl2r 1045 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  k  e.  ( 0 ... K
) )  ->  W  e.  B )
17852adantl 466 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  k  e.  ( 0 ... K
) )  ->  ( K  -  k )  e.  NN0 )
179172, 177, 1783jca 1171 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  k  e.  ( 0 ... K
) )  ->  ( R  e.  Ring  /\  W  e.  B  /\  ( K  -  k )  e.  NN0 ) )
180179, 55syl 16 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  k  e.  ( 0 ... K
) )  ->  ( W decompPMat  ( K  -  k
) )  e.  (
Base `  A )
)
181 eqid 2462 . . . . . . 7  |-  ( .r
`  A )  =  ( .r `  A
)
18245, 181rngcl 16994 . . . . . 6  |-  ( ( A  e.  Ring  /\  ( U decompPMat  k )  e.  (
Base `  A )  /\  ( W decompPMat  ( K  -  k ) )  e.  ( Base `  A
) )  ->  (
( U decompPMat  k ) ( .r `  A ) ( W decompPMat  ( K  -  k ) ) )  e.  ( Base `  A ) )
183171, 176, 180, 182syl3anc 1223 . . . . 5  |-  ( ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B
)  /\  K  e.  NN0 )  /\  k  e.  ( 0 ... K
) )  ->  (
( U decompPMat  k ) ( .r `  A ) ( W decompPMat  ( K  -  k ) ) )  e.  ( Base `  A ) )
184183ralrimiva 2873 . . . 4  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  A. k  e.  ( 0 ... K ) ( ( U decompPMat  k ) ( .r `  A
) ( W decompPMat  ( K  -  k ) ) )  e.  ( Base `  A ) )
18545, 169, 170, 184gsummptcl 16780 . . 3  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  ( A  gsumg  ( k  e.  ( 0 ... K )  |->  ( ( U decompPMat  k ) ( .r
`  A ) ( W decompPMat  ( K  -  k
) ) ) ) )  e.  ( Base `  A ) )
18623, 45eqmat 18688 . . 3  |-  ( ( ( ( U ( .r `  C ) W ) decompPMat  K )  e.  ( Base `  A
)  /\  ( A  gsumg  ( k  e.  ( 0 ... K )  |->  ( ( U decompPMat  k )
( .r `  A
) ( W decompPMat  ( K  -  k ) ) ) ) )  e.  ( Base `  A
) )  ->  (
( ( U ( .r `  C ) W ) decompPMat  K )  =  ( A  gsumg  ( k  e.  ( 0 ... K )  |->  ( ( U decompPMat  k ) ( .r
`  A ) ( W decompPMat  ( K  -  k
) ) ) ) )  <->  A. i  e.  N  A. j  e.  N  ( i ( ( U ( .r `  C ) W ) decompPMat  K ) j )  =  ( i ( A  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( ( U decompPMat  k ) ( .r `  A
) ( W decompPMat  ( K  -  k ) ) ) ) ) j ) ) )
187165, 185, 186syl2anc 661 . 2  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  ( ( ( U ( .r `  C ) W ) decompPMat  K )  =  ( A  gsumg  ( k  e.  ( 0 ... K ) 
|->  ( ( U decompPMat  k ) ( .r `  A
) ( W decompPMat  ( K  -  k ) ) ) ) )  <->  A. i  e.  N  A. j  e.  N  ( i
( ( U ( .r `  C ) W ) decompPMat  K )
j )  =  ( i ( A  gsumg  ( k  e.  ( 0 ... K )  |->  ( ( U decompPMat  k ) ( .r
`  A ) ( W decompPMat  ( K  -  k
) ) ) ) ) j ) ) )
188155, 187mpbird 232 1  |-  ( ( R  e.  Ring  /\  ( U  e.  B  /\  W  e.  B )  /\  K  e.  NN0 )  ->  ( ( U ( .r `  C
) W ) decompPMat  K )  =  ( A  gsumg  ( k  e.  ( 0 ... K )  |->  ( ( U decompPMat  k ) ( .r
`  A ) ( W decompPMat  ( K  -  k
) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 968    = wceq 1374    e. wcel 1762   A.wral 2809   _Vcvv 3108   <.cotp 4030    |-> cmpt 4500    X. cxp 4992   ` cfv 5581  (class class class)co 6277    |-> cmpt2 6279    ^m cmap 7412   Fincfn 7508   0cc0 9483    - cmin 9796   NN0cn0 10786   ...cfz 11663   Basecbs 14481   .rcmulr 14547   0gc0g 14686    gsumg cgsu 14687  CMndccmn 16589   Ringcrg 16981  Poly1cpl1 17982  coe1cco1 17983   maMul cmmul 18647   Mat cmat 18671   decompPMat cdecpmat 19025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-rep 4553  ax-sep 4563  ax-nul 4571  ax-pow 4620  ax-pr 4681  ax-un 6569  ax-inf2 8049  ax-cnex 9539  ax-resscn 9540  ax-1cn 9541  ax-icn 9542  ax-addcl 9543  ax-addrcl 9544  ax-mulcl 9545  ax-mulrcl 9546  ax-mulcom 9547  ax-addass 9548  ax-mulass 9549  ax-distr 9550  ax-i2m1 9551  ax-1ne0 9552  ax-1rid 9553  ax-rnegex 9554  ax-rrecex 9555  ax-cnre 9556  ax-pre-lttri 9557  ax-pre-lttrn 9558  ax-pre-ltadd 9559  ax-pre-mulgt0 9560
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-fal 1380  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-nel 2660  df-ral 2814  df-rex 2815  df-reu 2816  df-rmo 2817  df-rab 2818  df-v 3110  df-sbc 3327  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3781  df-if 3935  df-pw 4007  df-sn 4023  df-pr 4025  df-tp 4027  df-op 4029  df-ot 4031  df-uni 4241  df-int 4278  df-iun 4322  df-iin 4323  df-br 4443  df-opab 4501  df-mpt 4502  df-tr 4536  df-eprel 4786  df-id 4790  df-po 4795  df-so 4796  df-fr 4833  df-se 4834  df-we 4835  df-ord 4876  df-on 4877  df-lim 4878  df-suc 4879  df-xp 5000  df-rel 5001  df-cnv 5002  df-co 5003  df-dm 5004  df-rn 5005  df-res 5006  df-ima 5007  df-iota 5544  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-isom 5590  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-of 6517  df-ofr 6518  df-om 6674  df-1st 6776  df-2nd 6777  df-supp 6894  df-recs 7034  df-rdg 7068  df-1o 7122  df-2o 7123  df-oadd 7126  df-er 7303  df-map 7414  df-pm 7415  df-ixp 7462  df-en 7509  df-dom 7510  df-sdom 7511  df-fin 7512  df-fsupp 7821  df-sup 7892  df-oi 7926  df-card 8311  df-pnf 9621  df-mnf 9622  df-xr 9623  df-ltxr 9624  df-le 9625  df-sub 9798  df-neg 9799  df-nn 10528  df-2 10585  df-3 10586  df-4 10587  df-5 10588  df-6 10589  df-7 10590  df-8 10591  df-9 10592  df-10 10593  df-n0 10787  df-z 10856  df-dec 10968  df-uz 11074  df-fz 11664  df-fzo 11784  df-seq 12066  df-hash 12363  df-struct 14483  df-ndx 14484  df-slot 14485  df-base 14486  df-sets 14487  df-ress 14488  df-plusg 14559  df-mulr 14560  df-sca 14562  df-vsca 14563  df-ip 14564  df-tset 14565  df-ple 14566  df-ds 14568  df-hom 14570  df-cco 14571  df-0g 14688  df-gsum 14689  df-prds 14694  df-pws 14696  df-mre 14832  df-mrc 14833  df-acs 14835  df-mnd 15723  df-mhm 15772  df-submnd 15773  df-grp 15853  df-minusg 15854  df-sbg 15855  df-mulg 15856  df-subg 15988  df-ghm 16055  df-cntz 16145  df-cmn 16591  df-abl 16592  df-mgp 16927  df-ur 16939  df-rng 16983  df-subrg 17205  df-lmod 17292  df-lss 17357  df-sra 17596  df-rgmod 17597  df-psr 17771  df-mpl 17773  df-opsr 17775  df-psr1 17985  df-ply1 17987  df-coe1 17988  df-dsmm 18525  df-frlm 18540  df-mamu 18648  df-mat 18672  df-decpmat 19026
This theorem is referenced by:  decpmatmulsumfsupp  19036  pm2mpmhmlem1  19081  pm2mpmhmlem2  19082
  Copyright terms: Public domain W3C validator