Metamath Proof Explorer

Theorem decpmatmul

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)

Ref Expression
Hypotheses decpmatmul.p 
|- P = ( Poly1 ` R )
decpmatmul.c 
|- C = ( N Mat P )
decpmatmul.b 
|- B = ( Base ` C )
decpmatmul.a 
|- A = ( N Mat R )
Assertion decpmatmul 
|- ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> ( ( U ( .r ` C ) W ) decompPMat K ) = ( A gsum ( k e. ( 0 ... K ) |-> ( ( U decompPMat k ) ( .r ` A ) ( W decompPMat ( K - k ) ) ) ) ) )

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 decpmatmul.a 
 |-  A = ( N Mat R )
5 eqidd 
 |-  ( ( ( 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 gsum ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) ) ) = ( x e. N , y e. N |-> ( R gsum ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) ) ) )
6 oveq1 
 |-  ( x = i -> ( x ( U decompPMat k ) t ) = ( i ( U decompPMat k ) t ) )
7 oveq2 
 |-  ( y = j -> ( t ( W decompPMat ( K - k ) ) y ) = ( t ( W decompPMat ( K - k ) ) j ) )
8 6 7 oveqan12d 
 |-  ( ( 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 ) ) )
9 8 mpteq2dv 
 |-  ( ( 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 ) ) ) )
10 9 oveq2d 
 |-  ( ( x = i /\ y = j ) -> ( R gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) = ( R gsum ( t e. N |-> ( ( i ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) j ) ) ) ) )
11 10 mpteq2dv 
 |-  ( ( x = i /\ y = j ) -> ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) = ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( i ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) j ) ) ) ) ) )
12 11 oveq2d 
 |-  ( ( x = i /\ y = j ) -> ( R gsum ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) ) = ( R gsum ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( i ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) j ) ) ) ) ) ) )
13 12 adantl 
 |-  ( ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ ( x = i /\ y = j ) ) -> ( R gsum ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) ) = ( R gsum ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( i ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) j ) ) ) ) ) ) )
14 simprl 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
15 simprr 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
16 ovexd 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( R gsum ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( i ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) j ) ) ) ) ) ) e. _V )
17 5 13 14 15 16 ovmpod 
 |-  ( ( ( 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 gsum ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) ) ) j ) = ( R gsum ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( i ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) j ) ) ) ) ) ) )
18 2 3 matrcl 
 |-  ( U e. B -> ( N e. Fin /\ P e. _V ) )
19 18 simpld 
 |-  ( U e. B -> N e. Fin )
20 19 adantr 
 |-  ( ( U e. B /\ W e. B ) -> N e. Fin )
21 20 anim2i 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) ) -> ( R e. Ring /\ N e. Fin ) )
22 21 ancomd 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) ) -> ( N e. Fin /\ R e. Ring ) )
23 22 3adant3 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> ( N e. Fin /\ R e. Ring ) )
24 eqid 
 |-  ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. )
