Metamath Proof Explorer

Theorem pm2mpghm

Description: The transformation of polynomial matrices into polynomials over matrices is an additive group homomorphism. (Contributed by AV, 16-Oct-2019) (Revised by AV, 6-Dec-2019)

Ref Expression
Hypotheses pm2mpfo.p 
|- P = ( Poly1 ` R )
pm2mpfo.c 
|- C = ( N Mat P )
pm2mpfo.b 
|- B = ( Base ` C )
pm2mpfo.m 
|- .* = ( .s ` Q )
pm2mpfo.e 
|- .^ = ( .g ` ( mulGrp ` Q ) )
pm2mpfo.x 
|- X = ( var1 ` A )
pm2mpfo.a 
|- A = ( N Mat R )
pm2mpfo.q 
|- Q = ( Poly1 ` A )
pm2mpfo.l 
|- L = ( Base ` Q )
pm2mpfo.t 
|- T = ( N pMatToMatPoly R )
Assertion pm2mpghm 
|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( C GrpHom Q ) )

Proof

Step Hyp Ref Expression
1 pm2mpfo.p 
 |-  P = ( Poly1 ` R )
2 pm2mpfo.c 
 |-  C = ( N Mat P )
3 pm2mpfo.b 
 |-  B = ( Base ` C )
4 pm2mpfo.m 
 |-  .* = ( .s ` Q )
5 pm2mpfo.e 
 |-  .^ = ( .g ` ( mulGrp ` Q ) )
6 pm2mpfo.x 
 |-  X = ( var1 ` A )
7 pm2mpfo.a 
 |-  A = ( N Mat R )
8 pm2mpfo.q 
 |-  Q = ( Poly1 ` A )
9 pm2mpfo.l 
 |-  L = ( Base ` Q )
10 pm2mpfo.t 
 |-  T = ( N pMatToMatPoly R )
11 eqid 
 |-  ( +g ` C ) = ( +g ` C )
12 eqid 
 |-  ( +g ` Q ) = ( +g ` Q )
13 1 2 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
14 ringgrp 
 |-  ( C e. Ring -> C e. Grp )
15 13 14 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Grp )
16 7 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
17 8 ply1ring 
 |-  ( A e. Ring -> Q e. Ring )
18 16 17 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. Ring )
19 ringgrp 
 |-  ( Q e. Ring -> Q e. Grp )
20 18 19 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. Grp )
21 1 2 3 4 5 6 7 8 10 9 pm2mpf 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : B --> L )
22 ringmnd 
 |-  ( C e. Ring -> C e. Mnd )
23 13 22 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Mnd )
24 23 anim1i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( C e. Mnd /\ ( a e. B /\ b e. B ) ) )
25 3anass 
 |-  ( ( C e. Mnd /\ a e. B /\ b e. B ) <-> ( C e. Mnd /\ ( a e. B /\ b e. B ) ) )
