MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pmatcollpw3fi1lem1 Structured version   Unicode version

Theorem pmatcollpw3fi1lem1 19157
Description: Lemma 1 for pmatcollpw3fi1 19159. (Contributed by AV, 6-Nov-2019.) (Revised by AV, 4-Dec-2019.)
Hypotheses
Ref Expression
pmatcollpw.p  |-  P  =  (Poly1 `  R )
pmatcollpw.c  |-  C  =  ( N Mat  P )
pmatcollpw.b  |-  B  =  ( Base `  C
)
pmatcollpw.m  |-  .*  =  ( .s `  C )
pmatcollpw.e  |-  .^  =  (.g
`  (mulGrp `  P )
)
pmatcollpw.x  |-  X  =  (var1 `  R )
pmatcollpw.t  |-  T  =  ( N matToPolyMat  R )
pmatcollpw3.a  |-  A  =  ( N Mat  R )
pmatcollpw3.d  |-  D  =  ( Base `  A
)
pmatcollpw3fi1lem1.0  |-  .0.  =  ( 0g `  A )
pmatcollpw3fi1lem1.h  |-  H  =  ( l  e.  ( 0 ... 1 ) 
|->  if ( l  =  0 ,  ( G `
 0 ) ,  .0.  ) )
Assertion
Ref Expression
pmatcollpw3fi1lem1  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } )  /\  M  =  ( C  gsumg  ( n  e.  {
0 }  |->  ( ( n  .^  X )  .*  ( T `  ( G `  n )
) ) ) ) )  ->  M  =  ( C  gsumg  ( n  e.  ( 0 ... 1 ) 
|->  ( ( n  .^  X )  .*  ( T `  ( H `  n ) ) ) ) ) )
Distinct variable groups:    B, n    n, M    n, N    P, n    R, n    n, X    .^ , n    C, n    B, l    M, l    N, l    R, l    D, l, n    A, l    G, l, n
Allowed substitution hints:    A( n)    C( l)    P( l)    T( n, l)    .^ ( l)    H( n, l)    .* ( n, l)    X( l)    .0. ( n, l)

Proof of Theorem pmatcollpw3fi1lem1
StepHypRef Expression
1 simpr 461 . . . . 5  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  M  =  ( C  gsumg  ( n  e.  {
0 }  |->  ( ( n  .^  X )  .*  ( T `  ( G `  n )
) ) ) ) )  ->  M  =  ( C  gsumg  ( n  e.  {
0 }  |->  ( ( n  .^  X )  .*  ( T `  ( G `  n )
) ) ) ) )
2 pmatcollpw.p . . . . . . . . . . 11  |-  P  =  (Poly1 `  R )
3 pmatcollpw.c . . . . . . . . . . 11  |-  C  =  ( N Mat  P )
42, 3pmatring 19064 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  C  e.  Ring )
5 ringmnd 17078 . . . . . . . . . 10  |-  ( C  e.  Ring  ->  C  e. 
Mnd )
64, 5syl 16 . . . . . . . . 9  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  C  e.  Mnd )
76adantr 465 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  C  e.  Mnd )
8 pmatcollpw.b . . . . . . . . 9  |-  B  =  ( Base `  C
)
9 ringcmn 17100 . . . . . . . . . . 11  |-  ( C  e.  Ring  ->  C  e. CMnd
)
104, 9syl 16 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  C  e. CMnd )
1110adantr 465 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  C  e. CMnd )
12 snfi 7595 . . . . . . . . . 10  |-  { 0 }  e.  Fin
1312a1i 11 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  { 0 }  e.  Fin )
14 simplll 757 . . . . . . . . . . 11  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  ->  N  e.  Fin )
15 simpllr 758 . . . . . . . . . . 11  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  ->  R  e.  Ring )
16 elmapi 7439 . . . . . . . . . . . . 13  |-  ( G  e.  ( D  ^m  { 0 } )  ->  G : { 0 } --> D )
1716adantl 466 . . . . . . . . . . . 12  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  G : { 0 } --> D )
1817ffvelrnda 6013 . . . . . . . . . . 11  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  -> 
( G `  n
)  e.  D )
19 elsni 4036 . . . . . . . . . . . . 13  |-  ( n  e.  { 0 }  ->  n  =  0 )
20 0nn0 10813 . . . . . . . . . . . . 13  |-  0  e.  NN0
2119, 20syl6eqel 2537 . . . . . . . . . . . 12  |-  ( n  e.  { 0 }  ->  n  e.  NN0 )
2221adantl 466 . . . . . . . . . . 11  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  ->  n  e.  NN0 )
23 pmatcollpw3.a . . . . . . . . . . . 12  |-  A  =  ( N Mat  R )
24 pmatcollpw3.d . . . . . . . . . . . 12  |-  D  =  ( Base `  A
)
25 pmatcollpw.t . . . . . . . . . . . 12  |-  T  =  ( N matToPolyMat  R )
26 pmatcollpw.m . . . . . . . . . . . 12  |-  .*  =  ( .s `  C )
27 pmatcollpw.e . . . . . . . . . . . 12  |-  .^  =  (.g
`  (mulGrp `  P )
)
28 pmatcollpw.x . . . . . . . . . . . 12  |-  X  =  (var1 `  R )
2923, 24, 25, 2, 3, 8, 26, 27, 28mat2pmatscmxcl 19111 . . . . . . . . . . 11  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( ( G `  n )  e.  D  /\  n  e.  NN0 ) )  ->  (
( n  .^  X
)  .*  ( T `
 ( G `  n ) ) )  e.  B )
