Metamath Proof Explorer

Theorem pm2mpmhmlem2

Description: Lemma 2 for pm2mpmhm . (Contributed by AV, 22-Oct-2019) (Revised by AV, 6-Dec-2019)

Ref Expression
Hypotheses pm2mpmhm.p 
|- P = ( Poly1 ` R )
pm2mpmhm.c 
|- C = ( N Mat P )
pm2mpmhm.a 
|- A = ( N Mat R )
pm2mpmhm.q 
|- Q = ( Poly1 ` A )
pm2mpmhm.t 
|- T = ( N pMatToMatPoly R )
pm2mpmhm.b 
|- B = ( Base ` C )
Assertion pm2mpmhmlem2 
|- ( ( N e. Fin /\ R e. Ring ) -> A. x e. B A. y e. B ( T ` ( x ( .r ` C ) y ) ) = ( ( T ` x ) ( .r ` Q ) ( T ` y ) ) )

Proof

Step Hyp Ref Expression
1 pm2mpmhm.p 
 |-  P = ( Poly1 ` R )
2 pm2mpmhm.c 
 |-  C = ( N Mat P )
3 pm2mpmhm.a 
 |-  A = ( N Mat R )
4 pm2mpmhm.q 
 |-  Q = ( Poly1 ` A )
5 pm2mpmhm.t 
 |-  T = ( N pMatToMatPoly R )
6 pm2mpmhm.b 
 |-  B = ( Base ` C )
7 simpll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> N e. Fin )
8 simplr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> R e. Ring )
9 1 2 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
10 9 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> C e. Ring )
11 simpl 
 |-  ( ( x e. B /\ y e. B ) -> x e. B )
12 11 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> x e. B )
13 simpr 
 |-  ( ( x e. B /\ y e. B ) -> y e. B )
14 13 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> y e. B )
15 eqid 
 |-  ( .r ` C ) = ( .r ` C )
16 6 15 ringcl 
 |-  ( ( C e. Ring /\ x e. B /\ y e. B ) -> ( x ( .r ` C ) y ) e. B )
