Theorem mp2pm2mplem4 19602

Description: Lemma 4 for mp2pm2mp 19604. (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 19601	. 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 2402	. . . . . . . . 9 |- ( Base ` P ) = ( Base ` P )
11		eqid 2402	. . . . . . . . 9 |- ( 0g ` P ) = ( 0g ` P )
12	8	ply1ring 18609	. . . . . . . . . . . . 13 |- ( R e. Ring -> P e. Ring )
13	12	3ad2ant2 1019	. . . . . . . . . . . 12 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. Ring )
14		ringcmn 17549	. . . . . . . . . . . 12 |- ( P e. Ring -> P e. CMnd )
15	13, 14	syl 17	. . . . . . . . . . 11 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. CMnd )
16	15	ad3antrrr 728	. . . . . . . . . 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 1018	. . . . . . . . 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 1001	. . . . . . . . . . . . . 14 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> R e. Ring )
19	18	ad2antrr 724	. . . . . . . . . . . . 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 1018	. . . . . . . . . . . 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 463	. . . . . . . . . . 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 2402	. . . . . . . . . . . 12 |- ( Base ` R ) = ( Base ` R )
23		eqid 2402	. . . . . . . . . . . 12 |- ( Base ` A ) = ( Base ` A )
24		simpl2 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 ) -> i e. N )
25		simpl3 1002	. . . . . . . . . . . 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 1002	. . . . . . . . . . . . . . 15 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> O e. L )
27	26	ad2antrr 724	. . . . . . . . . . . . . 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 1018	. . . . . . . . . . . . 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 2402	. . . . . . . . . . . . . 14 |- (coe1 ` O ) = (coe1 ` O )
30	29, 3, 2, 23	coe1fvalcl 18571	. . . . . . . . . . . . 13 |- ( ( O e. L /\ k e. NN0 ) -> ( (coe1 ` O ) ` k ) e. ( Base ` A ) )
31	28, 30	sylan 469	. . . . . . . . . . . 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 19220	. . . . . . . . . . 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 459	. . . . . . . . . . 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 2402	. . . . . . . . . . . 12 |- (mulGrp ` P ) = (mulGrp ` P )
35	22, 8, 6, 4, 34, 5, 10	ply1tmcl 18633	. . . . . . . . . . 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 1230	. . . . . . . . . 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 2818	. . . . . . . . 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 1061	. . . . . . . . 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 6284	. . . . . . . . . . . . . . . . 17 |- ( ( (coe1 ` O ) ` x ) = ( 0g ` A ) -> ( i ( (coe1 ` O ) ` x ) j ) = ( i ( 0g ` A ) j ) )
40	39	oveq1d 6293	. . . . . . . . . . . . . . . 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 994	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( N e. Fin /\ R e. Ring ) )
42	41	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . 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 2402	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0g ` R ) = ( 0g ` R )
44	1, 43	mat0op 19213	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( a e. N , b e. N |-> ( 0g ` R ) ) )
45	42, 44	syl 17	. . . . . . . . . . . . . . . . . . . . 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 2403	. . . . . . . . . . . . . . . . . . . . 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 758	. . . . . . . . . . . . . . . . . . . . 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 5859	. . . . . . . . . . . . . . . . . . . . . 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 6411	. . . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . 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 6293	. . . . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . . . . . . . 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 18614	. . . . . . . . . . . . . . . . . . . . 21 |- ( R e. Ring -> R = (Scalar ` P ) )
56	54, 55	syl 17	. . . . . . . . . . . . . . . . . . . 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 5853	. . . . . . . . . . . . . . . . . . 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 6293	. . . . . . . . . . . . . . . . . 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 18613	. . . . . . . . . . . . . . . . . . . . 21 |- ( R e. Ring -> P e. LMod )
60	59	3ad2ant2 1019	. . . . . . . . . . . . . . . . . . . 20 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. LMod )
61	60	ad4antr 730	. . . . . . . . . . . . . . . . . . 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 459	. . . . . . . . . . . . . . . . . . . 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 18632	. . . . . . . . . . . . . . . . . . . 20 |- ( ( R e. Ring /\ x e. NN0 ) -> ( x E Y ) e. ( Base ` P ) )
64	54, 62, 63	syl2anc 659	. . . . . . . . . . . . . . . . . . 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 2402	. . . . . . . . . . . . . . . . . . . 20 |- (Scalar ` P ) = (Scalar ` P )
66		eqid 2402	. . . . . . . . . . . . . . . . . . . 20 |- ( 0g ` (Scalar ` P ) ) = ( 0g ` (Scalar ` P ) )
67	10, 65, 4, 66, 11	lmod0vs 17865	. . . . . . . . . . . . . . . . . . 19 |- ( ( P e. LMod /\ ( x E Y ) e. ( Base ` P ) ) -> ( ( 0g ` (Scalar ` P ) ) .x. ( x E Y ) ) = ( 0g ` P ) )
68	61, 64, 67	syl2anc 659	. . . . . . . . . . . . . . . . . 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 2447	. . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . 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 2465	. . . . . . . . . . . . . . 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 602	. . . . . . . . . . . . . 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 2812	. . . . . . . . . . . 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 438	. . . . . . . . . . 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 1195	. . . . . . . . . 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 4399	. . . . . . . . . . . 12 |- ( k = x -> ( s < k <-> s < x ) )
78		fveq2 5849	. . . . . . . . . . . . . . 15 |- ( k = x -> ( (coe1 ` O ) ` k ) = ( (coe1 ` O ) ` x ) )
79	78	oveqd 6295	. . . . . . . . . . . . . 14 |- ( k = x -> ( i ( (coe1 ` O ) ` k ) j ) = ( i ( (coe1 ` O ) ` x ) j ) )
80		oveq1 6285	. . . . . . . . . . . . . 14 |- ( k = x -> ( k E Y ) = ( x E Y ) )
81	79, 80	oveq12d 6296	. . . . . . . . . . . . 13 |- ( k = x -> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) = ( ( i ( (coe1 ` O ) ` x ) j ) .x. ( x E Y ) ) )
82	81	eqeq1d 2404	. . . . . . . . . . . 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 318	. . . . . . . . . . 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 3034	. . . . . . . . . 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 17335	. . . . . . . 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 5853	. . . . . . 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 5851	. . . . . 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 761	. . . . . . . 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 1018	. . . . . . 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 11826	. . . . . . . . . 10 |- ( k e. ( 0 ... s ) -> k e. NN0 )
92	36	expcom 433	. . . . . . . . . 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 17	. . . . . . . . 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 29	. . . . . . . 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 2816	. . . . . . 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 12124	. . . . . . 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 18664	. . . . . 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 2443	. . . . 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 6342	. . . 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 1018	. . . . . . . . . . 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 463	. . . . . . . . . 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 1001	. . . . . . . . . . 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 1002	. . . . . . . . . . 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 1018	. . . . . . . . . . . 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 475	. . . . . . . . . . 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 19220	. . . . . . . . . 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 464	. . . . . . . . . 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 18634	. . . . . . . . . 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 1230	. . . . . . . . 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 2406	. . . . . . . . . . 11 |- ( l = K -> ( l = k <-> K = k ) )
111	110	ifbid 3907	. . . . . . . . . 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 464	. . . . . . . . 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 1049	. . . . . . . . 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 6306	. . . . . . . . . . 11 |- ( i ( (coe1 ` O ) ` k ) j ) e. _V
115	114, 49	ifex 3953	. . . . . . . . . 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 5938	. . . . . . . 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 4481	. . . . . . 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 6294	. . . . . 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 6342	. . . . 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 724	. . . 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 4399	. . . . . . . . . . . . . 14 |- ( x = K -> ( s < x <-> s < K ) )
123		fveq2 5849	. . . . . . . . . . . . . . 15 |- ( x = K -> ( (coe1 ` O ) ` x ) = ( (coe1 ` O ) ` K ) )
124	123	eqeq1d 2404	. . . . . . . . . . . . . 14 |- ( x = K -> ( ( (coe1 ` O ) ` x ) = ( 0g ` A ) <-> ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) )
125	122, 124	imbi12d 318	. . . . . . . . . . . . 13 |- ( x = K -> ( ( s < x -> ( (coe1 ` O ) ` x ) = ( 0g ` A ) ) <-> ( s < K -> ( (coe1 ` O ) ` K ) = ( 0g ` A ) ) ) )
126	125	rspcva 3158	. . . . . . . . . . . 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 19213	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( i e. N , j e. N |-> ( 0g ` R ) ) )
128	127	eqcomd 2410	. . . . . . . . . . . . . . . . . . . 20 |- ( ( N e. Fin /\ R e. Ring ) -> ( i e. N , j e. N |-> ( 0g ` R ) ) = ( 0g ` A ) )
129	128	3adant3 1017	. . . . . . . . . . . . . . . . . . 19 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( i e. N , j e. N |-> ( 0g ` R ) ) = ( 0g ` A ) )
130	129	ad3antlr 729	. . . . . . . . . . . . . . . . . 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 11824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( k e. ( 0 ... s ) <-> ( k e. NN0 /\ s e. NN0 /\ k <_ s ) )
132		nn0re 10845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( k e. NN0 -> k e. RR )
133	132	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> k e. RR )
134		nn0re 10845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( s e. NN0 -> s e. RR )
135	134	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> s e. RR )
136		nn0re 10845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( K e. NN0 -> K e. RR )
137	136	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> K e. RR )
138		lelttr 9706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( k e. RR /\ s e. RR /\ K e. RR ) -> ( ( k <_ s /\ s < K ) -> k < K ) )
139	133, 135, 137, 138	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> ( ( k <_ s /\ s < K ) -> k < K ) )
140		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) /\ k < K ) -> k < K )
141	140	olcd 391	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) /\ k < K ) -> ( K < k \/ k < K ) )
142		df-ne 2600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( K =/= k <-> -. K = k )
143	132	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( k e. NN0 /\ s e. NN0 ) -> k e. RR )
144		lttri2 9698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( K e. RR /\ k e. RR ) -> ( K =/= k <-> ( K < k \/ k < K ) ) )
145	136, 143, 144	syl2anr 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> ( K =/= k <-> ( K < k \/ k < K ) ) )
146	145	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> ( k < K -> -. K = k ) )
150	139, 149	syld 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( k e. NN0 /\ s e. NN0 ) /\ K e. NN0 ) -> ( ( k <_ s /\ s < K ) -> -. K = k ) )
151	150	exp4b 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( k e. NN0 /\ k <_ s ) -> ( ( s e. NN0 /\ s < K ) -> ( K e. NN0 -> -. K = k ) ) )
156	155	3adant2 1016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 427	. . . . . . . . . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . . . . . . . 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 1018	. . . . . . . . . . . . . . . . . . . . . . . 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 427	. . . . . . . . . . . . . . . . . . . . . . 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 3896	. . . . . . . . . . . . . . . . . . . . . 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 4481	. . . . . . . . . . . . . . . . . . . . 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 6294	. . . . . . . . . . . . . . . . . . . 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 17527	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( R e. Ring -> R e. Mnd )
168	167	3ad2ant2 1019	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> R e. Mnd )
169		ovex 6306	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0 ... s ) e. _V
170	43	gsumz 16329	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( R e. Mnd /\ ( 0 ... s ) e. _V ) -> ( R gsumg ( k e. ( 0 ... s ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
171	168, 169, 170	sylancl 660	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( R gsumg ( k e. ( 0 ... s ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
172	171	ad3antlr 729	. . . . . . . . . . . . . . . . . . . . 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 1018	. . . . . . . . . . . . . . . . . . . 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 2443	. . . . . . . . . . . . . . . . . . 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 6342	. . . . . . . . . . . . . . . . . 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 459	. . . . . . . . . . . . . . . . . 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 2453	. . . . . . . . . . . . . . . . 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 432	. . . . . . . . . . . . . . . 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 613	. . . . . . . . . . . . . . 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 602	. . . . . . . . . . . . 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 17	. . . . . . . . . . 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 432	. . . . . . . . . 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 46	. . . . . . . 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 428	. . . . . . 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 430	. . . . . 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 29	. . . . 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 728	. . . . . . . . . . 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 464	. . . . . . . . . 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 1018	. . . . . . . . 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 9694	. . . . . . . . . . . . . . 15 |- ( ( K e. RR /\ s e. RR ) -> ( K <_ s <-> -. s < K ) )
195	136, 134, 194	syl2an 475	. . . . . . . . . . . . . 14 |- ( ( K e. NN0 /\ s e. NN0 ) -> ( K <_ s <-> -. s < K ) )
196		simpll 752	. . . . . . . . . . . . . . . 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 459	. . . . . . . . . . . . . . . 16 |- ( ( ( K e. NN0 /\ s e. NN0 ) /\ K <_ s ) -> K <_ s )
199		elfz2nn0 11824	. . . . . . . . . . . . . . . 16 |- ( K e. ( 0 ... s ) <-> ( K e. NN0 /\ s e. NN0 /\ K <_ s ) )
200	196, 197, 198, 199	syl3anbrc 1181	. . . . . . . . . . . . . . 15 |- ( ( ( K e. NN0 /\ s e. NN0 ) /\ K <_ s ) -> K e. ( 0 ... s ) )
201	200	ex 432	. . . . . . . . . . . . . 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 712	. . . . . . . . . . . 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 463	. . . . . . . . . . 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 428	. . . . . . . . . 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 1018	. . . . . . . . 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 2411	. . . . . . . . . . 11 |- ( K = k <-> k = K )
208		ifbi 3906	. . . . . . . . . . 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 4478	. . . . . . . . 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 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 ) -> i e. N )
212		simpl3 1002	. . . . . . . . . . . 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 464	. . . . . . . . . . . . . 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 1018	. . . . . . . . . . . . 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 469	. . . . . . . . . . . 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 19220	. . . . . . . . . . 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 472	. . . . . . . . . 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 2818	. . . . . . . . 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 17313	. . . . . . . 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 6342	. . . . . . 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 6313	. . . . . . . . . . . . . . 15 |- [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) = ( i [_ K / k ]_ ( (coe1 ` O ) ` k ) j )
222		csbfv 5886	. . . . . . . . . . . . . . . . 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 6295	. . . . . . . . . . . . . . 15 |- ( K e. NN0 -> ( i [_ K / k ]_ ( (coe1 ` O ) ` k ) j ) = ( i ( (coe1 ` O ) ` K ) j ) )
225	221, 224	syl5eq 2455	. . . . . . . . . . . . . 14 |- ( K e. NN0 -> [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) = ( i ( (coe1 ` O ) ` K ) j ) )
226	225	ad2antlr 725	. . . . . . . . . . . . 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 6344	. . . . . . . . . . . 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 6287	. . . . . . . . . . . . 13 |- ( ( i = a /\ j = b ) -> ( i ( (coe1 ` O ) ` K ) j ) = ( a ( (coe1 ` O ) ` K ) b ) )
229	228	adantl 464	. . . . . . . . . . . 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 758	. . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> b e. N )
232		ovex 6306	. . . . . . . . . . . . 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 6411	. . . . . . . . . . 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 2825	. . . . . . . . . 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 1000	. . . . . . . . . . . 12 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> N e. Fin )
237	222	oveqi 6291	. . . . . . . . . . . . . 14 |- ( i [_ K / k ]_ ( (coe1 ` O ) ` k ) j ) = ( i ( (coe1 ` O ) ` K ) j )
238	221, 237	eqtri 2431	. . . . . . . . . . . . 13 |- [_ K / k ]_ ( i ( (coe1 ` O ) ` k ) j ) = ( i ( (coe1 ` O ) ` K ) j )
239		simp2 998	. . . . . . . . . . . . . 14 |- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> i e. N )
240		simp3 999	. . . . . . . . . . . . . 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 18571	. . . . . . . . . . . . . . . 16 |- ( ( O e. L /\ K e. NN0 ) -> ( (coe1 ` O ) ` K ) e. ( Base ` A ) )
242	241	3ad2antl3 1161	. . . . . . . . . . . . . . 15 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( (coe1 ` O ) ` K ) e. ( Base ` A ) )
243	242	3ad2ant1 1018	. . . . . . . . . . . . . 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 19220	. . . . . . . . . . . . 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 2494	. . . . . . . . . . . 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 19217	. . . . . . . . . . 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 19218	. . . . . . . . . . 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 659	. . . . . . . . . 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 724	. . . . . . . 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 464	. . . . . . 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 2443	. . . . . 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 432	. . . . 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 2447	. . 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 2402	. . . . . 6 |- ( 0g ` A ) = ( 0g ` A )
257	29, 3, 2, 256	coe1sfi 18572	. . . . 5 |- ( O e. L -> (coe1 ` O ) finSupp ( 0g ` A ) )
258	26, 257	syl 17	. . . 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 18574	. . . . . 6 |- ( O e. L -> (coe1 ` O ) e. { x e. ( ( Base ` A ) ^m NN0 ) | x finSupp ( 0g ` A ) } )
260		elrabi 3204	. . . . . 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 18	. . . . 5 |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> (coe1 ` O ) e. ( ( Base ` A ) ^m NN0 ) )
262		fvex 5859	. . . . 5 |- ( 0g ` A ) e. _V
263		fsuppmapnn0ub 12145	. . . . 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 660	. . . 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 2949	. 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 2443	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 366   /\ wa 367   /\ w3a 974   = wceq 1405   e. wcel 1842   =/= wne 2598   A.wral 2754   E.wrex 2755   {crab 2758   _Vcvv 3059   [_csb 3373   ifcif 3885   class class class wbr 4395   |-> cmpt 4453   ` cfv 5569  (class class class)co 6278   |-> cmpt2 6280   ^m cmap 7457   Fincfn 7554   finSupp cfsupp 7863   RRcr 9521   0cc0 9522   < clt 9658   <_ cle 9659   NN0cn0 10836   ...cfz 11726   Basecbs 14841  Scalarcsca 14912   .scvsca 14913   0gc0g 15054   gsum_g cgsu 15055   Mndcmnd 16243  ._gcmg 16380  CMndccmn 17122  mulGrpcmgp 17461   Ringcrg 17518   LModclmod 17832  var₁cv1 18535  Poly₁cpl1 18536  coe₁cco1 18537   Mat cmat 19201   decompPMat cdecpmat 19555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4507  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574  ax-inf2 8091  ax-cnex 9578  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-mulcom 9586  ax-addass 9587  ax-mulass 9588  ax-distr 9589  ax-i2m1 9590  ax-1ne0 9591  ax-1rid 9592  ax-rnegex 9593  ax-rrecex 9594  ax-cnre 9595  ax-pre-lttri 9596  ax-pre-lttrn 9597  ax-pre-ltadd 9598  ax-pre-mulgt0 9599

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-fal 1411  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2759  df-rex 2760  df-reu 2761  df-rmo 2762  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-ot 3981  df-uni 4192  df-int 4228  df-iun 4273  df-iin 4274  df-br 4396  df-opab 4454  df-mpt 4455  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-se 4783  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-pred 5367  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-isom 5578  df-riota 6240  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-of 6521  df-ofr 6522  df-om 6684  df-1st 6784  df-2nd 6785  df-supp 6903  df-wrecs 7013  df-recs 7075  df-rdg 7113  df-1o 7167  df-2o 7168  df-oadd 7171  df-er 7348  df-map 7459  df-pm 7460  df-ixp 7508  df-en 7555  df-dom 7556  df-sdom 7557  df-fin 7558  df-fsupp 7864  df-sup 7935  df-oi 7969  df-card 8352  df-pnf 9660  df-mnf 9661  df-xr 9662  df-ltxr 9663  df-le 9664  df-sub 9843  df-neg 9844  df-nn 10577  df-2 10635  df-3 10636  df-4 10637  df-5 10638  df-6 10639  df-7 10640  df-8 10641  df-9 10642  df-10 10643  df-n0 10837  df-z 10906  df-dec 11020  df-uz 11128  df-fz 11727  df-fzo 11855  df-seq 12152  df-hash 12453  df-struct 14843  df-ndx 14844  df-slot 14845  df-base 14846  df-sets 14847  df-ress 14848  df-plusg 14922  df-mulr 14923  df-sca 14925  df-vsca 14926  df-ip 14927  df-tset 14928  df-ple 14929  df-ds 14931  df-hom 14933  df-cco 14934  df-0g 15056  df-gsum 15057  df-prds 15062  df-pws 15064  df-mre 15200  df-mrc 15201  df-acs 15203  df-mgm 16196  df-sgrp 16235  df-mnd 16245  df-mhm 16290  df-submnd 16291  df-grp 16381  df-minusg 16382  df-sbg 16383  df-mulg 16384  df-subg 16522  df-ghm 16589  df-cntz 16679  df-cmn 17124  df-abl 17125  df-mgp 17462  df-ur 17474  df-ring 17520  df-subrg 17747  df-lmod 17834  df-lss 17899  df-sra 18138  df-rgmod 18139  df-psr 18325  df-mvr 18326  df-mpl 18327  df-opsr 18329  df-psr1 18539  df-vr1 18540  df-ply1 18541  df-coe1 18542  df-dsmm 19061  df-frlm 19076  df-mat 19202  df-decpmat 19556

This theorem is referenced by:  mp2pm2mplem5  19603  mp2pm2mp  19604