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

Theorem mp2pm2mplem4 31250
Description: Lemma 4 for mp2pm2mp 31252. (Contributed by AV, 12-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 )
) ) ) )
mp2pm2mp.m  |-  .x.  =  ( .s `  P )
mp2pm2mp.e  |-  E  =  (.g `  (mulGrp `  P
) )
mp2pm2mp.y  |-  Y  =  (var1 `  R )
mp2pm2mp.i  |-  I  =  ( p  e.  L  |->  ( i  e.  N ,  j  e.  N  |->  ( P  gsumg  ( k  e.  NN0  |->  ( ( i ( (coe1 `  p ) `  k ) j ) 
.x.  ( k E Y ) ) ) ) ) )
Assertion
Ref Expression
mp2pm2mplem4  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  ->  (
( I `  O
) F K )  =  ( (coe1 `  O
) `  K )
)
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    E, p    L, p    N, p   
i, O, j, k, p    P, p    R, p    Y, p    .x. , p    i, L, j    P, i, j    .x. , k    i, E, j   
i, K, j    i, Y, j    .x. , i, j   
k, E    k, K, m    m, L    k, Y    m, O
Allowed substitution hints:    A( m, p)    B( p)    C( p)    P( m)    Q( i, j, p)    T( i, j, k, m, p)    .x. ( m)    E( m)    .^ ( i, j, p)    F( p)    I( i, j, k, m, p)    .* ( i, j, p)    K( p)    X( i, j, k, p)    Y( m)

Proof of Theorem mp2pm2mplem4
Dummy variables  b 
l  x  s  a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pmattomply1.p . . 3  |-  P  =  (Poly1 `  R )
2 pmattomply1.c . . 3  |-  C  =  ( N Mat  P )
3 pmattomply1.b . . 3  |-  B  =  ( Base `  C
)
4 pmattomply1.f . . 3  |-  F  =  ( m  e.  B ,  k  e.  NN0  |->  ( i  e.  N ,  j  e.  N  |->  ( (coe1 `  ( i m j ) ) `  k ) ) )
5 pmattomply1.m . . 3  |-  .*  =  ( .s `  Q )
6 pmattomply1.e . . 3  |-  .^  =  (.g
`  (mulGrp `  Q )
)
7 pmattomply1.x . . 3  |-  X  =  (var1 `  A )
8 pmattomply1.a . . 3  |-  A  =  ( N Mat  R )
9 pmattomply1.q . . 3  |-  Q  =  (Poly1 `  A )
10 pmattomply1.l . . 3  |-  L  =  ( Base `  Q
)
11 pmattomply1.t . . 3  |-  T  =  ( m  e.  B  |->  ( Q  gsumg  ( k  e.  NN0  |->  ( ( m F k )  .*  (
k  .^  X )
) ) ) )
12 mp2pm2mp.m . . 3  |-  .x.  =  ( .s `  P )
13 mp2pm2mp.e . . 3  |-  E  =  (.g `  (mulGrp `  P
) )
14 mp2pm2mp.y . . 3  |-  Y  =  (var1 `  R )
15 mp2pm2mp.i . . 3  |-  I  =  ( p  e.  L  |->  ( i  e.  N ,  j  e.  N  |->  ( P  gsumg  ( k  e.  NN0  |->  ( ( i ( (coe1 `  p ) `  k ) j ) 
.x.  ( k E Y ) ) ) ) ) )
161, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15mp2pm2mplem3 31249 . 2  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  ->  (
( I `  O
) F K )  =  ( i  e.  N ,  j  e.  N  |->  ( (coe1 `  ( P  gsumg  ( k  e.  NN0  |->  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) ) ) ) ) `  K
) ) )
17 eqid 2450 . . . . . . . . 9  |-  ( Base `  P )  =  (
Base `  P )
18 eqid 2450 . . . . . . . . 9  |-  ( 0g
`  P )  =  ( 0g `  P
)
191ply1rng 17796 . . . . . . . . . . . . 13  |-  ( R  e.  Ring  ->  P  e. 
Ring )
20193ad2ant2 1010 . . . . . . . . . . . 12  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  ->  P  e.  Ring )
21 rngcmn 16767 . . . . . . . . . . . 12  |-  ( P  e.  Ring  ->  P  e. CMnd
)
2220, 21syl 16 . . . . . . . . . . 11  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  ->  P  e. CMnd )
2322ad3antrrr 729 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  P  e. CMnd )
24233ad2ant1 1009 . . . . . . . . 9  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  P  e. CMnd )
25 simpl2 992 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  ->  R  e.  Ring )
2625ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  R  e.  Ring )
27263ad2ant1 1009 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  R  e.  Ring )
2827adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  NN0 )  ->  R  e.  Ring )
29 simpr 461 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  NN0 )  ->  k  e.  NN0 )
30 simpl2 992 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  NN0 )  ->  i  e.  N )
31 simpl3 993 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  NN0 )  ->  j  e.  N )
32 simpl3 993 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  ->  O  e.  L )
3332ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  O  e.  L )
34333ad2ant1 1009 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  O  e.  L )
35 eqid 2450 . . . . . . . . . . . . . 14  |-  (coe1 `  O
)  =  (coe1 `  O
)
36 eqid 2450 . . . . . . . . . . . . . 14  |-  ( Base `  A )  =  (
Base `  A )
3735, 10, 9, 36coe1fvalcl 30958 . . . . . . . . . . . . 13  |-  ( ( O  e.  L  /\  k  e.  NN0 )  -> 
( (coe1 `  O ) `  k )  e.  (
Base `  A )
)
3834, 37sylan 471 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  NN0 )  ->  (
(coe1 `  O ) `  k )  e.  (
Base `  A )
)
39 eqid 2450 . . . . . . . . . . . . 13  |-  ( Base `  R )  =  (
Base `  R )
408, 39matecl 18421 . . . . . . . . . . . 12  |-  ( ( i  e.  N  /\  j  e.  N  /\  ( (coe1 `  O ) `  k )  e.  (
Base `  A )
)  ->  ( i
( (coe1 `  O ) `  k ) j )  e.  ( Base `  R
) )
4130, 31, 38, 40syl3anc 1219 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  NN0 )  ->  (
i ( (coe1 `  O
) `  k )
j )  e.  (
Base `  R )
)
42 id 22 . . . . . . . . . . . 12  |-  ( R  e.  Ring  ->  R  e. 
Ring )
431, 17, 14, 13, 42, 39, 12smon1ply1 30969 . . . . . . . . . . 11  |-  ( ( R  e.  Ring  /\  k  e.  NN0  /\  ( i ( (coe1 `  O ) `  k ) j )  e.  ( Base `  R
) )  ->  (
( i ( (coe1 `  O ) `  k
) j )  .x.  ( k E Y ) )  e.  (
Base `  P )
)
4428, 29, 41, 43syl3anc 1219 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  NN0 )  ->  (
( i ( (coe1 `  O ) `  k
) j )  .x.  ( k E Y ) )  e.  (
Base `  P )
)
4544ralrimiva 2881 . . . . . . . . 9  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  A. k  e.  NN0  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) )  e.  ( Base `  P
) )
46 simp1lr 1052 . . . . . . . . 9  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  s  e.  NN0 )
47 oveq 6182 . . . . . . . . . . . . . . . . 17  |-  ( ( (coe1 `  O ) `  x )  =  ( 0g `  A )  ->  ( i ( (coe1 `  O ) `  x ) j )  =  ( i ( 0g `  A ) j ) )
4847oveq1d 6191 . . . . . . . . . . . . . . . 16  |-  ( ( (coe1 `  O ) `  x )  =  ( 0g `  A )  ->  ( ( i ( (coe1 `  O ) `  x ) j ) 
.x.  ( x E Y ) )  =  ( ( i ( 0g `  A ) j )  .x.  (
x E Y ) ) )
49 3simpa 985 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  ->  ( N  e.  Fin  /\  R  e.  Ring ) )
5049ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  ( N  e.  Fin  /\  R  e. 
Ring ) )
51 eqid 2450 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0g
`  R )  =  ( 0g `  R
)
528, 51mat0op 18415 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( 0g `  A
)  =  ( a  e.  N ,  b  e.  N  |->  ( 0g
`  R ) ) )
5350, 52syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  ( 0g `  A )  =  ( a  e.  N , 
b  e.  N  |->  ( 0g `  R ) ) )
54 eqidd 2451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  ( a  =  i  /\  b  =  j ) )  ->  ( 0g `  R )  =  ( 0g `  R ) )
55 simprl 755 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  i  e.  N )
56 simprr 756 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  j  e.  N )
57 fvex 5785 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0g
`  R )  e. 
_V
5857a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  ( 0g `  R )  e.  _V )
5953, 54, 55, 56, 58ovmpt2d 6304 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  ( i
( 0g `  A
) j )  =  ( 0g `  R
) )
6059adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  ->  ( i
( 0g `  A
) j )  =  ( 0g `  R
) )
6160oveq1d 6191 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  ->  ( (
i ( 0g `  A ) j ) 
.x.  ( x E Y ) )  =  ( ( 0g `  R )  .x.  (
x E Y ) ) )
6225ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  ->  R  e.  Ring )
631ply1sca 17801 . . . . . . . . . . . . . . . . . . . . 21  |-  ( R  e.  Ring  ->  R  =  (Scalar `  P )
)
6462, 63syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  ->  R  =  (Scalar `  P ) )
6564fveq2d 5779 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  ->  ( 0g `  R )  =  ( 0g `  (Scalar `  P ) ) )
6665oveq1d 6191 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  ->  ( ( 0g `  R )  .x.  ( x E Y ) )  =  ( ( 0g `  (Scalar `  P ) )  .x.  ( x E Y ) ) )
671ply1lmod 17800 . . . . . . . . . . . . . . . . . . . . 21  |-  ( R  e.  Ring  ->  P  e. 
LMod )
68673ad2ant2 1010 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  ->  P  e.  LMod )
6968ad4antr 731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  ->  P  e.  LMod )
70 eqid 2450 . . . . . . . . . . . . . . . . . . . . . . 23  |-  (mulGrp `  P )  =  (mulGrp `  P )
7170rngmgp 16743 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( P  e.  Ring  ->  (mulGrp `  P )  e.  Mnd )
7220, 71syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  ->  (mulGrp `  P )  e.  Mnd )
7372ad4antr 731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  ->  (mulGrp `  P
)  e.  Mnd )
74 simpr 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  ->  x  e.  NN0 )
7514, 1, 17vr1cl 17764 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( R  e.  Ring  ->  Y  e.  ( Base `  P
) )
76753ad2ant2 1010 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  ->  Y  e.  ( Base `  P
) )
7776ad4antr 731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  ->  Y  e.  ( Base `  P )
)
7870, 17mgpbas 16688 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Base `  P )  =  (
Base `  (mulGrp `  P
) )
7978, 13mulgnn0cl 15731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (mulGrp `  P )  e.  Mnd  /\  x  e. 
NN0  /\  Y  e.  ( Base `  P )
)  ->  ( x E Y )  e.  (
Base `  P )
)
8073, 74, 77, 79syl3anc 1219 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  ->  ( x E Y )  e.  (
Base `  P )
)
81 eqid 2450 . . . . . . . . . . . . . . . . . . . 20  |-  (Scalar `  P )  =  (Scalar `  P )
82 eqid 2450 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0g
`  (Scalar `  P )
)  =  ( 0g
`  (Scalar `  P )
)
8317, 81, 12, 82, 18lmod0vs 17073 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P  e.  LMod  /\  (
x E Y )  e.  ( Base `  P
) )  ->  (
( 0g `  (Scalar `  P ) )  .x.  ( x E Y ) )  =  ( 0g `  P ) )
8469, 80, 83syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  ->  ( ( 0g `  (Scalar `  P
) )  .x.  (
x E Y ) )  =  ( 0g
`  P ) )
8561, 66, 843eqtrd 2494 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  ->  ( (
i ( 0g `  A ) j ) 
.x.  ( x E Y ) )  =  ( 0g `  P
) )
8685adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  /\  s  < 
x )  ->  (
( i ( 0g
`  A ) j )  .x.  ( x E Y ) )  =  ( 0g `  P ) )
8748, 86sylan9eqr 2512 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  s  e. 
NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  /\  s  < 
x )  /\  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) )  ->  ( (
i ( (coe1 `  O
) `  x )
j )  .x.  (
x E Y ) )  =  ( 0g
`  P ) )
8887exp31 604 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  ->  ( s  <  x  ->  ( (
(coe1 `  O ) `  x )  =  ( 0g `  A )  ->  ( ( i ( (coe1 `  O ) `  x ) j ) 
.x.  ( x E Y ) )  =  ( 0g `  P
) ) ) )
8988a2d 26 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  /\  x  e.  NN0 )  ->  ( (
s  <  x  ->  ( (coe1 `  O ) `  x )  =  ( 0g `  A ) )  ->  ( s  <  x  ->  ( (
i ( (coe1 `  O
) `  x )
j )  .x.  (
x E Y ) )  =  ( 0g
`  P ) ) ) )
9089ralimdva 2875 . . . . . . . . . . . 12  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  ( A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) )  ->  A. x  e.  NN0  ( s  < 
x  ->  ( (
i ( (coe1 `  O
) `  x )
j )  .x.  (
x E Y ) )  =  ( 0g
`  P ) ) ) )
9190impancom 440 . . . . . . . . . . 11  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  (
( i  e.  N  /\  j  e.  N
)  ->  A. x  e.  NN0  ( s  < 
x  ->  ( (
i ( (coe1 `  O
) `  x )
j )  .x.  (
x E Y ) )  =  ( 0g
`  P ) ) ) )
92913impib 1186 . . . . . . . . . 10  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  A. x  e.  NN0  ( s  < 
x  ->  ( (
i ( (coe1 `  O
) `  x )
j )  .x.  (
x E Y ) )  =  ( 0g
`  P ) ) )
93 breq2 4380 . . . . . . . . . . . 12  |-  ( k  =  x  ->  (
s  <  k  <->  s  <  x ) )
94 fveq2 5775 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  (
(coe1 `  O ) `  k )  =  ( (coe1 `  O ) `  x ) )
9594oveqd 6193 . . . . . . . . . . . . . 14  |-  ( k  =  x  ->  (
i ( (coe1 `  O
) `  k )
j )  =  ( i ( (coe1 `  O
) `  x )
j ) )
96 oveq1 6183 . . . . . . . . . . . . . 14  |-  ( k  =  x  ->  (
k E Y )  =  ( x E Y ) )
9795, 96oveq12d 6194 . . . . . . . . . . . . 13  |-  ( k  =  x  ->  (
( i ( (coe1 `  O ) `  k
) j )  .x.  ( k E Y ) )  =  ( ( i ( (coe1 `  O ) `  x
) j )  .x.  ( x E Y ) ) )
9897eqeq1d 2452 . . . . . . . . . . . 12  |-  ( k  =  x  ->  (
( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) )  =  ( 0g `  P
)  <->  ( ( i ( (coe1 `  O ) `  x ) j ) 
.x.  ( x E Y ) )  =  ( 0g `  P
) ) )
9993, 98imbi12d 320 . . . . . . . . . . 11  |-  ( k  =  x  ->  (
( s  <  k  ->  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) )  =  ( 0g `  P
) )  <->  ( s  <  x  ->  ( (
i ( (coe1 `  O
) `  x )
j )  .x.  (
x E Y ) )  =  ( 0g
`  P ) ) ) )
10099cbvralv 3029 . . . . . . . . . 10  |-  ( A. k  e.  NN0  ( s  <  k  ->  (
( i ( (coe1 `  O ) `  k
) j )  .x.  ( k E Y ) )  =  ( 0g `  P ) )  <->  A. x  e.  NN0  ( s  <  x  ->  ( ( i ( (coe1 `  O ) `  x ) j ) 
.x.  ( x E Y ) )  =  ( 0g `  P
) ) )
10192, 100sylibr 212 . . . . . . . . 9  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  A. k  e.  NN0  ( s  < 
k  ->  ( (
i ( (coe1 `  O
) `  k )
j )  .x.  (
k E Y ) )  =  ( 0g
`  P ) ) )
10217, 18, 24, 45, 46, 101gsummptnn0fzv 30934 . . . . . . . 8  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  ( P  gsumg  ( k  e.  NN0  |->  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) ) ) )  =  ( P 
gsumg  ( k  e.  ( 0 ... s ) 
|->  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) ) ) ) )
103102fveq2d 5779 . . . . . . 7  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  (coe1 `  ( P  gsumg  ( k  e.  NN0  |->  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) ) ) ) )  =  (coe1 `  ( P  gsumg  ( k  e.  ( 0 ... s ) 
|->  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) ) ) ) ) )
104103fveq1d 5777 . . . . . 6  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  (
(coe1 `  ( P  gsumg  ( k  e.  NN0  |->  ( ( i ( (coe1 `  O
) `  k )
j )  .x.  (
k E Y ) ) ) ) ) `
 K )  =  ( (coe1 `  ( P  gsumg  ( k  e.  ( 0 ... s )  |->  ( ( i ( (coe1 `  O
) `  k )
j )  .x.  (
k E Y ) ) ) ) ) `
 K ) )