3014, 15, 18, 22, 29syl22anc 1228 . . . . . . . . . 10  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  -> 
( ( n  .^  X )  .*  ( T `  ( G `  n ) ) )  e.  B )
3130ralrimiva 2855 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  A. n  e.  { 0 }  (
( n  .^  X
)  .*  ( T `
 ( G `  n ) ) )  e.  B )
328, 11, 13, 31gsummptcl 16865 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  ( C  gsumg  ( n  e.  {
0 }  |->  ( ( n  .^  X )  .*  ( T `  ( G `  n )
) ) ) )  e.  B )
33 eqid 2441 . . . . . . . . 9  |-  ( +g  `  C )  =  ( +g  `  C )
34 eqid 2441 . . . . . . . . 9  |-  ( 0g
`  C )  =  ( 0g `  C
)
358, 33, 34mndrid 15813 . . . . . . . 8  |-  ( ( C  e.  Mnd  /\  ( C  gsumg  ( n  e.  {
0 }  |->  ( ( n  .^  X )  .*  ( T `  ( G `  n )
) ) ) )  e.  B )  -> 
( ( C  gsumg  ( n  e.  { 0 } 
|->  ( ( n  .^  X )  .*  ( T `  ( G `  n ) ) ) ) ) ( +g  `  C ) ( 0g
`  C ) )  =  ( C  gsumg  ( n  e.  { 0 } 
|->  ( ( n  .^  X )  .*  ( T `  ( G `  n ) ) ) ) ) )
367, 32, 35syl2anc 661 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  (
( C  gsumg  ( n  e.  {
0 }  |->  ( ( n  .^  X )  .*  ( T `  ( G `  n )
) ) ) ) ( +g  `  C
) ( 0g `  C ) )  =  ( C  gsumg  ( n  e.  {
0 }  |->  ( ( n  .^  X )  .*  ( T `  ( G `  n )
) ) ) ) )
37 0z 10878 . . . . . . . . . . . . 13  |-  0  e.  ZZ
38 fzsn 11731 . . . . . . . . . . . . 13  |-  ( 0  e.  ZZ  ->  (
0 ... 0 )  =  { 0 } )
3937, 38ax-mp 5 . . . . . . . . . . . 12  |-  ( 0 ... 0 )  =  { 0 }
4039eqcomi 2454 . . . . . . . . . . 11  |-  { 0 }  =  ( 0 ... 0 )
4140a1i 11 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  { 0 }  =  ( 0 ... 0 ) )
42 pmatcollpw3fi1lem1.h . . . . . . . . . . . . . . 15  |-  H  =  ( l  e.  ( 0 ... 1 ) 
|->  if ( l  =  0 ,  ( G `
 0 ) ,  .0.  ) )
4342a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  ->  H  =  ( l  e.  ( 0 ... 1
)  |->  if ( l  =  0 ,  ( G `  0 ) ,  .0.  ) ) )
44 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  /\  l  =  n )  ->  l  =  n )
4519ad2antlr 726 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  /\  l  =  n )  ->  n  =  0 )
4644, 45eqtrd 2482 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  /\  l  =  n )  ->  l  =  0 )
4746iftrued 3931 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  /\  l  =  n )  ->  if ( l  =  0 ,  ( G `
 0 ) ,  .0.  )  =  ( G `  0 ) )