17 10 12 14 16 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` C ) y ) e. B )
18 eqid 
 |-  ( .s ` Q ) = ( .s ` Q )
19 eqid 
 |-  ( .g ` ( mulGrp ` Q ) ) = ( .g ` ( mulGrp ` Q ) )
20 eqid 
 |-  ( var1 ` A ) = ( var1 ` A )
21 1 2 6 18 19 20 3 4 5 pm2mpfval 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( x ( .r ` C ) y ) e. B ) -> ( T ` ( x ( .r ` C ) y ) ) = ( Q gsum ( k e. NN0 |-> ( ( ( x ( .r ` C ) y ) decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) )
22 7 8 17 21 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( T ` ( x ( .r ` C ) y ) ) = ( Q gsum ( k e. NN0 |-> ( ( ( x ( .r ` C ) y ) decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) )
23 1 2 6 3 decpmatmul 
 |-  ( ( R e. Ring /\ ( x e. B /\ y e. B ) /\ k e. NN0 ) -> ( ( x ( .r ` C ) y ) decompPMat k ) = ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) )
24 23 ad4ant234 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> ( ( x ( .r ` C ) y ) decompPMat k ) = ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) )
25 24 oveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> ( ( ( x ( .r ` C ) y ) decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) = ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) )
26 25 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( k e. NN0 |-> ( ( ( x ( .r ` C ) y ) decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) = ( k e. NN0 |-> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) )
27 26 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( Q gsum ( k e. NN0 |-> ( ( ( x ( .r ` C ) y ) decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) = ( Q gsum ( k e. NN0 |-> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) )
28 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
29 3 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
30 29 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> A e. Ring )
31 eqid 
 |-  ( Base ` A ) = ( Base ` A )
32 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
33 ringcmn 
 |-  ( A e. Ring -> A e. CMnd )
34 29 33 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. CMnd )
35 34 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ k e. NN0 ) -> A e. CMnd )
36 fzfid 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ k e. NN0 ) -> ( 0 ... k ) e. Fin )
37 30 ad2antrr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> A e. Ring )
38 simp-5r 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> R e. Ring )
39 12 ad3antrrr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> x e. B )
40 elfznn0 
 |-  ( z e. ( 0 ... k ) -> z e. NN0 )
41 40 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> z e. NN0 )
42 1 2 6 3 31 decpmatcl 
 |-  ( ( R e. Ring /\ x e. B /\ z e. NN0 ) -> ( x decompPMat z ) e. ( Base ` A ) )
43 38 39 41 42 syl3anc 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> ( x decompPMat z ) e. ( Base ` A ) )
44 14 ad3antrrr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> y e. B )
45 fznn0sub 
 |-  ( z e. ( 0 ... k ) -> ( k - z ) e. NN0 )
46 45 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> ( k - z ) e. NN0 )
47 1 2 6 3 31 decpmatcl 
 |-  ( ( R e. Ring /\ y e. B /\ ( k - z ) e. NN0 ) -> ( y decompPMat ( k - z ) ) e. ( Base ` A ) )
48 38 44 46 47 syl3anc 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> ( y decompPMat ( k - z ) ) e. ( Base ` A ) )
49 eqid 
 |-  ( .r ` A ) = ( .r ` A )
50 31 49 ringcl 
 |-  ( ( A e. Ring /\ ( x decompPMat z ) e. ( Base ` A ) /\ ( y decompPMat ( k - z ) ) e. ( Base ` A ) ) -> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) e. ( Base ` A ) )
51 37 43 48 50 syl3anc 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) e. ( Base ` A ) )
52 51 ralrimiva 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ k e. NN0 ) -> A. z e. ( 0 ... k ) ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) e. ( Base ` A ) )
53 31 35 36 52 gsummptcl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ k e. NN0 ) -> ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) e. ( Base ` A ) )
54 53 ralrimiva 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> A. k e. NN0 ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) e. ( Base ` A ) )
55 1 2 6 3 49 32 decpmatmulsumfsupp 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( k e. NN0 |-> ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ) finSupp ( 0g ` A ) )
56 55 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( k e. NN0 |-> ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ) finSupp ( 0g ` A ) )
57 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> n e. NN0 )
58 4 28 20 19 30 31 18 32 54 56 57 gsummoncoe1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` n ) = [_ n / k ]_ ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) )
59 csbov2g 
 |-  ( n e. NN0 -> [_ n / k ]_ ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) = ( A gsum [_ n / k ]_ ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) )
60 id 
 |-  ( n e. NN0 -> n e. NN0 )
61 oveq2 
 |-  ( k = n -> ( 0 ... k ) = ( 0 ... n ) )
62 oveq1 
 |-  ( k = n -> ( k - z ) = ( n - z ) )
63 62 oveq2d 
 |-  ( k = n -> ( y decompPMat ( k - z ) ) = ( y decompPMat ( n - z ) ) )
64 63 oveq2d 
 |-  ( k = n -> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) = ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( n - z ) ) ) )
65 61 64 mpteq12dv 
 |-  ( k = n -> ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) = ( z e. ( 0 ... n ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( n - z ) ) ) ) )
66 65 adantl 
 |-  ( ( n e. NN0 /\ k = n ) -> ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) = ( z e. ( 0 ... n ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( n - z ) ) ) ) )
67 60 66 csbied 
 |-  ( n e. NN0 -> [_ n / k ]_ ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) = ( z e. ( 0 ... n ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( n - z ) ) ) ) )
68 67 oveq2d 
 |-  ( n e. NN0 -> ( A gsum [_ n / k ]_ ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) = ( A gsum ( z e. ( 0 ... n ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( n - z ) ) ) ) ) )
69 59 68 eqtrd 
 |-  ( n e. NN0 -> [_ n / k ]_ ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) = ( A gsum ( z e. ( 0 ... n ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( n - z ) ) ) ) ) )
70 69 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> [_ n / k ]_ ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) = ( A gsum ( z e. ( 0 ... n ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( n - z ) ) ) ) ) )
71 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( r e. NN0 |-> ( A gsum ( l e. ( 0 ... r ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( r - l ) ) ) ) ) ) = ( r e. NN0 |-> ( A gsum ( l e. ( 0 ... r ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( r - l ) ) ) ) ) ) )
72 oveq2 
 |-  ( r = n -> ( 0 ... r ) = ( 0 ... n ) )
73 fvoveq1 
 |-  ( r = n -> ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( r - l ) ) = ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( n - l ) ) )
74 73 oveq2d 
 |-  ( r = n -> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( r - l ) ) ) = ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( n - l ) ) ) )
75 72 74 mpteq12dv 
 |-  ( r = n -> ( l e. ( 0 ... r ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( r - l ) ) ) ) = ( l e. ( 0 ... n ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( n - l ) ) ) ) )
76 75 oveq2d 
 |-  ( r = n -> ( A gsum ( l e. ( 0 ... r ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( r - l ) ) ) ) ) = ( A gsum ( l e. ( 0 ... n ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( n - l ) ) ) ) ) )
77 76 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ r = n ) -> ( A gsum ( l e. ( 0 ... r ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( r - l ) ) ) ) ) = ( A gsum ( l e. ( 0 ... n ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( n - l ) ) ) ) ) )
78 ovexd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( A gsum ( l e. ( 0 ... n ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( n - l ) ) ) ) ) e. _V )
79 71 77 57 78 fvmptd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( ( r e. NN0 |-> ( A gsum ( l e. ( 0 ... r ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( r - l ) ) ) ) ) ) ` n ) = ( A gsum ( l e. ( 0 ... n ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( n - l ) ) ) ) ) )
80 eqid 
 |-  ( 0g ` Q ) = ( 0g ` Q )