26 24 25 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( C e. Mnd /\ a e. B /\ b e. B ) )
27 3 11 mndcl 
 |-  ( ( C e. Mnd /\ a e. B /\ b e. B ) -> ( a ( +g ` C ) b ) e. B )
28 26 27 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` C ) b ) e. B )
29 2 3 decpmatval 
 |-  ( ( ( a ( +g ` C ) b ) e. B /\ k e. NN0 ) -> ( ( a ( +g ` C ) b ) decompPMat k ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i ( a ( +g ` C ) b ) j ) ) ` k ) ) )
30 28 29 sylan 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( a ( +g ` C ) b ) decompPMat k ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i ( a ( +g ` C ) b ) j ) ) ` k ) ) )
31 simplll 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> N e. Fin )
32 fvexd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i a j ) ) ` k ) e. _V )
33 fvexd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i b j ) ) ` k ) e. _V )
34 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i a j ) ) ` k ) ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i a j ) ) ` k ) ) )
35 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i b j ) ) ` k ) ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i b j ) ) ` k ) ) )
36 31 31 32 33 34 35 offval22 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( i e. N , j e. N |-> ( ( coe1 ` ( i a j ) ) ` k ) ) oF ( +g ` R ) ( i e. N , j e. N |-> ( ( coe1 ` ( i b j ) ) ` k ) ) ) = ( i e. N , j e. N |-> ( ( ( coe1 ` ( i a j ) ) ` k ) ( +g ` R ) ( ( coe1 ` ( i b j ) ) ` k ) ) ) )
37 eqid 
 |-  ( Base ` R ) = ( Base ` R )
38 eqid 
 |-  ( Base ` A ) = ( Base ` A )
39 simpllr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> R e. Ring )
40 simprl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ a e. B ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
41 simprr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ a e. B ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
42 3 eleq2i 
 |-  ( a e. B <-> a e. ( Base ` C ) )
43 42 biimpi 
 |-  ( a e. B -> a e. ( Base ` C ) )
44 43 ad2antlr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ a e. B ) /\ ( i e. N /\ j e. N ) ) -> a e. ( Base ` C ) )
45 eqid 
 |-  ( Base ` P ) = ( Base ` P )
46 2 45 matecl 
 |-  ( ( i e. N /\ j e. N /\ a e. ( Base ` C ) ) -> ( i a j ) e. ( Base ` P ) )
47 40 41 44 46 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ a e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i a j ) e. ( Base ` P ) )
48 47 ex 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ a e. B ) -> ( ( i e. N /\ j e. N ) -> ( i a j ) e. ( Base ` P ) ) )
49 48 adantrr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( ( i e. N /\ j e. N ) -> ( i a j ) e. ( Base ` P ) ) )
50 49 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( i e. N /\ j e. N ) -> ( i a j ) e. ( Base ` P ) ) )
51 50 3impib 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ i e. N /\ j e. N ) -> ( i a j ) e. ( Base ` P ) )
52 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> k e. NN0 )
53 52 3ad2ant1 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ i e. N /\ j e. N ) -> k e. NN0 )
54 eqid 
 |-  ( coe1 ` ( i a j ) ) = ( coe1 ` ( i a j ) )
55 54 45 1 37 coe1fvalcl 
 |-  ( ( ( i a j ) e. ( Base ` P ) /\ k e. NN0 ) -> ( ( coe1 ` ( i a j ) ) ` k ) e. ( Base ` R ) )
56 51 53 55 syl2anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i a j ) ) ` k ) e. ( Base ` R ) )
57 7 37 38 31 39 56 matbas2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i a j ) ) ` k ) ) e. ( Base ` A ) )
58 simprl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ b e. B ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
59 simprr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ b e. B ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
60 3 eleq2i 
 |-  ( b e. B <-> b e. ( Base ` C ) )
