Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pmattomply1ghm Structured version   Unicode version

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.
StepHypRef 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 )
65ply1rng 17796 . . . 4  |-  ( R  e.  Ring  ->  P  e. 
Ring )
7 pmattomply1.c . . . . 5  |-  C  =  ( N Mat  P )
87matrng 18426 . . . 4  |-  ( ( N  e.  Fin  /\  P  e.  Ring )  ->  C  e.  Ring )
96, 8sylan2 474 . . 3  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  C  e.  Ring )
10 rnggrp 16742 . . 3  |-  ( C  e.  Ring  ->  C  e. 
Grp )
119, 10syl 16 . 2  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  C  e.  Grp )
12 pmattomply1.a . . . . 5  |-  A  =  ( N Mat  R )
1312matrng 18426 . . . 4  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  A  e.  Ring )
14 pmattomply1.q . . . . 5  |-  Q  =  (Poly1 `  A )
1514ply1rng 17796 . . . 4  |-  ( A  e.  Ring  ->  Q  e. 
Ring )
1613, 15syl 16 . . 3  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  Q  e.  Ring )
17 rnggrp 16742 . . 3  |-  ( Q  e.  Ring  ->  Q  e. 
Grp )
1816, 17syl 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 )
) ) ) )
245, 7, 1, 19, 20, 21, 22, 12, 14, 2, 23pmattomply1f 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 )
279, 26syl 16 . . . . . . . . . . . . . 14  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  C  e.  Mnd )
2827anim1i 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
) ) )
3028, 29sylibr 212 . . . . . . . . . . . 12  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B
) )  ->  ( C  e.  Mnd  /\  a  e.  B  /\  b  e.  B ) )
311, 3mndcl 15508 . . . . . . . . . . . 12  |-  ( ( C  e.  Mnd  /\  a  e.  B  /\  b  e.  B )  ->  ( a ( +g  `  C ) b )  e.  B )
3230, 31syl 16 . . . . . . . . . . 11  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B
) )  ->  (
a ( +g  `  C
) b )  e.  B )
3332adantr 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 ) )
3635fveq2d 5779 . . . . . . . . . . . . . . 15  |-  ( m  =  n  ->  (coe1 `  ( i m j ) )  =  (coe1 `  ( i n j ) ) )
3736fveq1d 5777 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  (
(coe1 `  ( i m j ) ) `  k )  =  ( (coe1 `  ( i n j ) ) `  k ) )
3837mpt2eq3dv 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 ) )
4039mpt2eq3dv 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 ) ) )
4138, 40cbvmpt2v 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 ) ) )
4219, 41eqtri 2478 . . . . . . . . . . 11  |-  F  =  ( n  e.  B ,  l  e.  NN0  |->  ( i  e.  N ,  j  e.  N  |->  ( (coe1 `  ( i n j ) ) `  l ) ) )
435, 7, 1, 42pmatcollpw1lem1 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
) ) )
4425, 33, 34, 43syl3anc 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
4645a1i 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
4847a1i 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 ) ) )
5125, 25, 46, 48, 49, 50offval22 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 )
571eleq2i 2526 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  e.  B  <->  a  e.  ( Base `  C )
)
5857biimpi 194 . . . . . . . . . . . . . . . . . . 19  |-  ( a  e.  B  ->  a  e.  ( Base `  C
) )
5958ad2antlr 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 )
617, 60matecl 18421 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  N  /\  j  e.  N  /\  a  e.  ( Base `  C ) )  -> 
( i a j )  e.  ( Base `  P ) )
6255, 56, 59, 61syl3anc 1219 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  a  e.  B )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  ( i
a j )  e.  ( Base `  P
) )
6362ex 434 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  a  e.  B
)  ->  ( (
i  e.  N  /\  j  e.  N )  ->  ( i a j )  e.  ( Base `  P ) ) )
6463adantrr 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
) ) )
6564adantr 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
) ) )
66653impib 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
) )
67343ad2ant1 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 ) )
6968, 60, 5, 52coe1fvalcl 30958 . . . . . . . . . . . . 13  |-  ( ( ( i a j )  e.  ( Base `  P )  /\  k  e.  NN0 )  ->  (
(coe1 `  ( i a j ) ) `  k )  e.  (
Base `  R )
)
7066, 67, 69syl2anc 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 )
)
7112, 52, 53, 25, 54, 70matbas2d 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 )
741eleq2i 2526 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  e.  B  <->  b  e.  ( Base `  C )
)
7574biimpi 194 . . . . . . . . . . . . . . . . . . 19  |-  ( b  e.  B  ->  b  e.  ( Base `  C
) )
7675ad2antlr 726 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  b  e.  B )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  b  e.  ( Base `  C )
)
777, 60matecl 18421 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  N  /\  j  e.  N  /\  b  e.  ( Base `  C ) )  -> 
( i b j )  e.  ( Base `  P ) )
7872, 73, 76, 77syl3anc 1219 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  b  e.  B )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  ( i
b j )  e.  ( Base `  P
) )
7978ex 434 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  b  e.  B
)  ->  ( (
i  e.  N  /\  j  e.  N )  ->  ( i b j )  e.  ( Base `  P ) ) )
8079adantrl 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
) ) )
8180adantr 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
) ) )
82813impib 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 ) )
8483, 60, 5, 52coe1fvalcl 30958 . . . . . . . . . . . . 13  |-  ( ( ( i b j )  e.  ( Base `  P )  /\  k  e.  NN0 )  ->  (
(coe1 `  ( i b j ) ) `  k )  e.  (
Base `  R )
)
8582, 67, 84syl2anc 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 )
)
8612, 52, 53, 25, 54, 85matbas2d 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 )
8912, 53, 87, 88matplusg2 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 ) ) ) )
9071, 86, 89syl2anc 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
) )
9291anim1i 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 )
) )
93923impb 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 )
957, 1, 3, 94matplusgcell 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 ) ) )
9693, 95syl 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 ) ) )
9796fveq2d 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 ) ) ) )
9897fveq1d 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 ) )
99543ad2ant1 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 )
1005, 60, 94, 88coe1addfv 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
) ) )
10199, 66, 82, 67, 100syl31anc 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
) ) )
10298, 101eqtrd 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
) ) )
103102mpt2eq3dva 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
) ) ) )
10451, 90, 1033eqtr4rd 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 ) ) ) )
10514ply1sca 17801 . . . . . . . . . . . . 13  |-  ( A  e.  Ring  ->  A  =  (Scalar `  Q )
)
10613, 105syl 16 . . . . . . . . . . . 12  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  A  =  (Scalar `  Q
) )
107106ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B ) )  /\  k  e.  NN0 )  ->  A  =  (Scalar `  Q
) )
108107fveq2d 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 )
111109, 110anim12i 566 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B
) )  ->  ( N  e.  Fin  /\  a  e.  B ) )
112111anim1i 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 ) )
114112, 113sylibr 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 ) )
1155, 7, 1, 42pmatcollpw1lem1 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
) ) )
116114, 115syl 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
) ) )
117116eqcomd 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 )
119109, 118anim12i 566 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B
) )  ->  ( N  e.  Fin  /\  b  e.  B ) )
120119anim1i 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 ) )
122120, 121sylibr 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 ) )
1235, 7, 1, 42pmatcollpw1lem1 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
) ) )
124122, 123syl 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
) ) )
125124eqcomd 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 ) )
126108, 117, 125oveq123d 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 ) ) )
12744, 104, 1263eqtrd 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 ) ) )
128127oveq1d 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 ) ) )
12914ply1lmod 17800 . . . . . . . . . 10  |-  ( A  e.  Ring  ->  Q  e. 
LMod )
13013, 129syl 16 . . . . . . . . 9  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  Q  e.  LMod )
131130ad2antrr 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 )
134133anim1i 568 . . . . . . . . . 10  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B ) )  /\  k  e.  NN0 )  -> 
( a  e.  B  /\  k  e.  NN0 ) )
1355, 7, 1, 42, 12, 53pmatcollpw1lem2 31210 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  k  e.  NN0 ) )  ->  (
a F k )  e.  ( Base `  A
) )
136132, 134, 135syl2anc 661 . . . . . . . . 9  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B ) )  /\  k  e.  NN0 )  -> 
( a F k )  e.  ( Base `  A ) )
137106eqcomd 2457 . . . . . . . . . . 11  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
(Scalar `  Q )  =  A )
138137ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B ) )  /\  k  e.  NN0 )  -> 
(Scalar `  Q )  =  A )
139138fveq2d 5779 . . . . . . . . 9  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B ) )  /\  k  e.  NN0 )  -> 
( Base `  (Scalar `  Q
) )  =  (
Base `  A )
)
140136, 139eleqtrrd 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 )
142141anim1i 568 . . . . . . . . . 10  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B ) )  /\  k  e.  NN0 )  -> 
( b  e.  B  /\  k  e.  NN0 ) )
1435, 7, 1, 42, 12, 53pmatcollpw1lem2 31210 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( b  e.  B  /\  k  e.  NN0 ) )  ->  (
b F k )  e.  ( Base `  A
) )
144132, 142, 143syl2anc 661 . . . . . . . . 9  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B ) )  /\  k  e.  NN0 )  -> 
( b F k )  e.  ( Base `  A ) )
145144, 139eleqtrrd 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 )
147146rngmgp 16743 . . . . . . . . . . 11  |-  ( Q  e.  Ring  ->  (mulGrp `  Q )  e.  Mnd )
14816, 147syl 16 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
(mulGrp `  Q )  e.  Mnd )
149148ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B ) )  /\  k  e.  NN0 )  -> 
(mulGrp `  Q )  e.  Mnd )
15022, 14, 2vr1cl 17764 . . . . . . . . . . 11  |-  ( A  e.  Ring  ->  X  e.  L )
15113, 150syl 16 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  X  e.  L )
152151ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B ) )  /\  k  e.  NN0 )  ->  X  e.  L )
153146, 2mgpbas 16688 . . . . . . . . . 10  |-  L  =  ( Base `  (mulGrp `  Q ) )
154153, 21mulgnn0cl 15731 . . . . . . . . 9  |-  ( ( (mulGrp `  Q )  e.  Mnd  /\  k  e. 
NN0  /\  X  e.  L )  ->  (
k  .^  X )  e.  L )
155149, 34, 152, 154syl3anc 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 )
)
1592, 4, 156, 20, 157, 158lmodvsdir 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 )
) ) )
160131, 140, 145, 155, 159syl13anc 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 )
) ) )
161128, 160eqtrd 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
) ) ) )
162161mpteq2dva 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 ) ) ) ) )
163162oveq2d 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
)
16616, 165syl 16 . . . . . 6  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  Q  e. CMnd )
167166adantr 465 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B
) )  ->  Q  e. CMnd )
168 nn0ex 10672 . . . . . 6  |-  NN0  e.  _V
169168a1i 11 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B
) )  ->  NN0  e.  _V )
170110anim2i 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 ) )
172170, 171sylibr 212 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B
) )  ->  ( N  e.  Fin  /\  R  e.  Ring  /\  a  e.  B ) )
1735, 7, 1, 42, 20, 21, 22, 12, 14, 2pmattomply1ghmlem1 31239 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  a  e.  B )  /\  k  e.  NN0 )  ->  (
( a F k )  .*  ( k 
.^  X ) )  e.  L )
174172, 173sylan 471 . . . . 5  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B ) )  /\  k  e.  NN0 )  -> 
( ( a F k )  .*  (
k  .^  X )
)  e.  L )
175118anim2i 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 ) )
177175, 176sylibr 212 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( a  e.  B  /\  b  e.  B
) )  ->  ( N  e.  Fin  /\  R  e.  Ring  /\  b  e.  B ) )
1785, 7, 1, 42, 20, 21, 22, 12, 14, 2pmattomply1ghmlem1 31239 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  b  e.  B )  /\  k  e.  NN0 )  ->  (
( b F k )  .*  ( k 
.^  X ) )  e.  L )
179177, 178sylan 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
) ) ) )
1825, 7, 1, 19, 20, 21, 22, 12, 14, 2pmattomply1ghmlem2 31240 . . . . . 6  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  a  e.  B )  ->  (
k  e.  NN0  |->  ( ( a F k )  .*  ( k  .^  X ) ) ) finSupp 
( 0g `  Q
) )
183172, 182syl 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
) )
1845, 7, 1, 19, 20, 21, 22, 12, 14, 2pmattomply1ghmlem2 31240 . . . . . 6  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  b  e.  B )  ->  (
k  e.  NN0  |->  ( ( b F k )  .*  ( k  .^  X ) ) ) finSupp 
( 0g `  Q
) )
185177, 184syl 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
) )
1862, 164, 4, 167, 169, 174, 179, 180, 181, 183, 185gsummptfsadd 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 )
) ) ) ) )
187163, 186eqtrd 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 ) ) ) ) ) )
1885, 7, 1, 19, 20, 21, 22, 12, 14, 2, 23pmattomply1 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 )
) ) ) )
18932, 188syl 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 )
) ) ) )
1905, 7, 1, 19, 20, 21, 22, 12, 14, 2, 23pmattomply1 31242 . . . . 5  |-  ( a  e.  B  ->  ( T `  a )  =  ( Q  gsumg  ( k  e.  NN0  |->  ( ( a F k )  .*  ( k  .^  X ) ) ) ) )
1915, 7, 1, 19, 20, 21, 22, 12, 14, 2, 23pmattomply1 31242 . . . . 5  |-  ( b  e.  B  ->  ( T `  b )  =  ( Q  gsumg  ( k  e.  NN0  |->  ( ( b F k )  .*  ( k  .^  X ) ) ) ) )
192190, 191oveqan12d 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 )
) ) ) ) )
193192adantl 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 ) ) ) ) ) )
194187, 189, 1933eqtr4d 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 ) ) )
1951, 2, 3, 4, 11, 18, 24, 194isghmd 15844 1  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  T  e.  ( C  GrpHom  Q ) )
Colors of variables: wff setvar class
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    gsumg cgsu 14467   Mndcmnd 15497   Grpcgrp 15498  .gcmg 15502    GrpHom cghm 15832  CMndccmn 16367  mulGrpcmgp 16682   Ringcrg 16737   LModclmod 17040  var1cv1 17725  Poly1cpl1 17726  coe1cco1 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
  Copyright terms: Public domain W3C validator