81 4 ply1ring 
 |-  ( A e. Ring -> Q e. Ring )
82 29 81 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. Ring )
83 ringcmn 
 |-  ( Q e. Ring -> Q e. CMnd )
84 82 83 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. CMnd )
85 84 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> Q e. CMnd )
86 nn0ex 
 |-  NN0 e. _V
87 86 a1i 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> NN0 e. _V )
88 11 anim2i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ x e. B ) )
89 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ x e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ x e. B ) )
90 88 89 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( N e. Fin /\ R e. Ring /\ x e. B ) )
91 90 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( N e. Fin /\ R e. Ring /\ x e. B ) )
92 1 2 6 18 19 20 3 4 28 pm2mpghmlem1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ x e. B ) /\ k e. NN0 ) -> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) e. ( Base ` Q ) )
93 91 92 sylan 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ k e. NN0 ) -> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) e. ( Base ` Q ) )
94 93 fmpttd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) : NN0 --> ( Base ` Q ) )
95 1 2 6 18 19 20 3 4 pm2mpghmlem2 
 |-  ( ( N e. Fin /\ R e. Ring /\ x e. B ) -> ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) finSupp ( 0g ` Q ) )
96 91 95 syl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) finSupp ( 0g ` Q ) )
97 28 80 85 87 94 96 gsumcl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) e. ( Base ` Q ) )
98 13 anim2i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ y e. B ) )
99 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ y e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ y e. B ) )
100 98 99 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( N e. Fin /\ R e. Ring /\ y e. B ) )
101 100 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( N e. Fin /\ R e. Ring /\ y e. B ) )
102 1 2 6 18 19 20 3 4 28 pm2mpghmlem1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ y e. B ) /\ k e. NN0 ) -> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) e. ( Base ` Q ) )
103 101 102 sylan 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ k e. NN0 ) -> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) e. ( Base ` Q ) )
104 103 fmpttd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) : NN0 --> ( Base ` Q ) )
105 7 8 14 3jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( N e. Fin /\ R e. Ring /\ y e. B ) )
106 105 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( N e. Fin /\ R e. Ring /\ y e. B ) )
107 1 2 6 18 19 20 3 4 pm2mpghmlem2 
 |-  ( ( N e. Fin /\ R e. Ring /\ y e. B ) -> ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) finSupp ( 0g ` Q ) )
108 106 107 syl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) finSupp ( 0g ` Q ) )
109 28 80 85 87 104 108 gsumcl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) e. ( Base ` Q ) )
110 eqid 
 |-  ( .r ` Q ) = ( .r ` Q )
111 4 110 49 28 coe1mul 
 |-  ( ( A e. Ring /\ ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) e. ( Base ` Q ) /\ ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) e. ( Base ` Q ) ) -> ( coe1 ` ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ) = ( r e. NN0 |-> ( A gsum ( l e. ( 0 ... r ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( r - l ) ) ) ) ) ) )
112 111 fveq1d 
 |-  ( ( A e. Ring /\ ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) e. ( Base ` Q ) /\ ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) e. ( Base ` Q ) ) -> ( ( coe1 ` ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ) ` n ) = ( ( r e. NN0 |-> ( A gsum ( l e. ( 0 ... r ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( r - l ) ) ) ) ) ) ` n ) )