61 60 biimpi 
 |-  ( b e. B -> b e. ( Base ` C ) )
62 61 ad2antlr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ b e. B ) /\ ( i e. N /\ j e. N ) ) -> b e. ( Base ` C ) )
63 2 45 matecl 
 |-  ( ( i e. N /\ j e. N /\ b e. ( Base ` C ) ) -> ( i b j ) e. ( Base ` P ) )
64 58 59 62 63 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ b e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i b j ) e. ( Base ` P ) )
65 64 ex 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ b e. B ) -> ( ( i e. N /\ j e. N ) -> ( i b j ) e. ( Base ` P ) ) )
66 65 adantrl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( ( i e. N /\ j e. N ) -> ( i b j ) e. ( Base ` P ) ) )
67 66 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( i e. N /\ j e. N ) -> ( i b j ) e. ( Base ` P ) ) )
68 67 3impib 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ i e. N /\ j e. N ) -> ( i b j ) e. ( Base ` P ) )
69 eqid 
 |-  ( coe1 ` ( i b j ) ) = ( coe1 ` ( i b j ) )
70 69 45 1 37 coe1fvalcl 
 |-  ( ( ( i b j ) e. ( Base ` P ) /\ k e. NN0 ) -> ( ( coe1 ` ( i b j ) ) ` k ) e. ( Base ` R ) )
71 68 53 70 syl2anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i b j ) ) ` k ) e. ( Base ` R ) )
72 7 37 38 31 39 71 matbas2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i b j ) ) ` k ) ) e. ( Base ` A ) )
73 eqid 
 |-  ( +g ` A ) = ( +g ` A )
74 eqid 
 |-  ( +g ` R ) = ( +g ` R )
75 7 38 73 74 matplusg2 
 |-  ( ( ( i e. N , j e. N |-> ( ( coe1 ` ( i a j ) ) ` k ) ) e. ( Base ` A ) /\ ( i e. N , j e. N |-> ( ( coe1 ` ( i b j ) ) ` k ) ) e. ( Base ` A ) ) -> ( ( i e. N , j e. N |-> ( ( coe1 ` ( i a j ) ) ` k ) ) ( +g ` A ) ( i e. N , j e. N |-> ( ( coe1 ` ( i b j ) ) ` k ) ) ) = ( ( i e. N , j e. N |-> ( ( coe1 ` ( i a j ) ) ` k ) ) oF ( +g ` R ) ( i e. N , j e. N |-> ( ( coe1 ` ( i b j ) ) ` k ) ) ) )
76 57 72 75 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( i e. N , j e. N |-> ( ( coe1 ` ( i a j ) ) ` k ) ) ( +g ` A ) ( i e. N , j e. N |-> ( ( coe1 ` ( i b j ) ) ` k ) ) ) = ( ( i e. N , j e. N |-> ( ( coe1 ` ( i a j ) ) ` k ) ) oF ( +g ` R ) ( i e. N , j e. N |-> ( ( coe1 ` ( i b j ) ) ` k ) ) ) )
77 simplr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( a e. B /\ b e. B ) )
78 77 anim1i 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( ( a e. B /\ b e. B ) /\ ( i e. N /\ j e. N ) ) )
79 78 3impb 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( a e. B /\ b e. B ) /\ ( i e. N /\ j e. N ) ) )
80 eqid 
 |-  ( +g ` P ) = ( +g ` P )
81 2 3 11 80 matplusgcell 
 |-  ( ( ( a e. B /\ b e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( a ( +g ` C ) b ) j ) = ( ( i a j ) ( +g ` P ) ( i b j ) ) )
82 79 81 syl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ i e. N /\ j e. N ) -> ( i ( a ( +g ` C ) b ) j ) = ( ( i a j ) ( +g ` P ) ( i b j ) ) )
83 82 fveq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ i e. N /\ j e. N ) -> ( coe1 ` ( i ( a ( +g ` C ) b ) j ) ) = ( coe1 ` ( ( i a j ) ( +g ` P ) ( i b j ) ) ) )
84 83 fveq1d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i ( a ( +g ` C ) b ) j ) ) ` k ) = ( ( coe1 ` ( ( i a j ) ( +g ` P ) ( i b j ) ) ) ` k ) )
85 39 3ad2ant1 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ i e. N /\ j e. N ) -> R e. Ring )
86 1 45 80 74 coe1addfv 
 |-  ( ( ( R e. Ring /\ ( i a j ) e. ( Base ` P ) /\ ( i b j ) e. ( Base ` P ) ) /\ k e. NN0 ) -> ( ( coe1 ` ( ( i a j ) ( +g ` P ) ( i b j ) ) ) ` k ) = ( ( ( coe1 ` ( i a j ) ) ` k ) ( +g ` R ) ( ( coe1 ` ( i b j ) ) ` k ) ) )
87 85 51 68 53 86 syl31anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( ( i a j ) ( +g ` P ) ( i b j ) ) ) ` k ) = ( ( ( coe1 ` ( i a j ) ) ` k ) ( +g ` R ) ( ( coe1 ` ( i b j ) ) ` k ) ) )
88 84 87 eqtrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i ( a ( +g ` C ) b ) j ) ) ` k ) = ( ( ( coe1 ` ( i a j ) ) ` k ) ( +g ` R ) ( ( coe1 ` ( i b j ) ) ` k ) ) )
89 88 mpoeq3dva 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i ( a ( +g ` C ) b ) j ) ) ` k ) ) = ( i e. N , j e. N |-> ( ( ( coe1 ` ( i a j ) ) ` k ) ( +g ` R ) ( ( coe1 ` ( i b j ) ) ` k ) ) ) )
90 36 76 89 3eqtr4rd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i ( a ( +g ` C ) b ) j ) ) ` k ) ) = ( ( i e. N , j e. N |-> ( ( coe1 ` ( i a j ) ) ` k ) ) ( +g ` A ) ( i e. N , j e. N |-> ( ( coe1 ` ( i b j ) ) ` k ) ) ) )
91 8 ply1sca 
 |-  ( A e. Ring -> A = ( Scalar ` Q ) )
92 16 91 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A = ( Scalar ` Q ) )
93 92 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> A = ( Scalar ` Q ) )
94 93 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( +g ` A ) = ( +g ` ( Scalar ` Q ) ) )
95 simprl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> a e. B )
96 2 3 decpmatval 
 |-  ( ( a e. B /\ k e. NN0 ) -> ( a decompPMat k ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i a j ) ) ` k ) ) )
97 95 96 sylan 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( a decompPMat k ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i a j ) ) ` k ) ) )
98 97 eqcomd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i a j ) ) ` k ) ) = ( a decompPMat k ) )
99 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> b e. B )
100 2 3 decpmatval 
 |-  ( ( b e. B /\ k e. NN0 ) -> ( b decompPMat k ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i b j ) ) ` k ) ) )
