Metamath Proof Explorer

Theorem cpmatmcllem

Description: Lemma for cpmatmcl . (Contributed by AV, 18-Nov-2019)

Ref Expression
Hypotheses cpmatsrngpmat.s 
|- S = ( N ConstPolyMat R )
cpmatsrngpmat.p 
|- P = ( Poly1 ` R )
cpmatsrngpmat.c 
|- C = ( N Mat P )
Assertion 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) )

Proof

Step Hyp Ref Expression
1 cpmatsrngpmat.s 
 |-  S = ( N ConstPolyMat R )
2 cpmatsrngpmat.p 
 |-  P = ( Poly1 ` R )
3 cpmatsrngpmat.c 
 |-  C = ( N Mat P )
4 eqid 
 |-  ( Base ` C ) = ( Base ` C )
5 1 2 3 4 cpmatelimp 
 |-  ( ( 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 ) ) ) )
6 1 2 3 4 cpmatelimp 
 |-  ( ( 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 ) ) ) )
7 6 adantr 
 |-  ( ( ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 ) ) )
11 9 10 bitr3i 
 |-  ( ( 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 
 |-  F/ c ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) )
13 nfra1 
 |-  F/ c A. c e. NN A. l e. N ( ( ( coe1 ` ( i x l ) ) ` c ) = ( 0g ` R ) /\ ( ( coe1 ` ( l y j ) ) ` c ) = ( 0g ` R ) )