105 simpllr 758 . . . . . . . 8  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  K  e.  NN0 )
1061053ad2ant1 1009 . . . . . . 7  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  K  e.  NN0 )
107 elfznn0 11568 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... s )  ->  k  e.  NN0 )
10844expcom 435 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  (
( i ( (coe1 `  O ) `  k
) j )  .x.  ( k E Y ) )  e.  (
Base `  P )
) )
109107, 108syl 16 . . . . . . . . 9  |-  ( k  e.  ( 0 ... s )  ->  (
( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  (
( i ( (coe1 `  O ) `  k
) j )  .x.  ( k E Y ) )  e.  (
Base `  P )
) )
110109com12 31 . . . . . . . 8  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  (
k  e.  ( 0 ... s )  -> 
( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) )  e.  ( Base `  P
) ) )
111110ralrimiv 2880 . . . . . . 7  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  A. k  e.  ( 0 ... s
) ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) )  e.  ( Base `  P
) )
112 fzfid 11882 . . . . . . 7  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  (
0 ... s )  e. 
Fin )
1131, 17, 27, 106, 111, 112coe1fzgsumd 30966 . . . . . 6  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  (
(coe1 `  ( P  gsumg  ( k  e.  ( 0 ... s )  |->  ( ( i ( (coe1 `  O
) `  k )
j )  .x.  (
k E Y ) ) ) ) ) `
 K )  =  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  ( (coe1 `  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) ) ) `
 K ) ) ) )