48 fveq2 5853 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  0  ->  ( G `  n )  =  ( G ` 
0 ) )
4948eqcomd 2449 . . . . . . . . . . . . . . . . 17  |-  ( n  =  0  ->  ( G `  0 )  =  ( G `  n ) )
5019, 49syl 16 . . . . . . . . . . . . . . . 16  |-  ( n  e.  { 0 }  ->  ( G ` 
0 )  =  ( G `  n ) )
5150ad2antlr 726 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  /\  l  =  n )  ->  ( G `  0
)  =  ( G `
 n ) )
5247, 51eqtrd 2482 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  /\  l  =  n )  ->  if ( l  =  0 ,  ( G `
 0 ) ,  .0.  )  =  ( G `  n ) )
53 1nn0 10814 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  NN0
5453a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  0  ->  1  e.  NN0 )
55 nn0uz 11121 . . . . . . . . . . . . . . . . . . 19  |-  NN0  =  ( ZZ>= `  0 )
5654, 55syl6eleq 2539 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  0  ->  1  e.  ( ZZ>= `  0 )
)
57 eluzfz1 11699 . . . . . . . . . . . . . . . . . 18  |-  ( 1  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... 1
) )
5856, 57syl 16 . . . . . . . . . . . . . . . . 17  |-  ( n  =  0  ->  0  e.  ( 0 ... 1
) )
59 eleq1 2513 . . . . . . . . . . . . . . . . 17  |-  ( n  =  0  ->  (
n  e.  ( 0 ... 1 )  <->  0  e.  ( 0 ... 1
) ) )
6058, 59mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( n  =  0  ->  n  e.  ( 0 ... 1
) )
6119, 60syl 16 . . . . . . . . . . . . . . 15  |-  ( n  e.  { 0 }  ->  n  e.  ( 0 ... 1 ) )
6261adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  ->  n  e.  ( 0 ... 1 ) )
63 ffvelrn 6011 . . . . . . . . . . . . . . . . . 18  |-  ( ( G : { 0 } --> D  /\  n  e.  { 0 } )  ->  ( G `  n )  e.  D
)
6463ex 434 . . . . . . . . . . . . . . . . 17  |-  ( G : { 0 } --> D  ->  ( n  e.  { 0 }  ->  ( G `  n )  e.  D ) )
6516, 64syl 16 . . . . . . . . . . . . . . . 16  |-  ( G  e.  ( D  ^m  { 0 } )  -> 
( n  e.  {
0 }  ->  ( G `  n )  e.  D ) )
6665adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  (
n  e.  { 0 }  ->  ( G `  n )  e.  D
) )
6766imp 429 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  -> 
( G `  n
)  e.  D )
6843, 52, 62, 67fvmptd 5943 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  -> 
( H `  n
)  =  ( G `
 n ) )
6968eqcomd 2449 . . . . . . . . . . . 12  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  -> 
( G `  n
)  =  ( H `
 n ) )
7069fveq2d 5857 . . . . . . . . . . 11  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  -> 
( T `  ( G `  n )
)  =  ( T `
 ( H `  n ) ) )
7170oveq2d 6294 . . . . . . . . . 10  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  {
0 } )  -> 
( ( n  .^  X )  .*  ( T `  ( G `  n ) ) )  =  ( ( n 
.^  X )  .*  ( T `  ( H `  n )
) ) )
7241, 71mpteq12dva 4511 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  (
n  e.  { 0 }  |->  ( ( n 
.^  X )  .*  ( T `  ( G `  n )
) ) )  =  ( n  e.  ( 0 ... 0 ) 
|->  ( ( n  .^  X )  .*  ( T `  ( H `  n ) ) ) ) )
7372oveq2d 6294 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  ( C  gsumg  ( n  e.  {
0 }  |->  ( ( n  .^  X )  .*  ( T `  ( G `  n )
) ) ) )  =  ( C  gsumg  ( n  e.  ( 0 ... 0 )  |->  ( ( n  .^  X )  .*  ( T `  ( H `  n )
) ) ) ) )
74 ovex 6306 . . . . . . . . . . 11  |-  ( 0  +  1 )  e. 
_V
7574a1i 11 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  (
0  +  1 )  e.  _V )
768, 34mndidcl 15809 . . . . . . . . . . . 12  |-  ( C  e.  Mnd  ->  ( 0g `  C )  e.  B )
776, 76syl 16 . . . . . . . . . . 11  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( 0g `  C
)  e.  B )
7877adantr 465 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  ( 0g `  C )  e.  B )
7942a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  ->  H  =  ( l  e.  ( 0 ... 1 ) 
|->  if ( l  =  0 ,  ( G `
 0 ) ,  .0.  ) ) )
80 0p1e1 10650 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  +  1 )  =  1
8180eqeq2i 2459 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  ( 0  +  1 )  <->  n  = 
1 )
82 ax-1ne0 9561 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  =/=  0
8382neii 2640 . . . . . . . . . . . . . . . . . . . . 21  |-  -.  1  =  0
84 eqeq1 2445 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  1  ->  (
n  =  0  <->  1  =  0 ) )
8583, 84mtbiri 303 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  -.  n  =  0 )
8681, 85sylbi 195 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  ( 0  +  1 )  ->  -.  n  =  0 )
8786ad2antlr 726 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  /\  l  =  n )  ->  -.  n  =  0 )
88 eqeq1 2445 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  n  ->  (
l  =  0  <->  n  =  0 ) )
8988notbid 294 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  n  ->  ( -.  l  =  0  <->  -.  n  =  0 ) )
9089adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  /\  l  =  n )  ->  ( -.  l  =  0  <->  -.  n  =  0 ) )
9187, 90mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  /\  l  =  n )  ->  -.  l  =  0 )
9291iffalsed 3934 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  /\  l  =  n )  ->  if ( l  =  0 ,  ( G ` 
0 ) ,  .0.  )  =  .0.  )
93 pmatcollpw3fi1lem1.0 . . . . . . . . . . . . . . . 16  |-  .0.  =  ( 0g `  A )
9492, 93syl6eq 2498 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  /\  l  =  n )  ->  if ( l  =  0 ,  ( G ` 
0 ) ,  .0.  )  =  ( 0g `  A ) )
9553a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  1  e.  NN0 )
9695, 55syl6eleq 2539 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  1  e.  ( ZZ>= `  0 )
)
97 eluzfz2 11700 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  e.  ( ZZ>= `  0
)  ->  1  e.  ( 0 ... 1
) )
9896, 97syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  1  e.  ( 0 ... 1
) )
99 eleq1 2513 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
n  e.  ( 0 ... 1 )  <->  1  e.  ( 0 ... 1
) ) )
10098, 99mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  n  e.  ( 0 ... 1
) )
10181, 100sylbi 195 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( 0  +  1 )  ->  n  e.  ( 0 ... 1
) )
102101adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  ->  n  e.  ( 0 ... 1
) )
103 fvex 5863 . . . . . . . . . . . . . . . 16  |-  ( 0g
`  A )  e. 
_V
104103a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  ->  ( 0g `  A )  e.  _V )
10579, 94, 102, 104fvmptd 5943 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  ->  ( H `  n )  =  ( 0g `  A ) )
106105fveq2d 5857 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  ->  ( T `  ( H `  n
) )  =  ( T `  ( 0g
`  A ) ) )
10723fveq2i 5856 . . . . . . . . . . . . . . . 16  |-  ( 0g
`  A )  =  ( 0g `  ( N Mat  R ) )
1083fveq2i 5856 . . . . . . . . . . . . . . . 16  |-  ( 0g
`  C )  =  ( 0g `  ( N Mat  P ) )
10925, 2, 107, 1080mat2pmat 19107 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  Ring  /\  N  e.  Fin )  ->  ( T `  ( 0g `  A ) )  =  ( 0g `  C
) )
110109ancoms 453 . . . . . . . . . . . . . 14  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( T `  ( 0g `  A ) )  =  ( 0g `  C ) )
111110ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  ->  ( T `  ( 0g `  A
) )  =  ( 0g `  C ) )
112106, 111eqtrd 2482 . . . . . . . . . . . 12  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  ->  ( T `  ( H `  n
) )  =  ( 0g `  C ) )
113112oveq2d 6294 . . . . . . . . . . 11  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  ->  ( (
n  .^  X )  .*  ( T `  ( H `  n )
) )  =  ( ( n  .^  X
)  .*  ( 0g
`  C ) ) )
1142, 3pmatlmod 19065 . . . . . . . . . . . . 13  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  C  e.  LMod )
115114ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  ->  C  e.  LMod )
116 simpllr 758 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  ->  R  e.  Ring )
117 eleq1 2513 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  (
n  e.  NN0  <->  1  e.  NN0 ) )
11895, 117mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  n  e.  NN0 )
11981, 118sylbi 195 . . . . . . . . . . . . . . 15  |-  ( n  =  ( 0  +  1 )  ->  n  e.  NN0 )
120119adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  ->  n  e.  NN0 )
121 eqid 2441 . . . . . . . . . . . . . . 15  |-  (mulGrp `  P )  =  (mulGrp `  P )
122 eqid 2441 . . . . . . . . . . . . . . 15  |-  ( Base `  P )  =  (
Base `  P )
1232, 28, 121, 27, 122ply1moncl 18183 . . . . . . . . . . . . . 14  |-  ( ( R  e.  Ring  /\  n  e.  NN0 )  ->  (
n  .^  X )  e.  ( Base `  P
) )
124116, 120, 123syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  ->  ( n  .^  X )  e.  (
Base `  P )
)
1252ply1ring 18160 . . . . . . . . . . . . . . . . . 18  |-  ( R  e.  Ring  ->  P  e. 
Ring )
1263matsca2 18792 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  Fin  /\  P  e.  Ring )  ->  P  =  (Scalar `  C
) )
127125, 126sylan2 474 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  P  =  (Scalar `  C
) )
128127eqcomd 2449 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
(Scalar `  C )  =  P )
129128fveq2d 5857 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( Base `  (Scalar `  C
) )  =  (
Base `  P )
)
130129eleq2d 2511 . . . . . . . . . . . . . 14  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( ( n  .^  X )  e.  (
Base `  (Scalar `  C
) )  <->  ( n  .^  X )  e.  (
Base `  P )
) )
131130ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  ->  ( (
n  .^  X )  e.  ( Base `  (Scalar `  C ) )  <->  ( n  .^  X )  e.  (
Base `  P )
) )
132124, 131mpbird 232 . . . . . . . . . . . 12  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  ->  ( n  .^  X )  e.  (
Base `  (Scalar `  C
) ) )
133 eqid 2441 . . . . . . . . . . . . 13  |-  (Scalar `  C )  =  (Scalar `  C )
134 eqid 2441 . . . . . . . . . . . . 13  |-  ( Base `  (Scalar `  C )
)  =  ( Base `  (Scalar `  C )
)
135133, 26, 134, 34lmodvs0 17417 . . . . . . . . . . . 12  |-  ( ( C  e.  LMod  /\  (
n  .^  X )  e.  ( Base `  (Scalar `  C ) ) )  ->  ( ( n 
.^  X )  .*  ( 0g `  C
) )  =  ( 0g `  C ) )
136115, 132, 135syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  ->  ( (
n  .^  X )  .*  ( 0g `  C
) )  =  ( 0g `  C ) )
137113, 136eqtrd 2482 . . . . . . . . . 10  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  =  ( 0  +  1 ) )  ->  ( (
n  .^  X )  .*  ( T `  ( H `  n )
) )  =  ( 0g `  C ) )
1388, 7, 75, 78, 137gsumsnd 16850 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  ( C  gsumg  ( n  e.  {
( 0  +  1 ) }  |->  ( ( n  .^  X )  .*  ( T `  ( H `  n )
) ) ) )  =  ( 0g `  C ) )
139138eqcomd 2449 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  ( 0g `  C )  =  ( C  gsumg  ( n  e.  {
( 0  +  1 ) }  |->  ( ( n  .^  X )  .*  ( T `  ( H `  n )
) ) ) ) )
14073, 139oveq12d 6296 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  (
( C  gsumg  ( n  e.  {
0 }  |->  ( ( n  .^  X )  .*  ( T `  ( G `  n )
) ) ) ) ( +g  `  C
) ( 0g `  C ) )  =  ( ( C  gsumg  ( n  e.  ( 0 ... 0 )  |->  ( ( n  .^  X )  .*  ( T `  ( H `  n )
) ) ) ) ( +g  `  C
) ( C  gsumg  ( n  e.  { ( 0  +  1 ) } 
|->  ( ( n  .^  X )  .*  ( T `  ( H `  n ) ) ) ) ) ) )
14136, 140eqtr3d 2484 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  ( C  gsumg  ( n  e.  {
0 }  |->  ( ( n  .^  X )  .*  ( T `  ( G `  n )
) ) ) )  =  ( ( C 
gsumg  ( n  e.  (
0 ... 0 )  |->  ( ( n  .^  X
)  .*  ( T `
 ( H `  n ) ) ) ) ) ( +g  `  C ) ( C 
gsumg  ( n  e.  { ( 0  +  1 ) }  |->  ( ( n 
.^  X )  .*  ( T `  ( H `  n )
) ) ) ) ) )
142141adantr 465 . . . . 5  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  M  =  ( C  gsumg  ( n  e.  {
0 }  |->  ( ( n  .^  X )  .*  ( T `  ( G `  n )
) ) ) ) )  ->  ( C  gsumg  ( n  e.  { 0 }  |->  ( ( n 
.^  X )  .*  ( T `  ( G `  n )
) ) ) )  =  ( ( C 
gsumg  ( n  e.  (
0 ... 0 )  |->  ( ( n  .^  X
)  .*  ( T `
 ( H `  n ) ) ) ) ) ( +g  `  C ) ( C 
gsumg  ( n  e.  { ( 0  +  1 ) }  |->  ( ( n 
.^  X )  .*  ( T `  ( H `  n )
) ) ) ) ) )
1431, 142eqtrd 2482 . . . 4  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  M  =  ( C  gsumg  ( n  e.  {
0 }  |->  ( ( n  .^  X )  .*  ( T `  ( G `  n )
) ) ) ) )  ->  M  =  ( ( C  gsumg  ( n  e.  ( 0 ... 0 )  |->  ( ( n  .^  X )  .*  ( T `  ( H `  n )
) ) ) ) ( +g  `  C
) ( C  gsumg  ( n  e.  { ( 0  +  1 ) } 
|->  ( ( n  .^  X )  .*  ( T `  ( H `  n ) ) ) ) ) ) )
1441433impa 1190 . . 3  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } )  /\  M  =  ( C  gsumg  ( n  e.  {
0 }  |->  ( ( n  .^  X )  .*  ( T `  ( G `  n )
) ) ) ) )  ->  M  =  ( ( C  gsumg  ( n  e.  ( 0 ... 0 )  |->  ( ( n  .^  X )  .*  ( T `  ( H `  n )
) ) ) ) ( +g  `  C
) ( C  gsumg  ( n  e.  { ( 0  +  1 ) } 
|->  ( ( n  .^  X )  .*  ( T `  ( H `  n ) ) ) ) ) ) )
14520a1i 11 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  0  e.  NN0 )
146 simplll 757 . . . . . 6  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  ( 0 ... ( 0  +  1 ) ) )  ->  N  e.  Fin )
147 simpllr 758 . . . . . 6  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  ( 0 ... ( 0  +  1 ) ) )  ->  R  e.  Ring )
148 id 22 . . . . . . . . . . . . 13  |-  ( G : { 0 } --> D  ->  G : { 0 } --> D )
149 c0ex 9590 . . . . . . . . . . . . . . 15  |-  0  e.  _V
150149snid 4039 . . . . . . . . . . . . . 14  |-  0  e.  { 0 }
151150a1i 11 . . . . . . . . . . . . 13  |-  ( G : { 0 } --> D  ->  0  e.  { 0 } )
152148, 151ffvelrnd 6014 . . . . . . . . . . . 12  |-  ( G : { 0 } --> D  ->  ( G `  0 )  e.  D )
15316, 152syl 16 . . . . . . . . . . 11  |-  ( G  e.  ( D  ^m  { 0 } )  -> 
( G `  0
)  e.  D )
154153ad2antlr 726 . . . . . . . . . 10  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  l  e.  ( 0 ... 1 ) )  ->  ( G `  0 )  e.  D )
15523matring 18815 . . . . . . . . . . . 12  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  A  e.  Ring )
15624, 93ring0cl 17091 . . . . . . . . . . . 12  |-  ( A  e.  Ring  ->  .0.  e.  D )
157155, 156syl 16 . . . . . . . . . . 11  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  .0.  e.  D )
158157ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  l  e.  ( 0 ... 1 ) )  ->  .0.  e.  D )
159154, 158ifcld 3966 . . . . . . . . 9  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  l  e.  ( 0 ... 1 ) )  ->  if (
l  =  0 ,  ( G `  0
) ,  .0.  )  e.  D )
160159, 42fmptd 6037 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  H : ( 0 ... 1 ) --> D )
16180oveq2i 6289 . . . . . . . . 9  |-  ( 0 ... ( 0  +  1 ) )  =  ( 0 ... 1
)
162161feq2i 5711 . . . . . . . 8  |-  ( H : ( 0 ... ( 0  +  1 ) ) --> D  <->  H :
( 0 ... 1
) --> D )
163160, 162sylibr 212 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  H : ( 0 ... ( 0  +  1 ) ) --> D )
164163ffvelrnda 6013 . . . . . 6  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  ( 0 ... ( 0  +  1 ) ) )  ->  ( H `  n )  e.  D
)
165 elfznn0 11776 . . . . . . 7  |-  ( n  e.  ( 0 ... ( 0  +  1 ) )  ->  n  e.  NN0 )
166165adantl 466 . . . . . 6  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  ( 0 ... ( 0  +  1 ) ) )  ->  n  e.  NN0 )
16723, 24, 25, 2, 3, 8, 26, 27, 28mat2pmatscmxcl 19111 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( ( H `  n )  e.  D  /\  n  e.  NN0 ) )  ->  (
( n  .^  X
)  .*  ( T `
 ( H `  n ) ) )  e.  B )