113 30 97 109 112 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( ( coe1 ` ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ) ` n ) = ( ( r e. NN0 |-> ( A gsum ( l e. ( 0 ... r ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( r - l ) ) ) ) ) ) ` n ) )
114 oveq2 
 |-  ( z = l -> ( x decompPMat z ) = ( x decompPMat l ) )
115 oveq2 
 |-  ( z = l -> ( n - z ) = ( n - l ) )
116 115 oveq2d 
 |-  ( z = l -> ( y decompPMat ( n - z ) ) = ( y decompPMat ( n - l ) ) )
117 114 116 oveq12d 
 |-  ( z = l -> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( n - z ) ) ) = ( ( x decompPMat l ) ( .r ` A ) ( y decompPMat ( n - l ) ) ) )
118 117 cbvmptv 
 |-  ( z e. ( 0 ... n ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( n - z ) ) ) ) = ( l e. ( 0 ... n ) |-> ( ( x decompPMat l ) ( .r ` A ) ( y decompPMat ( n - l ) ) ) )
119 29 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> A e. Ring )
120 simp-5r 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) /\ k e. NN0 ) -> R e. Ring )
121 12 ad3antrrr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) /\ k e. NN0 ) -> x e. B )
122 simpr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) /\ k e. NN0 ) -> k e. NN0 )
123 1 2 6 3 31 decpmatcl 
 |-  ( ( R e. Ring /\ x e. B /\ k e. NN0 ) -> ( x decompPMat k ) e. ( Base ` A ) )
124 120 121 122 123 syl3anc 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) /\ k e. NN0 ) -> ( x decompPMat k ) e. ( Base ` A ) )
125 124 ralrimiva 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> A. k e. NN0 ( x decompPMat k ) e. ( Base ` A ) )
126 8 12 jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( R e. Ring /\ x e. B ) )
127 126 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( R e. Ring /\ x e. B ) )
128 1 2 6 3 32 decpmatfsupp 
 |-  ( ( R e. Ring /\ x e. B ) -> ( k e. NN0 |-> ( x decompPMat k ) ) finSupp ( 0g ` A ) )
129 127 128 syl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( k e. NN0 |-> ( x decompPMat k ) ) finSupp ( 0g ` A ) )
130 elfznn0 
 |-  ( l e. ( 0 ... n ) -> l e. NN0 )
131 130 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> l e. NN0 )
132 4 28 20 19 119 31 18 32 125 129 131 gsummoncoe1 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) = [_ l / k ]_ ( x decompPMat k ) )
133 csbov2g 
 |-  ( l e. ( 0 ... n ) -> [_ l / k ]_ ( x decompPMat k ) = ( x decompPMat [_ l / k ]_ k ) )
134 csbvarg 
 |-  ( l e. ( 0 ... n ) -> [_ l / k ]_ k = l )
135 134 oveq2d 
 |-  ( l e. ( 0 ... n ) -> ( x decompPMat [_ l / k ]_ k ) = ( x decompPMat l ) )
136 133 135 eqtrd 
 |-  ( l e. ( 0 ... n ) -> [_ l / k ]_ ( x decompPMat k ) = ( x decompPMat l ) )
137 136 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> [_ l / k ]_ ( x decompPMat k ) = ( x decompPMat l ) )
138 132 137 eqtr2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( x decompPMat l ) = ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) )
139 14 ad3antrrr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) /\ k e. NN0 ) -> y e. B )
140 1 2 6 3 31 decpmatcl 
 |-  ( ( R e. Ring /\ y e. B /\ k e. NN0 ) -> ( y decompPMat k ) e. ( Base ` A ) )
141 120 139 122 140 syl3anc 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) /\ k e. NN0 ) -> ( y decompPMat k ) e. ( Base ` A ) )
142 141 ralrimiva 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> A. k e. NN0 ( y decompPMat k ) e. ( Base ` A ) )
143 8 14 jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( R e. Ring /\ y e. B ) )
144 143 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( R e. Ring /\ y e. B ) )
145 1 2 6 3 32 decpmatfsupp 
 |-  ( ( R e. Ring /\ y e. B ) -> ( k e. NN0 |-> ( y decompPMat k ) ) finSupp ( 0g ` A ) )