101 99 100 sylan 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( b decompPMat k ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i b j ) ) ` k ) ) )
102 101 eqcomd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i b j ) ) ` k ) ) = ( b decompPMat k ) )
103 94 98 102 oveq123d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( i e. N , j e. N |-> ( ( coe1 ` ( i a j ) ) ` k ) ) ( +g ` A ) ( i e. N , j e. N |-> ( ( coe1 ` ( i b j ) ) ` k ) ) ) = ( ( a decompPMat k ) ( +g ` ( Scalar ` Q ) ) ( b decompPMat k ) ) )
104 30 90 103 3eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( a ( +g ` C ) b ) decompPMat k ) = ( ( a decompPMat k ) ( +g ` ( Scalar ` Q ) ) ( b decompPMat k ) ) )
105 104 oveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( ( a ( +g ` C ) b ) decompPMat k ) .* ( k .^ X ) ) = ( ( ( a decompPMat k ) ( +g ` ( Scalar ` Q ) ) ( b decompPMat k ) ) .* ( k .^ X ) ) )
106 8 ply1lmod 
 |-  ( A e. Ring -> Q e. LMod )
107 16 106 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. LMod )
108 107 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> Q e. LMod )
109 simpl 
 |-  ( ( a e. B /\ b e. B ) -> a e. B )
110 109 ad2antlr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> a e. B )
111 1 2 3 7 38 decpmatcl 
 |-  ( ( R e. Ring /\ a e. B /\ k e. NN0 ) -> ( a decompPMat k ) e. ( Base ` A ) )
112 39 110 52 111 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( a decompPMat k ) e. ( Base ` A ) )
113 92 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Scalar ` Q ) = A )
114 113 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( Scalar ` Q ) = A )
115 114 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( Base ` ( Scalar ` Q ) ) = ( Base ` A ) )
116 112 115 eleqtrrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( a decompPMat k ) e. ( Base ` ( Scalar ` Q ) ) )
117 simpr 
 |-  ( ( a e. B /\ b e. B ) -> b e. B )
118 117 ad2antlr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> b e. B )
119 1 2 3 7 38 decpmatcl 
 |-  ( ( R e. Ring /\ b e. B /\ k e. NN0 ) -> ( b decompPMat k ) e. ( Base ` A ) )
120 39 118 52 119 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( b decompPMat k ) e. ( Base ` A ) )
121 120 115 eleqtrrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( b decompPMat k ) e. ( Base ` ( Scalar ` Q ) ) )
122 eqid 
 |-  ( mulGrp ` Q ) = ( mulGrp ` Q )
123 122 9 mgpbas 
 |-  L = ( Base ` ( mulGrp ` Q ) )
