Theorem mp2pm2mplem4 19437

Description: Lemma 4 for mp2pm2mp 19439. (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.

Step	Hyp	Ref	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 )
9	1, 2, 3, 4, 5, 6, 7, 8	mp2pm2mplem3 19436	. 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 2457	. . . . . . . . 9 |- ( Base ` P ) = ( Base ` P )
11		eqid 2457	. . . . . . . . 9 |- ( 0g ` P ) = ( 0g ` P )
12	8	ply1ring 18416	. . . . . . . . . . . . 13 |- ( R e. Ring -> P e. Ring )
13	12	3ad2ant2 1018	. . . . . . . . . . . 12 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. Ring )
14		ringcmn 17356	. . . . . . . . . . . 12 |- ( P e. Ring -> P e. CMnd )
15	13, 14	syl 16	. . . . . . . . . . 11 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. CMnd )
16	15	ad3antrrr 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 )
17	16	3ad2ant1 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 )
19	18	ad2antrr 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 )
20	19	3ad2ant1 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 )
21	20	adantr 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 2457	. . . . . . . . . . . 12 |- ( Base ` R ) = ( Base ` R )
23		eqid 2457	. . . . . . . . . . . 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 )
27	26	ad2antrr 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 )
28	27	3ad2ant1 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 2457	. . . . . . . . . . . . . 14 |- (coe1 ` O ) = (coe1 ` O )
30	29, 3, 2, 23	coe1fvalcl 18378	. . . . . . . . . . . . 13 |- ( ( O e. L /\ k e. NN0 ) -> ( (coe1 ` O ) ` k ) e. ( Base ` A ) )
31	28, 30	sylan 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 ) )
32	1, 22, 23, 24, 25, 31	matecld 19055	. . . . . . . . . . 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 2457	. . . . . . . . . . . 12 |- (mulGrp ` P ) = (mulGrp ` P )
35	22, 8, 6, 4, 34, 5, 10	ply1tmcl 18440	. . . . . . . . . . 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 ) )
36	21, 32, 33, 35	syl3anc 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 ) )
37	36	ralrimiva 2871	. . . . . . . . 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 6302	. . . . . . . . . . . . . . . . 17 |- ( ( (coe1 ` O ) ` x ) = ( 0g ` A ) -> ( i ( (coe1 ` O ) ` x ) j ) = ( i ( 0g ` A ) j ) )
40	39	oveq1d 6311	. . . . . . . . . . . . . . . 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 ) )
42	41	ad3antrrr 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 2457	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0g ` R ) = ( 0g ` R )
44	1, 43	mat0op 19048	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( a e. N , b e. N |-> ( 0g ` R ) ) )
45	42, 44	syl 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 2458	. . . . . . . . . . . . . . . . . . . . 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 756	. . . . . . . . . . . . . . . . . . . . 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 757	. . . . . . . . . . . . . . . . . . . . 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 5882	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 0g ` R ) e. _V
50	49	a1i 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 )
51	45, 46, 47, 48, 50	ovmpt2d 6429	. . . . . . . . . . . . . . . . . . . 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 ) )
52	51	adantr 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 ) )
53	52	oveq1d 6311	. . . . . . . . . . . . . . . . . 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 ) ) )
54	18	ad3antrrr 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 )
55	8	ply1sca 18421	. . . . . . . . . . . . . . . . . . . . 21 |- ( R e. Ring -> R = (Scalar ` P ) )
56	54, 55	syl 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 ) )
57	56	fveq2d 5876	. . . . . . . . . . . . . . . . . . 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 ) ) )
58	57	oveq1d 6311	. . . . . . . . . . . . . . . . . 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 ) ) )
59	8	ply1lmod 18420	. . . . . . . . . . . . . . . . . . . . 21 |- ( R e. Ring -> P e. LMod )
60	59	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . . 20 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. LMod )
61	60	ad4antr 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 )
63	8, 6, 34, 5, 10	ply1moncl 18439	. . . . . . . . . . . . . . . . . . . 20 |- ( ( R e. Ring /\ x e. NN0 ) -> ( x E Y ) e. ( Base ` P ) )
64	54, 62, 63	syl2anc 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 2457	. . . . . . . . . . . . . . . . . . . 20 |- (Scalar ` P ) = (Scalar ` P )
66		eqid 2457	. . . . . . . . . . . . . . . . . . . 20 |- ( 0g ` (Scalar ` P ) ) = ( 0g ` (Scalar ` P ) )
67	10, 65, 4, 66, 11	lmod0vs 17672	. . . . . . . . . . . . . . . . . . 19 |- ( ( P e. LMod /\ ( x E Y ) e. ( Base ` P ) ) -> ( ( 0g ` (Scalar ` P ) ) .x. ( x E Y ) ) = ( 0g ` P ) )
68	61, 64, 67	syl2anc 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 ) )
69	53, 58, 68	3eqtrd 2502	. . . . . . . . . . . . . . . . 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 ) )
70	69	adantr 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 ) )
71	40, 70	sylan9eqr 2520	. . . . . . . . . . . . . . 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 ) )
72	71	exp31 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 ) ) ) )
73	72	a2d 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 ) ) ) )
74	73	ralimdva 2865	. . . . . . . . . . . 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 ) ) ) )
75	74	impancom 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 ) ) ) )
76	75	3impib 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 4460	. . . . . . . . . . . 12 |- ( k = x -> ( s < k <-> s < x ) )
78		fveq2 5872	. . . . . . . . . . . . . . 15 |- ( k = x -> ( (coe1 ` O ) ` k ) = ( (coe1 ` O ) ` x ) )
79	78	oveqd 6313	. . . . . . . . . . . . . 14 |- ( k = x -> ( i ( (coe1 ` O ) ` k ) j ) = ( i ( (coe1 ` O ) ` x ) j ) )
80		oveq1 6303	. . . . . . . . . . . . . 14 |- ( k = x -> ( k E Y ) = ( x E Y ) )
81	79, 80	oveq12d 6314	. . . . . . . . . . . . 13 |- ( k = x -> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) = ( ( i ( (coe1 ` O ) ` x ) j ) .x. ( x E Y ) ) )
82	81	eqeq1d 2459	. . . . . . . . . . . 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 ) ) )
83	77, 82	imbi12d 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 ) ) ) )
84	83	cbvralv 3084	. . . . . . . . . 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 ) ) )
85	76, 84	sylibr 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 ) ) )
86	10, 11, 17, 37, 38, 85	gsummptnn0fzv 17142	. . . . . . . 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 ) ) ) ) )
87	86	fveq2d 5876	. . . . . . 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 ) ) ) ) ) )
88	87	fveq1d 5874	. . . . . 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 760	. . . . . . . 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 )
90	89	3ad2ant1 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 11797	. . . . . . . . . 10 |- ( k e. ( 0 ... s ) -> k e. NN0 )
92	36	expcom 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 ) ) )
93	91, 92	syl 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 ) ) )
94	93	com12 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 ) ) )
95	94	ralrimiv 2869	. . . . . . 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 12086	. . . . . . 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 )
97	8, 10, 20, 90, 95, 96	coe1fzgsumd 18471	. . . . . 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 ) ) ) )
98	88, 97	eqtrd 2498	. . . . 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 ) ) ) )
99	98	mpt2eq3dva 6360	. . . 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 ) ) ) ) )
100	18	3ad2ant1 1017	. . . . . . . . . . 11 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> R e. Ring )
101	100	adantr 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 )
104	26	3ad2ant1 1017	. . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> O e. L )
105	104, 91, 30	syl2an 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 ) )
106	1, 22, 23, 102, 103, 105	matecld 19055	. . . . . . . . . 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 ) )
107	91	adantl 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 )
108	43, 22, 8, 6, 4, 34, 5	coe1tm 18441	. . . . . . . . . 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 ) ) ) )
109	101, 106, 107, 108	syl3anc 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 2461	. . . . . . . . . . 11 |- ( l = K -> ( l = k <-> K = k ) )
111	110	ifbid 3966	. . . . . . . . . 10 |- ( l = K -> if ( l = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) = if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) )
112	111	adantl 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 6324	. . . . . . . . . . 11 |- ( i ( (coe1 ` O ) ` k ) j ) e. _V
115	114, 49	ifex 4013	. . . . . . . . . 10 |- if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) e. _V
116	115	a1i 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 )
117	109, 112, 113, 116	fvmptd 5961	. . . . . . . 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 ) ) )
118	117	mpteq2dva 4543	. . . . . . 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 ) ) ) )
119	118	oveq2d 6312	. . . . . 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 ) ) ) ) )
120	119	mpt2eq3dva 6360	. . . . 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 ) ) ) ) ) )
121	120	ad2antrr 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 4460	. . . . . . . . . . . . . 14 |- ( x = K -> ( s < x <-> s < K ) )
123		fveq2 5872	. . . . . . . . . . . . . . 15 |- ( x = K -> ( (coe1 ` O ) ` x ) = ( (coe1 ` O ) ` K ) )
124	123	eqeq1d 2459	. . . . . . . . . . . . . 14 |- ( x = K -> ( ( (coe1 ` O ) ` x ) = ( 0g ` A ) <-> ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) )
125	122, 124	imbi12d 320	. . . . . . . . . . . . 13 |- ( x = K -> ( ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) <-> ( s < K -> ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) ) )
126	125	rspcva 3208	. . . . . . . . . . . 12 |- ( ( K e. NN0 /\ A. x e. NN0 ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) ) -> ( s < K -> ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) )
127	1, 43	mat0op 19048	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( i e. N , j e. N |-> ( 0g ` R ) ) )
128	127	eqcomd 2465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( N e. Fin /\ R e. Ring ) -> ( i e. N , j e. N |-> ( 0g ` R ) ) = ( 0g ` A ) )
129	128	3adant3 1016	. . . . . . . . . . . . . . . . . . 19 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( i e. N , j e. N |-> ( 0g ` R ) ) = ( 0g ` A ) )
130	129	ad3antlr 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 11795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( k e. ( 0 ... s ) <-> ( k e. NN0 /\ s e. NN0 /\ k <_ s ) )
132		nn0re 10825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( k e. NN0 -> k e. RR )
133	132	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> k e. RR )
134		nn0re 10825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( s e. NN0 -> s e. RR )
135	134	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> s e. RR )
136		nn0re 10825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( K e. NN0 -> K e. RR )
137	136	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> K e. RR )
138		lelttr 9692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( k e. RR /\ s e. RR /\ K e. RR ) -> ( ( k <_ s /\ s < K ) -> k < K ) )
139	133, 135, 137, 138	syl3anc 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 )
141	140	olcd 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) /\ k < K ) -> ( K < k \/ k < K ) )
142		df-ne 2654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( K =/= k <-> -. K = k )
143	132	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( k e. NN0 /\ s e. NN0 ) -> k e. RR )
144		lttri2 9684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( K e. RR /\ k e. RR ) -> ( K =/= k <-> ( K < k \/ k < K ) ) )
145	136, 143, 144	syl2anr 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> ( K =/= k <-> ( K < k \/ k < K ) ) )
146	145	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) /\ k < K ) -> ( K =/= k <-> ( K < k \/ k < K ) ) )
147	142, 146	syl5bbr 259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) /\ k < K ) -> ( -. K = k <-> ( K < k \/ k < K ) ) )
148	141, 147	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) /\ k < K ) -> -. K = k )
149	148	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> ( k < K -> -. K = k ) )
150	139, 149	syld 44	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> ( ( k <_ s /\ s < K ) -> -. K = k ) )
151	150	exp4b 607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( k e. NN0 /\ s e. NN0 ) -> ( K e. NN0 -> ( k <_ s -> ( s < K -> -. K = k ) ) ) )
152	151	com24 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( k e. NN0 /\ s e. NN0 ) -> ( s < K -> ( k <_ s -> ( K e. NN0 -> -. K = k ) ) ) )
153	152	expimpd 603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( k e. NN0 -> ( ( s e. NN0 /\ s < K ) -> ( k <_ s -> ( K e. NN0 -> -. K = k ) ) ) )
154	153	com23 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( k e. NN0 -> ( k <_ s -> ( ( s e. NN0 /\ s < K ) -> ( K e. NN0 -> -. K = k ) ) ) )
155	154	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( k e. NN0 /\ k <_ s ) -> ( ( s e. NN0 /\ s < K ) -> ( K e. NN0 -> -. K = k ) ) )
156	155	3adant2 1015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( k e. NN0 /\ s e. NN0 /\ k <_ s ) -> ( ( s e. NN0 /\ s < K ) -> ( K e. NN0 -> -. K = k ) ) )
157	131, 156	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( k e. ( 0 ... s ) -> ( ( s e. NN0 /\ s < K ) -> ( K e. NN0 -> -. K = k ) ) )
158	157	com13 80	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( K e. NN0 -> ( ( s e. NN0 /\ s < K ) -> ( k e. ( 0 ... s ) -> -. K = k ) ) )
159	158	adantr 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 ) ) )
160	159	imp 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 ) )
161	160	adantr 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 ) )
162	161	3ad2ant1 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 ) )
163	162	imp 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 )
164	163	iffalsed 3955	. . . . . . . . . . . . . . . . . . . . . 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 ) )
165	164	mpteq2dva 4543	. . . . . . . . . . . . . . . . . . . . 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 ) ) )
166	165	oveq2d 6312	. . . . . . . . . . . . . . . . . . . 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		ringmnd 17334	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( R e. Ring -> R e. Mnd )
168	167	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> R e. Mnd )
169		ovex 6324	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0 ... s ) e. _V
170	43	gsumz 16132	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( R e. Mnd /\ ( 0 ... s ) e. _V ) -> ( R gsumg ( k e. ( 0 ... s ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
171	168, 169, 170	sylancl 662	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( R gsumg ( k e. ( 0 ... s ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
172	171	ad3antlr 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 ) )
173	172	3ad2ant1 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 ) )
174	166, 173	eqtrd 2498	. . . . . . . . . . . . . . . . . . 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 ) )
175	174	mpt2eq3dva 6360	. . . . . . . . . . . . . . . . . 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 ) )
177	130, 175, 176	3eqtr4d 2508	. . . . . . . . . . . . . . . . 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 ) )
178	177	ex 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 ) ) )
179	178	expr 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 ) ) ) )
180	179	a2d 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 ) ) ) )
181	180	exp31 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 ) ) ) ) ) )
182	181	com14 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 ) ) ) ) ) )
183	126, 182	syl 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 ) ) ) ) ) )
184	183	ex 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 ) ) ) ) ) ) )
185	184	com25 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 ) ) ) ) ) ) )
186	185	pm2.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 ) ) ) ) ) )
187	186	impcom 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 ) ) ) ) )
188	187	imp31 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 ) ) )
189	188	com12 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 ) ) )
190	168	ad3antrrr 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 )
191	190	adantl 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 )
192	191	3ad2ant1 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 )
193	169	a1i 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 9680	. . . . . . . . . . . . . . 15 |- ( ( K e. RR /\ s e. RR ) -> ( K <_ s <-> -. s < K ) )
195	136, 134, 194	syl2an 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 755	. . . . . . . . . . . . . . . 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 11795	. . . . . . . . . . . . . . . 16 |- ( K e. ( 0 ... s ) <-> ( K e. NN0 /\ s e. NN0 /\ K <_ s ) )
200	196, 197, 198, 199	syl3anbrc 1180	. . . . . . . . . . . . . . 15 |- ( ( ( K e. NN0 /\ s e. NN0 ) /\ K <_ s ) -> K e. ( 0 ... s ) )
201	200	ex 434	. . . . . . . . . . . . . 14 |- ( ( K e. NN0 /\ s e. NN0 ) -> ( K <_ s -> K e. ( 0 ... s ) ) )
202	195, 201	sylbird 235	. . . . . . . . . . . . 13 |- ( ( K e. NN0 /\ s e. NN0 ) -> ( -. s < K -> K e. ( 0 ... s ) ) )
203	202	adantll 713	. . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ s e. NN0 ) -> ( -. s < K -> K e. ( 0 ... s ) ) )
204	203	adantr 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 ) ) )
205	204	impcom 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 ) )
206	205	3ad2ant1 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 2466	. . . . . . . . . . 11 |- ( K = k <-> k = K )
208		ifbi 3965	. . . . . . . . . . 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 ) ) )
209	207, 208	ax-mp 5	. . . . . . . . . 10 |- if ( K = k , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) ) = if ( k = K , ( i ( (coe1 ` O ) ` k ) j ) , ( 0g ` R ) )
210	209	mpteq2i 4540	. . . . . . . . 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 )
213	27	adantl 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 )
214	213	3ad2ant1 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 )
215	214, 30	sylan 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 ) )
216	1, 22, 23, 211, 212, 215	matecld 19055	. . . . . . . . . . 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 ) )
217	91, 216	sylan2 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 ) )
218	217	ralrimiva 2871	. . . . . . . . 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 ) )
219	43, 192, 193, 206, 210, 218	gsummpt1n0 17119	. . . . . . . 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 ) )
220	219	mpt2eq3dva 6360	. . . . . . 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 6331	. . . . . . . . . . . . . . 15 |- [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) = ( i [_ K / k ]_ ( (coe1 ` O ) ` k ) j )
222		csbfv 5909	. . . . . . . . . . . . . . . . 17 |- [_ K / k ]_ ( (coe1 ` O ) ` k ) = ( (coe1 ` O ) ` K )
223	222	a1i 11	. . . . . . . . . . . . . . . 16 |- ( K e. NN0 -> [_ K / k ]_ ( (coe1 ` O ) ` k ) = ( (coe1 ` O ) ` K ) )
224	223	oveqd 6313	. . . . . . . . . . . . . . 15 |- ( K e. NN0 -> ( i [_ K / k ]_ ( (coe1 ` O ) ` k ) j ) = ( i ( (coe1 ` O ) ` K ) j ) )
225	221, 224	syl5eq 2510	. . . . . . . . . . . . . 14 |- ( K e. NN0 -> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) = ( i ( (coe1 ` O ) ` K ) j ) )
226	225	ad2antlr 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 ) )
227	226	mpt2eq3dv 6362	. . . . . . . . . . . 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 6305	. . . . . . . . . . . . 13 |- ( ( i = a /\ j = b ) -> ( i ( (coe1 ` O ) ` K ) j ) = ( a ( (coe1 ` O ) ` K ) b ) )
229	228	adantl 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 756	. . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> a e. N )
231		simprr 757	. . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> b e. N )
232		ovex 6324	. . . . . . . . . . . . 13 |- ( a ( (coe1 ` O ) ` K ) b ) e. _V
233	232	a1i 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 )
234	227, 229, 230, 231, 233	ovmpt2d 6429	. . . . . . . . . . 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 ) )
235	234	ralrimivva 2878	. . . . . . . . . 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 )
237	222	oveqi 6309	. . . . . . . . . . . . . 14 |- ( i [_ K / k ]_ ( (coe1 ` O ) ` k ) j ) = ( i ( (coe1 ` O ) ` K ) j )
238	221, 237	eqtri 2486	. . . . . . . . . . . . 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 )
241	29, 3, 2, 23	coe1fvalcl 18378	. . . . . . . . . . . . . . . 16 |- ( ( O e. L /\ K e. NN0 ) -> ( (coe1 ` O ) ` K ) e. ( Base ` A ) )
242	241	3ad2antl3 1160	. . . . . . . . . . . . . . 15 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( (coe1 ` O ) ` K ) e. ( Base ` A ) )
243	242	3ad2ant1 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 ) )
244	1, 22, 23, 239, 240, 243	matecld 19055	. . . . . . . . . . . . 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 ) )
245	238, 244	syl5eqel 2549	. . . . . . . . . . . 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 ) )
246	1, 22, 23, 236, 18, 245	matbas2d 19052	. . . . . . . . . . 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 ) )
247	1, 23	eqmat 19053	. . . . . . . . . . 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 ) ) )
248	246, 242, 247	syl2anc 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 ) ) )
249	235, 248	mpbird 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 ) )
250	249	ad2antrr 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 ) )
251	250	adantl 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 ) )
252	220, 251	eqtrd 2498	. . . . . 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 ) )
253	252	ex 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 ) ) )
254	189, 253	pm2.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 ) )
255	99, 121, 254	3eqtrd 2502	. . 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 2457	. . . . . 6 |- ( 0g ` A ) = ( 0g ` A )
257	29, 3, 2, 256	coe1sfi 18379	. . . . 5 |- ( O e. L -> (coe1 ` O ) finSupp ( 0g ` A ) )
258	26, 257	syl 16	. . . 4 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> (coe1 ` O ) finSupp ( 0g ` A ) )
259	29, 3, 2, 256, 23	coe1fsupp 18381	. . . . . 6 |- ( O e. L -> (coe1 ` O ) e. { x e. ( ( Base ` A ) ^m NN0 ) | x finSupp ( 0g ` A ) } )
260		elrabi 3254	. . . . . 6 |- ( (coe1 ` O ) e. { x e. ( ( Base ` A ) ^m NN0 ) | x finSupp ( 0g ` A ) } -> (coe1 ` O ) e. ( ( Base ` A ) ^m NN0 ) )
261	26, 259, 260	3syl 20	. . . . 5 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> (coe1 ` O ) e. ( ( Base ` A ) ^m NN0 ) )
262		fvex 5882	. . . . 5 |- ( 0g ` A ) e. _V
263		fsuppmapnn0ub 12104	. . . . 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 ) ) ) )
264	261, 262, 263	sylancl 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 ) ) ) )
265	258, 264	mpd 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 ) ) )
266	255, 265	r19.29a 2999	. 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 ) )
267	9, 266	eqtrd 2498	1 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( ( I ` O ) decompPMat K ) = ( (coe1 ` O ) ` K ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 973   = wceq 1395   e. wcel 1819   =/= wne 2652   A.wral 2807   E.wrex 2808   {crab 2811   _Vcvv 3109   [_csb 3430   ifcif 3944   class class class wbr 4456   |-> cmpt 4515   ` cfv 5594  (class class class)co 6296   |-> cmpt2 6298   ^m cmap 7438   Fincfn 7535   finSupp cfsupp 7847   RRcr 9508   0cc0 9509   < clt 9645   <_ cle 9646   NN0cn0 10816   ...cfz 11697   Basecbs 14644  Scalarcsca 14715   .scvsca 14716   0gc0g 14857   gsum_g cgsu 14858   Mndcmnd 16046  ._gcmg 16183  CMndccmn 16925  mulGrpcmgp 17268   Ringcrg 17325   LModclmod 17639  var₁cv1 18342  Poly₁cpl1 18343  coe₁cco1 18344   Mat cmat 19036   decompPMat cdecpmat 19390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-inf2 8075  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-fal 1401  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-ot 4041  df-uni 4252  df-int 4289  df-iun 4334  df-iin 4335  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-se 4848  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-of 6539  df-ofr 6540  df-om 6700  df-1st 6799  df-2nd 6800  df-supp 6918  df-recs 7060  df-rdg 7094  df-1o 7148  df-2o 7149  df-oadd 7152  df-er 7329  df-map 7440  df-pm 7441  df-ixp 7489  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-fsupp 7848  df-sup 7919  df-oi 7953  df-card 8337  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-nn 10557  df-2 10615  df-3 10616  df-4 10617  df-5 10618  df-6 10619  df-7 10620  df-8 10621  df-9 10622  df-10 10623  df-n0 10817  df-z 10886  df-dec 11001  df-uz 11107  df-fz 11698  df-fzo 11822  df-seq 12111  df-hash 12409  df-struct 14646  df-ndx 14647  df-slot 14648  df-base 14649  df-sets 14650  df-ress 14651  df-plusg 14725  df-mulr 14726  df-sca 14728  df-vsca 14729  df-ip 14730  df-tset 14731  df-ple 14732  df-ds 14734  df-hom 14736  df-cco 14737  df-0g 14859  df-gsum 14860  df-prds 14865  df-pws 14867  df-mre 15003  df-mrc 15004  df-acs 15006  df-mgm 15999  df-sgrp 16038  df-mnd 16048  df-mhm 16093  df-submnd 16094  df-grp 16184  df-minusg 16185  df-sbg 16186  df-mulg 16187  df-subg 16325  df-ghm 16392  df-cntz 16482  df-cmn 16927  df-abl 16928  df-mgp 17269  df-ur 17281  df-ring 17327  df-subrg 17554  df-lmod 17641  df-lss 17706  df-sra 17945  df-rgmod 17946  df-psr 18132  df-mvr 18133  df-mpl 18134  df-opsr 18136  df-psr1 18346  df-vr1 18347  df-ply1 18348  df-coe1 18349  df-dsmm 18890  df-frlm 18905  df-mat 19037  df-decpmat 19391

This theorem is referenced by:  mp2pm2mplem5  19438  mp2pm2mp  19439