MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp2pm2mplem4 Structured version   Unicode version
Theorem mp2pm2mplem4 19077
Description: Lemma 4 for mp2pm2mp 19079. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 5-Dec-2019.)
Hypotheses
Ref Expression
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 gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
mp2pm2mplem2.p |- P = (Poly1 ` R )
Assertion
Ref Expression
mp2pm2mplem4 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( ( I ` O ) decompPMat K ) = ( (coe1 ` O ) ` K ) )
Distinct variable groups:   E, p   L, p   i, N, j, p   i, O, j, p, k   P, p   R, p   Y, p   .x. , p   k, L   P, i, j, k   R, k   .x. , k   i, E, j   i, K, j   i, L, j   k, N   R, i, j   i, Y, j   .x. , i, j   A, i, j, k   k, E   k, K   k, Y
Allowed substitution hints:   A( p)   Q( i, j, k, p)   I( i, j, k, p)   K( p)
Proof of Theorem mp2pm2mplem4
Dummy variables a b s x l are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mp2pm2mp.a . . 3 |- A = ( N Mat R )
2 mp2pm2mp.q . . 3 |- Q = (Poly1 ` A )
3 mp2pm2mp.l . . 3 |- L = ( Base ` Q )
4 mp2pm2mp.m . . 3 |- .x. = ( .s ` P )
5 mp2pm2mp.e . . 3 |- E = (.g ` (mulGrp ` P ) )
6 mp2pm2mp.y . . 3 |- Y = (var1 ` R )
7 mp2pm2mp.i . . 3 |- I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
8 mp2pm2mplem2.p . . 3 |- P = (Poly1 ` R )
91, 2, 3, 4, 5, 6, 7, 8mp2pm2mplem3 19076 . 2 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( ( I ` O ) decompPMat K ) = ( i e. N , j e. N |-> ( (coe1 ` ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) ) )
10 eqid 2467 . . . . . . . . 9 |- ( Base ` P ) = ( Base ` P )
11 eqid 2467 . . . . . . . . 9 |- ( 0g ` P ) = ( 0g ` P )
128ply1rng 18060 . . . . . . . . . . . . 13 |- ( R e. Ring -> P e. Ring )
13123ad2ant2 1018 . . . . . . . . . . . 12 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. Ring )
14 rngcmn 17016 . . . . . . . . . . . 12 |- ( P e. Ring -> P e. CMnd )
1513, 14syl 16 . . . . . . . . . . 11 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. CMnd )
1615ad3antrrr 729 . . . . . . . . . 10 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> P e. CMnd )
17163ad2ant1 1017 . . . . . . . . 9 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> P e. CMnd )
18 simpl2 1000 . . . . . . . . . . . . . 14 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> R e. Ring )
1918ad2antrr 725 . . . . . . . . . . . . 13 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> R e. Ring )
20193ad2ant1 1017 . . . . . . . . . . . 12 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> R e. Ring )
2120adantr 465 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> R e. Ring )
22 eqid 2467 . . . . . . . . . . . 12 |- ( Base ` R ) = ( Base ` R )
23 eqid 2467 . . . . . . . . . . . 12 |- ( Base ` A ) = ( Base ` A )
24 simpl2 1000 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> i e. N )
25 simpl3 1001 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> j e. N )
26 simpl3 1001 . . . . . . . . . . . . . . 15 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> O e. L )
2726ad2antrr 725 . . . . . . . . . . . . . 14 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> O e. L )
28273ad2ant1 1017 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> O e. L )
29 eqid 2467 . . . . . . . . . . . . . 14 |- (coe1 ` O ) = (coe1 ` O )
3029, 3, 2, 23coe1fvalcl 18022 . . . . . . . . . . . . 13 |- ( ( O e. L /\ k e. NN0 ) -> ( (coe1 ` O ) ` k ) e. ( Base ` A ) )
3128, 30sylan 471 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> ( (coe1 ` O ) ` k ) e. ( Base ` A ) )
321, 22, 23, 24, 25, 31matecld 18695 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> ( i ( (coe1 ` O ) ` k ) j ) e. ( Base ` R ) )
33 simpr 461 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> k e. NN0 )
34 eqid 2467 . . . . . . . . . . . 12 |- (mulGrp ` P ) = (mulGrp ` P )
3522, 8, 6, 4, 34, 5, 10ply1tmcl 18084 . . . . . . . . . . 11 |- ( ( 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 ) )
3621, 32, 33, 35syl3anc 1228 . . . . . . . . . 10 |- ( ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) e. ( Base ` P ) )
3736ralrimiva 2878 . . . . . . . . 9 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> A. k e. NN0 ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) e. ( Base ` P ) )
38 simp1lr 1060 . . . . . . . . 9 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> s e. NN0 )
39 oveq 6288 . . . . . . . . . . . . . . . . 17 |- ( ( (coe1 ` O ) ` x ) = ( 0g ` A ) -> ( i ( (coe1 ` O ) ` x ) j ) = ( i ( 0g ` A ) j ) )
4039oveq1d 6297 . . . . . . . . . . . . . . . 16 |- ( ( (coe1 ` O ) ` x ) = ( 0g ` A ) -> ( ( i ( (coe1 ` O ) ` x ) j ) .x. ( x E Y ) ) = ( ( i ( 0g ` A ) j ) .x. ( x E Y ) ) )
41 3simpa 993 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( N e. Fin /\ R e. Ring ) )
4241ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( N e. Fin /\ R e. Ring ) )
43 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0g ` R ) = ( 0g ` R )
441, 43mat0op 18688 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( a e. N , b e. N |-> ( 0g ` R ) ) )
4542, 44syl 16 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( 0g ` A ) = ( a e. N , b e. N |-> ( 0g ` R ) ) )
46 eqidd 2468 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ ( a = i /\ b = j ) ) -> ( 0g ` R ) = ( 0g ` R ) )
47 simprl 755 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
48 simprr 756 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
49 fvex 5874 . . . . . . . . . . . . . . . . . . . . . 22 |- ( 0g ` R ) e. _V
5049a1i 11 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( 0g ` R ) e. _V )
5145, 46, 47, 48, 50ovmpt2d 6412 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( i ( 0g ` A ) j ) = ( 0g ` R ) )
5251adantr 465 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ x e. NN0 ) -> ( i ( 0g ` A ) j ) = ( 0g ` R ) )
5352oveq1d 6297 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ x e. NN0 ) -> ( ( i ( 0g ` A ) j ) .x. ( x E Y ) ) = ( ( 0g ` R ) .x. ( x E Y ) ) )
5418ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ x e. NN0 ) -> R e. Ring )
558ply1sca 18065 . . . . . . . . . . . . . . . . . . . . 21 |- ( R e. Ring -> R = (Scalar ` P ) )
5654, 55syl 16 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ x e. NN0 ) -> R = (Scalar ` P ) )
5756fveq2d 5868 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ x e. NN0 ) -> ( 0g ` R ) = ( 0g ` (Scalar ` P ) ) )
5857oveq1d 6297 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ x e. NN0 ) -> ( ( 0g ` R ) .x. ( x E Y ) ) = ( ( 0g ` (Scalar ` P ) ) .x. ( x E Y ) ) )
598ply1lmod 18064 . . . . . . . . . . . . . . . . . . . . 21 |- ( R e. Ring -> P e. LMod )
60593ad2ant2 1018 . . . . . . . . . . . . . . . . . . . 20 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. LMod )
6160ad4antr 731 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ x e. NN0 ) -> P e. LMod )
62 simpr 461 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ x e. NN0 ) -> x e. NN0 )
638, 6, 34, 5, 10ply1moncl 18083 . . . . . . . . . . . . . . . . . . . 20 |- ( ( R e. Ring /\ x e. NN0 ) -> ( x E Y ) e. ( Base ` P ) )
6454, 62, 63syl2anc 661 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ x e. NN0 ) -> ( x E Y ) e. ( Base ` P ) )
65 eqid 2467 . . . . . . . . . . . . . . . . . . . 20 |- (Scalar ` P ) = (Scalar ` P )
66 eqid 2467 . . . . . . . . . . . . . . . . . . . 20 |- ( 0g ` (Scalar ` P ) ) = ( 0g ` (Scalar ` P ) )
6710, 65, 4, 66, 11lmod0vs 17328 . . . . . . . . . . . . . . . . . . 19 |- ( ( P e. LMod /\ ( x E Y ) e. ( Base ` P ) ) -> ( ( 0g ` (Scalar ` P ) ) .x. ( x E Y ) ) = ( 0g ` P ) )
6861, 64, 67syl2anc 661 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ x e. NN0 ) -> ( ( 0g ` (Scalar ` P ) ) .x. ( x E Y ) ) = ( 0g ` P ) )
6953, 58, 683eqtrd 2512 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ x e. NN0 ) -> ( ( i ( 0g ` A ) j ) .x. ( x E Y ) ) = ( 0g ` P ) )
7069adantr 465 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ x e. NN0 ) /\ s < x ) -> ( ( i ( 0g ` A ) j ) .x. ( x E Y ) ) = ( 0g ` P ) )
7140, 70sylan9eqr 2530 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ x e. NN0 ) /\ s < x ) /\ ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) -> ( ( i ( (coe1 ` O ) ` x ) j ) .x. ( x E Y ) ) = ( 0g ` P ) )
7271exp31 604 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ x e. NN0 ) -> ( s < x -> ( ( (coe1 ` O ) ` x ) = ( 0g ` A ) -> ( ( i ( (coe1 ` O ) ` x ) j ) .x. ( x E Y ) ) = ( 0g ` P ) ) ) )
7372a2d 26 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ x e. NN0 ) -> ( ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) -> ( s < x -> ( ( i ( (coe1 ` O ) ` x ) j ) .x. ( x E Y ) ) = ( 0g ` P ) ) ) )
7473ralimdva 2872 . . . . . . . . . . . 12 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) -> A. x e. NN0 ( s < x -> ( ( i ( (coe1 ` O ) ` x ) j ) .x. ( x E Y ) ) = ( 0g ` P ) ) ) )
7574impancom 440 . . . . . . . . . . 11 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> ( ( i e. N /\ j e. N ) -> A. x e. NN0 ( s < x -> ( ( i ( (coe1 ` O ) ` x ) j ) .x. ( x E Y ) ) = ( 0g ` P ) ) ) )
76753impib 1194 . . . . . . . . . 10 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> A. x e. NN0 ( s < x -> ( ( i ( (coe1 ` O ) ` x ) j ) .x. ( x E Y ) ) = ( 0g ` P ) ) )
77 breq2 4451 . . . . . . . . . . . 12 |- ( k = x -> ( s < k <-> s < x ) )
78 fveq2 5864 . . . . . . . . . . . . . . 15 |- ( k = x -> ( (coe1 ` O ) ` k ) = ( (coe1 ` O ) ` x ) )
7978oveqd 6299 . . . . . . . . . . . . . 14 |- ( k = x -> ( i ( (coe1 ` O ) ` k ) j ) = ( i ( (coe1 ` O ) ` x ) j ) )
80 oveq1 6289 . . . . . . . . . . . . . 14 |- ( k = x -> ( k E Y ) = ( x E Y ) )
8179, 80oveq12d 6300 . . . . . . . . . . . . 13 |- ( k = x -> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) = ( ( i ( (coe1 ` O ) ` x ) j ) .x. ( x E Y ) ) )
8281eqeq1d 2469 . . . . . . . . . . . 12 |- ( k = x -> ( ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) = ( 0g ` P ) <-> ( ( i ( (coe1 ` O ) ` x ) j ) .x. ( x E Y ) ) = ( 0g ` P ) ) )
8377, 82imbi12d 320 . . . . . . . . . . 11 |- ( k = x -> ( ( s < k -> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) = ( 0g ` P ) ) <-> ( s < x -> ( ( i ( (coe1 ` O ) ` x ) j ) .x. ( x E Y ) ) = ( 0g ` P ) ) ) )
8483cbvralv 3088 . . . . . . . . . 10 |- ( A. k e. NN0 ( s < k -> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) = ( 0g ` P ) ) <-> A. x e. NN0 ( s < x -> ( ( i ( (coe1 ` O ) ` x ) j ) .x. ( x E Y ) ) = ( 0g ` P ) ) )
8576, 84sylibr 212 . . . . . . . . 9 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> A. k e. NN0 ( s < k -> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) = ( 0g ` P ) ) )
8610, 11, 17, 37, 38, 85gsummptnn0fzv 16806 . . . . . . . 8 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) = ( P gsumg ( k e. ( 0 ... s ) |-> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) )
8786fveq2d 5868 . . . . . . 7 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> (coe1 ` ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) = (coe1 ` ( P gsumg ( k e. ( 0 ... s ) |-> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
8887fveq1d 5866 . . . . . 6 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> ( (coe1 ` ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) = ( (coe1 ` ( P gsumg ( k e. ( 0 ... s ) |-> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) )
89 simpllr 758 . . . . . . . 8 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> K e. NN0 )
90893ad2ant1 1017 . . . . . . 7 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> K e. NN0 )
91 elfznn0 11766 . . . . . . . . . 10 |- ( k e. ( 0 ... s ) -> k e. NN0 )
9236expcom 435 . . . . . . . . . 10 |- ( k e. NN0 -> ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) e. ( Base ` P ) ) )
9391, 92syl 16 . . . . . . . . 9 |- ( k e. ( 0 ... s ) -> ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) e. ( Base ` P ) ) )
9493com12 31 . . . . . . . 8 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> ( k e. ( 0 ... s ) -> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) e. ( Base ` P ) ) )
9594ralrimiv 2876 . . . . . . 7 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> A. k e. ( 0 ... s ) ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) e. ( Base ` P ) )
96 fzfid 12047 . . . . . . 7 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> ( 0 ... s ) e. Fin )
978, 10, 20, 90, 95, 96coe1fzgsumd 18115 . . . . . 6 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> ( (coe1 ` ( P gsumg ( k e. ( 0 ... s ) |-> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) = ( R gsumg ( k e. ( 0 ... s ) |-> ( (coe1 ` ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ` K ) ) ) )
9888, 97eqtrd 2508 . . . . 5 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) /\ i e. N /\ j e. N ) -> ( (coe1 ` ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) = ( R gsumg ( k e. ( 0 ... s ) |-> ( (coe1 ` ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ` K ) ) ) )
9998mpt2eq3dva 6343 . . . 4 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> ( i e. N , j e. N |-> ( (coe1 ` ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) ) = ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> ( (coe1 ` ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ` K ) ) ) ) )
100183ad2ant1 1017 . . . . . . . . . . 11 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> R e. Ring )
101100adantr 465 . . . . . . . . . 10 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) /\ k e. ( 0 ... s ) ) -> R e. Ring )
102 simpl2 1000 . . . . . . . . . . 11 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) /\ k e. ( 0 ... s ) ) -> i e. N )
103 simpl3 1001 . . . . . . . . . . 11 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) /\ k e. ( 0 ... s ) ) -> j e. N )
104263ad2ant1 1017 . . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> O e. L )
105104, 91, 30syl2an 477 . . . . . . . . . . 11 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) /\ k e. ( 0 ... s ) ) -> ( (coe1 ` O ) ` k ) e. ( Base ` A ) )
1061, 22, 23, 102, 103, 105matecld 18695 . . . . . . . . . 10 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) /\ k e. ( 0 ... s ) ) -> ( i ( (coe1 ` O ) ` k ) j ) e. ( Base ` R ) )
10791adantl 466 . . . . . . . . . 10 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) /\ k e. ( 0 ... s ) ) -> k e. NN0 )
10843, 22, 8, 6, 4, 34, 5coe1tm 18085 . . . . . . . . . 10 |- ( ( R e. Ring /\ ( i ( (coe1 ` O ) ` k ) j ) e. ( Base ` R ) /\ k e. NN0 ) -> (coe1 ` ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) = ( l e. NN0 |-> if ( l = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) )
109101, 106, 107, 108syl3anc 1228 . . . . . . . . 9 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) /\ k e. ( 0 ... s ) ) -> (coe1 ` ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) = ( l e. NN0 |-> if ( l = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) )
110 eqeq1 2471 . . . . . . . . . . 11 |- ( l = K -> ( l = k <-> K = k ) )
111110ifbid 3961 . . . . . . . . . 10 |- ( l = K -> if ( l = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) = if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) )
112111adantl 466 . . . . . . . . 9 |- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) /\ k e. ( 0 ... s ) ) /\ l = K ) -> if ( l = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) = if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) )
113 simpl1r 1048 . . . . . . . . 9 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) /\ k e. ( 0 ... s ) ) -> K e. NN0 )
114 ovex 6307 . . . . . . . . . . 11 |- ( i ( (coe1 ` O ) ` k ) j ) e. _V
115114, 49ifex 4008 . . . . . . . . . 10 |- if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) e. _V
116115a1i 11 . . . . . . . . 9 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) /\ k e. ( 0 ... s ) ) -> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) e. _V )
117109, 112, 113, 116fvmptd 5953 . . . . . . . 8 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) /\ k e. ( 0 ... s ) ) -> ( (coe1 ` ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ` K ) = if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) )
118117mpteq2dva 4533 . . . . . . 7 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> ( k e. ( 0 ... s ) |-> ( (coe1 ` ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ` K ) ) = ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) )
119118oveq2d 6298 . . . . . 6 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> ( R gsumg ( k e. ( 0 ... s ) |-> ( (coe1 ` ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ` K ) ) ) = ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) )
120119mpt2eq3dva 6343 . . . . 5 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> ( (coe1 ` ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ` K ) ) ) ) = ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) )
121120ad2antrr 725 . . . 4 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> ( (coe1 ` ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ` K ) ) ) ) = ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) )
122 breq2 4451 . . . . . . . . . . . . . 14 |- ( x = K -> ( s < x <-> s < K ) )
123 fveq2 5864 . . . . . . . . . . . . . . 15 |- ( x = K -> ( (coe1 ` O ) ` x ) = ( (coe1 ` O ) ` K ) )
124123eqeq1d 2469 . . . . . . . . . . . . . 14 |- ( x = K -> ( ( (coe1 ` O ) ` x ) = ( 0g ` A ) <-> ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) )
125122, 124imbi12d 320 . . . . . . . . . . . . 13 |- ( x = K -> ( ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) <-> ( s < K -> ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) ) )
126125rspcva 3212 . . . . . . . . . . . 12 |- ( ( K e. NN0 /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> ( s < K -> ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) )
1271, 43mat0op 18688 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( i e. N , j e. N |-> ( 0g ` R ) ) )
128127eqcomd 2475 . . . . . . . . . . . . . . . . . . . 20 |- ( ( N e. Fin /\ R e. Ring ) -> ( i e. N , j e. N |-> ( 0g ` R ) ) = ( 0g ` A ) )
1291283adant3 1016 . . . . . . . . . . . . . . . . . . 19 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( i e. N , j e. N |-> ( 0g ` R ) ) = ( 0g ` A ) )
130129ad3antlr 730 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) /\ ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) -> ( i e. N , j e. N |-> ( 0g ` R ) ) = ( 0g ` A ) )
131 elfz2nn0 11764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( k e. ( 0 ... s ) <-> ( k e. NN0 /\ s e. NN0 /\ k <_ s ) )
132 nn0re 10800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( k e. NN0 -> k e. RR )
133132ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> k e. RR )
134 nn0re 10800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( s e. NN0 -> s e. RR )
135134ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> s e. RR )
136 nn0re 10800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( K e. NN0 -> K e. RR )
137136adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> K e. RR )
138 lelttr 9671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( k e. RR /\ s e. RR /\ K e. RR ) -> ( ( k <_ s /\ s < K ) -> k < K ) )
139133, 135, 137, 138syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> ( ( k <_ s /\ s < K ) -> k < K ) )
140 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) /\ k < K ) -> k < K )
141140olcd 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) /\ k < K ) -> ( K < k \/ k < K ) )
142 df-ne 2664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( K =/= k <-> -. K = k )
143132adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( k e. NN0 /\ s e. NN0 ) -> k e. RR )
144 lttri2 9663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( K e. RR /\ k e. RR ) -> ( K =/= k <-> ( K < k \/ k < K ) ) )
145136, 143, 144syl2anr 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> ( K =/= k <-> ( K < k \/ k < K ) ) )
146145adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) /\ k < K ) -> ( K =/= k <-> ( K < k \/ k < K ) ) )
147142, 146syl5bbr 259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) /\ k < K ) -> ( -. K = k <-> ( K < k \/ k < K ) ) )
148141, 147mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) /\ k < K ) -> -. K = k )
149148ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> ( k < K -> -. K = k ) )
150139, 149syld 44 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> ( ( k <_ s /\ s < K ) -> -. K = k ) )
151150exp4b 607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( k e. NN0 /\ s e. NN0 ) -> ( K e. NN0 -> ( k <_ s -> ( s < K -> -. K = k ) ) ) )
152151com24 87 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( k e. NN0 /\ s e. NN0 ) -> ( s < K -> ( k <_ s -> ( K e. NN0 -> -. K = k ) ) ) )
153152expimpd 603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( k e. NN0 -> ( ( s e. NN0 /\ s < K ) -> ( k <_ s -> ( K e. NN0 -> -. K = k ) ) ) )
154153com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( k e. NN0 -> ( k <_ s -> ( ( s e. NN0 /\ s < K ) -> ( K e. NN0 -> -. K = k ) ) ) )
155154imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( k e. NN0 /\ k <_ s ) -> ( ( s e. NN0 /\ s < K ) -> ( K e. NN0 -> -. K = k ) ) )
1561553adant2 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( k e. NN0 /\ s e. NN0 /\ k <_ s ) -> ( ( s e. NN0 /\ s < K ) -> ( K e. NN0 -> -. K = k ) ) )
157131, 156sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( k e. ( 0 ... s ) -> ( ( s e. NN0 /\ s < K ) -> ( K e. NN0 -> -. K = k ) ) )
158157com13 80 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( K e. NN0 -> ( ( s e. NN0 /\ s < K ) -> ( k e. ( 0 ... s ) -> -. K = k ) ) )
159158adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) -> ( ( s e. NN0 /\ s < K ) -> ( k e. ( 0 ... s ) -> -. K = k ) ) )
160159imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) -> ( k e. ( 0 ... s ) -> -. K = k ) )
161160adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) /\ ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) -> ( k e. ( 0 ... s ) -> -. K = k ) )
1621613ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) /\ ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) /\ i e. N /\ j e. N ) -> ( k e. ( 0 ... s ) -> -. K = k ) )
163162imp 429 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) /\ ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) /\ i e. N /\ j e. N ) /\ k e. ( 0 ... s ) ) -> -. K = k )
164163iffalsed 3950 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) /\ ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) /\ i e. N /\ j e. N ) /\ k e. ( 0 ... s ) ) -> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) = ( 0g ` R ) )
165164mpteq2dva 4533 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) /\ ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) /\ i e. N /\ j e. N ) -> ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) = ( k e. ( 0 ... s ) |-> ( 0g ` R ) ) )
166165oveq2d 6298 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) /\ ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) /\ i e. N /\ j e. N ) -> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) = ( R gsumg ( k e. ( 0 ... s ) |-> ( 0g ` R ) ) ) )
167 rngmnd 16995 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( R e. Ring -> R e. Mnd )
1681673ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> R e. Mnd )
169 ovex 6307 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0 ... s ) e. _V
17043gsumz 15824 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( R e. Mnd /\ ( 0 ... s ) e. _V ) -> ( R gsumg ( k e. ( 0 ... s ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
171168, 169, 170sylancl 662 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( R gsumg ( k e. ( 0 ... s ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
172171ad3antlr 730 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) /\ ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) -> ( R gsumg ( k e. ( 0 ... s ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
1731723ad2ant1 1017 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) /\ ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) /\ i e. N /\ j e. N ) -> ( R gsumg ( k e. ( 0 ... s ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
174166, 173eqtrd 2508 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) /\ ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) /\ i e. N /\ j e. N ) -> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) = ( 0g ` R ) )
175174mpt2eq3dva 6343 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) /\ ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( i e. N , j e. N |-> ( 0g ` R ) ) )
176 simpr 461 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) /\ ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) -> ( (coe1 ` O ) ` K ) = ( 0g ` A ) )
177130, 175, 1763eqtr4d 2518 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) /\ ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( (coe1 ` O ) ` K ) )
178177ex 434 . . . . . . . . . . . . . . . 16 |- ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ ( s e. NN0 /\ s < K ) ) -> ( ( (coe1 ` O ) ` K ) = ( 0g ` A ) -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( (coe1 ` O ) ` K ) ) )
179178expr 615 . . . . . . . . . . . . . . 15 |- ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ s e. NN0 ) -> ( s < K -> ( ( (coe1 ` O ) ` K ) = ( 0g ` A ) -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( (coe1 ` O ) ` K ) ) ) )
180179a2d 26 . . . . . . . . . . . . . 14 |- ( ( ( K e. NN0 /\ ( N e. Fin /\ R e. Ring /\ O e. L ) ) /\ s e. NN0 ) -> ( ( s < K -> ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) -> ( s < K -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( (coe1 ` O ) ` K ) ) ) )
181180exp31 604 . . . . . . . . . . . . 13 |- ( K e. NN0 -> ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( s e. NN0 -> ( ( s < K -> ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) -> ( s < K -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( (coe1 ` O ) ` K ) ) ) ) ) )
182181com14 88 . . . . . . . . . . . 12 |- ( ( s < K -> ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) -> ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( s e. NN0 -> ( K e. NN0 -> ( s < K -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( (coe1 ` O ) ` K ) ) ) ) ) )
183126, 182syl 16 . . . . . . . . . . 11 |- ( ( K e. NN0 /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( s e. NN0 -> ( K e. NN0 -> ( s < K -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( (coe1 ` O ) ` K ) ) ) ) ) )
184183ex 434 . . . . . . . . . 10 |- ( K e. NN0 -> ( A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) -> ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( s e. NN0 -> ( K e. NN0 -> ( s < K -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( (coe1 ` O ) ` K ) ) ) ) ) ) )
185184com25 91 . . . . . . . . 9 |- ( K e. NN0 -> ( K e. NN0 -> ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( s e. NN0 -> ( A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) -> ( s < K -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( (coe1 ` O ) ` K ) ) ) ) ) ) )
186185pm2.43i 47 . . . . . . . 8 |- ( K e. NN0 -> ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( s e. NN0 -> ( A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) -> ( s < K -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( (coe1 ` O ) ` K ) ) ) ) ) )
187186impcom 430 . . . . . . 7 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( s e. NN0 -> ( A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) -> ( s < K -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( (coe1 ` O ) ` K ) ) ) ) )
188187imp31 432 . . . . . 6 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> ( s < K -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( (coe1 ` O ) ` K ) ) )
189188com12 31 . . . . 5 |- ( s < K -> ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( (coe1 ` O ) ` K ) ) )
190168ad3antrrr 729 . . . . . . . . . . 11 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> R e. Mnd )
191190adantl 466 . . . . . . . . . 10 |- ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) -> R e. Mnd )
1921913ad2ant1 1017 . . . . . . . . 9 |- ( ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) /\ i e. N /\ j e. N ) -> R e. Mnd )
193169a1i 11 . . . . . . . . 9 |- ( ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) /\ i e. N /\ j e. N ) -> ( 0 ... s ) e. _V )
194 lenlt 9659 . . . . . . . . . . . . . . 15 |- ( ( K e. RR /\ s e. RR ) -> ( K <_ s <-> -. s < K ) )
195136, 134, 194syl2an 477 . . . . . . . . . . . . . 14 |- ( ( K e. NN0 /\ s e. NN0 ) -> ( K <_ s <-> -. s < K ) )
196 simpll 753 . . . . . . . . . . . . . . . 16 |- ( ( ( K e. NN0 /\ s e. NN0 ) /\ K <_ s ) -> K e. NN0 )
197 simplr 754 . . . . . . . . . . . . . . . 16 |- ( ( ( K e. NN0 /\ s e. NN0 ) /\ K <_ s ) -> s e. NN0 )
198 simpr 461 . . . . . . . . . . . . . . . 16 |- ( ( ( K e. NN0 /\ s e. NN0 ) /\ K <_ s ) -> K <_ s )
199 elfz2nn0 11764 . . . . . . . . . . . . . . . 16 |- ( K e. ( 0 ... s ) <-> ( K e. NN0 /\ s e. NN0 /\ K <_ s ) )
200196, 197, 198, 199syl3anbrc 1180 . . . . . . . . . . . . . . 15 |- ( ( ( K e. NN0 /\ s e. NN0 ) /\ K <_ s ) -> K e. ( 0 ... s ) )
201200ex 434 . . . . . . . . . . . . . 14 |- ( ( K e. NN0 /\ s e. NN0 ) -> ( K <_ s -> K e. ( 0 ... s ) ) )
202195, 201sylbird 235 . . . . . . . . . . . . 13 |- ( ( K e. NN0 /\ s e. NN0 ) -> ( -. s < K -> K e. ( 0 ... s ) ) )
203202adantll 713 . . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) -> ( -. s < K -> K e. ( 0 ... s ) ) )
204203adantr 465 . . . . . . . . . . 11 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> ( -. s < K -> K e. ( 0 ... s ) ) )
205204impcom 430 . . . . . . . . . 10 |- ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) -> K e. ( 0 ... s ) )
2062053ad2ant1 1017 . . . . . . . . 9 |- ( ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) /\ i e. N /\ j e. N ) -> K e. ( 0 ... s ) )
207 eqcom 2476 . . . . . . . . . . 11 |- ( K = k <-> k = K )
208 ifbi 3960 . . . . . . . . . . 11 |- ( ( K = k <-> k = K ) -> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) = if ( k = K , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) )
209207, 208ax-mp 5 . . . . . . . . . 10 |- if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) = if ( k = K , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) )
210209mpteq2i 4530 . . . . . . . . 9 |- ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) = ( k e. ( 0 ... s ) |-> if ( k = K , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) )
211 simpl2 1000 . . . . . . . . . . . 12 |- ( ( ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> i e. N )
212 simpl3 1001 . . . . . . . . . . . 12 |- ( ( ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> j e. N )
21327adantl 466 . . . . . . . . . . . . . 14 |- ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) -> O e. L )
2142133ad2ant1 1017 . . . . . . . . . . . . 13 |- ( ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) /\ i e. N /\ j e. N ) -> O e. L )
215214, 30sylan 471 . . . . . . . . . . . 12 |- ( ( ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> ( (coe1 ` O ) ` k ) e. ( Base ` A ) )
2161, 22, 23, 211, 212, 215matecld 18695 . . . . . . . . . . 11 |- ( ( ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> ( i ( (coe1 ` O ) ` k ) j ) e. ( Base ` R ) )
21791, 216sylan2 474 . . . . . . . . . 10 |- ( ( ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) /\ i e. N /\ j e. N ) /\ k e. ( 0 ... s ) ) -> ( i ( (coe1 ` O ) ` k ) j ) e. ( Base ` R ) )
218217ralrimiva 2878 . . . . . . . . 9 |- ( ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) /\ i e. N /\ j e. N ) -> A. k e. ( 0 ... s ) ( i ( (coe1 ` O ) ` k ) j ) e. ( Base ` R ) )
21943, 192, 193, 206, 210, 218gsummpt1n0 16783 . . . . . . . 8 |- ( ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) /\ i e. N /\ j e. N ) -> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) = [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) )
220219mpt2eq3dva 6343 . . . . . . 7 |- ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( i e. N , j e. N |-> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) ) )
221 csbov 6314 . . . . . . . . . . . . . . 15 |- [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) = ( i [_ K / k ]_ ( (coe1 ` O ) ` k ) j )
222 csbfv 5902 . . . . . . . . . . . . . . . . 17 |- [_ K / k ]_ ( (coe1 ` O ) ` k ) = ( (coe1 ` O ) ` K )
223222a1i 11 . . . . . . . . . . . . . . . 16 |- ( K e. NN0 -> [_ K / k ]_ ( (coe1 ` O ) ` k ) = ( (coe1 ` O ) ` K ) )
224223oveqd 6299 . . . . . . . . . . . . . . 15 |- ( K e. NN0 -> ( i [_ K / k ]_ ( (coe1 ` O ) ` k ) j ) = ( i ( (coe1 ` O ) ` K ) j ) )
225221, 224syl5eq 2520 . . . . . . . . . . . . . 14 |- ( K e. NN0 -> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) = ( i ( (coe1 ` O ) ` K ) j ) )
226225ad2antlr 726 . . . . . . . . . . . . 13 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) = ( i ( (coe1 ` O ) ` K ) j ) )
227226mpt2eq3dv 6345 . . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> ( i e. N , j e. N |-> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) ) = ( i e. N , j e. N |-> ( i ( (coe1 ` O ) ` K ) j ) ) )
228 oveq12 6291 . . . . . . . . . . . . 13 |- ( ( i = a /\ j = b ) -> ( i ( (coe1 ` O ) ` K ) j ) = ( a ( (coe1 ` O ) ` K ) b ) )
229228adantl 466 . . . . . . . . . . . 12 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ ( a e. N /\ b e. N ) ) /\ ( i = a /\ j = b ) ) -> ( i ( (coe1 ` O ) ` K ) j ) = ( a ( (coe1 ` O ) ` K ) b ) )
230 simprl 755 . . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> a e. N )
231 simprr 756 . . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> b e. N )
232 ovex 6307 . . . . . . . . . . . . 13 |- ( a ( (coe1 ` O ) ` K ) b ) e. _V
233232a1i 11 . . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> ( a ( (coe1 ` O ) ` K ) b ) e. _V )
234227, 229, 230, 231, 233ovmpt2d 6412 . . . . . . . . . . 11 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> ( a ( i e. N , j e. N |-> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) ) b ) = ( a ( (coe1 ` O ) ` K ) b ) )
235234ralrimivva 2885 . . . . . . . . . 10 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> A. a e. N A. b e. N ( a ( i e. N , j e. N |-> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) ) b ) = ( a ( (coe1 ` O ) ` K ) b ) )
236 simpl1 999 . . . . . . . . . . . 12 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> N e. Fin )
237222oveqi 6295 . . . . . . . . . . . . . 14 |- ( i [_ K / k ]_ ( (coe1 ` O ) ` k ) j ) = ( i ( (coe1 ` O ) ` K ) j )
238221, 237eqtri 2496 . . . . . . . . . . . . 13 |- [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) = ( i ( (coe1 ` O ) ` K ) j )
239 simp2 997 . . . . . . . . . . . . . 14 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> i e. N )
240 simp3 998 . . . . . . . . . . . . . 14 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> j e. N )
24129, 3, 2, 23coe1fvalcl 18022 . . . . . . . . . . . . . . . 16 |- ( ( O e. L /\ K e. NN0 ) -> ( (coe1 ` O ) ` K ) e. ( Base ` A ) )
2422413ad2antl3 1160 . . . . . . . . . . . . . . 15 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( (coe1 ` O ) ` K ) e. ( Base ` A ) )
2432423ad2ant1 1017 . . . . . . . . . . . . . 14 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> ( (coe1 ` O ) ` K ) e. ( Base ` A ) )
2441, 22, 23, 239, 240, 243matecld 18695 . . . . . . . . . . . . 13 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> ( i ( (coe1 ` O ) ` K ) j ) e. ( Base ` R ) )
245238, 244syl5eqel 2559 . . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) e. ( Base ` R ) )
2461, 22, 23, 236, 18, 245matbas2d 18692 . . . . . . . . . . 11 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( i e. N , j e. N |-> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) ) e. ( Base ` A ) )
2471, 23eqmat 18693 . . . . . . . . . . 11 |- ( ( ( i e. N , j e. N |-> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) ) e. ( Base ` A ) /\ ( (coe1 ` O ) ` K ) e. ( Base ` A ) ) -> ( ( i e. N , j e. N |-> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) ) = ( (coe1 ` O ) ` K ) <-> A. a e. N A. b e. N ( a ( i e. N , j e. N |-> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) ) b ) = ( a ( (coe1 ` O ) ` K ) b ) ) )
248246, 242, 247syl2anc 661 . . . . . . . . . 10 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( ( i e. N , j e. N |-> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) ) = ( (coe1 ` O ) ` K ) <-> A. a e. N A. b e. N ( a ( i e. N , j e. N |-> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) ) b ) = ( a ( (coe1 ` O ) ` K ) b ) ) )
249235, 248mpbird 232 . . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( i e. N , j e. N |-> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) ) = ( (coe1 ` O ) ` K ) )
250249ad2antrr 725 . . . . . . . 8 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> ( i e. N , j e. N |-> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) ) = ( (coe1 ` O ) ` K ) )
251250adantl 466 . . . . . . 7 |- ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) -> ( i e. N , j e. N |-> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) ) = ( (coe1 ` O ) ` K ) )
252220, 251eqtrd 2508 . . . . . 6 |- ( ( -. s < K /\ ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) ) -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( (coe1 ` O ) ` K ) )
253252ex 434 . . . . 5 |- ( -. s < K -> ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( (coe1 ` O ) ` K ) ) )
254189, 253pm2.61i 164 . . . 4 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> ( i e. N , j e. N |-> ( R gsumg ( k e. ( 0 ... s ) |-> if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) ) ) ) = ( (coe1 ` O ) ` K ) )
25599, 121, 2543eqtrd 2512 . . 3 |- ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> ( i e. N , j e. N |-> ( (coe1 ` ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) ) = ( (coe1 ` O ) ` K ) )
256 eqid 2467 . . . . . 6 |- ( 0g ` A ) = ( 0g ` A )
25729, 3, 2, 256coe1sfi 18023 . . . . 5 |- ( O e. L -> (coe1 ` O ) finSupp ( 0g ` A ) )
25826, 257syl 16 . . . 4 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> (coe1 ` O ) finSupp ( 0g ` A ) )
25929, 3, 2, 256, 23coe1fsupp 18025 . . . . . 6 |- ( O e. L -> (coe1 ` O ) e. { x e. ( ( Base ` A ) ^m NN0 ) | x finSupp ( 0g ` A ) } )
260 elrabi 3258 . . . . . 6 |- ( (coe1 ` O ) e. { x e. ( ( Base ` A ) ^m NN0 ) | x finSupp ( 0g ` A ) } -> (coe1 ` O ) e. ( ( Base ` A ) ^m NN0 ) )
26126, 259, 2603syl 20 . . . . 5 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> (coe1 ` O ) e. ( ( Base ` A ) ^m NN0 ) )
262 fvex 5874 . . . . 5 |- ( 0g ` A ) e. _V
263 fsuppmapnn0ub 12065 . . . . 5 |- ( ( (coe1 ` O ) e. ( ( Base ` A ) ^m NN0 ) /\ ( 0g ` A ) e. _V ) -> ( (coe1 ` O ) finSupp ( 0g ` A ) -> E. s e. NN0 A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) )
264261, 262, 263sylancl 662 . . . 4 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( (coe1 ` O ) finSupp ( 0g ` A ) -> E. s e. NN0 A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) )
265258, 264mpd 15 . . 3 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> E. s e. NN0 A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) )
266255, 265r19.29a 3003 . 2 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( i e. N , j e. N |-> ( (coe1 ` ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) ) = ( (coe1 ` O ) ` K ) )
2679, 266eqtrd 2508 1 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( ( I ` O ) decompPMat K ) = ( (coe1 ` O ) ` K ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   =/= wne 2662   A.wral 2814   E.wrex 2815   {crab 2818   _Vcvv 3113   [_csb 3435   ifcif 3939   class class class wbr 4447   |-> cmpt 4505   ` cfv 5586  (class class class)co 6282   |-> cmpt2 6284   ^m cmap 7417   Fincfn 7513   finSupp cfsupp 7825   RRcr 9487   0cc0 9488   < clt 9624   <_ cle 9625   NN0cn0 10791   ...cfz 11668   Basecbs 14486  Scalarcsca 14554   .scvsca 14555   0gc0g 14691   gsumg cgsu 14692   Mndcmnd 15722  .gcmg 15727  CMndccmn 16594  mulGrpcmgp 16931   Ringcrg 16986   LModclmod 17295  var1cv1 17986  Poly1cpl1 17987  coe1cco1 17988   Mat cmat 18676   decompPMat cdecpmat 19030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-inf2 8054  ax-cnex 9544  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-ot 4036  df-uni 4246  df-int 4283  df-iun 4327  df-iin 4328  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-isom 5595  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-of 6522  df-ofr 6523  df-om 6679  df-1st 6781  df-2nd 6782  df-supp 6899  df-recs 7039  df-rdg 7073  df-1o 7127  df-2o 7128  df-oadd 7131  df-er 7308  df-map 7419  df-pm 7420  df-ixp 7467  df-en 7514  df-dom 7515  df-sdom 7516  df-fin 7517  df-fsupp 7826  df-sup 7897  df-oi 7931  df-card 8316  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-nn 10533  df-2 10590  df-3 10591  df-4 10592  df-5 10593  df-6 10594  df-7 10595  df-8 10596  df-9 10597  df-10 10598  df-n0 10792  df-z 10861  df-dec 10973  df-uz 11079  df-fz 11669  df-fzo 11789  df-seq 12072  df-hash 12370  df-struct 14488  df-ndx 14489  df-slot 14490  df-base 14491  df-sets 14492  df-ress 14493  df-plusg 14564  df-mulr 14565  df-sca 14567  df-vsca 14568  df-ip 14569  df-tset 14570  df-ple 14571  df-ds 14573  df-hom 14575  df-cco 14576  df-0g 14693  df-gsum 14694  df-prds 14699  df-pws 14701  df-mre 14837  df-mrc 14838  df-acs 14840  df-mnd 15728  df-mhm 15777  df-submnd 15778  df-grp 15858  df-minusg 15859  df-sbg 15860  df-mulg 15861  df-subg 15993  df-ghm 16060  df-cntz 16150  df-cmn 16596  df-abl 16597  df-mgp 16932  df-ur 16944  df-rng 16988  df-subrg 17210  df-lmod 17297  df-lss 17362  df-sra 17601  df-rgmod 17602  df-psr 17776  df-mvr 17777  df-mpl 17778  df-opsr 17780  df-psr1 17990  df-vr1 17991  df-ply1 17992  df-coe1 17993  df-dsmm 18530  df-frlm 18545  df-mat 18677  df-decpmat 19031
This theorem is referenced by:  mp2pm2mplem5  19078  mp2pm2mp  19079
  Copyright terms: Public domain W3C validator