124 122 ringmgp 
 |-  ( Q e. Ring -> ( mulGrp ` Q ) e. Mnd )
125 18 124 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( mulGrp ` Q ) e. Mnd )
126 125 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( mulGrp ` Q ) e. Mnd )
127 6 8 9 vr1cl 
 |-  ( A e. Ring -> X e. L )
128 16 127 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> X e. L )
129 128 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> X e. L )
130 123 5 126 52 129 mulgnn0cld 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( k .^ X ) e. L )
131 eqid 
 |-  ( Scalar ` Q ) = ( Scalar ` Q )
132 eqid 
 |-  ( Base ` ( Scalar ` Q ) ) = ( Base ` ( Scalar ` Q ) )
133 eqid 
 |-  ( +g ` ( Scalar ` Q ) ) = ( +g ` ( Scalar ` Q ) )
134 9 12 131 4 132 133 lmodvsdir 
 |-  ( ( Q e. LMod /\ ( ( a decompPMat k ) e. ( Base ` ( Scalar ` Q ) ) /\ ( b decompPMat k ) e. ( Base ` ( Scalar ` Q ) ) /\ ( k .^ X ) e. L ) ) -> ( ( ( a decompPMat k ) ( +g ` ( Scalar ` Q ) ) ( b decompPMat k ) ) .* ( k .^ X ) ) = ( ( ( a decompPMat k ) .* ( k .^ X ) ) ( +g ` Q ) ( ( b decompPMat k ) .* ( k .^ X ) ) ) )
135 108 116 121 130 134 syl13anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( ( a decompPMat k ) ( +g ` ( Scalar ` Q ) ) ( b decompPMat k ) ) .* ( k .^ X ) ) = ( ( ( a decompPMat k ) .* ( k .^ X ) ) ( +g ` Q ) ( ( b decompPMat k ) .* ( k .^ X ) ) ) )
136 105 135 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( ( a ( +g ` C ) b ) decompPMat k ) .* ( k .^ X ) ) = ( ( ( a decompPMat k ) .* ( k .^ X ) ) ( +g ` Q ) ( ( b decompPMat k ) .* ( k .^ X ) ) ) )
137 136 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( k e. NN0 |-> ( ( ( a ( +g ` C ) b ) decompPMat k ) .* ( k .^ X ) ) ) = ( k e. NN0 |-> ( ( ( a decompPMat k ) .* ( k .^ X ) ) ( +g ` Q ) ( ( b decompPMat k ) .* ( k .^ X ) ) ) ) )
138 137 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( Q gsum ( k e. NN0 |-> ( ( ( a ( +g ` C ) b ) decompPMat k ) .* ( k .^ X ) ) ) ) = ( Q gsum ( k e. NN0 |-> ( ( ( a decompPMat k ) .* ( k .^ X ) ) ( +g ` Q ) ( ( b decompPMat k ) .* ( k .^ X ) ) ) ) ) )
139 eqid 
 |-  ( 0g ` Q ) = ( 0g ` Q )
140 ringcmn 
 |-  ( Q e. Ring -> Q e. CMnd )
141 18 140 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. CMnd )
142 141 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> Q e. CMnd )
143 nn0ex 
 |-  NN0 e. _V
144 143 a1i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> NN0 e. _V )
145 109 anim2i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ a e. B ) )
146 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ a e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ a e. B ) )
147 145 146 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( N e. Fin /\ R e. Ring /\ a e. B ) )
148 1 2 3 4 5 6 7 8 9 pm2mpghmlem1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ a e. B ) /\ k e. NN0 ) -> ( ( a decompPMat k ) .* ( k .^ X ) ) e. L )
149 147 148 sylan 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( a decompPMat k ) .* ( k .^ X ) ) e. L )
150 117 anim2i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ b e. B ) )
151 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ b e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ b e. B ) )
152 150 151 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( N e. Fin /\ R e. Ring /\ b e. B ) )
153 1 2 3 4 5 6 7 8 9 pm2mpghmlem1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ b e. B ) /\ k e. NN0 ) -> ( ( b decompPMat k ) .* ( k .^ X ) ) e. L )
154 152 153 sylan 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( b decompPMat k ) .* ( k .^ X ) ) e. L )
155 eqidd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( k e. NN0 |-> ( ( a decompPMat k ) .* ( k .^ X ) ) ) = ( k e. NN0 |-> ( ( a decompPMat k ) .* ( k .^ X ) ) ) )
156 eqidd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( k e. NN0 |-> ( ( b decompPMat k ) .* ( k .^ X ) ) ) = ( k e. NN0 |-> ( ( b decompPMat k ) .* ( k .^ X ) ) ) )
157 1 2 3 4 5 6 7 8 pm2mpghmlem2 
 |-  ( ( N e. Fin /\ R e. Ring /\ a e. B ) -> ( k e. NN0 |-> ( ( a decompPMat k ) .* ( k .^ X ) ) ) finSupp ( 0g ` Q ) )
158 147 157 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( k e. NN0 |-> ( ( a decompPMat k ) .* ( k .^ X ) ) ) finSupp ( 0g ` Q ) )
159 1 2 3 4 5 6 7 8 pm2mpghmlem2 
 |-  ( ( N e. Fin /\ R e. Ring /\ b e. B ) -> ( k e. NN0 |-> ( ( b decompPMat k ) .* ( k .^ X ) ) ) finSupp ( 0g ` Q ) )
160 152 159 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( k e. NN0 |-> ( ( b decompPMat k ) .* ( k .^ X ) ) ) finSupp ( 0g ` Q ) )
161 9 139 12 142 144 149 154 155 156 158 160 gsummptfsadd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( Q gsum ( k e. NN0 |-> ( ( ( a decompPMat k ) .* ( k .^ X ) ) ( +g ` Q ) ( ( b decompPMat k ) .* ( k .^ X ) ) ) ) ) = ( ( Q gsum ( k e. NN0 |-> ( ( a decompPMat k ) .* ( k .^ X ) ) ) ) ( +g ` Q ) ( Q gsum ( k e. NN0 |-> ( ( b decompPMat k ) .* ( k .^ X ) ) ) ) ) )
162 138 161 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( Q gsum ( k e. NN0 |-> ( ( ( a ( +g ` C ) b ) decompPMat k ) .* ( k .^ X ) ) ) ) = ( ( Q gsum ( k e. NN0 |-> ( ( a decompPMat k ) .* ( k .^ X ) ) ) ) ( +g ` Q ) ( Q gsum ( k e. NN0 |-> ( ( b decompPMat k ) .* ( k .^ X ) ) ) ) ) )
163 simpll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> N e. Fin )
164 simplr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> R e. Ring )
165 1 2 3 4 5 6 7 8 10 pm2mpfval 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( a ( +g ` C ) b ) e. B ) -> ( T ` ( a ( +g ` C ) b ) ) = ( Q gsum ( k e. NN0 |-> ( ( ( a ( +g ` C ) b ) decompPMat k ) .* ( k .^ X ) ) ) ) )
166 163 164 28 165 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( T ` ( a ( +g ` C ) b ) ) = ( Q gsum ( k e. NN0 |-> ( ( ( a ( +g ` C ) b ) decompPMat k ) .* ( k .^ X ) ) ) ) )
167 1 2 3 4 5 6 7 8 10 pm2mpfval 
 |-  ( ( N e. Fin /\ R e. Ring /\ a e. B ) -> ( T ` a ) = ( Q gsum ( k e. NN0 |-> ( ( a decompPMat k ) .* ( k .^ X ) ) ) ) )
168 163 164 95 167 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( T ` a ) = ( Q gsum ( k e. NN0 |-> ( ( a decompPMat k ) .* ( k .^ X ) ) ) ) )
169 1 2 3 4 5 6 7 8 10 pm2mpfval 
 |-  ( ( N e. Fin /\ R e. Ring /\ b e. B ) -> ( T ` b ) = ( Q gsum ( k e. NN0 |-> ( ( b decompPMat k ) .* ( k .^ X ) ) ) ) )
170 163 164 99 169 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( T ` b ) = ( Q gsum ( k e. NN0 |-> ( ( b decompPMat k ) .* ( k .^ X ) ) ) ) )
171 168 170 oveq12d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( ( T ` a ) ( +g ` Q ) ( T ` b ) ) = ( ( Q gsum ( k e. NN0 |-> ( ( a decompPMat k ) .* ( k .^ X ) ) ) ) ( +g ` Q ) ( Q gsum ( k e. NN0 |-> ( ( b decompPMat k ) .* ( k .^ X ) ) ) ) ) )
172 162 166 171 3eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( T ` ( a ( +g ` C ) b ) ) = ( ( T ` a ) ( +g ` Q ) ( T ` b ) ) )
173 3 9 11 12 15 20 21 172 isghmd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T e. ( C GrpHom Q ) )