146 144 145 syl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( k e. NN0 |-> ( y decompPMat k ) ) finSupp ( 0g ` A ) )
147 fznn0sub 
 |-  ( l e. ( 0 ... n ) -> ( n - l ) e. NN0 )
148 147 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( n - l ) e. NN0 )
149 4 28 20 19 119 31 18 32 142 146 148 gsummoncoe1 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( n - l ) ) = [_ ( n - l ) / k ]_ ( y decompPMat k ) )
150 ovex 
 |-  ( n - l ) e. _V
151 csbov2g 
 |-  ( ( n - l ) e. _V -> [_ ( n - l ) / k ]_ ( y decompPMat k ) = ( y decompPMat [_ ( n - l ) / k ]_ k ) )
152 150 151 mp1i 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> [_ ( n - l ) / k ]_ ( y decompPMat k ) = ( y decompPMat [_ ( n - l ) / k ]_ k ) )
153 csbvarg 
 |-  ( ( n - l ) e. _V -> [_ ( n - l ) / k ]_ k = ( n - l ) )
154 150 153 mp1i 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> [_ ( n - l ) / k ]_ k = ( n - l ) )
155 154 oveq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( y decompPMat [_ ( n - l ) / k ]_ k ) = ( y decompPMat ( n - l ) ) )
156 149 152 155 3eqtrrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( y decompPMat ( n - l ) ) = ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( n - l ) ) )
157 138 156 oveq12d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( ( x decompPMat l ) ( .r ` A ) ( y decompPMat ( n - l ) ) ) = ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( n - l ) ) ) )
158 157 mpteq2dva 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( l e. ( 0 ... n ) |-> ( ( x decompPMat l ) ( .r ` A ) ( y decompPMat ( n - l ) ) ) ) = ( l e. ( 0 ... n ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( n - l ) ) ) ) )
159 118 158 eqtrid 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( z e. ( 0 ... n ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( n - z ) ) ) ) = ( l e. ( 0 ... n ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( n - l ) ) ) ) )
160 159 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( A gsum ( z e. ( 0 ... n ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( n - z ) ) ) ) ) = ( A gsum ( l e. ( 0 ... n ) |-> ( ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) ( .r ` A ) ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` ( n - l ) ) ) ) ) )
161 79 113 160 3eqtr4rd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( A gsum ( z e. ( 0 ... n ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( n - z ) ) ) ) ) = ( ( coe1 ` ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ) ` n ) )
162 58 70 161 3eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` n ) = ( ( coe1 ` ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ) ` n ) )
163 162 ralrimiva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> A. n e. NN0 ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` n ) = ( ( coe1 ` ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ) ` n ) )
164 29 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> A e. Ring )
165 84 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> Q e. CMnd )
166 86 a1i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> NN0 e. _V )
167 4 ply1lmod 
 |-  ( A e. Ring -> Q e. LMod )
168 29 167 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. LMod )
169 168 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> Q e. LMod )
170 34 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> A e. CMnd )
171 fzfid 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> ( 0 ... k ) e. Fin )
172 29 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> A e. Ring )
173 simp-4r 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> R e. Ring )
174 simplrl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> x e. B )
175 174 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> x e. B )
176 40 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> z e. NN0 )
177 173 175 176 42 syl3anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> ( x decompPMat z ) e. ( Base ` A ) )
178 simplrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> y e. B )
179 178 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> y e. B )
180 45 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> ( k - z ) e. NN0 )
181 173 179 180 47 syl3anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> ( y decompPMat ( k - z ) ) e. ( Base ` A ) )
182 172 177 181 50 syl3anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) /\ z e. ( 0 ... k ) ) -> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) e. ( Base ` A ) )
183 182 ralrimiva 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> A. z e. ( 0 ... k ) ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) e. ( Base ` A ) )
184 31 170 171 183 gsummptcl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) e. ( Base ` A ) )
185 29 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> A e. Ring )
186 4 ply1sca 
 |-  ( A e. Ring -> A = ( Scalar ` Q ) )
187 185 186 syl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> A = ( Scalar ` Q ) )
188 187 eqcomd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> ( Scalar ` Q ) = A )
189 188 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> ( Base ` ( Scalar ` Q ) ) = ( Base ` A ) )
190 184 189 eleqtrrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) e. ( Base ` ( Scalar ` Q ) ) )
191 eqid 
 |-  ( mulGrp ` Q ) = ( mulGrp ` Q )
