Metamath Proof Explorer

Theorem mp2pm2mplem4

Description: Lemma 4 for mp2pm2mp . (Contributed by AV, 12-Oct-2019) (Revised by AV, 5-Dec-2019)

Ref Expression
Hypotheses mp2pm2mp.a 
|- A = ( N Mat R )
mp2pm2mp.q 
|- Q = ( Poly1 ` A )
mp2pm2mp.l 
|- L = ( Base ` Q )
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 gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
mp2pm2mplem2.p 
|- P = ( Poly1 ` R )
Assertion mp2pm2mplem4 
|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( ( I ` O ) decompPMat K ) = ( ( coe1 ` O ) ` K ) )

Proof

Step Hyp Ref Expression
1 mp2pm2mp.a 
 |-  A = ( N Mat R )
2 mp2pm2mp.q 
 |-  Q = ( Poly1 ` A )
3 mp2pm2mp.l 
 |-  L = ( Base ` Q )
4 mp2pm2mp.m 
 |-  .x. = ( .s ` P )
5 mp2pm2mp.e 
 |-  E = ( .g ` ( mulGrp ` P ) )
6 mp2pm2mp.y 
 |-  Y = ( var1 ` R )
7 mp2pm2mp.i 
 |-  I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
8 mp2pm2mplem2.p 
 |-  P = ( Poly1 ` R )
9 1 2 3 4 5 6 7 8 mp2pm2mplem3 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( ( I ` O ) decompPMat K ) = ( i e. N , j e. N |-> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) ) )
10 eqid 
 |-  ( Base ` P ) = ( Base ` P )
11 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
12 8 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
13 12 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. Ring )
14 ringcmn 
 |-  ( P e. Ring -> P e. CMnd )