25 4 24 matmulr 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
26 23 25 syl 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
27 26 adantr 
 |-  ( ( ( 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 ) )
28 27 adantr 
 |-  ( ( ( ( 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 ) )
29 28 eqcomd 
 |-  ( ( ( ( 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 >. ) )
30 29 oveqd 
 |-  ( ( ( ( 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 
 |-  ( Base ` R ) = ( Base ` R )
32 eqid 
 |-  ( .r ` R ) = ( .r ` R )
33 simp1 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> R e. Ring )
34 33 adantr 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> R e. Ring )
35 34 adantr 
 |-  ( ( ( ( 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 )
36 23 simpld 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> N e. Fin )
37 36 adantr 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> N e. Fin )
38 37 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> U e. B )
40 39 adantr 
 |-  ( ( ( ( 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 
 |-  ( k e. ( 0 ... K ) -> k e. NN0 )
42 41 adantl 
 |-  ( ( ( ( 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 )
43 35 40 42 3jca 
 |-  ( ( ( ( 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 eqid 
 |-  ( Base ` A ) = ( Base ` A )
45 1 2 3 4 44 decpmatcl 
 |-  ( ( R e. Ring /\ U e. B /\ k e. NN0 ) -> ( U decompPMat k ) e. ( Base ` A ) )
46 43 45 syl 
 |-  ( ( ( ( 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 ) )
47 4 31 44 matbas2i 
 |-  ( ( U decompPMat k ) e. ( Base ` A ) -> ( U decompPMat k ) e. ( ( Base ` R ) ^m ( N X. N ) ) )
48 46 47 syl 
 |-  ( ( ( ( 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 ) ) )
49 simpl2r 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> W e. B )
50 49 adantr 
 |-  ( ( ( ( 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 )
51 fznn0sub 
 |-  ( k e. ( 0 ... K ) -> ( K - k ) e. NN0 )
52 51 adantl 
 |-  ( ( ( ( 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 )
53 35 50 52 3jca 
 |-  ( ( ( ( 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 ) )
54 1 2 3 4 44 decpmatcl 
 |-  ( ( R e. Ring /\ W e. B /\ ( K - k ) e. NN0 ) -> ( W decompPMat ( K - k ) ) e. ( Base ` A ) )
55 53 54 syl 
 |-  ( ( ( ( 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 ) )
56 4 31 44 matbas2i 
 |-  ( ( W decompPMat ( K - k ) ) e. ( Base ` A ) -> ( W decompPMat ( K - k ) ) e. ( ( Base ` R ) ^m ( N X. N ) ) )
57 55 56 syl 
 |-  ( ( ( ( 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 ) ) )
58 24 31 32 35 38 38 38 48 57 mamuval 
 |-  ( ( ( ( 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 gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) )
59 30 58 eqtrd 
 |-  ( ( ( ( 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 gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) )
60 59 mpteq2dva 
 |-  ( ( ( 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 gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) ) )
61 60 oveq2d 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( A gsum ( k e. ( 0 ... K ) |-> ( ( U decompPMat k ) ( .r ` A ) ( W decompPMat ( K - k ) ) ) ) ) = ( A gsum ( k e. ( 0 ... K ) |-> ( x e. N , y e. N |-> ( R gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) ) ) )
62 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
63 ovexd 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( 0 ... K ) e. _V )
64 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
65 33 64 syl 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> R e. CMnd )
66 65 adantr 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> R e. CMnd )
67 66 adantr 
 |-  ( ( ( ( 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 )
68 67 3ad2ant1 
 |-  ( ( ( ( ( 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 )
69 38 3ad2ant1 
 |-  ( ( ( ( ( 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 )
70 35 3ad2ant1 
 |-  ( ( ( ( ( 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 )
71 70 adantr 
 |-  ( ( ( ( ( ( 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 )
72 simpl2 
 |-  ( ( ( ( ( ( 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 )
73 simpr 
 |-  ( ( ( ( ( ( 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 )
74 43 3ad2ant1 
 |-  ( ( ( ( ( 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 ) )
75 74 adantr 
 |-  ( ( ( ( ( ( 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 ) )
76 75 45 syl 
 |-  ( ( ( ( ( ( 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 ) )
77 4 31 44 72 73 76 matecld 
 |-  ( ( ( ( ( ( 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 ) )
78 simpl3 
 |-  ( ( ( ( ( ( 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 )
79 55 3ad2ant1 
 |-  ( ( ( ( ( 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 ) )
80 79 adantr 
 |-  ( ( ( ( ( ( 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 ) )
81 4 31 44 73 78 80 matecld 
 |-  ( ( ( ( ( ( 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 ) )
82 31 32 ringcl 
 |-  ( ( 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 ) )
83 71 77 81 82 syl3anc 
 |-  ( ( ( ( ( ( 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 ) )
84 83 ralrimiva 
 |-  ( ( ( ( ( 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 ) )
85 31 68 69 84 gsummptcl 
 |-  ( ( ( ( ( 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 gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) e. ( Base ` R ) )
86 4 31 44 38 35 85 matbas2d 
 |-  ( ( ( ( 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 gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) e. ( Base ` A ) )
87 eqid 
 |-  ( k e. ( 0 ... K ) |-> ( x e. N , y e. N |-> ( R gsum ( 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 gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) )
88 fzfid 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( 0 ... K ) e. Fin )
89 simpl 
 |-  ( ( N e. Fin /\ P e. _V ) -> N e. Fin )
90 89 89 jca 
 |-  ( ( N e. Fin /\ P e. _V ) -> ( N e. Fin /\ N e. Fin ) )
91 18 90 syl 
 |-  ( U e. B -> ( N e. Fin /\ N e. Fin ) )
92 91 adantr 
 |-  ( ( U e. B /\ W e. B ) -> ( N e. Fin /\ N e. Fin ) )
93 92 3ad2ant2 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> ( N e. Fin /\ N e. Fin ) )
94 93 adantr 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( N e. Fin /\ N e. Fin ) )
95 94 adantr 
 |-  ( ( ( ( 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 ) )
96 mpoexga 
 |-  ( ( N e. Fin /\ N e. Fin ) -> ( x e. N , y e. N |-> ( R gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) e. _V )
97 95 96 syl 
 |-  ( ( ( ( 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 gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) e. _V )
98 fvexd 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( 0g ` A ) e. _V )
99 87 88 97 98 fsuppmptdm 
 |-  ( ( ( 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 gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) ) finSupp ( 0g ` A ) )
100 4 44 62 37 63 34 86 99 matgsum 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( A gsum ( k e. ( 0 ... K ) |-> ( x e. N , y e. N |-> ( R gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) ) ) = ( x e. N , y e. N |-> ( R gsum ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) ) ) )
101 61 100 eqtrd 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( A gsum ( k e. ( 0 ... K ) |-> ( ( U decompPMat k ) ( .r ` A ) ( W decompPMat ( K - k ) ) ) ) ) = ( x e. N , y e. N |-> ( R gsum ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) ) ) )
102 101 oveqd 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( i ( A gsum ( k e. ( 0 ... K ) |-> ( ( U decompPMat k ) ( .r ` A ) ( W decompPMat ( K - k ) ) ) ) ) j ) = ( i ( x e. N , y e. N |-> ( R gsum ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( x ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) y ) ) ) ) ) ) ) j ) )
103 simpl2 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( U e. B /\ W e. B ) )
104 simpl3 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> K e. NN0 )
105 1 2 3 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 ( k e. ( 0 ... K ) |-> ( ( ( coe1 ` ( i U t ) ) ` k ) ( .r ` R ) ( ( coe1 ` ( t W j ) ) ` ( K - k ) ) ) ) ) ) ) )
106 37 34 103 14 15 104 105 syl213anc 
 |-  ( ( ( 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 gsum ( t e. N |-> ( R gsum ( k e. ( 0 ... K ) |-> ( ( ( coe1 ` ( i U t ) ) ` k ) ( .r ` R ) ( ( coe1 ` ( t W j ) ) ` ( K - k ) ) ) ) ) ) ) )
107 simpll1 
 |-  ( ( ( ( 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 )
108 simplrl 
 |-  ( ( ( ( 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 )
109 simprl 
 |-  ( ( ( ( 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 )
110 3 eleq2i 
 |-  ( U e. B <-> U e. ( Base ` C ) )
111 110 birani 
 |-  ( ( U e. B /\ W e. B ) -> U e. ( Base ` C ) )
112 111 3ad2ant2 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> U e. ( Base ` C ) )
113 112 adantr 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> U e. ( Base ` C ) )
114 113 adantr 
 |-  ( ( ( ( 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 ) )
115 eqid 
 |-  ( Base ` P ) = ( Base ` P )
116 2 115 matecl 
 |-  ( ( i e. N /\ t e. N /\ U e. ( Base ` C ) ) -> ( i U t ) e. ( Base ` P ) )
117 108 109 114 116 syl3anc 
 |-  ( ( ( ( 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 ) )
118 41 ad2antll 
 |-  ( ( ( ( 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 )
119 eqid 
 |-  ( coe1 ` ( i U t ) ) = ( coe1 ` ( i U t ) )
120 119 115 1 31 coe1fvalcl 
 |-  ( ( ( i U t ) e. ( Base ` P ) /\ k e. NN0 ) -> ( ( coe1 ` ( i U t ) ) ` k ) e. ( Base ` R ) )
121 117 118 120 syl2anc 
 |-  ( ( ( ( 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 ) )
122 simplrr 
 |-  ( ( ( ( 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 )
123 49 adantr 
 |-  ( ( ( ( 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 )
124 2 115 3 109 122 123 matecld 
 |-  ( ( ( ( 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 ) )
125 51 ad2antll 
 |-  ( ( ( ( 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 )
126 eqid 
 |-  ( coe1 ` ( t W j ) ) = ( coe1 ` ( t W j ) )
127 126 115 1 31 coe1fvalcl 
 |-  ( ( ( t W j ) e. ( Base ` P ) /\ ( K - k ) e. NN0 ) -> ( ( coe1 ` ( t W j ) ) ` ( K - k ) ) e. ( Base ` R ) )
128 124 125 127 syl2anc 
 |-  ( ( ( ( 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 ) )
129 31 32 ringcl 
 |-  ( ( 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 ) )
130 107 121 128 129 syl3anc 
 |-  ( ( ( ( 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 ) )
131 31 66 37 88 130 gsumcom3fi 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( R gsum ( t e. N |-> ( R gsum ( k e. ( 0 ... K ) |-> ( ( ( coe1 ` ( i U t ) ) ` k ) ( .r ` R ) ( ( coe1 ` ( t W j ) ) ` ( K - k ) ) ) ) ) ) ) = ( R gsum ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( ( coe1 ` ( i U t ) ) ` k ) ( .r ` R ) ( ( coe1 ` ( t W j ) ) ` ( K - k ) ) ) ) ) ) ) )
132 14 adantr 
 |-  ( ( ( ( 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 )
133 132 anim1i 
 |-  ( ( ( ( ( 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 ) )
134 1 2 3 decpmate 
 |-  ( ( ( 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 ) )
135 43 133 134 syl2an2r 
 |-  ( ( ( ( ( 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 ) )
136 simplrr 
 |-  ( ( ( ( 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 )
137 136 anim1ci 
 |-  ( ( ( ( ( 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 ) )
138 1 2 3 decpmate 
 |-  ( ( ( 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 ) ) )
139 53 137 138 syl2an2r 
 |-  ( ( ( ( ( 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 ) ) )
140 135 139 oveq12d 
 |-  ( ( ( ( ( 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 ) ) ) )
141 140 eqcomd 
 |-  ( ( ( ( ( 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 ) ) )
142 141 mpteq2dva 
 |-  ( ( ( ( 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 ) ) ) )
143 142 oveq2d 
 |-  ( ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ k e. ( 0 ... K ) ) -> ( R gsum ( t e. N |-> ( ( ( coe1 ` ( i U t ) ) ` k ) ( .r ` R ) ( ( coe1 ` ( t W j ) ) ` ( K - k ) ) ) ) ) = ( R gsum ( t e. N |-> ( ( i ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) j ) ) ) ) )
144 143 mpteq2dva 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( ( coe1 ` ( i U t ) ) ` k ) ( .r ` R ) ( ( coe1 ` ( t W j ) ) ` ( K - k ) ) ) ) ) ) = ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( i ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) j ) ) ) ) ) )
145 144 oveq2d 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( R gsum ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( ( coe1 ` ( i U t ) ) ` k ) ( .r ` R ) ( ( coe1 ` ( t W j ) ) ` ( K - k ) ) ) ) ) ) ) = ( R gsum ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( i ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) j ) ) ) ) ) ) )
146 106 131 145 3eqtrd 
 |-  ( ( ( 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 gsum ( k e. ( 0 ... K ) |-> ( R gsum ( t e. N |-> ( ( i ( U decompPMat k ) t ) ( .r ` R ) ( t ( W decompPMat ( K - k ) ) j ) ) ) ) ) ) )
147 17 102 146 3eqtr4rd 
 |-  ( ( ( 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 gsum ( k e. ( 0 ... K ) |-> ( ( U decompPMat k ) ( .r ` A ) ( W decompPMat ( K - k ) ) ) ) ) j ) )
148 147 ralrimivva 
 |-  ( ( 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 gsum ( k e. ( 0 ... K ) |-> ( ( U decompPMat k ) ( .r ` A ) ( W decompPMat ( K - k ) ) ) ) ) j ) )
149 1 2 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
150 22 149 syl 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) ) -> C e. Ring )
151 simprl 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) ) -> U e. B )
152 simprr 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) ) -> W e. B )
153 eqid 
 |-  ( .r ` C ) = ( .r ` C )
154 3 153 ringcl 
 |-  ( ( C e. Ring /\ U e. B /\ W e. B ) -> ( U ( .r ` C ) W ) e. B )
155 150 151 152 154 syl3anc 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) ) -> ( U ( .r ` C ) W ) e. B )
156 155 3adant3 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> ( U ( .r ` C ) W ) e. B )
157 1 2 3 4 44 decpmatcl 
 |-  ( ( R e. Ring /\ ( U ( .r ` C ) W ) e. B /\ K e. NN0 ) -> ( ( U ( .r ` C ) W ) decompPMat K ) e. ( Base ` A ) )
158 156 157 syld3an2 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> ( ( U ( .r ` C ) W ) decompPMat K ) e. ( Base ` A ) )
159 4 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
160 23 159 syl 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> A e. Ring )
161 ringcmn 
 |-  ( A e. Ring -> A e. CMnd )
162 160 161 syl 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> A e. CMnd )
163 fzfid 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> ( 0 ... K ) e. Fin )
164 160 adantr 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ k e. ( 0 ... K ) ) -> A e. Ring )
165 33 adantr 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ k e. ( 0 ... K ) ) -> R e. Ring )
166 simpl2l 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ k e. ( 0 ... K ) ) -> U e. B )
167 41 adantl 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ k e. ( 0 ... K ) ) -> k e. NN0 )
168 165 166 167 3jca 
 |-  ( ( ( 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 ) )
169 168 45 syl 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ k e. ( 0 ... K ) ) -> ( U decompPMat k ) e. ( Base ` A ) )
170 simpl2r 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ k e. ( 0 ... K ) ) -> W e. B )
171 51 adantl 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ k e. ( 0 ... K ) ) -> ( K - k ) e. NN0 )
172 165 170 171 3jca 
 |-  ( ( ( 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 ) )
173 172 54 syl 
 |-  ( ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) /\ k e. ( 0 ... K ) ) -> ( W decompPMat ( K - k ) ) e. ( Base ` A ) )
174 eqid 
 |-  ( .r ` A ) = ( .r ` A )
175 44 174 ringcl 
 |-  ( ( 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 ) )
176 164 169 173 175 syl3anc 
 |-  ( ( ( 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 ) )
177 176 ralrimiva 
 |-  ( ( 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 ) )
178 44 162 163 177 gsummptcl 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> ( A gsum ( k e. ( 0 ... K ) |-> ( ( U decompPMat k ) ( .r ` A ) ( W decompPMat ( K - k ) ) ) ) ) e. ( Base ` A ) )
179 4 44 eqmat 
 |-  ( ( ( ( U ( .r ` C ) W ) decompPMat K ) e. ( Base ` A ) /\ ( A gsum ( k e. ( 0 ... K ) |-> ( ( U decompPMat k ) ( .r ` A ) ( W decompPMat ( K - k ) ) ) ) ) e. ( Base ` A ) ) -> ( ( ( U ( .r ` C ) W ) decompPMat K ) = ( A gsum ( 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 gsum ( k e. ( 0 ... K ) |-> ( ( U decompPMat k ) ( .r ` A ) ( W decompPMat ( K - k ) ) ) ) ) j ) ) )
180 158 178 179 syl2anc 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> ( ( ( U ( .r ` C ) W ) decompPMat K ) = ( A gsum ( 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 gsum ( k e. ( 0 ... K ) |-> ( ( U decompPMat k ) ( .r ` A ) ( W decompPMat ( K - k ) ) ) ) ) j ) ) )
181 148 180 mpbird 
 |-  ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> ( ( U ( .r ` C ) W ) decompPMat K ) = ( A gsum ( k e. ( 0 ... K ) |-> ( ( U decompPMat k ) ( .r ` A ) ( W decompPMat ( K - k ) ) ) ) ) )