14 12 13 nfan 
 |-  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 
 |-  ( ( ( ( ( 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 
 |-  ( Base ` P ) = ( Base ` P )
17 simplrl 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) -> x e. ( Base ` C ) )
20 19 adantr 
 |-  ( ( ( ( ( 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 ) )
21 3 16 4 17 18 20 matecld 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) -> y e. ( Base ` C ) )
24 23 adantr 
 |-  ( ( ( ( ( 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 ) )
25 3 16 4 18 22 24 matecld 
 |-  ( ( ( ( ( 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 ) )
26 15 21 25 jca32 
 |-  ( ( ( ( ( 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 ) ) ) )
27 26 adantlr 
 |-  ( ( ( ( ( ( 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 
 |-  ( l = k -> ( i x l ) = ( i x k ) )
29 28 fveq2d 
 |-  ( l = k -> ( coe1 ` ( i x l ) ) = ( coe1 ` ( i x k ) ) )
30 29 fveq1d 
 |-  ( l = k -> ( ( coe1 ` ( i x l ) ) ` c ) = ( ( coe1 ` ( i x k ) ) ` c ) )
31 30 eqeq1d 
 |-  ( l = k -> ( ( ( coe1 ` ( i x l ) ) ` c ) = ( 0g ` R ) <-> ( ( coe1 ` ( i x k ) ) ` c ) = ( 0g ` R ) ) )
32 fvoveq1 
 |-  ( l = k -> ( coe1 ` ( l y j ) ) = ( coe1 ` ( k y j ) ) )
33 32 fveq1d 
 |-  ( l = k -> ( ( coe1 ` ( l y j ) ) ` c ) = ( ( coe1 ` ( k y j ) ) ` c ) )
34 33 eqeq1d 
 |-  ( l = k -> ( ( ( coe1 ` ( l y j ) ) ` c ) = ( 0g ` R ) <-> ( ( coe1 ` ( k y j ) ) ` c ) = ( 0g ` R ) ) )
35 31 34 anbi12d 
 |-  ( 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 ) ) ) )
36 35 rspcva 
 |-  ( ( 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 ) ) )
37 36 a1i 
 |-  ( ( ( ( ( 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 ) ) ) )
38 37 exp4b 
 |-  ( ( ( ( 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 ) ) ) ) ) )
39 38 com23 
 |-  ( ( ( ( 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 ) ) ) ) ) )
40 39 imp31 
 |-  ( ( ( ( ( ( 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 ) ) ) )
41 40 ralimdva 
 |-  ( ( ( ( ( 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 ) ) ) )
42 41 impancom 
 |-  ( ( ( ( ( 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 ) ) ) )
43 42 imp 
 |-  ( ( ( ( ( ( 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 ) ) )
44 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
45 eqid 
 |-  ( .r ` P ) = ( .r ` P )
46 2 16 44 45 cply1mul 
 |-  ( ( 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 ) ) )
47 27 43 46 sylc 
 |-  ( ( ( ( ( ( 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 ) )
48 47 r19.21bi 
 |-  ( ( ( ( ( ( ( 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 ) )
49 48 an32s 
 |-  ( ( ( ( ( ( ( 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 ) )
50 49 mpteq2dva 
 |-  ( ( ( ( ( ( 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 ) ) )
51 50 oveq2d 
 |-  ( ( ( ( ( ( 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 gsum ( k e. N |-> ( ( coe1 ` ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ` c ) ) ) = ( R gsum ( k e. N |-> ( 0g ` R ) ) ) )
52 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
53 52 anim2i 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( N e. Fin /\ R e. Mnd ) )
54 53 ancomd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( R e. Mnd /\ N e. Fin ) )
55 44 gsumz 
 |-  ( ( R e. Mnd /\ N e. Fin ) -> ( R gsum ( k e. N |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
56 54 55 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( R gsum ( k e. N |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
57 56 ad4antr 
 |-  ( ( ( ( ( ( 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 gsum ( k e. N |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
58 51 57 eqtrd 
 |-  ( ( ( ( ( ( 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 gsum ( k e. N |-> ( ( coe1 ` ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ` c ) ) ) = ( 0g ` R ) )
59 58 ex 
 |-  ( ( ( ( ( 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 gsum ( k e. N |-> ( ( coe1 ` ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ` c ) ) ) = ( 0g ` R ) ) )
60 14 59 ralrimi 
 |-  ( ( ( ( ( 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 gsum ( k e. N |-> ( ( coe1 ` ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ` c ) ) ) = ( 0g ` R ) )
61 simp-4r 
 |-  ( ( ( ( ( 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 )
62 nnnn0 
 |-  ( c e. NN -> c e. NN0 )
63 62 adantl 
 |-  ( ( ( ( ( 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 )
64 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
65 64 ad4antlr 
 |-  ( ( ( ( ( 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 )
66 16 45 ringcl 
 |-  ( ( 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 ) )
67 65 21 25 66 syl3anc 
 |-  ( ( ( ( ( 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 ) )
68 67 ralrimiva 
 |-  ( ( ( ( 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 ) )
69 68 adantr 
 |-  ( ( ( ( ( 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 ) )
70 simp-4l 
 |-  ( ( ( ( ( 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 )
71 2 16 61 63 69 70 coe1fzgsumd 
 |-  ( ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( R gsum ( k e. N |-> ( ( coe1 ` ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ` c ) ) ) )
72 71 eqeq1d 
 |-  ( ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) <-> ( R gsum ( k e. N |-> ( ( coe1 ` ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ` c ) ) ) = ( 0g ` R ) ) )
73 72 ralbidva 
 |-  ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) <-> A. c e. NN ( R gsum ( k e. N |-> ( ( coe1 ` ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ` c ) ) ) = ( 0g ` R ) ) )
74 73 adantr 
 |-  ( ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) <-> A. c e. NN ( R gsum ( k e. N |-> ( ( coe1 ` ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ` c ) ) ) = ( 0g ` R ) ) )
75 60 74 mpbird 
 |-  ( ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) )
76 75 ex 
 |-  ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) )
77 11 76 syl5bi 
 |-  ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) )
78 77 expd 
 |-  ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) ) )
79 78 expr 
 |-  ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) ) ) )
80 79 com23 
 |-  ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) ) ) )
81 80 imp31 
 |-  ( ( ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) )
82 81 ralimdva 
 |-  ( ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) )
83 8 82 syl5bi 
 |-  ( ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) )
84 83 ex 
 |-  ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) ) )
85 84 com23 
 |-  ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) ) )
86 85 impancom 
 |-  ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) ) )
87 86 imp 
 |-  ( ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) )
88 87 ralimdva 
 |-  ( ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) )
89 88 ex 
 |-  ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) ) )
90 89 expr 
 |-  ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) ) ) )
91 90 impd 
 |-  ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) ) )
92 7 91 syld 
 |-  ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) ) )
93 92 com23 
 |-  ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) ) )
94 93 ex 
 |-  ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) ) ) )
95 94 impd 
 |-  ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) ) )
96 5 95 syld 
 |-  ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) ) )
97 96 imp32 
 |-  ( ( ( 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 gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) )