15 13 14 syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. CMnd )
16 15 ad3antrrr 
 |-  ( ( ( ( ( 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 )
17 16 3ad2ant1 
 |-  ( ( ( ( ( ( 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 )
18 simpl2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> R e. Ring )
19 18 ad2antrr 
 |-  ( ( ( ( ( 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 )
20 19 3ad2ant1 
 |-  ( ( ( ( ( ( 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 )
21 20 adantr 
 |-  ( ( ( ( ( ( ( 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 )
22 eqid 
 |-  ( Base ` R ) = ( Base ` R )
23 eqid 
 |-  ( Base ` A ) = ( Base ` A )
24 simpl2 
 |-  ( ( ( ( ( ( ( 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 )
25 simpl3 
 |-  ( ( ( ( ( ( ( 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 )
26 simpl3 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> O e. L )
27 26 ad2antrr 
 |-  ( ( ( ( ( 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 )
28 27 3ad2ant1 
 |-  ( ( ( ( ( ( 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 )
29 eqid 
 |-  ( coe1 ` O ) = ( coe1 ` O )
30 29 3 2 23 coe1fvalcl 
 |-  ( ( O e. L /\ k e. NN0 ) -> ( ( coe1 ` O ) ` k ) e. ( Base ` A ) )
31 28 30 sylan 
 |-  ( ( ( ( ( ( ( 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 ) )
32 1 22 23 24 25 31 matecld 
 |-  ( ( ( ( ( ( ( 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 ) )
33 simpr 
 |-  ( ( ( ( ( ( ( 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 )
34 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
35 22 8 6 4 34 5 10 ply1tmcl 
 |-  ( ( R e. Ring /\ ( i ( ( coe1 ` O ) ` k ) j ) e. ( Base ` R ) /\ k e. NN0 ) -> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) e. ( Base ` P ) )
36 21 32 33 35 syl3anc 
 |-  ( ( ( ( ( ( ( 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 ) )
37 36 ralrimiva 
 |-  ( ( ( ( ( ( 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 ) )
38 simp1lr 
 |-  ( ( ( ( ( ( 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 )
39 oveq 
 |-  ( ( ( coe1 ` O ) ` x ) = ( 0g ` A ) -> ( i ( ( coe1 ` O ) ` x ) j ) = ( i ( 0g ` A ) j ) )
40 39 oveq1d 
 |-  ( ( ( coe1 ` O ) ` x ) = ( 0g ` A ) -> ( ( i ( ( coe1 ` O ) ` x ) j ) .x. ( x E Y ) ) = ( ( i ( 0g ` A ) j ) .x. ( x E Y ) ) )
41 3simpa 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( N e. Fin /\ R e. Ring ) )
42 41 ad3antrrr 
 |-  ( ( ( ( ( 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 ) )
43 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
44 1 43 mat0op 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( a e. N , b e. N |-> ( 0g ` R ) ) )
45 42 44 syl 
 |-  ( ( ( ( ( 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 ) ) )
46 eqidd 
 |-  ( ( ( ( ( ( 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 ) )
47 simprl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
48 simprr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
49 fvexd 
 |-  ( ( ( ( ( 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 )
50 45 46 47 48 49 ovmpod 
 |-  ( ( ( ( ( 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 ) )
51 50 adantr 
 |-  ( ( ( ( ( ( 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 ) )
52 51 oveq1d 
 |-  ( ( ( ( ( ( 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 ) ) )
53 18 ad3antrrr 
 |-  ( ( ( ( ( ( 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 )
54 8 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
55 53 54 syl 
 |-  ( ( ( ( ( ( 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 ) )
56 55 fveq2d 
 |-  ( ( ( ( ( ( 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 ) ) )
57 56 oveq1d 
 |-  ( ( ( ( ( ( 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 ) ) )
58 8 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
59 58 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. LMod )
60 59 ad4antr 
 |-  ( ( ( ( ( ( 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 )
61 simpr 
 |-  ( ( ( ( ( ( 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 )
62 8 6 34 5 10 ply1moncl 
 |-  ( ( R e. Ring /\ x e. NN0 ) -> ( x E Y ) e. ( Base ` P ) )
63 53 61 62 syl2anc 
 |-  ( ( ( ( ( ( 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 ) )
64 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
65 eqid 
 |-  ( 0g ` ( Scalar ` P ) ) = ( 0g ` ( Scalar ` P ) )
66 10 64 4 65 11 lmod0vs 
 |-  ( ( P e. LMod /\ ( x E Y ) e. ( Base ` P ) ) -> ( ( 0g ` ( Scalar ` P ) ) .x. ( x E Y ) ) = ( 0g ` P ) )
67 60 63 66 syl2anc 
 |-  ( ( ( ( ( ( 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 ) )
68 52 57 67 3eqtrd 
 |-  ( ( ( ( ( ( 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 ) )
69 68 adantr 
 |-  ( ( ( ( ( ( ( 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 ) )
70 40 69 sylan9eqr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
71 70 exp31 
 |-  ( ( ( ( ( ( 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 ) ) ) )
72 71 a2d 
 |-  ( ( ( ( ( ( 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 ) ) ) )
73 72 ralimdva 
 |-  ( ( ( ( ( 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 ) ) ) )
74 73 impancom 
 |-  ( ( ( ( ( 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 ) ) ) )
75 74 3impib 
 |-  ( ( ( ( ( ( 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 ) ) )
76 breq2 
 |-  ( k = x -> ( s < k <-> s < x ) )
77 fveq2 
 |-  ( k = x -> ( ( coe1 ` O ) ` k ) = ( ( coe1 ` O ) ` x ) )
78 77 oveqd 
 |-  ( k = x -> ( i ( ( coe1 ` O ) ` k ) j ) = ( i ( ( coe1 ` O ) ` x ) j ) )
79 oveq1 
 |-  ( k = x -> ( k E Y ) = ( x E Y ) )
80 78 79 oveq12d 
 |-  ( k = x -> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) = ( ( i ( ( coe1 ` O ) ` x ) j ) .x. ( x E Y ) ) )
81 80 eqeq1d 
 |-  ( k = x -> ( ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) = ( 0g ` P ) <-> ( ( i ( ( coe1 ` O ) ` x ) j ) .x. ( x E Y ) ) = ( 0g ` P ) ) )
82 76 81 imbi12d 
 |-  ( 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 ) ) ) )
83 82 cbvralvw 
 |-  ( 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 ) ) )
84 75 83 sylibr 
 |-  ( ( ( ( ( ( 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 ) ) )
85 10 11 17 37 38 84 gsummptnn0fz 
 |-  ( ( ( ( ( ( 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 gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) = ( P gsum ( k e. ( 0 ... s ) |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) )
86 85 fveq2d 
 |-  ( ( ( ( ( ( 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 gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) = ( coe1 ` ( P gsum ( k e. ( 0 ... s ) |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
87 86 fveq1d 
 |-  ( ( ( ( ( ( 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 gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) = ( ( coe1 ` ( P gsum ( k e. ( 0 ... s ) |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) )
88 simpllr 
 |-  ( ( ( ( ( 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 )
89 88 3ad2ant1 
 |-  ( ( ( ( ( ( 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 )
90 36 expcom 
 |-  ( 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 ) ) )
91 elfznn0 
 |-  ( k e. ( 0 ... s ) -> k e. NN0 )
92 90 91 syl11 
 |-  ( ( ( ( ( ( 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 ) ) )
93 92 ralrimiv 
 |-  ( ( ( ( ( ( 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 ) )
94 fzfid 
 |-  ( ( ( ( ( ( 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 )
95 8 10 20 89 93 94 coe1fzgsumd 
 |-  ( ( ( ( ( ( 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 gsum ( k e. ( 0 ... s ) |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) = ( R gsum ( k e. ( 0 ... s ) |-> ( ( coe1 ` ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ` K ) ) ) )
96 87 95 eqtrd 
 |-  ( ( ( ( ( ( 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 gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) = ( R gsum ( k e. ( 0 ... s ) |-> ( ( coe1 ` ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ` K ) ) ) )
97 96 mpoeq3dva 
 |-  ( ( ( ( ( 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 gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) ) = ( i e. N , j e. N |-> ( R gsum ( k e. ( 0 ... s ) |-> ( ( coe1 ` ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ` K ) ) ) ) )
98 18 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> R e. Ring )
99 98 adantr 
 |-  ( ( ( ( ( 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 )
100 simpl2 
 |-  ( ( ( ( ( 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 )
101 simpl3 
 |-  ( ( ( ( ( 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 )
102 26 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> O e. L )
103 102 91 30 syl2an 
 |-  ( ( ( ( ( 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 ) )
104 1 22 23 100 101 103 matecld 
 |-  ( ( ( ( ( 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 ) )
105 91 adantl 
 |-  ( ( ( ( ( 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 )
106 43 22 8 6 4 34 5 coe1tm 
 |-  ( ( 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 ) ) ) )
107 99 104 105 106 syl3anc 
 |-  ( ( ( ( ( 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 ) ) ) )
108 eqeq1 
 |-  ( l = K -> ( l = k <-> K = k ) )
109 108 ifbid 
 |-  ( l = K -> if ( l = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) = if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) )
110 109 adantl 
 |-  ( ( ( ( ( ( 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 ) ) )
111 simpl1r 
 |-  ( ( ( ( ( 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 )
112 ovex 
 |-  ( i ( ( coe1 ` O ) ` k ) j ) e. _V
113 fvex 
 |-  ( 0g ` R ) e. _V
114 112 113 ifex 
 |-  if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) e. _V
115 114 a1i 
 |-  ( ( ( ( ( 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 )
116 107 110 111 115 fvmptd 
 |-  ( ( ( ( ( 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 ) ) )
117 116 mpteq2dva 
 |-  ( ( ( ( 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 ) ) ) )
118 117 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> ( R gsum ( k e. ( 0 ... s ) |-> ( ( coe1 ` ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ` K ) ) ) = ( R gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) )
119 118 mpoeq3dva 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( i e. N , j e. N |-> ( R gsum ( k e. ( 0 ... s ) |-> ( ( coe1 ` ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ` K ) ) ) ) = ( i e. N , j e. N |-> ( R gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) )
120 119 ad2antrr 
 |-  ( ( ( ( ( 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 gsum ( k e. ( 0 ... s ) |-> ( ( coe1 ` ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ` K ) ) ) ) = ( i e. N , j e. N |-> ( R gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) )
121 breq2 
 |-  ( x = K -> ( s < x <-> s < K ) )
122 fveqeq2 
 |-  ( x = K -> ( ( ( coe1 ` O ) ` x ) = ( 0g ` A ) <-> ( ( coe1 ` O ) ` K ) = ( 0g ` A ) ) )
123 121 122 imbi12d 
 |-  ( x = K -> ( ( s < x -> ( ( coe1 ` O ) ` x ) = ( 0g ` A ) ) <-> ( s < K -> ( ( coe1 ` O ) ` K ) = ( 0g ` A ) ) ) )
124 123 rspcva 
 |-  ( ( K e. NN0 /\ A. x e. NN0 ( s < x -> ( ( coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> ( s < K -> ( ( coe1 ` O ) ` K ) = ( 0g ` A ) ) )
125 1 43 mat0op 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( i e. N , j e. N |-> ( 0g ` R ) ) )
126 125 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( i e. N , j e. N |-> ( 0g ` R ) ) = ( 0g ` A ) )
127 126 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( i e. N , j e. N |-> ( 0g ` R ) ) = ( 0g ` A ) )
128 127 ad3antlr 
 |-  ( ( ( ( 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 ) )
129 elfz2nn0 
 |-  ( k e. ( 0 ... s ) <-> ( k e. NN0 /\ s e. NN0 /\ k <_ s ) )
130 nn0re 
 |-  ( k e. NN0 -> k e. RR )
131 130 ad2antrr 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> k e. RR )
132 nn0re 
 |-  ( s e. NN0 -> s e. RR )
133 132 ad2antlr 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> s e. RR )
134 nn0re 
 |-  ( K e. NN0 -> K e. RR )
135 134 adantl 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> K e. RR )
136 lelttr 
 |-  ( ( k e. RR /\ s e. RR /\ K e. RR ) -> ( ( k <_ s /\ s < K ) -> k < K ) )
137 131 133 135 136 syl3anc 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> ( ( k <_ s /\ s < K ) -> k < K ) )
138 animorr 
 |-  ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) /\ k < K ) -> ( K < k \/ k < K ) )
139 df-ne 
 |-  ( K =/= k <-> -. K = k )
140 130 adantr 
 |-  ( ( k e. NN0 /\ s e. NN0 ) -> k e. RR )
141 lttri2 
 |-  ( ( K e. RR /\ k e. RR ) -> ( K =/= k <-> ( K < k \/ k < K ) ) )
142 134 140 141 syl2anr 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> ( K =/= k <-> ( K < k \/ k < K ) ) )
143 142 adantr 
 |-  ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) /\ k < K ) -> ( K =/= k <-> ( K < k \/ k < K ) ) )
144 139 143 bitr3id 
 |-  ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) /\ k < K ) -> ( -. K = k <-> ( K < k \/ k < K ) ) )
145 138 144 mpbird 
 |-  ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) /\ k < K ) -> -. K = k )
146 145 ex 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> ( k < K -> -. K = k ) )
147 137 146 syld 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> ( ( k <_ s /\ s < K ) -> -. K = k ) )
148 147 exp4b 
 |-  ( ( k e. NN0 /\ s e. NN0 ) -> ( K e. NN0 -> ( k <_ s -> ( s < K -> -. K = k ) ) ) )
149 148 com24 
 |-  ( ( k e. NN0 /\ s e. NN0 ) -> ( s < K -> ( k <_ s -> ( K e. NN0 -> -. K = k ) ) ) )
150 149 expimpd 
 |-  ( k e. NN0 -> ( ( s e. NN0 /\ s < K ) -> ( k <_ s -> ( K e. NN0 -> -. K = k ) ) ) )
151 150 com23 
 |-  ( k e. NN0 -> ( k <_ s -> ( ( s e. NN0 /\ s < K ) -> ( K e. NN0 -> -. K = k ) ) ) )
152 151 imp 
 |-  ( ( k e. NN0 /\ k <_ s ) -> ( ( s e. NN0 /\ s < K ) -> ( K e. NN0 -> -. K = k ) ) )
153 152 3adant2 
 |-  ( ( k e. NN0 /\ s e. NN0 /\ k <_ s ) -> ( ( s e. NN0 /\ s < K ) -> ( K e. NN0 -> -. K = k ) ) )
154 129 153 sylbi 
 |-  ( k e. ( 0 ... s ) -> ( ( s e. NN0 /\ s < K ) -> ( K e. NN0 -> -. K = k ) ) )
155 154 com13 
 |-  ( K e. NN0 -> ( ( s e. NN0 /\ s < K ) -> ( k e. ( 0 ... s ) -> -. K = k ) ) )
156 155 adantr 
 |-  ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) -> ( ( s e. NN0 /\ s < K ) -> ( k e. ( 0 ... s ) -> -. K = k ) ) )
157 156 imp 
 |-  ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) -> ( k e. ( 0 ... s ) -> -. K = k ) )
158 157 adantr 
 |-  ( ( ( ( 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 ) )
159 158 3ad2ant1 
 |-  ( ( ( ( ( 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 ) )
160 159 imp 
 |-  ( ( ( ( ( ( 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 )
161 160 iffalsed 
 |-  ( ( ( ( ( ( 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 ) )
162 161 mpteq2dva 
 |-  ( ( ( ( ( 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 ) ) )
163 162 oveq2d 
 |-  ( ( ( ( ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) = ( R gsum ( k e. ( 0 ... s ) |-> ( 0g ` R ) ) ) )
164 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
165 164 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> R e. Mnd )
166 ovex 
 |-  ( 0 ... s ) e. _V
167 43 gsumz 
 |-  ( ( R e. Mnd /\ ( 0 ... s ) e. _V ) -> ( R gsum ( k e. ( 0 ... s ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
168 165 166 167 sylancl 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( R gsum ( k e. ( 0 ... s ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
169 168 ad3antlr 
 |-  ( ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) /\ ( ( coe1 ` O ) ` K ) = ( 0g ` A ) ) -> ( R gsum ( k e. ( 0 ... s ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
170 169 3ad2ant1 
 |-  ( ( ( ( ( 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 gsum ( k e. ( 0 ... s ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
171 163 170 eqtrd 
 |-  ( ( ( ( ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) = ( 0g ` R ) )
172 171 mpoeq3dva 
 |-  ( ( ( ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( i e. N , j e. N |-> ( 0g ` R ) ) )
173 simpr 
 |-  ( ( ( ( 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 ) )
174 128 172 173 3eqtr4d 
 |-  ( ( ( ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( ( coe1 ` O ) ` K ) )
175 174 ex 
 |-  ( ( ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( ( coe1 ` O ) ` K ) ) )
176 175 expr 
 |-  ( ( ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( ( coe1 ` O ) ` K ) ) ) )
177 176 a2d 
 |-  ( ( ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( ( coe1 ` O ) ` K ) ) ) )
178 177 exp31 
 |-  ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( ( coe1 ` O ) ` K ) ) ) ) ) )
179 178 com14 
 |-  ( ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( ( coe1 ` O ) ` K ) ) ) ) ) )
180 124 179 syl 
 |-  ( ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( ( coe1 ` O ) ` K ) ) ) ) ) )
181 180 ex 
 |-  ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( ( coe1 ` O ) ` K ) ) ) ) ) ) )
182 181 com25 
 |-  ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( ( coe1 ` O ) ` K ) ) ) ) ) ) )
183 182 pm2.43i 
 |-  ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( ( coe1 ` O ) ` K ) ) ) ) ) )
184 183 impcom 
 |-  ( ( ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( ( coe1 ` O ) ` K ) ) ) ) )
185 184 imp31 
 |-  ( ( ( ( ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( ( coe1 ` O ) ` K ) ) )
186 185 com12 
 |-  ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( ( coe1 ` O ) ` K ) ) )
187 165 ad3antrrr 
 |-  ( ( ( ( ( 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 )
188 187 adantl 
 |-  ( ( -. 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 )
189 188 3ad2ant1 
 |-  ( ( ( -. 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 )
190 ovexd 
 |-  ( ( ( -. 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 )
191 lenlt 
 |-  ( ( K e. RR /\ s e. RR ) -> ( K <_ s <-> -. s < K ) )
192 134 132 191 syl2an 
 |-  ( ( K e. NN0 /\ s e. NN0 ) -> ( K <_ s <-> -. s < K ) )
193 simpll 
 |-  ( ( ( K e. NN0 /\ s e. NN0 ) /\ K <_ s ) -> K e. NN0 )
194 simplr 
 |-  ( ( ( K e. NN0 /\ s e. NN0 ) /\ K <_ s ) -> s e. NN0 )
195 simpr 
 |-  ( ( ( K e. NN0 /\ s e. NN0 ) /\ K <_ s ) -> K <_ s )
196 elfz2nn0 
 |-  ( K e. ( 0 ... s ) <-> ( K e. NN0 /\ s e. NN0 /\ K <_ s ) )
197 193 194 195 196 syl3anbrc 
 |-  ( ( ( K e. NN0 /\ s e. NN0 ) /\ K <_ s ) -> K e. ( 0 ... s ) )
198 197 ex 
 |-  ( ( K e. NN0 /\ s e. NN0 ) -> ( K <_ s -> K e. ( 0 ... s ) ) )
199 192 198 sylbird 
 |-  ( ( K e. NN0 /\ s e. NN0 ) -> ( -. s < K -> K e. ( 0 ... s ) ) )
200 199 ad4ant23 
 |-  ( ( ( ( ( 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 ) ) )
201 200 impcom 
 |-  ( ( -. 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 ) )
202 201 3ad2ant1 
 |-  ( ( ( -. 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 ) )
203 eqcom 
 |-  ( K = k <-> k = K )
204 ifbi 
 |-  ( ( K = k <-> k = K ) -> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) = if ( k = K , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) )
205 203 204 ax-mp 
 |-  if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) = if ( k = K , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) )
206 205 mpteq2i 
 |-  ( 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 ) ) )
207 simpl2 
 |-  ( ( ( ( -. 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 )
208 simpl3 
 |-  ( ( ( ( -. 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 )
209 27 adantl 
 |-  ( ( -. 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 )
210 209 3ad2ant1 
 |-  ( ( ( -. 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 )
211 210 30 sylan 
 |-  ( ( ( ( -. 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 ) )
212 1 22 23 207 208 211 matecld 
 |-  ( ( ( ( -. 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 ) )
213 91 212 sylan2 
 |-  ( ( ( ( -. 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 ) )
214 213 ralrimiva 
 |-  ( ( ( -. 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 ) )
215 43 189 190 202 206 214 gsummpt1n0 
 |-  ( ( ( -. 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) = [_ K / k ]_ ( i ( ( coe1 ` O ) ` k ) j ) )
216 215 mpoeq3dva 
 |-  ( ( -. 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 gsum ( 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 ) ) )
217 csbov 
 |-  [_ K / k ]_ ( i ( ( coe1 ` O ) ` k ) j ) = ( i [_ K / k ]_ ( ( coe1 ` O ) ` k ) j )
218 csbfv 
 |-  [_ K / k ]_ ( ( coe1 ` O ) ` k ) = ( ( coe1 ` O ) ` K )
219 218 a1i 
 |-  ( K e. NN0 -> [_ K / k ]_ ( ( coe1 ` O ) ` k ) = ( ( coe1 ` O ) ` K ) )
220 219 oveqd 
 |-  ( K e. NN0 -> ( i [_ K / k ]_ ( ( coe1 ` O ) ` k ) j ) = ( i ( ( coe1 ` O ) ` K ) j ) )
221 217 220 syl5eq 
 |-  ( K e. NN0 -> [_ K / k ]_ ( i ( ( coe1 ` O ) ` k ) j ) = ( i ( ( coe1 ` O ) ` K ) j ) )
222 221 ad2antlr 
 |-  ( ( ( ( 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 ) )
223 222 mpoeq3dv 
 |-  ( ( ( ( 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 ) ) )
224 oveq12 
 |-  ( ( i = a /\ j = b ) -> ( i ( ( coe1 ` O ) ` K ) j ) = ( a ( ( coe1 ` O ) ` K ) b ) )
225 224 adantl 
 |-  ( ( ( ( ( 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 ) )
226 simprl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> a e. N )
227 simprr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> b e. N )
228 ovexd 
 |-  ( ( ( ( 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 )
229 223 225 226 227 228 ovmpod 
 |-  ( ( ( ( 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 ) )
230 229 ralrimivva 
 |-  ( ( ( 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 ) )
231 simpl1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> N e. Fin )
232 218 oveqi 
 |-  ( i [_ K / k ]_ ( ( coe1 ` O ) ` k ) j ) = ( i ( ( coe1 ` O ) ` K ) j )
233 217 232 eqtri 
 |-  [_ K / k ]_ ( i ( ( coe1 ` O ) ` k ) j ) = ( i ( ( coe1 ` O ) ` K ) j )
234 simp2 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> i e. N )
235 simp3 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> j e. N )
236 29 3 2 23 coe1fvalcl 
 |-  ( ( O e. L /\ K e. NN0 ) -> ( ( coe1 ` O ) ` K ) e. ( Base ` A ) )
237 236 3ad2antl3 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( ( coe1 ` O ) ` K ) e. ( Base ` A ) )
238 237 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` O ) ` K ) e. ( Base ` A ) )
239 1 22 23 234 235 238 matecld 
 |-  ( ( ( ( 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 ) )
240 233 239 eqeltrid 
 |-  ( ( ( ( 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 ) )
241 1 22 23 231 18 240 matbas2d 
 |-  ( ( ( 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 ) )
242 1 23 eqmat 
 |-  ( ( ( 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 ) ) )
243 241 237 242 syl2anc 
 |-  ( ( ( 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 ) ) )
244 230 243 mpbird 
 |-  ( ( ( 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 ) )
245 244 ad2antrr 
 |-  ( ( ( ( ( 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 ) )
246 245 adantl 
 |-  ( ( -. 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 ) )
247 216 246 eqtrd 
 |-  ( ( -. 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( ( coe1 ` O ) ` K ) )
248 247 ex 
 |-  ( -. 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( ( coe1 ` O ) ` K ) ) )
249 186 248 pm2.61i 
 |-  ( ( ( ( ( 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 gsum ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( ( coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( ( coe1 ` O ) ` K ) )
250 97 120 249 3eqtrd 
 |-  ( ( ( ( ( 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 gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) ) = ( ( coe1 ` O ) ` K ) )
251 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
252 29 3 2 251 coe1sfi 
 |-  ( O e. L -> ( coe1 ` O ) finSupp ( 0g ` A ) )
253 26 252 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( coe1 ` O ) finSupp ( 0g ` A ) )
254 29 3 2 251 23 coe1fsupp 
 |-  ( O e. L -> ( coe1 ` O ) e. { x e. ( ( Base ` A ) ^m NN0 ) | x finSupp ( 0g ` A ) } )
255 elrabi 
 |-  ( ( coe1 ` O ) e. { x e. ( ( Base ` A ) ^m NN0 ) | x finSupp ( 0g ` A ) } -> ( coe1 ` O ) e. ( ( Base ` A ) ^m NN0 ) )
256 26 254 255 3syl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( coe1 ` O ) e. ( ( Base ` A ) ^m NN0 ) )
257 fvex 
 |-  ( 0g ` A ) e. _V
258 fsuppmapnn0ub 
 |-  ( ( ( 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 ) ) ) )
259 256 257 258 sylancl 
 |-  ( ( ( 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 ) ) ) )
260 253 259 mpd 
 |-  ( ( ( 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 ) ) )
261 250 260 r19.29a 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) ) = ( ( coe1 ` O ) ` K ) )
262 9 261 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( ( I ` O ) decompPMat K ) = ( ( coe1 ` O ) ` K ) )