168146, 147, 164, 166, 167syl22anc 1228 . . . . 5  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  {
0 } ) )  /\  n  e.  ( 0 ... ( 0  +  1 ) ) )  ->  ( (
n  .^  X )  .*  ( T `  ( H `  n )
) )  e.  B
)
1698, 33, 11, 145, 168gsummptfzsplit 16823 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } ) )  ->  ( C  gsumg  ( n  e.  ( 0 ... ( 0  +  1 ) ) 
|->  ( ( n  .^  X )  .*  ( T `  ( H `  n ) ) ) ) )  =  ( ( C  gsumg  ( n  e.  ( 0 ... 0 ) 
|->  ( ( n  .^  X )  .*  ( T `  ( H `  n ) ) ) ) ) ( +g  `  C ) ( C 
gsumg  ( n  e.  { ( 0  +  1 ) }  |->  ( ( n 
.^  X )  .*  ( T `  ( H `  n )
) ) ) ) ) )
1701693adant3 1015 . . 3  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } )  /\  M  =  ( C  gsumg  ( n  e.  {
0 }  |->  ( ( n  .^  X )  .*  ( T `  ( G `  n )
) ) ) ) )  ->  ( C  gsumg  ( n  e.  ( 0 ... ( 0  +  1 ) )  |->  ( ( n  .^  X
)  .*  ( T `
 ( H `  n ) ) ) ) )  =  ( ( C  gsumg  ( n  e.  ( 0 ... 0 ) 
|->  ( ( n  .^  X )  .*  ( T `  ( H `  n ) ) ) ) ) ( +g  `  C ) ( C 
gsumg  ( n  e.  { ( 0  +  1 ) }  |->  ( ( n 
.^  X )  .*  ( T `  ( H `  n )
) ) ) ) ) )
171144, 170eqtr4d 2485 . 2  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } )  /\  M  =  ( C  gsumg  ( n  e.  {
0 }  |->  ( ( n  .^  X )  .*  ( T `  ( G `  n )
) ) ) ) )  ->  M  =  ( C  gsumg  ( n  e.  ( 0 ... ( 0  +  1 ) ) 
|->  ( ( n  .^  X )  .*  ( T `  ( H `  n ) ) ) ) ) )
172 mpteq1 4514 . . . 4  |-  ( ( 0 ... ( 0  +  1 ) )  =  ( 0 ... 1 )  ->  (
n  e.  ( 0 ... ( 0  +  1 ) )  |->  ( ( n  .^  X
)  .*  ( T `
 ( H `  n ) ) ) )  =  ( n  e.  ( 0 ... 1 )  |->  ( ( n  .^  X )  .*  ( T `  ( H `  n )
) ) ) )
173161, 172ax-mp 5 . . 3  |-  ( n  e.  ( 0 ... ( 0  +  1 ) )  |->  ( ( n  .^  X )  .*  ( T `  ( H `  n )
) ) )  =  ( n  e.  ( 0 ... 1 ) 
|->  ( ( n  .^  X )  .*  ( T `  ( H `  n ) ) ) )
174173oveq2i 6289 . 2  |-  ( C 
gsumg  ( n  e.  (
0 ... ( 0  +  1 ) )  |->  ( ( n  .^  X
)  .*  ( T `
 ( H `  n ) ) ) ) )  =  ( C  gsumg  ( n  e.  ( 0 ... 1 ) 
|->  ( ( n  .^  X )  .*  ( T `  ( H `  n ) ) ) ) )
175171, 174syl6eq 2498 1  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  G  e.  ( D  ^m  { 0 } )  /\  M  =  ( C  gsumg  ( n  e.  {
0 }  |->  ( ( n  .^  X )  .*  ( T `  ( G `  n )
) ) ) ) )  ->  M  =  ( C  gsumg  ( n  e.  ( 0 ... 1 ) 
|->  ( ( n  .^  X )  .*  ( T `  ( H `  n ) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 972    = wceq 1381    e. wcel 1802   _Vcvv 3093   ifcif 3923   {csn 4011    |-> cmpt 4492   -->wf 5571   ` cfv 5575  (class class class)co 6278    ^m cmap 7419   Fincfn 7515   0cc0 9492   1c1 9493    + caddc 9495   NN0cn0 10798   ZZcz 10867   ZZ>=cuz 11087   ...cfz 11678   Basecbs 14506   +g cplusg 14571  Scalarcsca 14574   .scvsca 14575   0gc0g 14711    gsumg cgsu 14712   Mndcmnd 15790  .gcmg 15927  CMndccmn 16669  mulGrpcmgp 17012   Ringcrg 17069   LModclmod 17383  var1cv1 18086  Poly1cpl1 18087   Mat cmat 18779   matToPolyMat cmat2pmat 19075
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4545  ax-sep 4555  ax-nul 4563  ax-pow 4612  ax-pr 4673  ax-un 6574  ax-inf2 8058  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-fal 1387  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3419  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-pss 3475  df-nul 3769  df-if 3924  df-pw 3996  df-sn 4012  df-pr 4014  df-tp 4016  df-op 4018  df-ot 4020  df-uni 4232  df-int 4269  df-iun 4314  df-iin 4315  df-br 4435  df-opab 4493  df-mpt 4494  df-tr 4528  df-eprel 4778  df-id 4782  df-po 4787  df-so 4788  df-fr 4825  df-se 4826  df-we 4827  df-ord 4868  df-on 4869  df-lim 4870  df-suc 4871  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-rn 4997  df-res 4998  df-ima 4999  df-iota 5538  df-fun 5577  df-fn 5578  df-f 5579  df-f1 5580  df-fo 5581  df-f1o 5582  df-fv 5583  df-isom 5584  df-riota 6239  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-of 6522  df-ofr 6523  df-om 6683  df-1st 6782  df-2nd 6783  df-supp 6901  df-recs 7041  df-rdg 7075  df-1o 7129  df-2o 7130  df-oadd 7133  df-er 7310  df-map 7421  df-pm 7422  df-ixp 7469  df-en 7516  df-dom 7517  df-sdom 7518  df-fin 7519  df-fsupp 7829  df-sup 7900  df-oi 7935  df-card 8320  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9809  df-neg 9810  df-nn 10540  df-2 10597  df-3 10598  df-4 10599  df-5 10600  df-6 10601  df-7 10602  df-8 10603  df-9 10604  df-10 10605  df-n0 10799  df-z 10868  df-dec 10982  df-uz 11088  df-fz 11679  df-fzo 11801  df-seq 12084  df-hash 12382  df-struct 14508  df-ndx 14509  df-slot 14510  df-base 14511  df-sets 14512  df-ress 14513  df-plusg 14584  df-mulr 14585  df-sca 14587  df-vsca 14588  df-ip 14589  df-tset 14590  df-ple 14591  df-ds 14593  df-hom 14595  df-cco 14596  df-0g 14713  df-gsum 14714  df-prds 14719  df-pws 14721  df-mre 14857  df-mrc 14858  df-acs 14860  df-mgm 15743  df-sgrp 15782  df-mnd 15792  df-mhm 15837  df-submnd 15838  df-grp 15928  df-minusg 15929  df-sbg 15930  df-mulg 15931  df-subg 16069  df-ghm 16136  df-cntz 16226  df-cmn 16671  df-abl 16672  df-mgp 17013  df-ur 17025  df-ring 17071  df-subrg 17298  df-lmod 17385  df-lss 17450  df-sra 17689  df-rgmod 17690  df-ascl 17834  df-psr 17876  df-mvr 17877  df-mpl 17878  df-opsr 17880  df-psr1 18090  df-vr1 18091  df-ply1 18092  df-dsmm 18633  df-frlm 18648  df-mamu 18756  df-mat 18780  df-mat2pmat 19078
This theorem is referenced by:  pmatcollpw3fi1lem2  19158
  Copyright terms: Public domain W3C validator