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

Theorem cpmatmcllem 19677
Description: Lemma for cpmatmcl 19678. (Contributed by AV, 18-Nov-2019.)
Hypotheses
Ref Expression
cpmatsrngpmat.s  |-  S  =  ( N ConstPolyMat  R )
cpmatsrngpmat.p  |-  P  =  (Poly1 `  R )
cpmatsrngpmat.c  |-  C  =  ( N Mat  P )
Assertion
Ref Expression
cpmatmcllem  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( x  e.  S  /\  y  e.  S
) )  ->  A. i  e.  N  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r
`  P ) ( k y j ) ) ) ) ) `
 c )  =  ( 0g `  R
) )
Distinct variable groups:    C, i,
j    i, N, j    R, i, j    C, c    N, c, x, y, i, j    P, c    R, c, x, y    y, S    C, k    k, N, c, i, j, x, y    P, k    R, k
Allowed substitution hints:    C( x, y)    P( x, y, i, j)    S( x, i, j, k, c)

Proof of Theorem cpmatmcllem
Dummy variable  l is distinct from all other variables.
StepHypRef Expression
1 cpmatsrngpmat.s . . . 4  |-  S  =  ( N ConstPolyMat  R )
2 cpmatsrngpmat.p . . . 4  |-  P  =  (Poly1 `  R )
3 cpmatsrngpmat.c . . . 4  |-  C  =  ( N Mat  P )
4 eqid 2422 . . . 4  |-  ( Base `  C )  =  (
Base `  C )
51, 2, 3, 4cpmatelimp 19671 . . 3  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( x  e.  S  ->  ( x  e.  (
Base `  C )  /\  A. i  e.  N  A. l  e.  N  A. c  e.  NN  ( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R ) ) ) )
61, 2, 3, 4cpmatelimp 19671 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( y  e.  S  ->  ( y  e.  (
Base `  C )  /\  A. l  e.  N  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R ) ) ) )
76adantr 466 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  x  e.  ( Base `  C ) )  ->  ( y  e.  S  ->  ( y  e.  ( Base `  C
)  /\  A. l  e.  N  A. j  e.  N  A. c  e.  NN  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) ) )
8 ralcom 2922 . . . . . . . . . . . . . . . 16  |-  ( A. l  e.  N  A. j  e.  N  A. c  e.  NN  (
(coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R )  <->  A. j  e.  N  A. l  e.  N  A. c  e.  NN  ( (coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R ) )
9 r19.26-2 2889 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. l  e.  N  A. c  e.  NN  (
( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) )  <->  ( A. l  e.  N  A. c  e.  NN  (
(coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  A. l  e.  N  A. c  e.  NN  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )
10 ralcom 2922 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. l  e.  N  A. c  e.  NN  (
( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) )  <->  A. c  e.  NN  A. l  e.  N  ( ( (coe1 `  ( i x l ) ) `  c
)  =  ( 0g
`  R )  /\  ( (coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R ) ) )
119, 10bitr3i 254 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A. l  e.  N  A. c  e.  NN  ( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  A. l  e.  N  A. c  e.  NN  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) )  <->  A. c  e.  NN  A. l  e.  N  ( ( (coe1 `  ( i x l ) ) `  c
)  =  ( 0g
`  R )  /\  ( (coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R ) ) )
12 nfv 1755 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/ c ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )
13 nfra1 2740 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/ c A. c  e.  NN  A. l  e.  N  ( ( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) )
1412, 13nfan 1988 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ c ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) ) )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  A. c  e.  NN  A. l  e.  N  (
( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )
15 simp-4r 775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  k  e.  N )  ->  R  e.  Ring )
16 eqid 2422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( Base `  P )  =  (
Base `  P )
17 simplrl 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  k  e.  N )  ->  i  e.  N )
18 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  k  e.  N )  ->  k  e.  N )
19 simplrl 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C
)  /\  y  e.  ( Base `  C )
) )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  x  e.  ( Base `  C )
)
2019adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  k  e.  N )  ->  x  e.  ( Base `  C
) )
213, 16, 4, 17, 18, 20matecld 19386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  k  e.  N )  ->  (
i x k )  e.  ( Base `  P
) )
22 simplrr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  k  e.  N )  ->  j  e.  N )
23 simplrr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C
)  /\  y  e.  ( Base `  C )
) )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  y  e.  ( Base `  C )
)
2423adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  k  e.  N )  ->  y  e.  ( Base `  C
) )
253, 16, 4, 18, 22, 24matecld 19386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  k  e.  N )  ->  (
k y j )  e.  ( Base `  P
) )
2615, 21, 25jca32 537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  k  e.  N )  ->  ( R  e.  Ring  /\  (
( i x k )  e.  ( Base `  P )  /\  (
k y j )  e.  ( Base `  P
) ) ) )
2726adantlr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) ) )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  A. c  e.  NN  A. l  e.  N  (
( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )  /\  k  e.  N
)  ->  ( R  e.  Ring  /\  ( (
i x k )  e.  ( Base `  P
)  /\  ( k
y j )  e.  ( Base `  P
) ) ) )
28 oveq2 6250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( l  =  k  ->  (
i x l )  =  ( i x k ) )
2928fveq2d 5822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( l  =  k  ->  (coe1 `  ( i x l ) )  =  (coe1 `  ( i x k ) ) )
3029fveq1d 5820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( l  =  k  ->  (
(coe1 `  ( i x l ) ) `  c )  =  ( (coe1 `  ( i x k ) ) `  c ) )
3130eqeq1d 2424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( l  =  k  ->  (
( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  <-> 
( (coe1 `  ( i x k ) ) `  c )  =  ( 0g `  R ) ) )
32 oveq1 6249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( l  =  k  ->  (
l y j )  =  ( k y j ) )
3332fveq2d 5822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( l  =  k  ->  (coe1 `  ( l y j ) )  =  (coe1 `  ( k y j ) ) )
3433fveq1d 5820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( l  =  k  ->  (
(coe1 `  ( l y j ) ) `  c )  =  ( (coe1 `  ( k y j ) ) `  c ) )
3534eqeq1d 2424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( l  =  k  ->  (
( (coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R )  <-> 
( (coe1 `  ( k y j ) ) `  c )  =  ( 0g `  R ) ) )
3631, 35anbi12d 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( l  =  k  ->  (
( ( (coe1 `  (
i x l ) ) `  c )  =  ( 0g `  R )  /\  (
(coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R ) )  <->  ( ( (coe1 `  ( i x k ) ) `  c
)  =  ( 0g
`  R )  /\  ( (coe1 `  ( k y j ) ) `  c )  =  ( 0g `  R ) ) ) )
3736rspcva 3116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( k  e.  N  /\  A. l  e.  N  ( ( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )  ->  ( ( (coe1 `  ( i x k ) ) `  c
)  =  ( 0g
`  R )  /\  ( (coe1 `  ( k y j ) ) `  c )  =  ( 0g `  R ) ) )
3837a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  c  e.  NN )  ->  (
( k  e.  N  /\  A. l  e.  N  ( ( (coe1 `  (
i x l ) ) `  c )  =  ( 0g `  R )  /\  (
(coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R ) ) )  ->  (
( (coe1 `  ( i x k ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
k y j ) ) `  c )  =  ( 0g `  R ) ) ) )
3938exp4b 610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C
)  /\  y  e.  ( Base `  C )
) )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  ( c  e.  NN  ->  ( k  e.  N  ->  ( A. l  e.  N  (
( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) )  -> 
( ( (coe1 `  (
i x k ) ) `  c )  =  ( 0g `  R )  /\  (
(coe1 `  ( k y j ) ) `  c )  =  ( 0g `  R ) ) ) ) ) )
4039com23 81 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C
)  /\  y  e.  ( Base `  C )
) )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  ( k  e.  N  ->  ( c  e.  NN  ->  ( A. l  e.  N  ( ( (coe1 `  (
i x l ) ) `  c )  =  ( 0g `  R )  /\  (
(coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R ) )  ->  ( (
(coe1 `  ( i x k ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
k y j ) ) `  c )  =  ( 0g `  R ) ) ) ) ) )
4140imp31 433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) ) )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  k  e.  N )  /\  c  e.  NN )  ->  ( A. l  e.  N  ( (
(coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) )  -> 
( ( (coe1 `  (
i x k ) ) `  c )  =  ( 0g `  R )  /\  (
(coe1 `  ( k y j ) ) `  c )  =  ( 0g `  R ) ) ) )
4241ralimdva 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  k  e.  N )  ->  ( A. c  e.  NN  A. l  e.  N  ( ( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) )  ->  A. c  e.  NN  ( ( (coe1 `  (
i x k ) ) `  c )  =  ( 0g `  R )  /\  (
(coe1 `  ( k y j ) ) `  c )  =  ( 0g `  R ) ) ) )
4342impancom 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  A. c  e.  NN  A. l  e.  N  ( (
(coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )  ->  ( k  e.  N  ->  A. c  e.  NN  ( ( (coe1 `  ( i x k ) ) `  c
)  =  ( 0g
`  R )  /\  ( (coe1 `  ( k y j ) ) `  c )  =  ( 0g `  R ) ) ) )
4443imp 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) ) )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  A. c  e.  NN  A. l  e.  N  (
( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )  /\  k  e.  N
)  ->  A. c  e.  NN  ( ( (coe1 `  ( i x k ) ) `  c
)  =  ( 0g
`  R )  /\  ( (coe1 `  ( k y j ) ) `  c )  =  ( 0g `  R ) ) )
45 eqid 2422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( 0g
`  R )  =  ( 0g `  R
)
46 eqid 2422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( .r
`  P )  =  ( .r `  P
)
472, 16, 45, 46cply1mul 18823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( R  e.  Ring  /\  (
( i x k )  e.  ( Base `  P )  /\  (
k y j )  e.  ( Base `  P
) ) )  -> 
( A. c  e.  NN  ( ( (coe1 `  ( i x k ) ) `  c
)  =  ( 0g
`  R )  /\  ( (coe1 `  ( k y j ) ) `  c )  =  ( 0g `  R ) )  ->  A. c  e.  NN  ( (coe1 `  (
( i x k ) ( .r `  P ) ( k y j ) ) ) `  c )  =  ( 0g `  R ) ) )
4827, 44, 47sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) ) )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  A. c  e.  NN  A. l  e.  N  (
( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )  /\  k  e.  N
)  ->  A. c  e.  NN  ( (coe1 `  (
( i x k ) ( .r `  P ) ( k y j ) ) ) `  c )  =  ( 0g `  R ) )
4948r19.21bi 2728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( x  e.  (
Base `  C )  /\  y  e.  ( Base `  C ) ) )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  A. c  e.  NN  A. l  e.  N  (
( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )  /\  k  e.  N
)  /\  c  e.  NN )  ->  ( (coe1 `  ( ( i x k ) ( .r
`  P ) ( k y j ) ) ) `  c
)  =  ( 0g
`  R ) )
5049an32s 811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( x  e.  (
Base `  C )  /\  y  e.  ( Base `  C ) ) )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  A. c  e.  NN  A. l  e.  N  (
( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )  /\  c  e.  NN )  /\  k  e.  N
)  ->  ( (coe1 `  ( ( i x k ) ( .r
`  P ) ( k y j ) ) ) `  c
)  =  ( 0g
`  R ) )
5150mpteq2dva 4446 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) ) )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  A. c  e.  NN  A. l  e.  N  (
( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )  /\  c  e.  NN )  ->  ( k  e.  N  |->  ( (coe1 `  (
( i x k ) ( .r `  P ) ( k y j ) ) ) `  c ) )  =  ( k  e.  N  |->  ( 0g
`  R ) ) )
5251oveq2d 6258 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) ) )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  A. c  e.  NN  A. l  e.  N  (
( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )  /\  c  e.  NN )  ->  ( R  gsumg  ( k  e.  N  |->  ( (coe1 `  ( ( i x k ) ( .r
`  P ) ( k y j ) ) ) `  c
) ) )  =  ( R  gsumg  ( k  e.  N  |->  ( 0g `  R
) ) ) )
53 ringmnd 17725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( R  e.  Ring  ->  R  e. 
Mnd )
5453anim2i 571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( N  e.  Fin  /\  R  e.  Mnd )
)
5554ancomd 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( R  e.  Mnd  /\  N  e.  Fin )
)
5645gsumz 16557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( R  e.  Mnd  /\  N  e.  Fin )  ->  ( R  gsumg  ( k  e.  N  |->  ( 0g `  R
) ) )  =  ( 0g `  R
) )
5755, 56syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( R  gsumg  ( k  e.  N  |->  ( 0g `  R
) ) )  =  ( 0g `  R
) )
5857ad4antr 736 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) ) )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  A. c  e.  NN  A. l  e.  N  (
( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )  /\  c  e.  NN )  ->  ( R  gsumg  ( k  e.  N  |->  ( 0g
`  R ) ) )  =  ( 0g
`  R ) )
5952, 58eqtrd 2456 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) ) )  /\  ( i  e.  N  /\  j  e.  N ) )  /\  A. c  e.  NN  A. l  e.  N  (
( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )  /\  c  e.  NN )  ->  ( R  gsumg  ( k  e.  N  |->  ( (coe1 `  ( ( i x k ) ( .r
`  P ) ( k y j ) ) ) `  c
) ) )  =  ( 0g `  R
) )
6059ex 435 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  A. c  e.  NN  A. l  e.  N  ( (
(coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )  ->  ( c  e.  NN  ->  ( R  gsumg  ( k  e.  N  |->  ( (coe1 `  ( ( i x k ) ( .r `  P ) ( k y j ) ) ) `  c ) ) )  =  ( 0g `  R ) ) )
6114, 60ralrimi 2759 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  A. c  e.  NN  A. l  e.  N  ( (
(coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )  ->  A. c  e.  NN  ( R  gsumg  ( k  e.  N  |->  ( (coe1 `  ( ( i x k ) ( .r `  P ) ( k y j ) ) ) `  c ) ) )  =  ( 0g `  R ) )
62 simp-4r 775 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  c  e.  NN )  ->  R  e.  Ring )
63 nnnn0 10820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  NN  ->  c  e.  NN0 )
6463adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  c  e.  NN )  ->  c  e.  NN0 )
652ply1ring 18777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( R  e.  Ring  ->  P  e. 
Ring )
6665ad4antlr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  k  e.  N )  ->  P  e.  Ring )
6716, 46ringcl 17730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( P  e.  Ring  /\  (
i x k )  e.  ( Base `  P
)  /\  ( k
y j )  e.  ( Base `  P
) )  ->  (
( i x k ) ( .r `  P ) ( k y j ) )  e.  ( Base `  P
) )
6866, 21, 25, 67syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  k  e.  N )  ->  (
( i x k ) ( .r `  P ) ( k y j ) )  e.  ( Base `  P
) )
6968ralrimiva 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C
)  /\  y  e.  ( Base `  C )
) )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  A. k  e.  N  ( (
i x k ) ( .r `  P
) ( k y j ) )  e.  ( Base `  P
) )
7069adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  c  e.  NN )  ->  A. k  e.  N  ( (
i x k ) ( .r `  P
) ( k y j ) )  e.  ( Base `  P
) )
71 simp-4l 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  c  e.  NN )  ->  N  e.  Fin )
722, 16, 62, 64, 70, 71coe1fzgsumd 18832 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  c  e.  NN )  ->  (
(coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( R 
gsumg  ( k  e.  N  |->  ( (coe1 `  ( ( i x k ) ( .r `  P ) ( k y j ) ) ) `  c ) ) ) )
7372eqeq1d 2424 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  c  e.  NN )  ->  (
( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R )  <->  ( R  gsumg  ( k  e.  N  |->  ( (coe1 `  ( ( i x k ) ( .r `  P ) ( k y j ) ) ) `  c ) ) )  =  ( 0g `  R ) ) )
7473ralbidva 2795 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C
)  /\  y  e.  ( Base `  C )
) )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  ( A. c  e.  NN  (
(coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R )  <->  A. c  e.  NN  ( R  gsumg  ( k  e.  N  |->  ( (coe1 `  ( ( i x k ) ( .r
`  P ) ( k y j ) ) ) `  c
) ) )  =  ( 0g `  R
) ) )
7574adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  A. c  e.  NN  A. l  e.  N  ( (
(coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )  ->  ( A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r
`  P ) ( k y j ) ) ) ) ) `
 c )  =  ( 0g `  R
)  <->  A. c  e.  NN  ( R  gsumg  ( k  e.  N  |->  ( (coe1 `  ( ( i x k ) ( .r `  P ) ( k y j ) ) ) `  c ) ) )  =  ( 0g `  R ) ) )
7661, 75mpbird 235 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  ( i  e.  N  /\  j  e.  N
) )  /\  A. c  e.  NN  A. l  e.  N  ( (
(coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) ) )  ->  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R ) )
7776ex 435 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C
)  /\  y  e.  ( Base `  C )
) )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  ( A. c  e.  NN  A. l  e.  N  ( (
(coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) )  ->  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R ) ) )
7811, 77syl5bi 220 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C
)  /\  y  e.  ( Base `  C )
) )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  ( ( A. l  e.  N  A. c  e.  NN  ( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  /\  A. l  e.  N  A. c  e.  NN  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) )  ->  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R ) ) )
7978expd 437 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C
)  /\  y  e.  ( Base `  C )
) )  /\  (
i  e.  N  /\  j  e.  N )
)  ->  ( A. l  e.  N  A. c  e.  NN  (
(coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  ->  ( A. l  e.  N  A. c  e.  NN  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R )  ->  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r
`  P ) ( k y j ) ) ) ) ) `
 c )  =  ( 0g `  R
) ) ) )
8079expr 618 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C
)  /\  y  e.  ( Base `  C )
) )  /\  i  e.  N )  ->  (
j  e.  N  -> 
( A. l  e.  N  A. c  e.  NN  ( (coe1 `  (
i x l ) ) `  c )  =  ( 0g `  R )  ->  ( A. l  e.  N  A. c  e.  NN  ( (coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R )  ->  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R ) ) ) ) )
8180com23 81 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C
)  /\  y  e.  ( Base `  C )
) )  /\  i  e.  N )  ->  ( A. l  e.  N  A. c  e.  NN  ( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  ->  ( j  e.  N  ->  ( A. l  e.  N  A. c  e.  NN  (
(coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R )  ->  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R ) ) ) ) )
8281imp31 433 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) ) )  /\  i  e.  N
)  /\  A. l  e.  N  A. c  e.  NN  ( (coe1 `  (
i x l ) ) `  c )  =  ( 0g `  R ) )  /\  j  e.  N )  ->  ( A. l  e.  N  A. c  e.  NN  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R )  ->  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r
`  P ) ( k y j ) ) ) ) ) `
 c )  =  ( 0g `  R
) ) )
8382ralimdva 2767 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  i  e.  N )  /\  A. l  e.  N  A. c  e.  NN  ( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R ) )  ->  ( A. j  e.  N  A. l  e.  N  A. c  e.  NN  (
(coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R )  ->  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R ) ) )
848, 83syl5bi 220 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  i  e.  N )  /\  A. l  e.  N  A. c  e.  NN  ( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R ) )  ->  ( A. l  e.  N  A. j  e.  N  A. c  e.  NN  (
(coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R )  ->  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R ) ) )
8584ex 435 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C
)  /\  y  e.  ( Base `  C )
) )  /\  i  e.  N )  ->  ( A. l  e.  N  A. c  e.  NN  ( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  ->  ( A. l  e.  N  A. j  e.  N  A. c  e.  NN  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R )  ->  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r
`  P ) ( k y j ) ) ) ) ) `
 c )  =  ( 0g `  R
) ) ) )
8685com23 81 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C
)  /\  y  e.  ( Base `  C )
) )  /\  i  e.  N )  ->  ( A. l  e.  N  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R )  ->  ( A. l  e.  N  A. c  e.  NN  ( (coe1 `  (
i x l ) ) `  c )  =  ( 0g `  R )  ->  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r
`  P ) ( k y j ) ) ) ) ) `
 c )  =  ( 0g `  R
) ) ) )
8786impancom 441 . . . . . . . . . . . 12  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C
)  /\  y  e.  ( Base `  C )
) )  /\  A. l  e.  N  A. j  e.  N  A. c  e.  NN  (
(coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R ) )  ->  ( i  e.  N  ->  ( A. l  e.  N  A. c  e.  NN  (
(coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  ->  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R ) ) ) )
8887imp 430 . . . . . . . . . . 11  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  (
x  e.  ( Base `  C )  /\  y  e.  ( Base `  C
) ) )  /\  A. l  e.  N  A. j  e.  N  A. c  e.  NN  (
(coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R ) )  /\  i  e.  N )  ->  ( A. l  e.  N  A. c  e.  NN  ( (coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  ->  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R ) ) )
8988ralimdva 2767 . . . . . . . . . 10  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  Ring )  /\  ( x  e.  ( Base `  C
)  /\  y  e.  ( Base `  C )
) )  /\  A. l  e.  N  A. j  e.  N  A. c  e.  NN  (
(coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R ) )  ->  ( A. i  e.  N  A. l  e.  N  A. c  e.  NN  (
(coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  ->  A. i  e.  N  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R ) ) )
9089ex 435 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( x  e.  (
Base `  C )  /\  y  e.  ( Base `  C ) ) )  ->  ( A. l  e.  N  A. j  e.  N  A. c  e.  NN  (
(coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R )  ->  ( A. i  e.  N  A. l  e.  N  A. c  e.  NN  ( (coe1 `  (
i x l ) ) `  c )  =  ( 0g `  R )  ->  A. i  e.  N  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r
`  P ) ( k y j ) ) ) ) ) `
 c )  =  ( 0g `  R
) ) ) )
9190expr 618 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  x  e.  ( Base `  C ) )  ->  ( y  e.  ( Base `  C
)  ->  ( A. l  e.  N  A. j  e.  N  A. c  e.  NN  (
(coe1 `  ( l y j ) ) `  c )  =  ( 0g `  R )  ->  ( A. i  e.  N  A. l  e.  N  A. c  e.  NN  ( (coe1 `  (
i x l ) ) `  c )  =  ( 0g `  R )  ->  A. i  e.  N  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r
`  P ) ( k y j ) ) ) ) ) `
 c )  =  ( 0g `  R
) ) ) ) )
9291impd 432 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  x  e.  ( Base `  C ) )  ->  ( ( y  e.  ( Base `  C
)  /\  A. l  e.  N  A. j  e.  N  A. c  e.  NN  ( (coe1 `  (
l y j ) ) `  c )  =  ( 0g `  R ) )  -> 
( A. i  e.  N  A. l  e.  N  A. c  e.  NN  ( (coe1 `  (
i x l ) ) `  c )  =  ( 0g `  R )  ->  A. i  e.  N  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r
`  P ) ( k y j ) ) ) ) ) `
 c )  =  ( 0g `  R
) ) ) )
937, 92syld 45 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  x  e.  ( Base `  C ) )  ->  ( y  e.  S  ->  ( A. i  e.  N  A. l  e.  N  A. c  e.  NN  (
(coe1 `  ( i x l ) ) `  c )  =  ( 0g `  R )  ->  A. i  e.  N  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R ) ) ) )
9493com23 81 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  x  e.  ( Base `  C ) )  ->  ( A. i  e.  N  A. l  e.  N  A. c  e.  NN  ( (coe1 `  (
i x l ) ) `  c )  =  ( 0g `  R )  ->  (
y  e.  S  ->  A. i  e.  N  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R ) ) ) )
9594ex 435 . . . 4  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( x  e.  (
Base `  C )  ->  ( A. i  e.  N  A. l  e.  N  A. c  e.  NN  ( (coe1 `  (
i x l ) ) `  c )  =  ( 0g `  R )  ->  (
y  e.  S  ->  A. i  e.  N  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R ) ) ) ) )
9695impd 432 . . 3  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( ( x  e.  ( Base `  C
)  /\  A. i  e.  N  A. l  e.  N  A. c  e.  NN  ( (coe1 `  (
i x l ) ) `  c )  =  ( 0g `  R ) )  -> 
( y  e.  S  ->  A. i  e.  N  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R ) ) ) )
975, 96syld 45 . 2  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( x  e.  S  ->  ( y  e.  S  ->  A. i  e.  N  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r `  P
) ( k y j ) ) ) ) ) `  c
)  =  ( 0g
`  R ) ) ) )
9897imp32 434 1  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( x  e.  S  /\  y  e.  S
) )  ->  A. i  e.  N  A. j  e.  N  A. c  e.  NN  ( (coe1 `  ( P  gsumg  ( k  e.  N  |->  ( ( i x k ) ( .r
`  P ) ( k y j ) ) ) ) ) `
 c )  =  ( 0g `  R
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1872   A.wral 2708    |-> cmpt 4418   ` cfv 5537  (class class class)co 6242   Fincfn 7517   NNcn 10553   NN0cn0 10813   Basecbs 15057   .rcmulr 15127   0gc0g 15274    gsumg cgsu 15275   Mndcmnd 16471   Ringcrg 17716  Poly1cpl1 18706  coe1cco1 18707   Mat cmat 19367   ConstPolyMat ccpmat 19662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-rep 4472  ax-sep 4482  ax-nul 4491  ax-pow 4538  ax-pr 4596  ax-un 6534  ax-inf2 8092  ax-cnex 9539  ax-resscn 9540  ax-1cn 9541  ax-icn 9542  ax-addcl 9543  ax-addrcl 9544  ax-mulcl 9545  ax-mulrcl 9546  ax-mulcom 9547  ax-addass 9548  ax-mulass 9549  ax-distr 9550  ax-i2m1 9551  ax-1ne0 9552  ax-1rid 9553  ax-rnegex 9554  ax-rrecex 9555  ax-cnre 9556  ax-pre-lttri 9557  ax-pre-lttrn 9558  ax-pre-ltadd 9559  ax-pre-mulgt0 9560
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-nel 2596  df-ral 2713  df-rex 2714  df-reu 2715  df-rmo 2716  df-rab 2717  df-v 3018  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-tp 3939  df-op 3941  df-ot 3943  df-uni 4156  df-int 4192  df-iun 4237  df-iin 4238  df-br 4360  df-opab 4419  df-mpt 4420  df-tr 4455  df-eprel 4700  df-id 4704  df-po 4710  df-so 4711  df-fr 4748  df-se 4749  df-we 4750  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-res 4801  df-ima 4802  df-pred 5335  df-ord 5381  df-on 5382  df-lim 5383  df-suc 5384  df-iota 5501  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-isom 5546  df-riota 6204  df-ov 6245  df-oprab 6246  df-mpt2 6247  df-of 6482  df-ofr 6483  df-om 6644  df-1st 6744  df-2nd 6745  df-supp 6863  df-wrecs 6976  df-recs 7038  df-rdg 7076  df-1o 7130  df-2o 7131  df-oadd 7134  df-er 7311  df-map 7422  df-pm 7423  df-ixp 7471  df-en 7518  df-dom 7519  df-sdom 7520  df-fin 7521  df-fsupp 7830  df-sup 7902  df-oi 7971  df-card 8318  df-pnf 9621  df-mnf 9622  df-xr 9623  df-ltxr 9624  df-le 9625  df-sub 9806  df-neg 9807  df-nn 10554  df-2 10612  df-3 10613  df-4 10614  df-5 10615  df-6 10616  df-7 10617  df-8 10618  df-9 10619  df-10 10620  df-n0 10814  df-z 10882  df-dec 10996  df-uz 11104  df-fz 11729  df-fzo 11860  df-seq 12157  df-hash 12459  df-struct 15059  df-ndx 15060  df-slot 15061  df-base 15062  df-sets 15063  df-ress 15064  df-plusg 15139  df-mulr 15140  df-sca 15142  df-vsca 15143  df-ip 15144  df-tset 15145  df-ple 15146  df-ds 15148  df-hom 15150  df-cco 15151  df-0g 15276  df-gsum 15277  df-prds 15282  df-pws 15284  df-mre 15428  df-mrc 15429  df-acs 15431  df-mgm 16424  df-sgrp 16463  df-mnd 16473  df-mhm 16518  df-submnd 16519  df-grp 16609  df-minusg 16610  df-mulg 16612  df-subg 16750  df-ghm 16817  df-cntz 16907  df-cmn 17368  df-abl 17369  df-mgp 17660  df-ur 17672  df-ring 17718  df-subrg 17942  df-sra 18331  df-rgmod 18332  df-psr 18516  df-mpl 18518  df-opsr 18520  df-psr1 18709  df-ply1 18711  df-coe1 18712  df-dsmm 19230  df-frlm 19245  df-mat 19368  df-cpmat 19665
This theorem is referenced by:  cpmatmcl  19678
  Copyright terms: Public domain W3C validator