114104, 113eqtrd 2490 . . . . 5  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  (
(coe1 `  ( P  gsumg  ( k  e.  NN0  |->  ( ( i ( (coe1 `  O
) `  k )
j )  .x.  (
k E Y ) ) ) ) ) `
 K )  =  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  ( (coe1 `  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) ) ) `
 K ) ) ) )
115114mpt2eq3dva 6235 . . . 4  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  (
i  e.  N , 
j  e.  N  |->  ( (coe1 `  ( P  gsumg  ( k  e.  NN0  |->  ( ( i ( (coe1 `  O
) `  k )
j )  .x.  (
k E Y ) ) ) ) ) `
 K ) )  =  ( i  e.  N ,  j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  ( (coe1 `  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) ) ) `
 K ) ) ) ) )
116253ad2ant1 1009 . . . . . . . . . . 11  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  ->  R  e.  Ring )
117116adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  ( 0 ... s
) )  ->  R  e.  Ring )
118 simpl2 992 . . . . . . . . . . 11  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  ( 0 ... s
) )  ->  i  e.  N )
119 simpl3 993 . . . . . . . . . . 11  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  ( 0 ... s
) )  ->  j  e.  N )
120323ad2ant1 1009 . . . . . . . . . . . 12  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  ->  O  e.  L )
121120, 107, 37syl2an 477 . . . . . . . . . . 11  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  ( 0 ... s
) )  ->  (
(coe1 `  O ) `  k )  e.  (
Base `  A )
)
122118, 119, 121, 40syl3anc 1219 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  ( 0 ... s
) )  ->  (
i ( (coe1 `  O
) `  k )
j )  e.  (
Base `  R )
)
123107adantl 466 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  ( 0 ... s
) )  ->  k  e.  NN0 )
12451, 39, 1, 14, 12, 70, 13coe1tm 17820 . . . . . . . . . 10  |-  ( ( R  e.  Ring  /\  (
i ( (coe1 `  O
) `  k )
j )  e.  (
Base `  R )  /\  k  e.  NN0 )  ->  (coe1 `  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) ) )  =  ( l  e. 
NN0  |->  if ( l  =  k ,  ( i ( (coe1 `  O
) `  k )
j ) ,  ( 0g `  R ) ) ) )
125117, 122, 123, 124syl3anc 1219 . . . . . . . . 9  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  ( 0 ... s
) )  ->  (coe1 `  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) ) )  =  ( l  e. 
NN0  |->  if ( l  =  k ,  ( i ( (coe1 `  O
) `  k )
j ) ,  ( 0g `  R ) ) ) )
126 eqeq1 2453 . . . . . . . . . . 11  |-  ( l  =  K  ->  (
l  =  k  <->  K  =  k ) )
127126ifbid 3895 . . . . . . . . . 10  |-  ( l  =  K  ->  if ( l  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) )  =  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) )
128127adantl 466 . . . . . . . . 9  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  ( 0 ... s
) )  /\  l  =  K )  ->  if ( l  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) )  =  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) )
129 simpl1r 1040 . . . . . . . . 9  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  ( 0 ... s
) )  ->  K  e.  NN0 )
130 ovex 6201 . . . . . . . . . . 11  |-  ( i ( (coe1 `  O ) `  k ) j )  e.  _V
131130, 57ifex 3942 . . . . . . . . . 10  |-  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k
) j ) ,  ( 0g `  R
) )  e.  _V
132131a1i 11 . . . . . . . . 9  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  ( 0 ... s
) )  ->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) )  e. 
_V )
133125, 128, 129, 132fvmptd 5864 . . . . . . . 8  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  ( 0 ... s
) )  ->  (
(coe1 `  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) ) ) `
 K )  =  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) )