192 4 20 191 19 28 ply1moncl 
 |-  ( ( A e. Ring /\ k e. NN0 ) -> ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) e. ( Base ` Q ) )
193 185 192 sylancom 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) e. ( Base ` Q ) )
194 eqid 
 |-  ( Scalar ` Q ) = ( Scalar ` Q )
195 eqid 
 |-  ( Base ` ( Scalar ` Q ) ) = ( Base ` ( Scalar ` Q ) )
196 28 194 18 195 lmodvscl 
 |-  ( ( Q e. LMod /\ ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) e. ( Base ` ( Scalar ` Q ) ) /\ ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) e. ( Base ` Q ) ) -> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) e. ( Base ` Q ) )
197 169 190 193 196 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) e. ( Base ` Q ) )
198 197 fmpttd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( k e. NN0 |-> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) : NN0 --> ( Base ` Q ) )
199 1 2 6 18 19 20 3 4 28 5 pm2mpmhmlem1 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( k e. NN0 |-> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) finSupp ( 0g ` Q ) )
200 28 80 165 166 198 199 gsumcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( Q gsum ( k e. NN0 |-> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) e. ( Base ` Q ) )
201 82 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> Q e. Ring )
202 90 92 sylan 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) e. ( Base ` Q ) )
203 202 fmpttd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) : NN0 --> ( Base ` Q ) )
204 90 95 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) finSupp ( 0g ` Q ) )
205 28 80 165 166 203 204 gsumcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) e. ( Base ` Q ) )
206 100 102 sylan 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ k e. NN0 ) -> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) e. ( Base ` Q ) )
207 206 fmpttd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) : NN0 --> ( Base ` Q ) )
208 7 8 14 107 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) finSupp ( 0g ` Q ) )
209 28 80 165 166 207 208 gsumcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) e. ( Base ` Q ) )
210 28 110 ringcl 
 |-  ( ( Q e. Ring /\ ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) e. ( Base ` Q ) /\ ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) e. ( Base ` Q ) ) -> ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) e. ( Base ` Q ) )
211 201 205 209 210 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) e. ( Base ` Q ) )
212 eqid 
 |-  ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) = ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) )
213 eqid 
 |-  ( coe1 ` ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ) = ( coe1 ` ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) )
214 4 28 212 213 ply1coe1eq 
 |-  ( ( A e. Ring /\ ( Q gsum ( k e. NN0 |-> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) e. ( Base ` Q ) /\ ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) e. ( Base ` Q ) ) -> ( A. n e. NN0 ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` n ) = ( ( coe1 ` ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ) ` n ) <-> ( Q gsum ( k e. NN0 |-> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) = ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ) )
215 164 200 211 214 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( A. n e. NN0 ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` n ) = ( ( coe1 ` ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ) ` n ) <-> ( Q gsum ( k e. NN0 |-> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) = ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ) )
216 163 215 mpbid 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( Q gsum ( k e. NN0 |-> ( ( A gsum ( z e. ( 0 ... k ) |-> ( ( x decompPMat z ) ( .r ` A ) ( y decompPMat ( k - z ) ) ) ) ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) = ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) )
217 22 27 216 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( T ` ( x ( .r ` C ) y ) ) = ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) )
218 1 2 6 18 19 20 3 4 5 pm2mpfval 
 |-  ( ( N e. Fin /\ R e. Ring /\ x e. B ) -> ( T ` x ) = ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) )
219 7 8 12 218 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( T ` x ) = ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) )
220 1 2 6 18 19 20 3 4 5 pm2mpfval 
 |-  ( ( N e. Fin /\ R e. Ring /\ y e. B ) -> ( T ` y ) = ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) )
221 7 8 14 220 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( T ` y ) = ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) )
222 219 221 oveq12d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( T ` x ) ( .r ` Q ) ( T ` y ) ) = ( ( Q gsum ( k e. NN0 |-> ( ( x decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ( .r ` Q ) ( Q gsum ( k e. NN0 |-> ( ( y decompPMat k ) ( .s ` Q ) ( k ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) )
223 217 222 eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( T ` ( x ( .r ` C ) y ) ) = ( ( T ` x ) ( .r ` Q ) ( T ` y ) ) )
224 223 ralrimivva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. x e. B A. y e. B ( T ` ( x ( .r ` C ) y ) ) = ( ( T ` x ) ( .r ` Q ) ( T ` y ) ) )