Theorem pmattomply1ghm 31256

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

Hypotheses

Ref	Expression
pmattomply1.p	|- P = (Poly1 ` R )
pmattomply1.c	|- C = ( N Mat P )
pmattomply1.b	|- B = ( Base ` C )
pmattomply1.f	|- F = ( m e. B , k e. NN0 |-> ( i e. N , j e. N |-> ( (coe1 ` ( i m j ) ) ` k ) ) )
pmattomply1.m	|- .* = ( .s ` Q )
pmattomply1.e	|- .^ = (.g ` (mulGrp ` Q ) )
pmattomply1.x	|- X = (var1 ` A )
pmattomply1.a	|- A = ( N Mat R )
pmattomply1.q	|- Q = (Poly1 ` A )
pmattomply1.l	|- L = ( Base ` Q )
pmattomply1.t	|- T = ( m e. B |-> ( Q gsumg ( k e. NN0 |-> ( ( m F k ) .* ( k .^ X ) ) ) ) )

Assertion

Ref	Expression
pmattomply1ghm	|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( C GrpHom Q ) )

Distinct variable groups:   B, k, m, i, j   i, N, j, k   R, i, j, k   m, F   Q, m   m, X   .* , m   .^ , m   A, i, j, k   C, i, j, k, m   i, F, j, k   k, L   m, N   P, k   .* , k   R, m   Q, k   .^ , k   i, L, j, m   P, i, j, m   k, X

Allowed substitution hints:   A( m)   Q( i, j)   T( i, j, k, m)   .^ ( i, j)   .* ( i, j)   X( i, j)

Proof of Theorem pmattomply1ghm

Dummy variables b l n a are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		pmattomply1.b	. 2 |- B = ( Base ` C )
2		pmattomply1.l	. 2 |- L = ( Base ` Q )
3		eqid 2450	. 2 |- ( +g ` C ) = ( +g ` C )
4		eqid 2450	. 2 |- ( +g ` Q ) = ( +g ` Q )
5		pmattomply1.p	. . . . 5 |- P = (Poly1 ` R )
6	5	ply1rng 17796	. . . 4 |- ( R e. Ring -> P e. Ring )
7		pmattomply1.c	. . . . 5 |- C = ( N Mat P )
8	7	matrng 18426	. . . 4 |- ( ( N e. Fin /\ P e. Ring ) -> C e. Ring )
9	6, 8	sylan2 474	. . 3 |- ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
10		rnggrp 16742	. . 3 |- ( C e. Ring -> C e. Grp )
11	9, 10	syl 16	. 2 |- ( ( N e. Fin /\ R e. Ring ) -> C e. Grp )
12		pmattomply1.a	. . . . 5 |- A = ( N Mat R )
13	12	matrng 18426	. . . 4 |- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
14		pmattomply1.q	. . . . 5 |- Q = (Poly1 ` A )
15	14	ply1rng 17796	. . . 4 |- ( A e. Ring -> Q e. Ring )
16	13, 15	syl 16	. . 3 |- ( ( N e. Fin /\ R e. Ring ) -> Q e. Ring )
17		rnggrp 16742	. . 3 |- ( Q e. Ring -> Q e. Grp )
18	16, 17	syl 16	. 2 |- ( ( N e. Fin /\ R e. Ring ) -> Q e. Grp )
19		pmattomply1.f	. . 3 |- F = ( m e. B , k e. NN0 |-> ( i e. N , j e. N |-> ( (coe1 ` ( i m j ) ) ` k ) ) )
20		pmattomply1.m	. . 3 |- .* = ( .s ` Q )
21		pmattomply1.e	. . 3 |- .^ = (.g ` (mulGrp ` Q ) )
22		pmattomply1.x	. . 3 |- X = (var1 ` A )
23		pmattomply1.t	. . 3 |- T = ( m e. B |-> ( Q gsumg ( k e. NN0 |-> ( ( m F k ) .* ( k .^ X ) ) ) ) )
24	5, 7, 1, 19, 20, 21, 22, 12, 14, 2, 23	pmattomply1f 31244	. 2 |- ( ( N e. Fin /\ R e. Ring ) -> T : B --> L )
25		simplll 757	. . . . . . . . . 10 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> N e. Fin )
26		rngmnd 16746	. . . . . . . . . . . . . . 15 |- ( C e. Ring -> C e. Mnd )
27	9, 26	syl 16	. . . . . . . . . . . . . 14 |- ( ( N e. Fin /\ R e. Ring ) -> C e. Mnd )
28	27	anim1i 568	. . . . . . . . . . . . 13 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( C e. Mnd /\ ( a e. B /\ b e. B ) ) )
29		3anass 969	. . . . . . . . . . . . 13 |- ( ( C e. Mnd /\ a e. B /\ b e. B ) <-> ( C e. Mnd /\ ( a e. B /\ b e. B ) ) )
30	28, 29	sylibr 212	. . . . . . . . . . . 12 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( C e. Mnd /\ a e. B /\ b e. B ) )
31	1, 3	mndcl 15508	. . . . . . . . . . . 12 |- ( ( C e. Mnd /\ a e. B /\ b e. B ) -> ( a ( +g ` C ) b ) e. B )
32	30, 31	syl 16	. . . . . . . . . . 11 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` C ) b ) e. B )
33	32	adantr 465	. . . . . . . . . 10 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( a ( +g ` C ) b ) e. B )
34		simpr 461	. . . . . . . . . 10 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> k e. NN0 )
35		oveq 6182	. . . . . . . . . . . . . . . 16 |- ( m = n -> ( i m j ) = ( i n j ) )
36	35	fveq2d 5779	. . . . . . . . . . . . . . 15 |- ( m = n -> (coe1 ` ( i m j ) ) = (coe1 ` ( i n j ) ) )
37	36	fveq1d 5777	. . . . . . . . . . . . . 14 |- ( m = n -> ( (coe1 ` ( i m j ) ) ` k ) = ( (coe1 ` ( i n j ) ) ` k ) )
38	37	mpt2eq3dv 6237	. . . . . . . . . . . . 13 |- ( m = n -> ( i e. N , j e. N |-> ( (coe1 ` ( i m j ) ) ` k ) ) = ( i e. N , j e. N |-> ( (coe1 ` ( i n j ) ) ` k ) ) )
39		fveq2 5775	. . . . . . . . . . . . . 14 |- ( k = l -> ( (coe1 ` ( i n j ) ) ` k ) = ( (coe1 ` ( i n j ) ) ` l ) )
40	39	mpt2eq3dv 6237	. . . . . . . . . . . . 13 |- ( k = l -> ( i e. N , j e. N |-> ( (coe1 ` ( i n j ) ) ` k ) ) = ( i e. N , j e. N |-> ( (coe1 ` ( i n j ) ) ` l ) ) )
41	38, 40	cbvmpt2v 6251	. . . . . . . . . . . 12 |- ( m e. B , k e. NN0 |-> ( i e. N , j e. N |-> ( (coe1 ` ( i m j ) ) ` k ) ) ) = ( n e. B , l e. NN0 |-> ( i e. N , j e. N |-> ( (coe1 ` ( i n j ) ) ` l ) ) )
42	19, 41	eqtri 2478	. . . . . . . . . . 11 |- F = ( n e. B , l e. NN0 |-> ( i e. N , j e. N |-> ( (coe1 ` ( i n j ) ) ` l ) ) )
43	5, 7, 1, 42	pmatcollpw1lem1 31209	. . . . . . . . . 10 |- ( ( N e. Fin /\ ( a ( +g ` C ) b ) e. B /\ k e. NN0 ) -> ( ( a ( +g ` C ) b ) F k ) = ( i e. N , j e. N |-> ( (coe1 ` ( i ( a ( +g ` C ) b ) j ) ) ` k ) ) )
44	25, 33, 34, 43	syl3anc 1219	. . . . . . . . 9 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( a ( +g ` C ) b ) F k ) = ( i e. N , j e. N |-> ( (coe1 ` ( i ( a ( +g ` C ) b ) j ) ) ` k ) ) )
45		fvex 5785	. . . . . . . . . . . 12 |- ( (coe1 ` ( i a j ) ) ` k ) e. _V
46	45	a1i 11	. . . . . . . . . . 11 |- ( ( ( ( ( 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 )
47		fvex 5785	. . . . . . . . . . . 12 |- ( (coe1 ` ( i b j ) ) ` k ) e. _V
48	47	a1i 11	. . . . . . . . . . 11 |- ( ( ( ( ( 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 )
49		eqidd 2451	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) )
50		eqidd 2451	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) )
51	25, 25, 46, 48, 49, 50	offval22 6738	. . . . . . . . . 10 |- ( ( ( ( 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 ) ) ) )
52		eqid 2450	. . . . . . . . . . . 12 |- ( Base ` R ) = ( Base ` R )
53		eqid 2450	. . . . . . . . . . . 12 |- ( Base ` A ) = ( Base ` A )
54		simpllr 758	. . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> R e. Ring )
55		simprl 755	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ a e. B ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
56		simprr 756	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ a e. B ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
57	1	eleq2i 2526	. . . . . . . . . . . . . . . . . . . 20 |- ( a e. B <-> a e. ( Base ` C ) )
58	57	biimpi 194	. . . . . . . . . . . . . . . . . . 19 |- ( a e. B -> a e. ( Base ` C ) )
59	58	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ a e. B ) /\ ( i e. N /\ j e. N ) ) -> a e. ( Base ` C ) )
60		eqid 2450	. . . . . . . . . . . . . . . . . . 19 |- ( Base ` P ) = ( Base ` P )
61	7, 60	matecl 18421	. . . . . . . . . . . . . . . . . 18 |- ( ( i e. N /\ j e. N /\ a e. ( Base ` C ) ) -> ( i a j ) e. ( Base ` P ) )
62	55, 56, 59, 61	syl3anc 1219	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ a e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i a j ) e. ( Base ` P ) )
63	62	ex 434	. . . . . . . . . . . . . . . 16 |- ( ( ( N e. Fin /\ R e. Ring ) /\ a e. B ) -> ( ( i e. N /\ j e. N ) -> ( i a j ) e. ( Base ` P ) ) )
64	63	adantrr 716	. . . . . . . . . . . . . . 15 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( ( i e. N /\ j e. N ) -> ( i a j ) e. ( Base ` P ) ) )
65	64	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) ) )
66	65	3impib 1186	. . . . . . . . . . . . 13 |- ( ( ( ( ( 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 ) )
67	34	3ad2ant1 1009	. . . . . . . . . . . . 13 |- ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ i e. N /\ j e. N ) -> k e. NN0 )
68		eqid 2450	. . . . . . . . . . . . . 14 |- (coe1 ` ( i a j ) ) = (coe1 ` ( i a j ) )
69	68, 60, 5, 52	coe1fvalcl 30958	. . . . . . . . . . . . 13 |- ( ( ( i a j ) e. ( Base ` P ) /\ k e. NN0 ) -> ( (coe1 ` ( i a j ) ) ` k ) e. ( Base ` R ) )
70	66, 67, 69	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) )
71	12, 52, 53, 25, 54, 70	matbas2d 18419	. . . . . . . . . . 11 |- ( ( ( ( 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 ) )
72		simprl 755	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ b e. B ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
73		simprr 756	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ b e. B ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
74	1	eleq2i 2526	. . . . . . . . . . . . . . . . . . . 20 |- ( b e. B <-> b e. ( Base ` C ) )
75	74	biimpi 194	. . . . . . . . . . . . . . . . . . 19 |- ( b e. B -> b e. ( Base ` C ) )
76	75	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ b e. B ) /\ ( i e. N /\ j e. N ) ) -> b e. ( Base ` C ) )
77	7, 60	matecl 18421	. . . . . . . . . . . . . . . . . 18 |- ( ( i e. N /\ j e. N /\ b e. ( Base ` C ) ) -> ( i b j ) e. ( Base ` P ) )
78	72, 73, 76, 77	syl3anc 1219	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ b e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i b j ) e. ( Base ` P ) )
79	78	ex 434	. . . . . . . . . . . . . . . 16 |- ( ( ( N e. Fin /\ R e. Ring ) /\ b e. B ) -> ( ( i e. N /\ j e. N ) -> ( i b j ) e. ( Base ` P ) ) )
80	79	adantrl 715	. . . . . . . . . . . . . . 15 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( ( i e. N /\ j e. N ) -> ( i b j ) e. ( Base ` P ) ) )
81	80	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) ) )
82	81	3impib 1186	. . . . . . . . . . . . 13 |- ( ( ( ( ( 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 ) )
83		eqid 2450	. . . . . . . . . . . . . 14 |- (coe1 ` ( i b j ) ) = (coe1 ` ( i b j ) )
84	83, 60, 5, 52	coe1fvalcl 30958	. . . . . . . . . . . . 13 |- ( ( ( i b j ) e. ( Base ` P ) /\ k e. NN0 ) -> ( (coe1 ` ( i b j ) ) ` k ) e. ( Base ` R ) )
85	82, 67, 84	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) )
86	12, 52, 53, 25, 54, 85	matbas2d 18419	. . . . . . . . . . 11 |- ( ( ( ( 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 ) )
87		eqid 2450	. . . . . . . . . . . 12 |- ( +g ` A ) = ( +g ` A )
88		eqid 2450	. . . . . . . . . . . 12 |- ( +g ` R ) = ( +g ` R )
89	12, 53, 87, 88	matplusg2 18423	. . . . . . . . . . 11 |- ( ( ( 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 ) ) ) )
90	71, 86, 89	syl2anc 661	. . . . . . . . . 10 |- ( ( ( ( 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 ) ) ) )
91		simplr 754	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( a e. B /\ b e. B ) )
92	91	anim1i 568	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 ) ) )
93	92	3impb 1184	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 ) ) )
94		eqid 2450	. . . . . . . . . . . . . . . 16 |- ( +g ` P ) = ( +g ` P )
95	7, 1, 3, 94	matplusgcell 30991	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) )
96	93, 95	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ( ( 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 ) ) )
97	96	fveq2d 5779	. . . . . . . . . . . . 13 |- ( ( ( ( ( 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 ) ) ) )
98	97	fveq1d 5777	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) )
99	54	3ad2ant1 1009	. . . . . . . . . . . . 13 |- ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) /\ i e. N /\ j e. N ) -> R e. Ring )
100	5, 60, 94, 88	coe1addfv 17812	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
101	99, 66, 82, 67, 100	syl31anc 1222	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) ) )
102	98, 101	eqtrd 2490	. . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) )
103	102	mpt2eq3dva 6235	. . . . . . . . . 10 |- ( ( ( ( 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 ) ) ) )
104	51, 90, 103	3eqtr4rd 2501	. . . . . . . . 9 |- ( ( ( ( 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 ) ) ) )
105	14	ply1sca 17801	. . . . . . . . . . . . 13 |- ( A e. Ring -> A = (Scalar ` Q ) )
106	13, 105	syl 16	. . . . . . . . . . . 12 |- ( ( N e. Fin /\ R e. Ring ) -> A = (Scalar ` Q ) )
107	106	ad2antrr 725	. . . . . . . . . . 11 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> A = (Scalar ` Q ) )
108	107	fveq2d 5779	. . . . . . . . . 10 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( +g ` A ) = ( +g ` (Scalar ` Q ) ) )
109		simpl 457	. . . . . . . . . . . . . . 15 |- ( ( N e. Fin /\ R e. Ring ) -> N e. Fin )
110		simpl 457	. . . . . . . . . . . . . . 15 |- ( ( a e. B /\ b e. B ) -> a e. B )
111	109, 110	anim12i 566	. . . . . . . . . . . . . 14 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( N e. Fin /\ a e. B ) )
112	111	anim1i 568	. . . . . . . . . . . . 13 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( N e. Fin /\ a e. B ) /\ k e. NN0 ) )
113		df-3an 967	. . . . . . . . . . . . 13 |- ( ( N e. Fin /\ a e. B /\ k e. NN0 ) <-> ( ( N e. Fin /\ a e. B ) /\ k e. NN0 ) )
114	112, 113	sylibr 212	. . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( N e. Fin /\ a e. B /\ k e. NN0 ) )
115	5, 7, 1, 42	pmatcollpw1lem1 31209	. . . . . . . . . . . 12 |- ( ( N e. Fin /\ a e. B /\ k e. NN0 ) -> ( a F k ) = ( i e. N , j e. N |-> ( (coe1 ` ( i a j ) ) ` k ) ) )
116	114, 115	syl 16	. . . . . . . . . . 11 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( a F k ) = ( i e. N , j e. N |-> ( (coe1 ` ( i a j ) ) ` k ) ) )
117	116	eqcomd 2457	. . . . . . . . . 10 |- ( ( ( ( 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 F k ) )
118		simpr 461	. . . . . . . . . . . . . . 15 |- ( ( a e. B /\ b e. B ) -> b e. B )
119	109, 118	anim12i 566	. . . . . . . . . . . . . 14 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( N e. Fin /\ b e. B ) )
120	119	anim1i 568	. . . . . . . . . . . . 13 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( N e. Fin /\ b e. B ) /\ k e. NN0 ) )
121		df-3an 967	. . . . . . . . . . . . 13 |- ( ( N e. Fin /\ b e. B /\ k e. NN0 ) <-> ( ( N e. Fin /\ b e. B ) /\ k e. NN0 ) )
122	120, 121	sylibr 212	. . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( N e. Fin /\ b e. B /\ k e. NN0 ) )
123	5, 7, 1, 42	pmatcollpw1lem1 31209	. . . . . . . . . . . 12 |- ( ( N e. Fin /\ b e. B /\ k e. NN0 ) -> ( b F k ) = ( i e. N , j e. N |-> ( (coe1 ` ( i b j ) ) ` k ) ) )
124	122, 123	syl 16	. . . . . . . . . . 11 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( b F k ) = ( i e. N , j e. N |-> ( (coe1 ` ( i b j ) ) ` k ) ) )
125	124	eqcomd 2457	. . . . . . . . . 10 |- ( ( ( ( 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 F k ) )
126	108, 117, 125	oveq123d 6197	. . . . . . . . 9 |- ( ( ( ( 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 F k ) ( +g ` (Scalar ` Q ) ) ( b F k ) ) )
127	44, 104, 126	3eqtrd 2494	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( a ( +g ` C ) b ) F k ) = ( ( a F k ) ( +g ` (Scalar ` Q ) ) ( b F k ) ) )
128	127	oveq1d 6191	. . . . . . 7 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( ( a ( +g ` C ) b ) F k ) .* ( k .^ X ) ) = ( ( ( a F k ) ( +g ` (Scalar ` Q ) ) ( b F k ) ) .* ( k .^ X ) ) )
129	14	ply1lmod 17800	. . . . . . . . . 10 |- ( A e. Ring -> Q e. LMod )
130	13, 129	syl 16	. . . . . . . . 9 |- ( ( N e. Fin /\ R e. Ring ) -> Q e. LMod )
131	130	ad2antrr 725	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> Q e. LMod )
132		simpll 753	. . . . . . . . . 10 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( N e. Fin /\ R e. Ring ) )
133		simprl 755	. . . . . . . . . . 11 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> a e. B )
134	133	anim1i 568	. . . . . . . . . 10 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( a e. B /\ k e. NN0 ) )
135	5, 7, 1, 42, 12, 53	pmatcollpw1lem2 31210	. . . . . . . . . 10 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ k e. NN0 ) ) -> ( a F k ) e. ( Base ` A ) )
136	132, 134, 135	syl2anc 661	. . . . . . . . 9 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( a F k ) e. ( Base ` A ) )
137	106	eqcomd 2457	. . . . . . . . . . 11 |- ( ( N e. Fin /\ R e. Ring ) -> (Scalar ` Q ) = A )
138	137	ad2antrr 725	. . . . . . . . . 10 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> (Scalar ` Q ) = A )
139	138	fveq2d 5779	. . . . . . . . 9 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( Base ` (Scalar ` Q ) ) = ( Base ` A ) )
140	136, 139	eleqtrrd 2539	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( a F k ) e. ( Base ` (Scalar ` Q ) ) )
141		simprr 756	. . . . . . . . . . 11 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> b e. B )
142	141	anim1i 568	. . . . . . . . . 10 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( b e. B /\ k e. NN0 ) )
143	5, 7, 1, 42, 12, 53	pmatcollpw1lem2 31210	. . . . . . . . . 10 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( b e. B /\ k e. NN0 ) ) -> ( b F k ) e. ( Base ` A ) )
144	132, 142, 143	syl2anc 661	. . . . . . . . 9 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( b F k ) e. ( Base ` A ) )
145	144, 139	eleqtrrd 2539	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( b F k ) e. ( Base ` (Scalar ` Q ) ) )
146		eqid 2450	. . . . . . . . . . . 12 |- (mulGrp ` Q ) = (mulGrp ` Q )
147	146	rngmgp 16743	. . . . . . . . . . 11 |- ( Q e. Ring -> (mulGrp ` Q ) e. Mnd )
148	16, 147	syl 16	. . . . . . . . . 10 |- ( ( N e. Fin /\ R e. Ring ) -> (mulGrp ` Q ) e. Mnd )
149	148	ad2antrr 725	. . . . . . . . 9 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> (mulGrp ` Q ) e. Mnd )
150	22, 14, 2	vr1cl 17764	. . . . . . . . . . 11 |- ( A e. Ring -> X e. L )
151	13, 150	syl 16	. . . . . . . . . 10 |- ( ( N e. Fin /\ R e. Ring ) -> X e. L )
152	151	ad2antrr 725	. . . . . . . . 9 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> X e. L )
153	146, 2	mgpbas 16688	. . . . . . . . . 10 |- L = ( Base ` (mulGrp ` Q ) )
154	153, 21	mulgnn0cl 15731	. . . . . . . . 9 |- ( ( (mulGrp ` Q ) e. Mnd /\ k e. NN0 /\ X e. L ) -> ( k .^ X ) e. L )
155	149, 34, 152, 154	syl3anc 1219	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( k .^ X ) e. L )
156		eqid 2450	. . . . . . . . 9 |- (Scalar ` Q ) = (Scalar ` Q )
157		eqid 2450	. . . . . . . . 9 |- ( Base ` (Scalar ` Q ) ) = ( Base ` (Scalar ` Q ) )
158		eqid 2450	. . . . . . . . 9 |- ( +g ` (Scalar ` Q ) ) = ( +g ` (Scalar ` Q ) )
159	2, 4, 156, 20, 157, 158	lmodvsdir 17064	. . . . . . . 8 |- ( ( Q e. LMod /\ ( ( a F k ) e. ( Base ` (Scalar ` Q ) ) /\ ( b F k ) e. ( Base ` (Scalar ` Q ) ) /\ ( k .^ X ) e. L ) ) -> ( ( ( a F k ) ( +g ` (Scalar ` Q ) ) ( b F k ) ) .* ( k .^ X ) ) = ( ( ( a F k ) .* ( k .^ X ) ) ( +g ` Q ) ( ( b F k ) .* ( k .^ X ) ) ) )
160	131, 140, 145, 155, 159	syl13anc 1221	. . . . . . 7 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( ( a F k ) ( +g ` (Scalar ` Q ) ) ( b F k ) ) .* ( k .^ X ) ) = ( ( ( a F k ) .* ( k .^ X ) ) ( +g ` Q ) ( ( b F k ) .* ( k .^ X ) ) ) )
161	128, 160	eqtrd 2490	. . . . . 6 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( ( a ( +g ` C ) b ) F k ) .* ( k .^ X ) ) = ( ( ( a F k ) .* ( k .^ X ) ) ( +g ` Q ) ( ( b F k ) .* ( k .^ X ) ) ) )
162	161	mpteq2dva 4462	. . . . 5 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( k e. NN0 |-> ( ( ( a ( +g ` C ) b ) F k ) .* ( k .^ X ) ) ) = ( k e. NN0 |-> ( ( ( a F k ) .* ( k .^ X ) ) ( +g ` Q ) ( ( b F k ) .* ( k .^ X ) ) ) ) )
163	162	oveq2d 6192	. . . 4 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( Q gsumg ( k e. NN0 |-> ( ( ( a ( +g ` C ) b ) F k ) .* ( k .^ X ) ) ) ) = ( Q gsumg ( k e. NN0 |-> ( ( ( a F k ) .* ( k .^ X ) ) ( +g ` Q ) ( ( b F k ) .* ( k .^ X ) ) ) ) ) )
164		eqid 2450	. . . . 5 |- ( 0g ` Q ) = ( 0g ` Q )
165		rngcmn 16767	. . . . . . 7 |- ( Q e. Ring -> Q e. CMnd )
166	16, 165	syl 16	. . . . . 6 |- ( ( N e. Fin /\ R e. Ring ) -> Q e. CMnd )
167	166	adantr 465	. . . . 5 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> Q e. CMnd )
168		nn0ex 10672	. . . . . 6 |- NN0 e. _V
169	168	a1i 11	. . . . 5 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> NN0 e. _V )
170	110	anim2i 569	. . . . . . 7 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ a e. B ) )
171		df-3an 967	. . . . . . 7 |- ( ( N e. Fin /\ R e. Ring /\ a e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ a e. B ) )
172	170, 171	sylibr 212	. . . . . 6 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( N e. Fin /\ R e. Ring /\ a e. B ) )
173	5, 7, 1, 42, 20, 21, 22, 12, 14, 2	pmattomply1ghmlem1 31239	. . . . . 6 |- ( ( ( N e. Fin /\ R e. Ring /\ a e. B ) /\ k e. NN0 ) -> ( ( a F k ) .* ( k .^ X ) ) e. L )
174	172, 173	sylan 471	. . . . 5 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( a F k ) .* ( k .^ X ) ) e. L )
175	118	anim2i 569	. . . . . . 7 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ b e. B ) )
176		df-3an 967	. . . . . . 7 |- ( ( N e. Fin /\ R e. Ring /\ b e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ b e. B ) )
177	175, 176	sylibr 212	. . . . . 6 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( N e. Fin /\ R e. Ring /\ b e. B ) )
178	5, 7, 1, 42, 20, 21, 22, 12, 14, 2	pmattomply1ghmlem1 31239	. . . . . 6 |- ( ( ( N e. Fin /\ R e. Ring /\ b e. B ) /\ k e. NN0 ) -> ( ( b F k ) .* ( k .^ X ) ) e. L )
179	177, 178	sylan 471	. . . . 5 |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) /\ k e. NN0 ) -> ( ( b F k ) .* ( k .^ X ) ) e. L )
180		eqidd 2451	. . . . 5 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( k e. NN0 |-> ( ( a F k ) .* ( k .^ X ) ) ) = ( k e. NN0 |-> ( ( a F k ) .* ( k .^ X ) ) ) )
181		eqidd 2451	. . . . 5 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( k e. NN0 |-> ( ( b F k ) .* ( k .^ X ) ) ) = ( k e. NN0 |-> ( ( b F k ) .* ( k .^ X ) ) ) )
182	5, 7, 1, 19, 20, 21, 22, 12, 14, 2	pmattomply1ghmlem2 31240	. . . . . 6 |- ( ( N e. Fin /\ R e. Ring /\ a e. B ) -> ( k e. NN0 |-> ( ( a F k ) .* ( k .^ X ) ) ) finSupp ( 0g ` Q ) )
183	172, 182	syl 16	. . . . 5 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( k e. NN0 |-> ( ( a F k ) .* ( k .^ X ) ) ) finSupp ( 0g ` Q ) )
184	5, 7, 1, 19, 20, 21, 22, 12, 14, 2	pmattomply1ghmlem2 31240	. . . . . 6 |- ( ( N e. Fin /\ R e. Ring /\ b e. B ) -> ( k e. NN0 |-> ( ( b F k ) .* ( k .^ X ) ) ) finSupp ( 0g ` Q ) )
185	177, 184	syl 16	. . . . 5 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( k e. NN0 |-> ( ( b F k ) .* ( k .^ X ) ) ) finSupp ( 0g ` Q ) )
186	2, 164, 4, 167, 169, 174, 179, 180, 181, 183, 185	gsummptfsadd 16504	. . . 4 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( Q gsumg ( k e. NN0 |-> ( ( ( a F k ) .* ( k .^ X ) ) ( +g ` Q ) ( ( b F k ) .* ( k .^ X ) ) ) ) ) = ( ( Q gsumg ( k e. NN0 |-> ( ( a F k ) .* ( k .^ X ) ) ) ) ( +g ` Q ) ( Q gsumg ( k e. NN0 |-> ( ( b F k ) .* ( k .^ X ) ) ) ) ) )
187	163, 186	eqtrd 2490	. . 3 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( Q gsumg ( k e. NN0 |-> ( ( ( a ( +g ` C ) b ) F k ) .* ( k .^ X ) ) ) ) = ( ( Q gsumg ( k e. NN0 |-> ( ( a F k ) .* ( k .^ X ) ) ) ) ( +g ` Q ) ( Q gsumg ( k e. NN0 |-> ( ( b F k ) .* ( k .^ X ) ) ) ) ) )
188	5, 7, 1, 19, 20, 21, 22, 12, 14, 2, 23	pmattomply1 31242	. . . 4 |- ( ( a ( +g ` C ) b ) e. B -> ( T ` ( a ( +g ` C ) b ) ) = ( Q gsumg ( k e. NN0 |-> ( ( ( a ( +g ` C ) b ) F k ) .* ( k .^ X ) ) ) ) )
189	32, 188	syl 16	. . 3 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( T ` ( a ( +g ` C ) b ) ) = ( Q gsumg ( k e. NN0 |-> ( ( ( a ( +g ` C ) b ) F k ) .* ( k .^ X ) ) ) ) )
190	5, 7, 1, 19, 20, 21, 22, 12, 14, 2, 23	pmattomply1 31242	. . . . 5 |- ( a e. B -> ( T ` a ) = ( Q gsumg ( k e. NN0 |-> ( ( a F k ) .* ( k .^ X ) ) ) ) )
191	5, 7, 1, 19, 20, 21, 22, 12, 14, 2, 23	pmattomply1 31242	. . . . 5 |- ( b e. B -> ( T ` b ) = ( Q gsumg ( k e. NN0 |-> ( ( b F k ) .* ( k .^ X ) ) ) ) )
192	190, 191	oveqan12d 6195	. . . 4 |- ( ( a e. B /\ b e. B ) -> ( ( T ` a ) ( +g ` Q ) ( T ` b ) ) = ( ( Q gsumg ( k e. NN0 |-> ( ( a F k ) .* ( k .^ X ) ) ) ) ( +g ` Q ) ( Q gsumg ( k e. NN0 |-> ( ( b F k ) .* ( k .^ X ) ) ) ) ) )
193	192	adantl 466	. . 3 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( ( T ` a ) ( +g ` Q ) ( T ` b ) ) = ( ( Q gsumg ( k e. NN0 |-> ( ( a F k ) .* ( k .^ X ) ) ) ) ( +g ` Q ) ( Q gsumg ( k e. NN0 |-> ( ( b F k ) .* ( k .^ X ) ) ) ) ) )
194	187, 189, 193	3eqtr4d 2500	. 2 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( a e. B /\ b e. B ) ) -> ( T ` ( a ( +g ` C ) b ) ) = ( ( T ` a ) ( +g ` Q ) ( T ` b ) ) )
195	1, 2, 3, 4, 11, 18, 24, 194	isghmd 15844	1 |- ( ( N e. Fin /\ R e. Ring ) -> T e. ( C GrpHom Q ) )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 965   = wceq 1370   e. wcel 1757   _Vcvv 3054   class class class wbr 4376   |-> cmpt 4434   ` cfv 5502  (class class class)co 6176   |-> cmpt2 6178   oFcof 6404   Fincfn 7396   finSupp cfsupp 7707   NN0cn0 10666   Basecbs 14262   +g cplusg 14326  Scalarcsca 14329   .scvsca 14330   0gc0g 14466   gsum_g cgsu 14467   Mndcmnd 15497   Grpcgrp 15498  ._gcmg 15502   GrpHom cghm 15832  CMndccmn 16367  mulGrpcmgp 16682   Ringcrg 16737   LModclmod 17040  var₁cv1 17725  Poly₁cpl1 17726  coe₁cco1 17727   Mat cmat 18375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-rep 4487  ax-sep 4497  ax-nul 4505  ax-pow 4554  ax-pr 4615  ax-un 6458  ax-inf2 7934  ax-cnex 9425  ax-resscn 9426  ax-1cn 9427  ax-icn 9428  ax-addcl 9429  ax-addrcl 9430  ax-mulcl 9431  ax-mulrcl 9432  ax-mulcom 9433  ax-addass 9434  ax-mulass 9435  ax-distr 9436  ax-i2m1 9437  ax-1ne0 9438  ax-1rid 9439  ax-rnegex 9440  ax-rrecex 9441  ax-cnre 9442  ax-pre-lttri 9443  ax-pre-lttrn 9444  ax-pre-ltadd 9445  ax-pre-mulgt0 9446

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-nel 2644  df-ral 2797  df-rex 2798  df-reu 2799  df-rmo 2800  df-rab 2801  df-v 3056  df-sbc 3271  df-csb 3373  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-pss 3428  df-nul 3722  df-if 3876  df-pw 3946  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-ot 3970  df-uni 4176  df-int 4213  df-iun 4257  df-iin 4258  df-br 4377  df-opab 4435  df-mpt 4436  df-tr 4470  df-eprel 4716  df-id 4720  df-po 4725  df-so 4726  df-fr 4763  df-se 4764  df-we 4765  df-ord 4806  df-on 4807  df-lim 4808  df-suc 4809  df-xp 4930  df-rel 4931  df-cnv 4932  df-co 4933  df-dm 4934  df-rn 4935  df-res 4936  df-ima 4937  df-iota 5465  df-fun 5504  df-fn 5505  df-f 5506  df-f1 5507  df-fo 5508  df-f1o 5509  df-fv 5510  df-isom 5511  df-riota 6137  df-ov 6179  df-oprab 6180  df-mpt2 6181  df-of 6406  df-ofr 6407  df-om 6563  df-1st 6663  df-2nd 6664  df-supp 6777  df-recs 6918  df-rdg 6952  df-1o 7006  df-2o 7007  df-oadd 7010  df-er 7187  df-map 7302  df-pm 7303  df-ixp 7350  df-en 7397  df-dom 7398  df-sdom 7399  df-fin 7400  df-fsupp 7708  df-sup 7778  df-oi 7811  df-card 8196  df-pnf 9507  df-mnf 9508  df-xr 9509  df-ltxr 9510  df-le 9511  df-sub 9684  df-neg 9685  df-nn 10410  df-2 10467  df-3 10468  df-4 10469  df-5 10470  df-6 10471  df-7 10472  df-8 10473  df-9 10474  df-10 10475  df-n0 10667  df-z 10734  df-dec 10843  df-uz 10949  df-fz 11525  df-fzo 11636  df-seq 11894  df-hash 12191  df-struct 14264  df-ndx 14265  df-slot 14266  df-base 14267  df-sets 14268  df-ress 14269  df-plusg 14339  df-mulr 14340  df-sca 14342  df-vsca 14343  df-ip 14344  df-tset 14345  df-ple 14346  df-ds 14348  df-hom 14350  df-cco 14351  df-0g 14468  df-gsum 14469  df-prds 14474  df-pws 14476  df-mre 14612  df-mrc 14613  df-acs 14615  df-mnd 15503  df-mhm 15552  df-submnd 15553  df-grp 15633  df-minusg 15634  df-sbg 15635  df-mulg 15636  df-subg 15766  df-ghm 15833  df-cntz 15923  df-cmn 16369  df-abl 16370  df-mgp 16683  df-ur 16695  df-rng 16739  df-subrg 16955  df-lmod 17042  df-lss 17106  df-sra 17345  df-rgmod 17346  df-psr 17515  df-mvr 17516  df-mpl 17517  df-opsr 17519  df-psr1 17729  df-vr1 17730  df-ply1 17731  df-coe1 17732  df-dsmm 18252  df-frlm 18267  df-mamu 18376  df-mat 18377

This theorem is referenced by:  pmattomply1grpiso  31257  pmattomply1rhm  31262  pmat2matp  31265