134133mpteq2dva 4462 . . . . . . 7  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  ->  (
k  e.  ( 0 ... s )  |->  ( (coe1 `  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) ) ) `
 K ) )  =  ( k  e.  ( 0 ... s
)  |->  if ( K  =  k ,  ( i ( (coe1 `  O
) `  k )
j ) ,  ( 0g `  R ) ) ) )
135134oveq2d 6192 . . . . . 6  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  ->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  ( (coe1 `  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) ) ) `
 K ) ) )  =  ( R 
gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) ) )
136135mpt2eq3dva 6235 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  ->  (
i  e.  N , 
j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  ( (coe1 `  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) ) ) `
 K ) ) ) )  =  ( i  e.  N , 
j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) ) ) )
137136ad2antrr 725 . . . 4  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  (
i  e.  N , 
j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  ( (coe1 `  ( ( i ( (coe1 `  O ) `  k ) j ) 
.x.  ( k E Y ) ) ) `
 K ) ) ) )  =  ( i  e.  N , 
j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) ) ) )
138 breq2 4380 . . . . . . . . . . . . . 14  |-  ( x  =  K  ->  (
s  <  x  <->  s  <  K ) )
139 fveq2 5775 . . . . . . . . . . . . . . 15  |-  ( x  =  K  ->  (
(coe1 `  O ) `  x )  =  ( (coe1 `  O ) `  K ) )
140139eqeq1d 2452 . . . . . . . . . . . . . 14  |-  ( x  =  K  ->  (
( (coe1 `  O ) `  x )  =  ( 0g `  A )  <-> 
( (coe1 `  O ) `  K )  =  ( 0g `  A ) ) )
141138, 140imbi12d 320 . . . . . . . . . . . . 13  |-  ( x  =  K  ->  (
( s  <  x  ->  ( (coe1 `  O ) `  x )  =  ( 0g `  A ) )  <->  ( s  < 
K  ->  ( (coe1 `  O ) `  K
)  =  ( 0g
`  A ) ) ) )
142141rspcva 3153 . . . . . . . . . . . 12  |-  ( ( K  e.  NN0  /\  A. x  e.  NN0  (
s  <  x  ->  ( (coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  (
s  <  K  ->  ( (coe1 `  O ) `  K )  =  ( 0g `  A ) ) )
1438, 51mat0op 18415 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( 0g `  A
)  =  ( i  e.  N ,  j  e.  N  |->  ( 0g
`  R ) ) )
144143eqcomd 2457 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( i  e.  N ,  j  e.  N  |->  ( 0g `  R
) )  =  ( 0g `  A ) )
1451443adant3 1008 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  ->  (
i  e.  N , 
j  e.  N  |->  ( 0g `  R ) )  =  ( 0g
`  A ) )
146145ad3antlr 730 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( K  e. 
NN0  /\  ( N  e.  Fin  /\  R  e. 
Ring  /\  O  e.  L
) )  /\  (
s  e.  NN0  /\  s  <  K ) )  /\  ( (coe1 `  O
) `  K )  =  ( 0g `  A ) )  -> 
( i  e.  N ,  j  e.  N  |->  ( 0g `  R
) )  =  ( 0g `  A ) )
147 elfz2nn0 11567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( k  e.  ( 0 ... s )  <->  ( k  e.  NN0  /\  s  e. 
NN0  /\  k  <_  s ) )
148 nn0re 10675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( k  e.  NN0  ->  k  e.  RR )
149148ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  K  e.  NN0 )  ->  k  e.  RR )
150 nn0re 10675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( s  e.  NN0  ->  s  e.  RR )
151150ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  K  e.  NN0 )  ->  s  e.  RR )
152 nn0re 10675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( K  e.  NN0  ->  K  e.  RR )
153152adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  K  e.  NN0 )  ->  K  e.  RR )
154 lelttr 9552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( k  e.  RR  /\  s  e.  RR  /\  K  e.  RR )  ->  (
( k  <_  s  /\  s  <  K )  ->  k  <  K
) )
155149, 151, 153, 154syl3anc 1219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  K  e.  NN0 )  ->  ( ( k  <_  s  /\  s  <  K )  ->  k  <  K ) )
156 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( k  e. 
NN0  /\  s  e.  NN0 )  /\  K  e. 
NN0 )  /\  k  <  K )  ->  k  <  K )
157156olcd 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( k  e. 
NN0  /\  s  e.  NN0 )  /\  K  e. 
NN0 )  /\  k  <  K )  ->  ( K  <  k  \/  k  <  K ) )
158 df-ne 2643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( K  =/=  k  <->  -.  K  =  k )
159148adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( k  e.  NN0  /\  s  e.  NN0 )  -> 
k  e.  RR )
160 lttri2 9544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( K  e.  RR  /\  k  e.  RR )  ->  ( K  =/=  k  <->  ( K  <  k  \/  k  <  K ) ) )
161152, 159, 160syl2anr 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  K  e.  NN0 )  ->  ( K  =/=  k  <->  ( K  < 
k  \/  k  < 
K ) ) )
162161adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( k  e. 
NN0  /\  s  e.  NN0 )  /\  K  e. 
NN0 )  /\  k  <  K )  ->  ( K  =/=  k  <->  ( K  <  k  \/  k  < 
K ) ) )
163158, 162syl5bbr 259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( k  e. 
NN0  /\  s  e.  NN0 )  /\  K  e. 
NN0 )  /\  k  <  K )  ->  ( -.  K  =  k  <->  ( K  <  k  \/  k  <  K ) ) )
164157, 163mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( k  e. 
NN0  /\  s  e.  NN0 )  /\  K  e. 
NN0 )  /\  k  <  K )  ->  -.  K  =  k )
165164ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  K  e.  NN0 )  ->  ( k  < 
K  ->  -.  K  =  k ) )
166155, 165syld 44 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  K  e.  NN0 )  ->  ( ( k  <_  s  /\  s  <  K )  ->  -.  K  =  k )
)
167166exp4b 607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( k  e.  NN0  /\  s  e.  NN0 )  -> 
( K  e.  NN0  ->  ( k  <_  s  ->  ( s  <  K  ->  -.  K  =  k ) ) ) )
168167com24 87 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( k  e.  NN0  /\  s  e.  NN0 )  -> 
( s  <  K  ->  ( k  <_  s  ->  ( K  e.  NN0  ->  -.  K  =  k ) ) ) )
169168expimpd 603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( k  e.  NN0  ->  ( ( s  e.  NN0  /\  s  <  K )  -> 
( k  <_  s  ->  ( K  e.  NN0  ->  -.  K  =  k ) ) ) )
170169com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  e.  NN0  ->  ( k  <_  s  ->  (
( s  e.  NN0  /\  s  <  K )  ->  ( K  e. 
NN0  ->  -.  K  =  k ) ) ) )
171170imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( k  e.  NN0  /\  k  <_  s )  -> 
( ( s  e. 
NN0  /\  s  <  K )  ->  ( K  e.  NN0  ->  -.  K  =  k ) ) )
1721713adant2 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( k  e.  NN0  /\  s  e.  NN0  /\  k  <_  s )  ->  (
( s  e.  NN0  /\  s  <  K )  ->  ( K  e. 
NN0  ->  -.  K  =  k ) ) )
173147, 172sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  e.  ( 0 ... s )  ->  (
( s  e.  NN0  /\  s  <  K )  ->  ( K  e. 
NN0  ->  -.  K  =  k ) ) )
174173com13 80 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( K  e.  NN0  ->  ( ( s  e.  NN0  /\  s  <  K )  -> 
( k  e.  ( 0 ... s )  ->  -.  K  =  k ) ) )
175174adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( K  e.  NN0  /\  ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L ) )  -> 
( ( s  e. 
NN0  /\  s  <  K )  ->  ( k  e.  ( 0 ... s
)  ->  -.  K  =  k ) ) )
176175imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( K  e.  NN0  /\  ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L ) )  /\  ( s  e.  NN0  /\  s  <  K ) )  ->  ( k  e.  ( 0 ... s
)  ->  -.  K  =  k ) )
177176adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( K  e. 
NN0  /\  ( N  e.  Fin  /\  R  e. 
Ring  /\  O  e.  L
) )  /\  (
s  e.  NN0  /\  s  <  K ) )  /\  ( (coe1 `  O
) `  K )  =  ( 0g `  A ) )  -> 
( k  e.  ( 0 ... s )  ->  -.  K  =  k ) )
1781773ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( K  e.  NN0  /\  ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L ) )  /\  ( s  e.  NN0  /\  s  <  K ) )  /\  ( (coe1 `  O ) `  K
)  =  ( 0g
`  A ) )  /\  i  e.  N  /\  j  e.  N
)  ->  ( k  e.  ( 0 ... s
)  ->  -.  K  =  k ) )
179178imp 429 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( K  e.  NN0  /\  ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L ) )  /\  ( s  e.  NN0  /\  s  <  K ) )  /\  ( (coe1 `  O ) `  K
)  =  ( 0g
`  A ) )  /\  i  e.  N  /\  j  e.  N
)  /\  k  e.  ( 0 ... s
) )  ->  -.  K  =  k )
180 iffalse 3883 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  K  =  k  ->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) )  =  ( 0g `  R
) )
181179, 180syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( K  e.  NN0  /\  ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L ) )  /\  ( s  e.  NN0  /\  s  <  K ) )  /\  ( (coe1 `  O ) `  K
)  =  ( 0g
`  A ) )  /\  i  e.  N  /\  j  e.  N
)  /\  k  e.  ( 0 ... s
) )  ->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) )  =  ( 0g `  R
) )
182181mpteq2dva 4462 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( K  e.  NN0  /\  ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L ) )  /\  ( s  e.  NN0  /\  s  <  K ) )  /\  ( (coe1 `  O ) `  K
)  =  ( 0g
`  A ) )  /\  i  e.  N  /\  j  e.  N
)  ->  ( k  e.  ( 0 ... s
)  |->  if ( K  =  k ,  ( i ( (coe1 `  O
) `  k )
j ) ,  ( 0g `  R ) ) )  =  ( k  e.  ( 0 ... s )  |->  ( 0g `  R ) ) )
183182oveq2d 6192 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( K  e.  NN0  /\  ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L ) )  /\  ( s  e.  NN0  /\  s  <  K ) )  /\  ( (coe1 `  O ) `  K
)  =  ( 0g
`  A ) )  /\  i  e.  N  /\  j  e.  N
)  ->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) )  =  ( R 
gsumg  ( k  e.  ( 0 ... s ) 
|->  ( 0g `  R
) ) ) )
184 rngmnd 16746 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( R  e.  Ring  ->  R  e. 
Mnd )
1851843ad2ant2 1010 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  ->  R  e.  Mnd )
186 ovex 6201 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0 ... s )  e. 
_V
18751gsumz 15599 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  Mnd  /\  ( 0 ... s
)  e.  _V )  ->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  ( 0g `  R
) ) )  =  ( 0g `  R
) )
188185, 186, 187sylancl 662 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  ->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  ( 0g `  R
) ) )  =  ( 0g `  R
) )
189188ad3antlr 730 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( K  e. 
NN0  /\  ( N  e.  Fin  /\  R  e. 
Ring  /\  O  e.  L
) )  /\  (
s  e.  NN0  /\  s  <  K ) )  /\  ( (coe1 `  O
) `  K )  =  ( 0g `  A ) )  -> 
( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  ( 0g `  R
) ) )  =  ( 0g `  R
) )
1901893ad2ant1 1009 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( K  e.  NN0  /\  ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L ) )  /\  ( s  e.  NN0  /\  s  <  K ) )  /\  ( (coe1 `  O ) `  K
)  =  ( 0g
`  A ) )  /\  i  e.  N  /\  j  e.  N
)  ->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  ( 0g `  R ) ) )  =  ( 0g `  R ) )
191183, 190eqtrd 2490 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( K  e.  NN0  /\  ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L ) )  /\  ( s  e.  NN0  /\  s  <  K ) )  /\  ( (coe1 `  O ) `  K
)  =  ( 0g
`  A ) )  /\  i  e.  N  /\  j  e.  N
)  ->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) )  =  ( 0g
`  R ) )
192191mpt2eq3dva 6235 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( K  e. 
NN0  /\  ( N  e.  Fin  /\  R  e. 
Ring  /\  O  e.  L
) )  /\  (
s  e.  NN0  /\  s  <  K ) )  /\  ( (coe1 `  O
) `  K )  =  ( 0g `  A ) )  -> 
( i  e.  N ,  j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) ) )  =  ( i  e.  N , 
j  e.  N  |->  ( 0g `  R ) ) )
193 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( K  e. 
NN0  /\  ( N  e.  Fin  /\  R  e. 
Ring  /\  O  e.  L
) )  /\  (
s  e.  NN0  /\  s  <  K ) )  /\  ( (coe1 `  O
) `  K )  =  ( 0g `  A ) )  -> 
( (coe1 `  O ) `  K )  =  ( 0g `  A ) )
194146, 192, 1933eqtr4d 2500 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( K  e. 
NN0  /\  ( N  e.  Fin  /\  R  e. 
Ring  /\  O  e.  L
) )  /\  (
s  e.  NN0  /\  s  <  K ) )  /\  ( (coe1 `  O
) `  K )  =  ( 0g `  A ) )  -> 
( i  e.  N ,  j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) ) )  =  ( (coe1 `  O ) `  K ) )
195194ex 434 . . . . . . . . . . . . . . . 16  |-  ( ( ( K  e.  NN0  /\  ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L ) )  /\  ( s  e.  NN0  /\  s  <  K ) )  ->  ( (
(coe1 `  O ) `  K )  =  ( 0g `  A )  ->  ( i  e.  N ,  j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k
) j ) ,  ( 0g `  R
) ) ) ) )  =  ( (coe1 `  O ) `  K
) ) )
196195expr 615 . . . . . . . . . . . . . . 15  |-  ( ( ( K  e.  NN0  /\  ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L ) )  /\  s  e.  NN0 )  -> 
( s  <  K  ->  ( ( (coe1 `  O
) `  K )  =  ( 0g `  A )  ->  (
i  e.  N , 
j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) ) )  =  ( (coe1 `  O ) `  K ) ) ) )
197196a2d 26 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  NN0  /\  ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L ) )  /\  s  e.  NN0 )  -> 
( ( s  < 
K  ->  ( (coe1 `  O ) `  K
)  =  ( 0g
`  A ) )  ->  ( s  < 
K  ->  ( i  e.  N ,  j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k
) j ) ,  ( 0g `  R
) ) ) ) )  =  ( (coe1 `  O ) `  K
) ) ) )
198197exp31 604 . . . . . . . . . . . . 13  |-  ( K  e.  NN0  ->  ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  ->  (
s  e.  NN0  ->  ( ( s  <  K  ->  ( (coe1 `  O ) `  K )  =  ( 0g `  A ) )  ->  ( s  <  K  ->  ( i  e.  N ,  j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k
) j ) ,  ( 0g `  R
) ) ) ) )  =  ( (coe1 `  O ) `  K
) ) ) ) ) )
199198com14 88 . . . . . . . . . . . 12  |-  ( ( s  <  K  -> 
( (coe1 `  O ) `  K )  =  ( 0g `  A ) )  ->  ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  ->  (
s  e.  NN0  ->  ( K  e.  NN0  ->  ( s  <  K  -> 
( i  e.  N ,  j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) ) )  =  ( (coe1 `  O ) `  K ) ) ) ) ) )
200142, 199syl 16 . . . . . . . . . . 11  |-  ( ( K  e.  NN0  /\  A. x  e.  NN0  (
s  <  x  ->  ( (coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  (
( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  ->  (
s  e.  NN0  ->  ( K  e.  NN0  ->  ( s  <  K  -> 
( i  e.  N ,  j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) ) )  =  ( (coe1 `  O ) `  K ) ) ) ) ) )
201200ex 434 . . . . . . . . . 10  |-  ( K  e.  NN0  ->  ( A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) )  ->  ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  ->  (
s  e.  NN0  ->  ( K  e.  NN0  ->  ( s  <  K  -> 
( i  e.  N ,  j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) ) )  =  ( (coe1 `  O ) `  K ) ) ) ) ) ) )
202201com25 91 . . . . . . . . 9  |-  ( K  e.  NN0  ->  ( K  e.  NN0  ->  ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  ->  (
s  e.  NN0  ->  ( A. x  e.  NN0  ( s  <  x  ->  ( (coe1 `  O ) `  x )  =  ( 0g `  A ) )  ->  ( s  <  K  ->  ( i  e.  N ,  j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k
) j ) ,  ( 0g `  R
) ) ) ) )  =  ( (coe1 `  O ) `  K
) ) ) ) ) ) )
203202pm2.43i 47 . . . . . . . 8  |-  ( K  e.  NN0  ->  ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  ->  (
s  e.  NN0  ->  ( A. x  e.  NN0  ( s  <  x  ->  ( (coe1 `  O ) `  x )  =  ( 0g `  A ) )  ->  ( s  <  K  ->  ( i  e.  N ,  j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k
) j ) ,  ( 0g `  R
) ) ) ) )  =  ( (coe1 `  O ) `  K
) ) ) ) ) )
204203impcom 430 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  ->  (
s  e.  NN0  ->  ( A. x  e.  NN0  ( s  <  x  ->  ( (coe1 `  O ) `  x )  =  ( 0g `  A ) )  ->  ( s  <  K  ->  ( i  e.  N ,  j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k
) j ) ,  ( 0g `  R
) ) ) ) )  =  ( (coe1 `  O ) `  K
) ) ) ) )
205204imp31 432 . . . . . 6  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  (
s  <  K  ->  ( i  e.  N , 
j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) ) )  =  ( (coe1 `  O ) `  K ) ) )
206205com12 31 . . . . 5  |-  ( s  <  K  ->  (
( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  (
i  e.  N , 
j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) ) )  =  ( (coe1 `  O ) `  K ) ) )
207185ad3antrrr 729 . . . . . . . . . . 11  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  R  e.  Mnd )
208207adantl 466 . . . . . . . . . 10  |-  ( ( -.  s  <  K  /\  ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  ->  R  e.  Mnd )
2092083ad2ant1 1009 . . . . . . . . 9  |-  ( ( ( -.  s  < 
K  /\  ( (
( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  s  e. 
NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  R  e.  Mnd )
210186a1i 11 . . . . . . . . 9  |-  ( ( ( -.  s  < 
K  /\  ( (
( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  s  e. 
NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  ( 0 ... s
)  e.  _V )
211 lenlt 9540 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  RR  /\  s  e.  RR )  ->  ( K  <_  s  <->  -.  s  <  K ) )
212152, 150, 211syl2an 477 . . . . . . . . . . . . . 14  |-  ( ( K  e.  NN0  /\  s  e.  NN0 )  -> 
( K  <_  s  <->  -.  s  <  K ) )
213 simpll 753 . . . . . . . . . . . . . . . 16  |-  ( ( ( K  e.  NN0  /\  s  e.  NN0 )  /\  K  <_  s )  ->  K  e.  NN0 )
214 simplr 754 . . . . . . . . . . . . . . . 16  |-  ( ( ( K  e.  NN0  /\  s  e.  NN0 )  /\  K  <_  s )  ->  s  e.  NN0 )
215 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( K  e.  NN0  /\  s  e.  NN0 )  /\  K  <_  s )  ->  K  <_  s
)
216 elfz2nn0 11567 . . . . . . . . . . . . . . . 16  |-  ( K  e.  ( 0 ... s )  <->  ( K  e.  NN0  /\  s  e. 
NN0  /\  K  <_  s ) )
217213, 214, 215, 216syl3anbrc 1172 . . . . . . . . . . . . . . 15  |-  ( ( ( K  e.  NN0  /\  s  e.  NN0 )  /\  K  <_  s )  ->  K  e.  ( 0 ... s ) )
218217ex 434 . . . . . . . . . . . . . 14  |-  ( ( K  e.  NN0  /\  s  e.  NN0 )  -> 
( K  <_  s  ->  K  e.  ( 0 ... s ) ) )
219212, 218sylbird 235 . . . . . . . . . . . . 13  |-  ( ( K  e.  NN0  /\  s  e.  NN0 )  -> 
( -.  s  < 
K  ->  K  e.  ( 0 ... s
) ) )
220219adantll 713 . . . . . . . . . . . 12  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  s  e. 
NN0 )  ->  ( -.  s  <  K  ->  K  e.  ( 0 ... s ) ) )
221220adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  ( -.  s  <  K  ->  K  e.  ( 0 ... s ) ) )
222221impcom 430 . . . . . . . . . 10  |-  ( ( -.  s  <  K  /\  ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  ->  K  e.  ( 0 ... s ) )
2232223ad2ant1 1009 . . . . . . . . 9  |-  ( ( ( -.  s  < 
K  /\  ( (
( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  s  e. 
NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  K  e.  ( 0 ... s ) )
224 eqcom 2458 . . . . . . . . . . 11  |-  ( K  =  k  <->  k  =  K )
225 ifbi 3894 . . . . . . . . . . 11  |-  ( ( K  =  k  <->  k  =  K )  ->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) )  =  if ( k  =  K ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) )
226224, 225ax-mp 5 . . . . . . . . . 10  |-  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k
) j ) ,  ( 0g `  R
) )  =  if ( k  =  K ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) )
227226mpteq2i 4459 . . . . . . . . 9  |-  ( k  e.  ( 0 ... s )  |->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k
) j ) ,  ( 0g `  R
) ) )  =  ( k  e.  ( 0 ... s ) 
|->  if ( k  =  K ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) )
228 simpl2 992 . . . . . . . . . . . 12  |-  ( ( ( ( -.  s  <  K  /\  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  s  e. 
NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  NN0 )  ->  i  e.  N
)
229 simpl3 993 . . . . . . . . . . . 12  |-  ( ( ( ( -.  s  <  K  /\  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  s  e. 
NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  NN0 )  ->  j  e.  N
)
23033adantl 466 . . . . . . . . . . . . . 14  |-  ( ( -.  s  <  K  /\  ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  ->  O  e.  L )
2312303ad2ant1 1009 . . . . . . . . . . . . 13  |-  ( ( ( -.  s  < 
K  /\  ( (
( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  s  e. 
NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  O  e.  L )
232231, 37sylan 471 . . . . . . . . . . . 12  |-  ( ( ( ( -.  s  <  K  /\  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  s  e. 
NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  NN0 )  ->  ( (coe1 `  O
) `  k )  e.  ( Base `  A
) )
233228, 229, 232, 40syl3anc 1219 . . . . . . . . . . 11  |-  ( ( ( ( -.  s  <  K  /\  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  s  e. 
NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  NN0 )  ->  ( i ( (coe1 `  O ) `  k ) j )  e.  ( Base `  R
) )
234107, 233sylan2 474 . . . . . . . . . 10  |-  ( ( ( ( -.  s  <  K  /\  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  s  e. 
NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  /\  i  e.  N  /\  j  e.  N )  /\  k  e.  (
0 ... s ) )  ->  ( i ( (coe1 `  O ) `  k ) j )  e.  ( Base `  R
) )
235234ralrimiva 2881 . . . . . . . . 9  |-  ( ( ( -.  s  < 
K  /\  ( (
( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  s  e. 
NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  A. k  e.  ( 0 ... s ) ( i ( (coe1 `  O ) `  k
) j )  e.  ( Base `  R
) )
23651, 209, 210, 223, 227, 235gsummpt1n0 16547 . . . . . . . 8  |-  ( ( ( -.  s  < 
K  /\  ( (
( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  s  e. 
NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  /\  i  e.  N  /\  j  e.  N )  ->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) )  =  [_ K  /  k ]_ (
i ( (coe1 `  O
) `  k )
j ) )
237236mpt2eq3dva 6235 . . . . . . 7  |-  ( ( -.  s  <  K  /\  ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  -> 
( i  e.  N ,  j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) ) )  =  ( i  e.  N , 
j  e.  N  |->  [_ K  /  k ]_ (
i ( (coe1 `  O
) `  k )
j ) ) )
238 csbov 6208 . . . . . . . . . . . . . . 15  |-  [_ K  /  k ]_ (
i ( (coe1 `  O
) `  k )
j )  =  ( i [_ K  / 
k ]_ ( (coe1 `  O
) `  k )
j )
239 csbfv 5813 . . . . . . . . . . . . . . . . 17  |-  [_ K  /  k ]_ (
(coe1 `  O ) `  k )  =  ( (coe1 `  O ) `  K )
240239a1i 11 . . . . . . . . . . . . . . . 16  |-  ( K  e.  NN0  ->  [_ K  /  k ]_ (
(coe1 `  O ) `  k )  =  ( (coe1 `  O ) `  K ) )
241240oveqd 6193 . . . . . . . . . . . . . . 15  |-  ( K  e.  NN0  ->  ( i
[_ K  /  k ]_ ( (coe1 `  O ) `  k ) j )  =  ( i ( (coe1 `  O ) `  K ) j ) )
242238, 241syl5eq 2502 . . . . . . . . . . . . . 14  |-  ( K  e.  NN0  ->  [_ K  /  k ]_ (
i ( (coe1 `  O
) `  k )
j )  =  ( i ( (coe1 `  O
) `  K )
j ) )
243242ad2antlr 726 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  ( a  e.  N  /\  b  e.  N ) )  ->  [_ K  /  k ]_ ( i ( (coe1 `  O ) `  k
) j )  =  ( i ( (coe1 `  O ) `  K
) j ) )
244243mpt2eq3dv 6237 . . . . . . . . . . . 12  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  ( a  e.  N  /\  b  e.  N ) )  -> 
( i  e.  N ,  j  e.  N  |-> 
[_ K  /  k ]_ ( i ( (coe1 `  O ) `  k
) j ) )  =  ( i  e.  N ,  j  e.  N  |->  ( i ( (coe1 `  O ) `  K ) j ) ) )
245 oveq12 6185 . . . . . . . . . . . . 13  |-  ( ( i  =  a  /\  j  =  b )  ->  ( i ( (coe1 `  O ) `  K
) j )  =  ( a ( (coe1 `  O ) `  K
) b ) )
246245adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  (
a  e.  N  /\  b  e.  N )
)  /\  ( i  =  a  /\  j  =  b ) )  ->  ( i ( (coe1 `  O ) `  K ) j )  =  ( a ( (coe1 `  O ) `  K ) b ) )
247 simprl 755 . . . . . . . . . . . 12  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  ( a  e.  N  /\  b  e.  N ) )  -> 
a  e.  N )
248 simprr 756 . . . . . . . . . . . 12  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  ( a  e.  N  /\  b  e.  N ) )  -> 
b  e.  N )
249 ovex 6201 . . . . . . . . . . . . 13  |-  ( a ( (coe1 `  O ) `  K ) b )  e.  _V
250249a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  ( a  e.  N  /\  b  e.  N ) )  -> 
( a ( (coe1 `  O ) `  K
) b )  e. 
_V )
251244, 246, 247, 248, 250ovmpt2d 6304 . . . . . . . . . . 11  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  ( a  e.  N  /\  b  e.  N ) )  -> 
( a ( i  e.  N ,  j  e.  N  |->  [_ K  /  k ]_ (
i ( (coe1 `  O
) `  k )
j ) ) b )  =  ( a ( (coe1 `  O ) `  K ) b ) )
252251ralrimivva 2890 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  ->  A. a  e.  N  A. b  e.  N  ( a
( i  e.  N ,  j  e.  N  |-> 
[_ K  /  k ]_ ( i ( (coe1 `  O ) `  k
) j ) ) b )  =  ( a ( (coe1 `  O
) `  K )
b ) )
253 simpl1 991 . . . . . . . . . . . 12  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  ->  N  e.  Fin )
254239oveqi 6189 . . . . . . . . . . . . . 14  |-  ( i
[_ K  /  k ]_ ( (coe1 `  O ) `  k ) j )  =  ( i ( (coe1 `  O ) `  K ) j )
255238, 254eqtri 2478 . . . . . . . . . . . . 13  |-  [_ K  /  k ]_ (
i ( (coe1 `  O
) `  k )
j )  =  ( i ( (coe1 `  O
) `  K )
j )
256 simp2 989 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  ->  i  e.  N )
257 simp3 990 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  ->  j  e.  N )
25835, 10, 9, 36coe1fvalcl 30958 . . . . . . . . . . . . . . . 16  |-  ( ( O  e.  L  /\  K  e.  NN0 )  -> 
( (coe1 `  O ) `  K )  e.  (
Base `  A )
)
2592583ad2antl3 1152 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  ->  (
(coe1 `  O ) `  K )  e.  (
Base `  A )
)
2602593ad2ant1 1009 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  ->  (
(coe1 `  O ) `  K )  e.  (
Base `  A )
)
2618, 39matecl 18421 . . . . . . . . . . . . . 14  |-  ( ( i  e.  N  /\  j  e.  N  /\  ( (coe1 `  O ) `  K )  e.  (
Base `  A )
)  ->  ( i
( (coe1 `  O ) `  K ) j )  e.  ( Base `  R
) )
262256, 257, 260, 261syl3anc 1219 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  ->  (
i ( (coe1 `  O
) `  K )
j )  e.  (
Base `  R )
)
263255, 262syl5eqel 2540 . . . . . . . . . . . 12  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring  /\  O  e.  L
)  /\  K  e.  NN0 )  /\  i  e.  N  /\  j  e.  N )  ->  [_ K  /  k ]_ (
i ( (coe1 `  O
) `  k )
j )  e.  (
Base `  R )
)
2648, 39, 36, 253, 25, 263matbas2d 18419 . . . . . . . . . . 11  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  ->  (
i  e.  N , 
j  e.  N  |->  [_ K  /  k ]_ (
i ( (coe1 `  O
) `  k )
j ) )  e.  ( Base `  A
) )
2658, 36eqmat 30989 . . . . . . . . . . 11  |-  ( ( ( i  e.  N ,  j  e.  N  |-> 
[_ K  /  k ]_ ( i ( (coe1 `  O ) `  k
) j ) )  e.  ( Base `  A
)  /\  ( (coe1 `  O ) `  K
)  e.  ( Base `  A ) )  -> 
( ( i  e.  N ,  j  e.  N  |->  [_ K  /  k ]_ ( i ( (coe1 `  O ) `  k
) j ) )  =  ( (coe1 `  O
) `  K )  <->  A. a  e.  N  A. b  e.  N  (
a ( i  e.  N ,  j  e.  N  |->  [_ K  /  k ]_ ( i ( (coe1 `  O ) `  k
) j ) ) b )  =  ( a ( (coe1 `  O
) `  K )
b ) ) )
266264, 259, 265syl2anc 661 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  ->  (
( i  e.  N ,  j  e.  N  |-> 
[_ K  /  k ]_ ( i ( (coe1 `  O ) `  k
) j ) )  =  ( (coe1 `  O
) `  K )  <->  A. a  e.  N  A. b  e.  N  (
a ( i  e.  N ,  j  e.  N  |->  [_ K  /  k ]_ ( i ( (coe1 `  O ) `  k
) j ) ) b )  =  ( a ( (coe1 `  O
) `  K )
b ) ) )
267252, 266mpbird 232 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  ->  (
i  e.  N , 
j  e.  N  |->  [_ K  /  k ]_ (
i ( (coe1 `  O
) `  k )
j ) )  =  ( (coe1 `  O ) `  K ) )
268267ad2antrr 725 . . . . . . . 8  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  (
i  e.  N , 
j  e.  N  |->  [_ K  /  k ]_ (
i ( (coe1 `  O
) `  k )
j ) )  =  ( (coe1 `  O ) `  K ) )
269268adantl 466 . . . . . . 7  |-  ( ( -.  s  <  K  /\  ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  -> 
( i  e.  N ,  j  e.  N  |-> 
[_ K  /  k ]_ ( i ( (coe1 `  O ) `  k
) j ) )  =  ( (coe1 `  O
) `  K )
)
270237, 269eqtrd 2490 . . . . . 6  |-  ( ( -.  s  <  K  /\  ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )  -> 
( i  e.  N ,  j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) ) )  =  ( (coe1 `  O ) `  K ) )
271270ex 434 . . . . 5  |-  ( -.  s  <  K  -> 
( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  (
i  e.  N , 
j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) ) )  =  ( (coe1 `  O ) `  K ) ) )
272206, 271pm2.61i 164 . . . 4  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  (
i  e.  N , 
j  e.  N  |->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( K  =  k ,  ( i ( (coe1 `  O ) `  k ) j ) ,  ( 0g `  R ) ) ) ) )  =  ( (coe1 `  O ) `  K ) )
273115, 137, 2723eqtrd 2494 . . 3  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  (
(coe1 `  O ) `  x )  =  ( 0g `  A ) ) )  ->  (
i  e.  N , 
j  e.  N  |->  ( (coe1 `  ( P  gsumg  ( k  e.  NN0  |->  ( ( i ( (coe1 `  O
) `  k )
j )  .x.  (
k E Y ) ) ) ) ) `
 K ) )  =  ( (coe1 `  O
) `  K )
)
274 eqid 2450 . . . . . 6  |-  ( 0g
`  A )  =  ( 0g `  A
)
27535, 10, 9, 274coe1sfi 17761 . . . . 5  |-  ( O  e.  L  ->  (coe1 `  O ) finSupp  ( 0g `  A ) )
27632, 275syl 16 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  ->  (coe1 `  O ) finSupp  ( 0g `  A ) )
27735, 10, 9, 36, 274coe1fsupp 30959 . . . . . 6  |-  ( O  e.  L  ->  (coe1 `  O )  e.  {
x  e.  ( (
Base `  A )  ^m  NN0 )  |  x finSupp 
( 0g `  A
) } )
278 elrabi 3197 . . . . . 6  |-  ( (coe1 `  O )  e.  {
x  e.  ( (
Base `  A )  ^m  NN0 )  |  x finSupp 
( 0g `  A
) }  ->  (coe1 `  O )  e.  ( ( Base `  A
)  ^m  NN0 ) )
27932, 277, 2783syl 20 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  ->  (coe1 `  O )  e.  ( ( Base `  A
)  ^m  NN0 ) )
280 fvex 5785 . . . . 5  |-  ( 0g
`  A )  e. 
_V
281 fsuppmapnn0ub 30920 . . . . 5  |-  ( ( (coe1 `  O )  e.  ( ( Base `  A
)  ^m  NN0 )  /\  ( 0g `  A )  e.  _V )  -> 
( (coe1 `  O ) finSupp  ( 0g `  A )  ->  E. s  e.  NN0  A. x  e.  NN0  (
s  <  x  ->  ( (coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )
282279, 280, 281sylancl 662 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  ->  (
(coe1 `  O ) finSupp  ( 0g `  A )  ->  E. s  e.  NN0  A. x  e.  NN0  (
s  <  x  ->  ( (coe1 `  O ) `  x )  =  ( 0g `  A ) ) ) )
283276, 282mpd 15 . . 3  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.  L )  /\  K  e.  NN0 )  ->  E. s  e.  NN0  A. x  e. 
NN0  ( s  < 
x  ->  ( (coe1 `  O ) `  x
)  =  ( 0g
`  A ) ) )
284273, 283r19.29a 2944 . 2  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  O  e.